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

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:

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

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.

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

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

Instrucciones importantes:

• Para implementar el lenguaje, tiene que 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:

{+ 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"

Recuerde que puede testear estos errores con test/exn.

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:

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

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

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

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:

"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 {f {p : Bool}} {&& p {! p}}}
                          {f {> 3 4}}})
  'Any 

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

¿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?

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:

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