Tarea 1b (Entrega: Jueves 18 de Abril de 2023 - fecha por confirmar)

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

En esta tarea van a implementar un lenguaje simple con funciones de primer orden, tipos de datos básicos y pares. Para implementar este lenguaje necesitaremos un parser (lo implementamos en la tarea 1a), y un interprete, dividiremos el desarrollo de esta tarea en dos partes (más una opcional). Primero, el lenguaje contará sólo con chequeo dinámico de tipos (parte 1), para luego agregar verificación de tipos estáticos (parte 2). Opcionalmente (como bonus), puede agregar contratos dinámicos para funciones (parte 3).

Deben entregar via U-cursos un archivo .zip que contenga los siguientes archivos: p1.rkt, p1-test.rkt, p2.rkt, p2-test.rkt, archivos que deberán contener las funcionalidades solicitadas en cada pregunta y los tests respectivos.

Si lo desea, puede obtener un bonus resolviendo la tercera parte, que es opcional: p3.rkt y p3-test.rkt. Más detalles al final del documento.

Deben entregar vía U-Cursos un único archivo .zip que contenga todos los archivos de su entrega.

En esta parte, vamos a implementar un lenguaje que incluye primitivas útiles (números, booleanos, pares, y operadores simples), identificadores locales (with con una cantidad arbitraria de identificadores), y definiciones de funciones top-level de múltiples argumentos.

La gramática BNF del lenguaje se define a continuación:

<prog>   ::= {<fundef>* <expr>}
 
<fundef> ::= {define {<id> <id>*} <expr>}
 
<expr>   ::= <num>
           | <id>
           | <bool>
           | {cons <expr> <expr>}
           | {add1 <expr>}
           | {+ <expr> <expr>}
           | {- <expr> <expr>}
           | {< <expr> <expr>}
           | {= <expr> <expr>}
           | {! <expr>}
           | {&& <expr> <expr>}
           | {|| <expr> <expr>}
           | {fst <expr>}
           | {snd <expr>}
           | {if <expr> <expr> <expr>}
           | {with {<binding>*} <expr>}
           | {<id> <expr>*}
 
<binding> ::= (<id> <expr>)
 

Esta gramática es similar a la presentada en la tarea 1a, con las siguientes diferencias.

• Se agregan dos operadores booleanos extra, estos son && y ||.
• Se agregan pares, un par define utilizando cons, y las expresiones fst y snd permiten obtienen el primer y segundo elemento, respectivamente (similar a car y cdr de Racket).

Los programas que terminan reducen a valores. Estos pueden ser números, booleanos o pares de valores. Siguiendo buenas prácticas, definimos un tipo de dato inductivo Val para los valores (provisto en el código fuente de la parte 1). Note que nuestro lenguaje no trabajará con valores de Racket, por lo que necesitaremos funciones de lifting para poder aplicar funciones de Racket a nuestros Val (por ejemplo, los operadores aritméticos).

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

{
   {with {{x 3}
          {y {+ 1 2}}}
       {if {= x y} x y}}
}
 
{
   {with {{x 5}
          {y 42}}
       {cons x z}}
}
 
{
   {define {sum x y z} {+ x {+ y z}}}
   {define {cadr x} {fst {snd x}}}
   {with {{x 9}
          {y {cons 1 {cons 3 4}}}}
       {sum x {fst y} {cadr y}} }
}

Observaciones importantes:

• Recuerde que la estructura del BNF dicta la estructura de las funciones que procesan los programas, definiciones, expresiones, etc.
• Al implementar el lenguaje, asegúrese de hacerlo utilizando ambientes, y no una función de substitución.
• La semántica debe considerar alcance léxico, no dinámico.
• Verifique en tiempo de ejecución que los argumentos de los operadores numéricos sean numéricos. Y que los argumentos de los operadores de pares sean pares (En la parte 2 se alineará la verificación dinámica con la verificación estática).
• Considere que la igualdad solo es válida sobre números.
• La condición de una expresión if debe ser un booleano.
• Puede definir funciones de lift para aplicar operadores de Racket a valores del lenguaje.
• En caso de programas con errores dinámicos, su intérprete tiene que reportarlos explícitamente. Por ejemplo:

