Parte 1: sistema de tipos

1. Implemente un interprete para un lenguaje con booleanos, numeros, if, y funciones de primera clase con scope léxico.
2. Implemente un verificador de tipos para este lenguaje, basado en el simply-typed lambda calculus

Parte 2: contratos

1. Extienda su lenguaje con la posibilidad de aumentar tipos con contratos sobre números. Un contrato es una función que expresa alguna condición arbitraria sobre un valor. Por ejemplo (usando una sintaxis arbitraria, pero algo intuitiva):

(define (in-range min max)
  (lambda (v)
    (and (> v min) (< v max))))
    
(lambda (n : nat[(in-range 0 10)]) ...)

Esa función sólo acepta un parámetro númerico en el rango ]0;10[.

1. Los contratos no pueden ser verificados estáticamente (¿porque?). Extienda su interprete para enforzar contratos. Al igual que el PLAI Scheme, su interprete debe generar un error cada vez que se viola un contrato, reportando lo más precisamente posible sobre la causa del error (sugerencia: pueden diseñar su lenguaje tal que sea posible darle un nombre a las lambdas, y usar ese nombre para reportar sobre funciones, que sean contratos o no).
2. Extienda su sistema de contratos para poder especificar un contrato sobre el valor retornado por una función.

Parte 3: contratos de orden superior

PLT Scheme tiene un sistema de contratos que permite especificar contratos de orden superior, o sea, contratos sobre funciones. Por ejemplo:

(define foo
  (lambda (f : nat[(in-range 0 10)] -> nat[(in-range 20 30)])
     ...))

La función foo acepta como parámetro una función que debe respetar el hecho de que: dado un parámetro entre 0 y 10, retorna un valor entre 20 y 30. Analiza cuando es posible verificar cumplimiento de un contrato de orden superior. Notese que en el ejemplo, el contrato sobre el parámetro f puede fallar si (a) f es aplicada con un parametro que no esta entre 0 y 10 (ahi la “culpa” es de quien aplica f), o si (b) dado un parámetro correcto, f no retorna un valor entre 20 y 30 (ahi la “culpa” es de f).

1. Extienda su lenguaje para soportar contratos de orden superior (nuevamente, pueden usar el nombre de las funciones para reportar sobre quien tiene la “culpa” al momento de una violación de contrato).

Parte 4 (opcional pregrado / obligatorio posgrado)

1. Formalize su lenguaje con contratos de orden superior
2. Explique y formule precisamente una noción de coherencia (soundness) para este lenguaje
3. Demuestre la coherencia de su lenguaje.

Instrucciones

Como siempre, para cada paso entregue código debidamente comentado, con tests y ejemplos ilustrativos.

Para la parte 4, use LaTeX (o algo equivalente, si hay ;)), y entregue un PDF. Si necesita ayuda con LaTeX, estudie ese breve ejemplo.

Puntaje:

• pregrado: P1=2 / P2=2 / P3=2 / P4=+1 (opcional)
• posgrado: P1=1 / P2=1.5 / P3=1.5 / P4=2

Fecha de entrega: Miercoles 22 de Septiembre, por U-Cursos.