2015/1 -- Tarea 3
Fecha de Entrega: Viernes 5 de Junio
Recuerden las reglas de entrega.
P1 - Estructuras Inductivas y Pattern Matching (2.0pt)
Defina un lenguaje con funciones de primera clase de múltiples argumentos, en donde los únicos otros valores son estructuras definibles por el usuario. Una definición de estructuras inductivas cuenta con una definición de tipo, y sus constructores asociados usando deftype. Para esta pregunta solo considere los tipos como anotaciones y asuma que no hay dos definiciones para tipos ni constructores con el mismo nombre (incluso para tipos distintos). En el siguiente ejemplo el programador define los números naturales a través de un tipo inductivo nat y dos constructores O y S, que simbolizan el 0 y el sucesor de un natural, respectivamente.
(run '{{deftype nat {O : nat} {S : {nat -> nat}}} {O}}) > "(O) : nat"
Cada constructor genera estructuras del tipo nat al ser aplicado. Puede representar sus estructuras como le parezca conveniente pero la función run siempre debe retornar un String con el tipo correspondiente como en los ejemplos. Dos tipos de constructores son posibles, con o sin argumentos. En el ejemplo O corresponde a un constructor que no requiere parámetros y construye un elemento de tipo nat ({O : nat} es un azucar sintáctico para una función con tipo () → nat). El constructor S usa un elemento de tipo nat para construir otro elemento de tipo nat. El tipo expr posee dos constructores num y add que usa dos expr para construir un elemento.
(run '{{deftype nat {O : nat} {S : {nat -> nat}}} {deftype expr {num : {nat -> expr}} {add : {expr expr -> expr}}} {add {num {S {O}}} {num {O}}}}) > "(add (num (S (O))) (num (O))) : expr"
Asociar una función a un nombre se realiza usando def, donde las funciones tienen anotación de tipo para sus argumentos y retorno. En el caso de pred, la función utiliza pattern matching para retornar su resultado, en ese caso se espera que primero se interprete el elemento a matchear n para luego ir comprobando uno a uno, con que patrón coincide. Si en un case el patrón incluye un identificador libre, este funciona como un binding para el cuerpo del caso (ejemplo case {S n1} ⇒ n1})
(run '{{deftype nat {O : nat} {S : {nat -> nat}}} {def pred {n : nat} : nat {match n {{case {O} => {O}} {case {S n1} => n1}}}} {pred {S {O}}}}) > "(O) : nat"
En caso de no encontrar un case que corresponda:
(test/exn (run '{{deftype bool {t : bool} {f : bool}} {def not {b : bool} : bool {match b {{case {t} => {f}}}}} {not {f}}) "match error")
De todas formas un identificador puede servir para hacer match de los casos restantes:
(run '{{deftype day {monday : day} {tuesday : day} {wednesday : day} {thursday : day} {friday : day} {saturday : day} {sunday : day}} {deftype bool {t : bool} {f : bool}} {def weekday {d : day} : bool {match d {{case {saturday} => {f}} {case {sunday} => {f}} {case otherday => {t}}}}} {weekday {monday}}}) > "(t) : bool"
Funciones definidas con def pueden ser recursivas y tener más de un argumento.
(run '{{deftype bool {t : bool} {f : bool}} {deftype nat {O : nat} {S : {nat -> nat}}} {def not {b : bool} : bool {match b {{case {t} => {f}} {case {f} => {t}}}}} {def even {n : nat} {b : bool} : bool {match n {{case {O} => b} {case {S n1} => {even n1 {not b}}}}}} {even {S {S {S {O}}}} {t}}}) > "(f) : bool"
Las funciones se representan por el simbolo lambda:
(run '{{deftype bool {t : bool} {f : bool}} {fun {x : bool} x}) > "λ"
A continuación se presenta la gramática BNF del lenguaje. Observe que la definición de funciones con def permite múltiples argumentos y por tanto el constructor de tipos → recibe una lista de tipos en la entrada. Puede asumir que para toda la tarea nunca se van a entregar dos argumentos con el mismo nombre.
<prog> ::= {<def>* <expr>} <def> ::= {deftype <id> {<id> : <type>}+} | {def <id> {<id> : <type>}* : <type> <expr>} <type> ::= <id> | {<type>+ -> <type>} <expr> ::= <id> | {fun {<id> : <type>}+ <expr>} | {match <expr> {<case>+}} | {<expr> <expr>*} <case> ::= {case <pattern> => <expr>} <pattern> ::= <id> | {<id> <id>*}
- Defina el AST para soportar programas del lenguaje. Note que un programa es una lista de definiciones seguida de una expresión. Dos tipos de definiciones son posibles
deftypeydef. - Defina la función
parser :: s-expr → Exprque parsea el lenguaje - Defina la función
interp :: Expr Env → Valque evalua un programa con semántica eager. - Defina la función
run :: s-expr → Stringque toma un programa fuente y retorna la representación en String del valor resultante de la interpretación con su tipo anotado. Es recomendable definir una función auxiliar que le permita pasar de su representación de estructuras a la notación de los ejemplos con Strings.
P2 - Sistema de Tipos (2.0pt)
Para el lenguaje de esta tarea, se solicita crear un sistema de tipos. Los tipos del lenguaje corresponden a los tipos definidos con deftype y a los creados con el constructor de tipos →.
Las definiciones de funciones llevan anotado el tipo de retorno, pues es necesario para verificar la correctitud de funciones recursivas.
Defina un sistema de tipos con la función typeof :: s-expr → String que retorna el tipo de un programa o termina en error según los siguientes casos:
(error “TYPE ERROR: wrong argument type”): En caso de que algún argumento no tenga el tipo esperado para el tipo de entrada de la función en una aplicación.(error “TYPE ERROR: application of a non-function”): Cuando se intente aplicar un valor que no es función.(error “TYPE ERROR: non-uniform pattern”): En caso de que los patrones de un match no sean del mismo tipo.(error “TYPE ERROR: non-uniform match return type”): Si los tipos de retorno de match no son del mismo tipo.(error “TYPE ERROR: incomplete match”): Si no todos los constructores de tipo están cubiertos por un match.(error “TYPE ERROR: wrong return type”): Si en una definición 'def' el tipo de retorno es distinto al tipo declarado.(error “TYPE ERROR: redefinition”): Si existen dosdeftype, constructores odefcon el mismo nombre.(error “TYPE ERROR: incorrect constructor type”): Si el tipo de salida de un constructor no corresponde al tipo que define sudeftype.
Nuevamente, el output de la función es un String. Ejemplos:
(typeof '{{deftype nat {O : nat} {S : {nat -> nat}}} {O}}) > "nat"
Los constructores tienen tipos de función con →. La ausencia de argumentos se representa por () como sigue:
(typeof '{{deftype nat {O : nat} {S : {nat -> nat}}} O}) "() -> nat"
(test/exn (typeof '{{deftype bool {t : bool} {f : bool}} {deftype nat {O : nat} {S : {nat -> nat}}} {S {t}}}) "TYPE ERROR: wrong argument type")
P3 - Análisis de Terminación (2.0pt)
Tener un lenguaje donde los valores son estructuras inductivas permite detectar casos de recursión estructural, lo que permite concluir sintácticamente cuando una función termina. Por ejemplo en el siguiente caso es posible saber que la función even termina sin ejecutarla, pues sus posibles retornos son valores directos o llamados recursivos con argumentos que corresponden a sub-estructuras:
(terminate '{{deftype bool {t : bool} {f : bool}} {deftype nat {O : nat} {S : {nat -> nat}}} {def even {n : nat} : bool {match n {{case {O} => {t}} {case {S n1} => {match n1 {{case {O} => {f}} {case {S n2} => {even n2}}}}}}}} {even {S {S {O}}}}}) > "terminate"
No así como en el siguiente caso:
(terminate '{{deftype nat {O : nat} {S : {nat -> nat}}} {def inf {n : nat} : nat {match n {{case {O} => {O}} {case {S n1} => {inf n}}}}} {inf {S {O}}}}) > "cannot detect structural recursion"
Pues si bien un caso de match corresponde a un constructor aplicado sin argumentos, el otro caso corresponde a una llamada donde el argumento no se reduce.
Implemente la función terminate :: s-expr → String que intenta decidir si un programa termina o no. La función terminate debe verificar cada def según sigue:
- Si la función no es recursiva, termina
- Si la función es recursiva entonces todas las llamadas recursivas deben reducir en al menos un argumento y este debe ser el mismo en todos los casos.
- Se considera como argumento disminuido estructuralmente a un identificador extraído de un match, siempre y cuando el argumento de match sea directamente un identificador.
- Considere que para cualquier argumento de una llamada recursiva, si no es un identificador proveniente de un match, no puede saber si disminuye estructuralmente.
Para la realización de está pregunta puede asumir que las verificaciones de tipo ya fueron realizadas. Por ejemplo ya no debe preocuparse de los casos donde no están definidos todos los patrones de un match.
(terminate '{{deftype bool {t : bool} {f : bool}} {deftype nat {O : nat} {S : {nat -> nat}}} {def weird {n1 : nat} {n2 : nat} : bool {match n2 {{case {O} => {t}} {case {S n3} => {match n1 {{case {O} => {weird n3 {S n1}}} {case {S n4} => {weird n4 n2}}}}}}}} {O}}) > "terminate"
En el caso anterior existen dos llamadas recursivas a weird. La primera llamada recursiva {weird n3 {S n1}} disminuye en el primer argumento, pero no necesariamente en el segundo y la segunda llamada recursiva {weird n4 n2} disminuye en ambos argumentos. Por lo tanto la función reduce en el primer argumento.
(terminate '{{deftype bool {t : bool} {f : bool}} {deftype nat {O : nat} {S : {nat -> nat}}} {def weird {n1 : nat} {n2 : nat} : bool {match n2 {{case {O} => {t}} {case {S n3} => {match n1 {{case {O} => {weird n3 {S n1}}} {case {S n4} => {weird {S n4} n2}}}}}}}} {O}}) > "cannot detect structural recursion"
En el último caso, se debe detectar que la primera llamada recursiva {weird n3 {S n1}} disminuye en el primer argumento y que la segunda llamada recursiva {weird {S n4} n2}} no disminuye en ninguno. Por lo tanto no se puede deducir si la función es estructuralmente recursiva.