{+ 1 {cons 3 4}}

debe fallar 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 Pair"

Recuerde que puede verificar si un test lanza una excepción con test/exn.

Mediante una función run recibimos un programa en sintaxis concreta y lo interpretamos para producir un valor.

• Obtenemos el programa a partir de la entrega con parse :: s-Prog → Prog
• Ejecutamos el programa resultante con interp :: Expr Env List[Fundef] → Val or error

Para desarrollar el intérprete, dividiremos su implementación en las siguientes funciones:

En esta parte vamos a extender el lenguaje 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 incluyen anotaciones de tipos en cada uno de sus argumentos y también para el tipo de retorno.
• Las expresiones with pueden incluir anotaciones de tipos en cada identificador introducido.

La nueva sintaxis concreta es la siguiente:

;; <prog> y <expr> no cambian
 
<fundef> ::= {define {<id> {arg}*} : <type> <expr>} 
 
<arg>    ::= {<id> : <type>} 
 
<binding> ::= {<id> [: <type>] <expr>}
 
<type>   ::= Num | Bool | {Pair <type> <type>}

En el BNF utilizamos [ ] para denotar que algo es opcional. Note que with no incluye anotación del tipo del cuerpo y que los tipos de los identificadores son opcionales. Por otro lado, el tipo de retorno de una función siempre debe estar presente, al igual que el de cada uno de sus argumentos.

A continuación puede ver ejemplos de programas en la nueva sintaxis, los que (además) están bien tipados:

{
  {with {{x : Num 5}
         {y : Num 10}} 
     {+ x y}}
}
 
{
  {with {{x 5}}
     {with {{y : Num {+ x 1}}} 
        {+ x y}}
}
 
{
  {define {add-pair {p : {Pair Num Num}} {x : Num}} : {Pair Num Num} 
    {cons {+ {fst p} x} {+ {snd p} x}}}
  {add-pair {cons 1 1} 1}
}
 
{
  {define {id {x : Num}} : Num x}
  {id 5}
}
 
{
  {define {sum {x : Num} {y : Num} {z : Num}} : Num 
    {+ x {+ y z}}}
  {define {cadr {x : {Pair Num {Pair Num Num}}}} : Num 
    {fst {snd x}}}
  {with {{x 9}
         {y {cons 1 {cons 3 4}}}}
     {sum x {fst y} {cadr y}} }
}

Note que se agregó el nodo <arg> al BNF, el cual especifica la sintaxis concreta de un argumento de función.

1. [0.0 pts] Defina el tipo de datos Arg que representa a un argumento de función en el AST.
2. [0.0 pts] Implemente la función parse-arg que parsea un argumento de función.
3. [0.0 pts] Modifique la función parse-fundef para que utilice parse-arg para parsear los argumentos.

Además de lo anterior, observe que el nodo <binding> en el BNF cambió, y ahora puede incluir una anotación opcional de tipo para el identificador que se introduce.

1. [0.0 pts] Modifique el tipo de datos Binding para que pueda almacenar el tipo del identificador.
2. [0.0 pts] Modifique la función parse-binding para que acepte una anotación opcional de tipo. Nota: Cuando no se especifica el tipo, puede guardar el valor #f en el lugar donde se almacenaría el tipo.

Para poder realizar un checkeo de tipos estático, necesitaremos:

1. [0.0 pts] Implementar la función typecheck-expr :: Exp → Type/err que toma una expresión y nos retorna su tipo, o lanza un error.
2. [0.0 pts] Implementar typecheck-fundef :: Fundef → Type/err que recibe una definición de función de primer orden y nos retorna su tipo, o lanza un error.
3. [0.0 pts] Implementar typecheck :: Prog → Type/err que toma un programa y nos retorna su tipo, o lanza un error.
4. [0.0 pts] Extender la función run para que verifique el tipo del programa (este paso puede fallar) antes de interpretarlo.

Observaciones importantes:

• 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 cuál).
• 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.
• Debe definir los tipos de los operadores primitivos de manera exacta, p.ej. < es una operación que toma dos Num y retorna Bool.
• Considere que la igualdad (=) solo puede comparar números.
• Para una expresión if la condición debe tener tipo Bool y ambas ramas deben tener el mismo tipo t. El tipo resultante de la expresión if es t.
• Para with se verifica que todos los argumentos cumplan con el tipo declarado y el tipo resultante será el del cuerpo de la expresión. Si los identificadores no tienen tipo explícito, entonces se les asigna el de la expresión asociada.
• 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. El tipo resultante de una aplicación es el tipo de retorno de la función aplicada.

