Differences

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

--- teaching:cc4101:tareas:2021-1:tarea1 [2021/04/12 21:35] – removed 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: 7 de mayo de 2021) ======
+==== Tipos estáticos, tipos opcionales, contratos ====
+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.).
+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.
+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.
+</note>
+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.
+<note important>
+Cada parte de esta tarea vale lo mismo: 2 puntos. La asignación de puntaje por parte sigue la misma estructura:
+    * 0.2 para soportar la sintaxis indicada (parser bien definido y estructurado)
+    * 1.5 para las funcionalidades (p.ej. interprete para la P1)
+    * 0.3 para testing (cobertura de todos los casos relevantes)
+</note>
+===== Parte 1. Lenguaje con funciones de primer orden =====
+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.
+Aquí está la gramática BNF del lenguaje:
+<code scheme>
+<prog>   ::= {<fundef>* <expr>}
+<fundef> ::= {define {<id> <id>*} <expr>}
+<expr>   ::= <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.
+<note>Recuerde que la estructura del BNF dicta la estructura de las funciones que procesan los programas, definiciones, expresiones, etc.</note>
+Algunos ejemplos de programas válidos para este lenguaje pueden ser:
+<code scheme>
+{ ;; 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>
+En esta parte, su función ''run'' debe, como en clases, parsear y luego interpretar.
+**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:
+<code scheme>{+ 1 #f}</code>
+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)
+<code scheme>"Runtime type error: expected Number found Boolean"</code>
+Recuerde que puede testear estos errores con ''test/exn''.
+-----
+===== 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
+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
+<arg>    ::= <id> | {<id> : <type>}
+<expr>   ::= ... | {with { {<id> [: <type>] <expr>}* } <expr>}  ; los otros casos no cambian
+<type>   ::= Num | Bool| Any
+</code>
+Note que ''%%with%%'' no incluye anotación del tipo del cuerpo.
+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.
+<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>
+{{with {{x : Num 5} {y : Num 10}} {+ x y}}}
+{{define {gt42 x} : Bool {> x 42}}
+ {gt42 43}}
+{{define {id {x : Num}} x}
+ {id 5}}
+{{define {add2 {x : Num}} {+ x 2}}
+ {with {{oops #f}}
+   {add2 oops}}}
+</code>
+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.
+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>
+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:
+<code scheme>
+{{define {positive x} : Bool {> x 0}}
+ {define {div {x : Num @ positive} y}
+           {/ y x}}
+ {div 5 3}}
+</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>
+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.
+**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>