Fecha de Entrega: Viernes 5 de Junio
Recuerden las reglas de entrega.
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>*}
deftype
y def
.parser :: s-expr → Expr
que parsea el lenguajeinterp :: Expr Env → Val
que evalua un programa con semántica eager.run :: s-expr → String
que 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.
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 dos deftype
, constructores o def
con el mismo nombre.(error “TYPE ERROR: incorrect constructor type”)
: Si el tipo de salida de un constructor no corresponde al tipo que define su deftype
.
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")
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:
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.