Comportamiento del typecheck:

• Necesitará almacenar en un ambiente el tipo de las variables introducidas por algún bind para poder completar el typecheck.
• El typecheck de un operador unario o binario verifica que el tipo de los datos que recibe correspondan con los tipos de los datos que se esperan para ese operador.
• El typecheck de un with verifica para cada binding que la expresión cumpla con el tipo declarado para esa variable, en caso de que la variable no tenga un tipo declarado, este se obtiene a partir de la expresión.
• El typecheck de la aplicación de una función de primer orden verifica cumple con la aridad de la función, y que el tipo de los parámetros que recibe correspondan con los tipos de los datos declarados en su firma.

Para los errores:

• Los errores de identificadores libres (o funciones no definidas). Este error debe detectarse estáticamente.
• 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})
  (numT)  

  > (typecheck '{{define {f {p : Bool}} {if p 23 42}}
                          {f {< 3 4}}})
  (numT) 

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

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

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

  > (typecheck '{{with {{x : Num 5} {y : Num #t} {z : Num 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> : <type>}        ; como antes
           | {<id> : <type> @ <contract>}  ; lo único nuevo

Un contrato corresponde a un predicado, una función que recibe exactamente un argumento y retorna un booleano. Un ejemplo de programa válido puede ser:

{{define {positive {x : Num}} {< 0 x}}
 {define {sub {x : Num @ positive} {y : Num}} : Num
           {- y x}}
 {sub 5 3}}

Donde el argumento x posee como contrato la función positive, que comprueba en tiempo de ejecución que x sea mayor que 0.

• Extienda nuevamente su función run para que verifique los contratos en tiempo de ejecución.

Observaciones importantes:

• En el intérprete, cuando se efectúa una aplicación de función, se debe que verificar que los argumentos cumplan con los contratos declarados (en caso de que existan).
• Cuando el contrato no se cumpla, se debe lanzar un error con el siguiente patrón:

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

• Una función usada como contrato debe aceptar un solo argumento de cualquier tipo válido y debe retornar un valor de tipo Bool. En caso de no cumplir esta condición se debe lanzar un error con el siguiente patrón:

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

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

Más ejemplos:

{{define {positive {x : Num}} : Bool {< 0 x}}
 {define {negate {x : Num @ positive}} : Num {- 0 x}}
 {negate 23}}

{{define {pair-non-zero? {p : {Pair Num Num}}} : Bool {&& {= 0 {fst p}} {= 0 {snd p}}}}
 {define {pair-div {p : {Pair Num Num} @ pair-non-zero?}} : Num {/ {fst x} {snd x}}}
 {+ {pair-div {cons 30 5}} {pair-div {cons 60 0}}}
}
"Runtime contract error: (60,0) does not satisfy pair-non-zero?"

> (run '{{define {add {x : Num} {y : Num}} : Num {+ x y}}
         {define {oh-no {x : Num @ add}} : Bool x}
         {oh-no 21 21}})
"Static contract error: invalid type for add"