Table of Contents

Tarea 1 (Entrega: 24 de Abril de 2022)

Tipos estáticos y 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.).

En esta tarea van a implementar un lenguaje simple con funciones de primer orden, tipos de datos básicos y pares. 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) y finalmente agregar contratos dinámicos para funciones (parte 3).


Consulte las normas de entrega de tareas en http://pleiad.cl/teaching/cc4101. Recuerden que tienen que seguir la metodología vista en las primeras clases y dejar sus funciones debidamente documentadas.

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

La asignación de puntaje, de cada pregunta, sigue la siguiente estructura:
  • 0.2 para soportar la sintaxis indicada (parser bien definido y estructurado)
  • 0.3 para testing (cobertura de todos los casos relevantes)
  • Puntaje restante para las funcionalidades (p.ej. intérprete para la P1)

Parte 1. Lenguaje con funciones de primer orden (2.0 ptos.)

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.

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

<prog>   ::= {<fundef>* <expr>}
 
<fundef> ::= {define {<id> <id>*} <expr>}
 
<expr>   ::= <num>
           | <id>
           | <bool>
           | {cons <expr> <expr>}
           | {+ <expr> <expr>}
           | {< <expr> <expr>}
           | {= <expr> <expr>}
           | {fst <expr>}
           | {snd <expr>}
           | {if <expr> <expr> <expr>}
           | {with {{<id> <expr>}*} <expr>}
           | {<id> <expr>*}
 

Un programa está compuesto de 0 o más 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 fst y snd obtienen el primer y segundo elemento de un par, respectivamente (similar a car y cdr de Racket). Las demás expresiones siguen la presentación estándar vista en clases.

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

{ ;; Programa de Ejemplo 1
   {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}} }
}
{ ;; Programa de Ejemplo 2
   {with {{x 5} {y 42} {z {cons 11 -3}}}
         z}
}
{ ;; Programa de Ejemplo 3
   {define {triple x} {+ x {+ x x}}}
   {define {add2 x} {+ 2 x}}
   {add2 {triple 2}}
}
 
{ ;; Programa de Ejemplo 4
   {with {{x 3} {y {+ 1 2}}}
         {if {= x y} x y}}
}

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

Observaciones importantes:

{+ 1 {cons 3 4}}

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

Recuerde que puede testear estos errores con test/exn.


Parte 2. Verificación estática de tipos (2.5 ptos.)

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:

La nueva sintaxis es la siguiente:

;; <prog> no cambia
 
<fundef> ::= {define {<id> <arg>*} [: <type>] <expr>} 
 
<arg>    ::= {<id> : <type>}
 
<expr>   ::= ... | {with { {<id> [: <type>] <expr>}* } <expr>}  ; los otros casos no cambian
 
<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. Igualmente, el tipo de retorno de una función es opcional, pero el de cada argumento es necesario. Para funciones recursivas, pueden asumir que el tipo de retorno tiene que ser especificado.

Los programas siguientes están bien tipados:

{ ; Programa de ejemplo 1
  {with {{x : Num 5} {y : Num 10}} 
    {+ x y}}
}
 
{ ; Programa de ejemplo 2
  {with {{x 5}}
    {with {{y : Num {+ x 1}}} 
      {+ x y}}
}
 
{ ; Programa de ejemplo 3
  {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}
}
 
{ ; Programa de ejemplo 4
  {define {id {x : Num}} x}
  {id 5}
}
 
{ ; Programa de ejemplo 5
  {define {sum {x : Num} {y : Num} {z : 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}} }
}

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.

Observaciones importantes:

Para los errores:

"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}} {if p 23 42}}
                          {f {< 3 4}}})
  (Num) 
  > (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?


Parte 3. Contratos en funciones de primer orden (1.5 ptos.)

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 x posee como contrato la función positive, que comprueba en tiempo de ejecución que x sea mayor que 0.

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.

Observaciones importantes:

Más ejemplos:

{{define {positive {x : Num}} {< 0 x}}
 {define {negate {x : Num @ positive}} -x}
 {negate 23}}
{{define {pair-lt100? {x : {Pair Num Num}}} {if {< {fst x} 100} {< {snd x} 100} #f}}
 {define {sum-pair {x : {Pair Num Num} @ pair-lt100?} {+ {fst x} {snd x}}}}
 {< 200 {sum-pair {cons 80 50}}}}
> (run '{{define {add {x : Num} {y : Num}} {+ x y}}
         {define {oh-no {x : Num @ add}} x}
                    #t}
         {oh-no 21 21}})
"Static contract error: invalid type for add"