Differences

This shows you the differences between two versions of the page.

--- teaching:cc4101:tareas:2021-1:tarea1 [2021/03/29 16:23] – created tvallejos
+++ teaching:cc4101:tareas:2021-1:tarea1 [2021/05/10 14:34] (current) – P3, add '}' on first example bortiz
@@ Line 1: / Line 1: @@
-====== Tarea 1 (Entrega: 23 de abril de 2021) ======
+====== Tarea 1 (Entrega: 7 de mayo de 2021) ======
+==== Tipos estáticos, tipos opcionales, contratos ====
-Esta tarea se distribuye con un archivo zip {{teaching:cc4101:tareas:2020-1:base.zip |base}} que contiene 3 archivos: main.rkt, tests.rkt, y machine.rkt. Los archivos main.rkt y tests.rkt están incompletos, y en ellos tienen que implementar lo que se solicita en las preguntas siguientes. **No deben modificar el archivo machine.rkt**: es una implementación completa de la máquina a la cual van a compilar su lenguaje. Tampoco deben agregar tests para la funciones del archivo machine.rkt, sino solo para aquellas funciones que ustedes definen.
+Ya se habrán dado cuenta que ciertos lenguajes tienen tipos estáticos (C/C++, Java, C#, Scala, etc.) y otros tienen tipos dinámicos (Python, Racket, JavaScript, etc.). Más aún, ciertos lenguajes como Racket tienen contratos, que permiten expresar propiedades más finas. Además, muchos lenguajes originalmente dinámicos ahora tienen tipos opcionales (Python, TypeScript, Hack, etc.).
-Deben entregar via U-cursos **un archivo .zip** que contenga los archivos main.rkt y tests.rkt.
+En esta tarea van a dejar atrás toda confusión al respecto! Van a implementar un lenguaje simple (con funciones de primer orden, tipos de datos básicos, y operadores sobre ellos), primero con sólo checkeo dinámico de tipos (parte 1), luego le van a agregar verificación de tipos estáticos (parte 2), incluyendo tipos opcionales con un tipo "comodín" ''Any'', y finalmente van a agregar contratos dinámicos (parte 3).
+Al final de esta tarea, tendrán implementado un lenguaje bastante original que permite mezclar checkeo estático y dinámico de tipos y propiedades!
-<note important>Consulte las normas de entrega de tareas en http://pleiad.cl/teaching/cc4101</note>
-**¡Los tests, los contratos y las descripciones forman parte de su evaluación!**
+----
-===== 1. Funciones de primera clase con tipos declarados [1.5pt] =====
-En esta tarea agregaremos anotaciones de tipos a un lenguaje con funciones de primera clase. La sintaxis concreta del lenguaje es la mostrada a continuación: <code scheme>
-<s-expr> ::= <num>
-         | <id>
-         | {+ <s-expr> <s-expr>}
-         | {- <s-expr> <s-expr>}
-         | {with {<id> : <type> <s-expr>} <s-expr>}
-         | {fun {<id> : <type>} [: <type>] <s-expr>}
-         | {<s-expr> <s-expr>}
-<type> ::= Num
+<note important>Consulte las normas de entrega de tareas en http://pleiad.cl/teaching/cc4101.
-         | {<type> -> <type>}
+Recuerden que tienen que seguir la metodología [[https://users.dcc.uchile.cl/~etanter/preplai/defun.html|vista en las primeras clases]] y dejar sus funciones debidamente documentadas.
-</code>
+</note>
-Note que ''%%with%%'' no incluye anotación del tipo del cuerpo, y el tipo de retorno de las funciones es opcional (los '[' ']' son parte de la notación BNF, especificando que lo que va adentro es opcional).
-Por ejemplo, los programas siguientes son válidos: <code scheme>
-{with {x : Num 5} {+ x 3}}
-{fun {x : Num} : Num
-  {+ x 3}}
-{fun {x : Num}
+Deben entregar via U-cursos **un archivo .zip** que contenga los siguientes archivos: ''t1.rkt'' para el desarrollo de la tarea, y  ''p1-tests.rkt'', ''p2-tests.rkt'' y ''p3-tests.rkt'', para los tests de cada una de las partes.
-  {+ x 3}}
-</code>
-  * (0.3) Defina la función ''%%(parse-type type)%%'' que parsea solo la gramática de tipos. Ademas en caso de error, debe retornar el error "Parse error" <code scheme>
-> (parse-type '{{Num -> Num} -> Num})
-(TFun (TFun (TNum) (TNum)) (TNum))
-> (parse-type '{Num ->  })
+<note important>
-"Parse error"
+Cada parte de esta tarea vale lo mismo: 2 puntos. La asignación de puntaje por parte sigue la misma estructura:
-</code>
+    * 0.2 para soportar la sintaxis indicada (parser bien definido y estructurado)
-  * (0.9) Defina la función ''%%(parse s-expr)%%'' para que acepte la gramática completa del lenguaje. Utilice la función ''%%(Parse-type type)%%'' en los puntos donde deba identificar tipos. Además, la función ''%%parse%%'' debe reemplazar el ''%%with%%'' por una aplicación de función. Ejemplos: <code scheme>
+    * 1.5 para las funcionalidades (p.ej. interprete para la P1)
-> (parse '{fun {x : Num} : Num {+ x 1}})
+    * 0.3 para testing (cobertura de todos los casos relevantes)
-(fun 'x (TNum) (add (id 'x) (num 1)) (TNum))
+</note>
-> (parse '{with {y : Num 2}
+===== Parte 1. Lenguaje con funciones de primer orden =====
-             {+ x y}})
+En esta parte, vamos a implementar un lenguaje que incluye primitivas útiles (números, booleanos, y sus operadores), identificadores locales (''with'' con n identificadores), y definiciones de funciones //top-level// de múltiples argumentos.
-(app (fun 'y (TNum) (add (id 'x) (id 'y)) #f) (num 2))
-</code>
-**Note que se usa ''%%#f%%'' cuando una función no tiene anotado un tipo de retorno.**
+Aquí está la gramática BNF del lenguaje:
+<code scheme>
+<prog>   ::= {<fundef>* <expr>}
-  * (0.3) Defina la función ''%%(prettify type)%%'' que tome un tipo y lo escriba en la sintaxis concreta.<code scheme>
+<fundef> ::= {define {<id> <id>*} <expr>}
-> (prettify (TNum))
-'Num
-> (prettify (TFun (TNum) (TFun (TNum) (TNum)))
+<expr>   ::= <num>
-'(Num -> (Num -> Num))
+           | <id>
+           | <bool>
+           | {<unop> <expr>}
+           | {<binop> <expr> <expr>}
+           | {if <expr> <expr> <expr>}
+           | {with {{<id> <expr>}*} <expr>}
+           | {<id> <expr>*}
+<unop>   ::= ! | add1 | sub1
+<binop>  ::= + | - | * | / | && | = | < | ...
 </code>
+Un programa está compuesto de (0 o más -- por eso la estrella ''*'' en el BNF) definiciones de funciones, además de una expresión final que sirve de punto de entrada (como el //main// en C y Java). Una definición de función incluye el nombre de la función, el nombre de los parámetros formales, y finalmente la expresión del cuerpo de la función. Las expresiones son estándar. Note que se define un nodo para cada familia de operadores (unarios y binarios), para evitar tener un nodo propio a cada operador en el AST.
-===== 2. Verificación de Tipos [1.5pt] =====
+<note>Recuerde que la estructura del BNF dicta la estructura de las funciones que procesan los programas, definiciones, expresiones, etc.</note>
-Se implementará el chequeo de tipos de una expresión en presencia de funciones de primera clase.
-  * (1.0) Implemente la función ''%%(typeof expr)%%'' que calcula el tipo de la expresión dada o falla con un mensaje de error en caso de que la expresión no sea válida. Para la validación, considere lo siguiente:
-     * Para una función con el tipo de retorno anotado, se valida que la expresión del cuerpo tenga el mismo tipo que el tipo de retorno declarado.
-     * Para una función sin el tipo de retorno anotado, el tipo resultante considera el tipo calculado del cuerpo de la función.
-     * Para la aplicación de función se valida que la expresión en posición de función sea efectivamente una función.
-     * Para la aplicación de función también se valida que el tipo de la expresión de argumento de la aplicación coincide con el tipo esperado del argumento de la función.
-     * Para la aplicación de un operador numerico se valida que sus operandos tengan el tipo correcto ''%%'Num%%''.
-Los mensaje de error de tipo tienen que seguir el siguiente patrón:
+Algunos ejemplos de programas válidos para este lenguaje pueden ser:
 <code scheme>
-"Type error in expression <E> position <n>: expected <T1> found <T2>"
+{ ;; Programa de Ejemplo 1
+   {define {sum x y z} {+ x {+ y z}}}
+   {define {max x y} {if {< x y} y x}}
+   {with {{x 9}}
+        {sum {max x 6} 2 -10} }
+}
+{ ;; Programa de Ejemplo 2
+   {with {{x 5} {y 7} {z 42}}
+         z}
+}
+{ ;; Programa de Ejemplo 3
+   {define {triple x} {* 3 x}}
+   {define {add2 x} {+ 2 x}}
+   {add2 {triple 2}}
+}
 </code>
- donde E es la expresión donde ocurrió el error, n es la sub-expresión donde se manifestó, T1 es el tipo esperado y T2 el tipo encontrado. Utilice su función prettify para mostrar errores legibles.
+En esta parte, su función ''run'' debe, como en clases, parsear y luego interpretar.
-**Note que la única forma de tener error de tipo de función, es cuando el tipo de retorno está anotado.**
+**Instrucciones importantes**:
+  * Para implementar el lenguaje, tiene que [[https://users.dcc.uchile.cl/~etanter/play-interps/Functions_with_Environments.html|usar ambientes]], y no una función de substitución.
+  * Tienen que verificar que los argumentos de los operadores booleanos sean booleanos (eso para alinear la verificación dinámica con la verificación estática que harán en la parte 2)
+  * En caso de programas con errores dinámicos, su interprete tiene que reportarlos explícitamente. Por ejemplo:
-Para el caso cuando hay algún identificador libre, el patrón es:
+<code scheme>{+ 1 #f}</code>
-<code scheme>
+debe caerse en tiempo de ejecución con un error (se levantan con ''(error msg)'', tal como lo hacemos en clase con los identificadores libres)
-"Type error: free identifier: <x>"
+<code scheme>"Runtime type error: expected Number found Boolean"</code>
-</code>
+Recuerde que puede testear estos errores con ''test/exn''.
- donde <x> es el identificador libre.
-Algunos ejemplos:
-  <code scheme>
-  > (typeof (parse '{fun {x : Num} : Num 5}))
-  (TFun (TNum) (TNum))
-  > (typeof (parse '{fun {x : Num} x}))
-  (TFun (TNum) (TNum))
-  > (typeof (parse '{{fun {x : Num} x} 1}))
-  (TNum)
-  > (typeof (parse '{fun {x : Num} : {Num -> Num} 10}))
-  "Type error in expression fun position 1: expected (Num -> Num) found Num"
-  > (typeof (parse '{1 2}))
-  "Type error in expression app position 1: expected (?T -> ?S) found Num"
-  > (typeof (parse '{{fun {x : Num} : Num {+ x x}} {fun {x : Num} : Num 5}}))
-  "Type error in expression app position 2: expected Num found (Num -> Num)"
-  >(typeof (parse '{fun{x : Num}{+ x {fun{z : Num} 1}}}))
-  "Type error in expression + position 2: expected Num found (Num -> Num)"
-  > (typeof (parse 'y))
-  "Type error: free identifier: y"</code>
-**Note que debe manejar identificadores adecuadamente, considere la implementación de un ambiente que almacene tipos.**
+-----
+===== Parte 2. Verificación estática y opcional de tipos =====
+En esta parte vamos a extender el lenguaje de la Parte 1 con anotaciones de tipos y verificación estática de ellos. Las diferencias en la sintaxis del lenguaje respecto de la parte anterior son:
+  * las declaraciones de función aceptan anotaciones de tipos en cada uno de sus argumentos, y también para el retorno
+  * las expresiones ''with'' aceptan anotaciones de tipos en cada identificador introducido
-    * (0.5) Implemente la función ''%%(typecheck s-expr)%%'' que retorna el tipo de un programa, en un formato legible:
+Observe que las anotaciones de tipos son siempre *opcionales* (en el BNF aquí usamos ''['' '']'' para especificar que lo que va adentro es opcional). La sintaxis es la siguiente:
+<code scheme>
+<fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} ; <prog> no cambia
-<code scheme>
+<arg>    ::= <id> | {<id> : <type>}
->(typecheck '3)
-'Num
->(typecheck  '{fun {f : Num} : Num 10})
+<expr>   ::= ... | {with { {<id> [: <type>] <expr>}* } <expr>}  ; los otros casos no cambian
-'(Num -> Num)
->(typecheck  '{+ 2 {fun {x : Num} : Num x}})
+<type>   ::= Num | Bool| Any
-  "Type error in expression + position 2: expected Num found (Num -> Num)"
+</code>
+Note que ''%%with%%'' no incluye anotación del tipo del cuerpo.
-</code>
+Para soportar la verificación opcional, lo que haremos es introducir un tipo comodín ''Any''. Cuando el usuario omite una anotación tipo, significa lo mismo que especificar ''Any''. El tipo ''Any'' es compatible con cualquier otro tipo: si una función espera un argumento de tipo ''Bool'', es válido pasarle algo de tipo ''Any''. Y vice versa: si una función espera un argumento de tipo ''Any'', es válido pasarle cualquier tipo de argumento.
-===== 3. Compilación [3.0pt]=====
-Ahora vamos a compilar nuestro lenguaje a una máquina abstracta basada en stack. La máquina es similar a la conocida SECD(([[https://en.wikipedia.org/wiki/SECD_machine|https://en.wikipedia.org/wiki/SECD_machine]])), la cual no trabaja con identificadores, sino que solo con índices. La máquina SECD consume una lista de instrucciones, utiliza un stack para almacenar datos temporales y posee un ambiente que, a diferencia del ambiente visto normalmente en el curso, es un arreglo con valores sin identificadores. La máquina SECD ya está definida en el archivo machine.rkt.
-La función ''%%(exec-machine ins-list)%%'' le permitirá ejecutar una lista de instrucciones en la máquina. <code scheme>
-> (exec-machine (list (INT-CONST 6) (INT-CONST 1) (ADD)))
-> (exec-machine (list (INT-CONST 3) (CLOSURE (list (ACCESS 0) (RETURN))) (APPLY)))
-</code>
-**Tome un tiempo para experimentar con la función ''%%exec-machine%%'' y el set de instrucciones antes de realizar los próximos ejercicios.**
-==== Índices De Bruijn ====
-Una forma de eliminar nombres de variables o identificadores de una expresión, es usando índices De Bruijn. Anteriormente vimos que la máquina SECD trabaja solo con índices, por lo que en esta sección vamos a hacer el paso de identificadores a dichos números, usando indices De Bruijn((La explicación detallada de como funcionan se puede encontrar en la sección 3.5 del [[http://cs.brown.edu/~sk/Publications/Books/ProgLangs/2007-04-26/plai-2007-04-26.pdf|PLAI]])).
-  * (1.5) Implemente la función ''%%deBruijn%%'' que toma una expresión y la recorre reemplazando los identificadores no libres, con los índices De Bruijn (nodos ''%%(acc n)%%'') manteniendo el scope léxico. La salida de esta función no debería tener nodos del tipo ''%%fun%%'', ni ''%% id%%''. En su lugar debería contener nodos del tipo ''%%fun-db%%'' y ''%%acc%%''. El resto de los nodos no varía.
-**Hint: le podría ser útil recordar que el intérprete visto en clases usa un ambiente para asociar identificadores a valores.**
+<note>
+Obviamente, usar el tipo ''Any'' puede terminar mal... con errores de ejecución! Pero al menos sabemos que si todos los tipos son definidos y no son ''Any'', entonces no pueden haber errores de tipos en ejecución.
+</note>
+Los programas siguientes son válidos, y bien tipados:
 <code scheme>
-> (deBruijn
+{{with {{x : Num 5} {y : Num 10}} {+ x y}}}
-   (parse '{+ 1 {with {x : Num 1}
-                           {with {y : Num 2}
-                                 {+ x y}}}}))
-(add
- (num 1)
- (app
-  (fun-db
-   (app (fun-db (add (acc 1) (acc 0))) (num 2)))
-  (num 1)))
-> (deBruijn (add (num 1) (id 'x)))
-"Free identifier: x"
-</code>
-==== De AST a código de máquina ====
-Vamos a abordar la compilación del AST de una expresión al set de instrucciones de la SECD.
-A continuación se presenta el esquema de compilación que permite hacer el paso del AST de una expresión a una lista de instrucciones (revise el archivo machine.rkt, todas las definiciones están comentadas y puede encontrar la sintaxis completa de las instrucciones). Note que solo es el paso a notación polaca inversa:  <code>
-C((num n)) = (INT-CONST n)
+{{define {gt42 x} : Bool {> x 42}}
-C((add a1 a2)) = C(a2);C(a1);(ADD)
+ {gt42 43}}
-C((sub a1 a2)) = C(a2);C(a1);(SUB)
-C((app f a)) = C(a); C(f);(APPLY)
+{{define {id {x : Num}} x}
+ {id 5}}
+{{define {add2 {x : Num}} {+ x 2}}
+ {with {{oops #f}}
+   {add2 oops}}}
 </code>
-La compilación de un nodo ''%%(acc n)%%'' es la siguiente:
+En particular, fíjese que el último ejemplo está bien tipado solamente porque se usa ''Any'' para ''oops''. Se debe caer con un error de tipo en ejecución (tal como en el parte 1). Si uno cambia la declaración de ''oops'' para especificar que es de tipo ''Bool''), entonces el programa ya no tipea, es decir, se reporta el error estáticamente.
-<code>
-C((acc n)) = (ACCESS n)
+En esta parte, deben definir una nueva función ''typecheck'' que toma un programa y nos retorna su tipo, o un error. A su vez, su función ''run'' debe parsear, typecheckear (este paso puede fallar), y luego interpretar.
+**Instrucciones**:
+  * Recuerden que la gramática BNF dicta la estructura de sus definiciones
+  * La verificación de tipos de un programa consiste en verificar que todas las definiciones de función estén bien tipadas, y que la última expresión tiene un tipo (no importa cual).
+  * Para una definición de función, se valida que la expresión del cuerpo tenga el mismo tipo que el tipo de retorno declarado, suponiendo que cada argumento tiene el tipo declarado. Recuerde que si no se especifica un tipo, se considera ''Any'', y que ''Any'' es válido en cualquier posición.
+  * Debe definir los tipos de los operadores primitivos de manera exacta, p.ej. ''%%!%%'' es como una función de ''Bool'' a ''Bool''. Para ''='', considere que solamente se aplica a números.
+  * Para una expresión ''%%if%%'' se verifica que la condición tenga tipo ''%%'Bool%%'' y que ambas ramas tengan el mismo tipo ''%%t%%''. El tipo resultante es t.
+  * Para ''%%with%%'' se verifica que todos los argumentos cumplan con el tipo y el tipo resultante será el del cuerpo de la expresión.
+  * En la aplicación de función se valida que el número de argumentos coincide, y que el tipo de los argumentos coincide con los tipos esperados de la función aplicada. La aplicación en sí tiene el tipo de retorno de la función aplicada.
+Para los errores:
+  * Los errores de identificadores libres (o funciones no definidas) se tienen que detectar estáticamente, antes o durante la verificación de tipos.
+  * Los mensajes de error de tipo detectados estáticamente tienen que seguir el siguiente patrón:
+<code scheme>"Static type error: expected T1 found T2"</code> donde ''T1'' es el tipo esperado y ''T2'' el tipo encontrado.
+Algunos ejemplos (no representan todos los casos, es de su responsabilidad entregar //test suites// completos):
+ <code scheme>
+  >  (typecheck '{3})
+  'Num  </code> <code scheme>
+  > (typecheck '{{define {f {p : Bool}} {&& p {! p}}}
+                          {f {> 3 4}}})
+  'Any </code> <code scheme>
+  > (typecheck '{{define {one {x : Num}} 1}
+                          {one #t}})
+  "Static type error: expected Num found Bool" </code> <code scheme>
+  > (typecheck '{{> 10 #t}})
+  "Static type error: expected Num found Bool"</code> <code scheme>
+   > (typecheck '{{if 73 #t #t}})
+  "Static type error: expected Bool found Num"</code> <code scheme>
+  > (typecheck '{{with {{x 5} {y : Num #t} {z 42}}
+                            z}})
+  "Static type error: expected Num found Bool"</code>
+¿Puede efectivamente convencerse de que todo programa que pasa la verificación de tipo no se cae con un error de tipo durante la ejecución?
+----
+===== Parte 3. Contratos en funciones de primer orden (2.0 pt) =====
+Ahora vamos a añadir verificación dinámica mediante contratos a las funciones de nuestro lenguaje. El único cambio en la sintaxis del lenguaje se ve reflejado en la definición de funciones, donde ahora se puede definir además un contrato para cada argumento:
+<code scheme>
+<fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} ; como antes
+<arg>    ::= <id> | {<id> : <type>}        ; como antes
+           | {<id> [: <type>] @ <contract>}  ; lo único nuevo
 </code>
-La compilación de una función puede ser inferida del ejemplo a continuación: <code scheme>
+Un contrato corresponde a un predicado, una función que reciba exactamente un argumento y retorne un booleano. Un ejemplo de programa válido puede ser:
-> (compile (deBruijn (parse '{{fun {x : Num} : Num
+<code scheme>
-                                   {+ x 10}} {+ 2 3}})))
+{{define {positive x} : Bool {> x 0}}
-(list
+ {define {div {x : Num @ positive} y}
- (INT-CONST 3)
+           {/ y x}}
- (INT-CONST 2)
+ {div 5 3}}
- (ADD)
- (CLOSURE (list (INT-CONST 10) (ACCESS 0) (ADD) (RETURN)))
- (APPLY))
 </code>
+Donde el ''x'' posee como contrato la función ''positive'', que comprueba en tiempo de ejecución que ''x'' sea mayor que 0.
+Note que la información de tipo estático es opcional, por lo que uno puede especificar una función solamente mediante contratos.
+<code scheme>
+{{define {positive x} : Bool {> x 0}}
+ {define {div {x @ positive} y}  ; aquí sólo se especifica un contrato
+           {/ y x}}
+ {div 5 3}}
+</code>
-  * (1.0) Implemente la función ''%%(compile expr)%%'' que dada una expresión con índices De Bruijn genera la lista de instrucciones siguiendo el esquema de compilación descrito anteriormente.
+En esta parte, su función ''run'' debe hacer lo mismo que en la parte 2. Solamente que la interpretación ahora incluye verificar contratos.
-  * (0.5) Implemente la función ''%%(typed-compile s-expr)%%'' que se encarga de todo el proceso de generación de código desde un programa, considerando el parsing, la validación de tipos, y la transformación con índices De Bruijn. Note que esta función solo genera código de maquina si la expresión esta bien tipada, sino produce el error correspondiente.
+**Instrucciones**:
+  * En el intérprete, cuando se efectua una aplicación de función, se tiene que verificar que sus argumentos cumplan con los contratos declarados (de existir -- sino, procede como antes).
+  * Cuando el contrato no se cumpla, el patrón de error es: <code scheme>
+"Runtime contract error: <v> does not satisfy <contract>"
+</code> donde ''<v>'' es el valor al que se le aplicó el contrato <contract> el nombre de este.
+  * Para poder ser usado como contrato, una función *debe* tener aceptar un argumento de tipo ''Any'' y retornar un valor de tipo ''Bool''. Sino, el patrón de error es : <code scheme>
+"Static contract error: invalid type for <c>"
+</code>  donde ''<c>'' es el nombre del contrato que no tipa.
+Más ejemplos:
+<code scheme>
+{{define {lt100 x} {< x 100}}
+ {define {positive x} : Bool {> x 0}}
+ {define {percentage? x} : Bool {&& {lt100 x} {positive x}}}
+ {define {calc {x @ positive} {y @ percentage?}}
+           {/ {* y y} x}}
+ {calc 25 3}}
+</code>
+<code scheme>
+> (run '{{define {add x y} : Num {+ x y}}
+         {define {oh-no {x @ add} y}
+                    #t}
+         {oh-no 21 21}})
+"Static contract error: invalid type for add"
+</code>