Tarea 1 (Entrega: 7 de mayo de 2021)

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!

Deben entregar via U-cursos un archivo .zip que contenga los archivos t1.rkt, p1-tests.rkt, p2-tests.rkt y p3-tests.rkt, los cuales deben que implementar lo que se solicita en las preguntas siguientes.

En esta parte, buscamos definir un lenguaje que incluye primitivas útiles (números, booleanos, y sus operadores), que admita el uso de with (con n variables), y definiciones de funciones top-level de múltiples argumentos.

Aquí está la gramática BNF del lenguaje:

<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>  ::= + | - | * | / | && | eq? | < | ...

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).

Algunos ejemplos de programas válidos para este lenguaje pueden ser:

{ ;; 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}}
}
 
{ ;; Programa de Ejemplo 4
   {define {two-or-forty-two? x} {or {eq? x 2} {eq? x 42}}}
   {define {magic x y} {if {two-or-forty-two x}
                           {two-or-forty-two y}
                           #f}}
   {magic 42 2}
}

Instrucciones importantes:

• Para implementar el lenguaje, tiene que usar ambientes, y no una función de substitución.
• En caso de programas con errores dinámicos, su interprete tiene que reportarlos explícitamente. Por ejemplo:

{+ 1 #f}

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)

"Runtime type error: expected Number found Boolean"

En esta parte, su función run debe, como en clases, parsear y luego interpretar.

En esta parte usaremos de base el lenguaje logrado en la pregunta 1 y le añadiremos anotaciones de tipos. Las diferencias en la sintaxis del lenguaje (con respecto a 1), serán que en esta parte las declaraciones de función y las expresiones with aceptan tipos opcionales en cada uno de sus argumentos y que además, las funciones pueden poseer anotado un tipo de retorno (también opcional).

La sintaxis es la siguiente:

<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

Note que los [ ] son parte de la notación BNF, especificando que lo que va adentro es opcional. 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 no especifica ningú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.

Los programas siguientes son válidos, y bien tipados:

{{with {x : Num 5} {+ x 3}}}
 
{{define {gt42 x} : Bool {> x 42}}
 {gt42 43}}
 
{{define {id {x : Num}} x}
 {id 5}}
 
{{define {add1 {x : Num}} {+ x 1}}
 {with {oops #f}
   {add1 oops}}}

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.
• Deben definir los tipos de los operadores primitivos de manera exacta, p.ej. ! es como una función de Bool a Bool. Para eq?, considere que es de tipo Any Any → Bool, para poder comparar números o booleanos (ojo, comparar un booleano con un numero debe levantar un error de tipo dinámico).
• Para la sentencia 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:
  1. El número de argumentos coincide
  2. El tipo de los argumentos coincida con los tipos esperados de la función aplicada (aquí nuevamente, módulo Any).

Para los errores:

• Los errores de identificadores libres se tienen que detectar estáticamente, antes o durante la verificación de tipos.
• Los mensaje de error de tipo tienen que seguir el siguiente patrón:

"Static type error: expected T1 found T2"

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):

  >  (typecheck '{3})
  'Num  

  > (typecheck '{{define {false {p : Bool}} {&& p {not p}}}
                          {false {> 3 4}}})
  'Bool 

  > (typecheck '{{define {one {x : Num}} 1}
                          {one #t}})
  "Static type error: expected Num found Bool" 

  > (typecheck '{> 10 #t})
  "Static type error: expected Num found Bool"

   > (typecheck '{if 73 #t #t})
  "Static type error: expected Bool found Num"

  > (typecheck '{with {{x 5} {y : Num #t} {z 42}}
                            z})
  "Static type error: expected Num found Bool"

Tomando como base el lenguaje generado en el ítem anterior, se procede a añadir una verificación dinámica mediante contratos en funciones de primer orden. 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:

<fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} ; como antes
<arg>    ::= <id> | {<id> : <type>}        ; como antes
           | {<id> [: <type>] @ <contract>}  ; lo único nuevo

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:

{{define {positive x} : Bool {> x 0}}
 {define {div {x : Num @ positive} y}
           {/ y x}}
 {div 5 3}}

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.

{{define {positive x} : Bool {> x 0}}
 {define {div {x @ positive} y}  ; aquí sólo se especifica un contrato
           {/ y x}}
 {div 5 3}}

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:

  "Runtime contract error: <v> does not satisfy <contract>"

  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 :

  "Static contract error: invalid type for <c>"

  donde <c> es el nombre del contrato que no tipa.

Más ejemplos:

{{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}}

> (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"