Skip to content

Latest commit

 

History

History
101 lines (70 loc) · 3.68 KB

README.md

File metadata and controls

101 lines (70 loc) · 3.68 KB
Raw

Abordaje Funcional a EDSLs

ECI 2024

Se desea implementar un pequeño EDSL para representar proposiciones basadas en comparaciones entre números naturales, el cual tiene las siguientes construcciones:

  • val: valor natural
  • eq: igualdad entre naturales
  • lt: relación de menor entre naturales
  • not: negación
  • and: conjunción
  • or: disyunción

Sistema de Tipos

Asociado al EDSL se tiene un sistema de tipos que está formado por las reglas que se presentan a continuación. Como es habitual, el juicio p : t significa que la expresión p tiene tipo t. El lenguaje maneja dos tipos (integer y boolean).

$$ \frac{}{\vdash\texttt{val} \ n : \texttt{integer}} \tag{Val} $$

$$ \frac{ \vdash p_1 : \texttt{integer} \quad \vdash p_2 : \texttt{integer}}{\vdash \texttt{eq} \ p_1 \ p_2 : \texttt{boolean}} \tag{Eq} $$

$$ \frac{\vdash p_1 : \texttt{integer} \quad \vdash p_2 : \texttt{integer}}{\vdash \texttt{lt} \ p_1 \ p_2 : \texttt{boolean}} \tag{Lt} $$

$$ \frac{\vdash p : \texttt{boolean}}{\vdash \texttt{not} \ p : \texttt{boolean}} \tag{Not} $$

$$ \frac{\vdash p_1 : \texttt{boolean} \quad \vdash p_2 : \texttt{boolean}}{\vdash \texttt{and} \ p_1 \ p_2 : \texttt{boolean}} \tag{And} $$

$$ \frac{\vdash p_1 : \texttt{boolean} \quad \vdash p_2 : \texttt{boolean}}{\vdash \texttt{or} \ p_1 \ p_2 : \texttt{boolean}} \tag{Or} $$

Ejemplos de expresiones bien tipadas:

  • var 4 : integer
  • lt (var 4) (var 5) : boolean
  • or (not (lt (var 4) (var 3))) (eq (var 4) (var 3)) : boolean

Ejemplos de expresiones no tipadas:

  • or (var 4) (var 5)
  • not (var 4)
  • eq (lt (var 4) (var 3)) (var 5)

Requisitos

Considerando que la interpretación estándar de las proposiciones es su valor de verdad o el propio natural n en el caso de expresiones de la forma val n, se pide:

  1. Implementar el EDSL como un shallow embedding bien tipado en Haskell siguiendo el enfoque tagless-final. Interprete los tipos integer y boolean como tipos de Haskell.

  2. Implementar el EDSL como un deep embedding bien tipado en Haskell utilizando GADTs. Definir la función eval que evalúa una expresión bien tipada de tipo t y retorna un valor de ese tipo.

  3. Dada la siguiente gramática que describe una sintaxis concreta para el lenguaje:

    prop ::= term "\/" prop | term
term ::= factor "/\" term | factor
factor ::= '~' prop 
        | '(' prop ')' 
        | '(' prop '=' prop ')' 
        | '(' prop '<' prop ')' 
        | N
    • (a) Definir una nueva interpretación para los puntos 1 y 2 que retorne un String que represente el programa en esa sintaxis.
    • (b) Definir un tipo UProp, de kind *, que represente el árbol de sintaxis abstracta no tipado del lenguaje.
    • (c) Escribir un parser del lenguaje utilizando los combinadores vistos en el curso (puede optar por usar los combinadores aplicativos o monádicos) y que retorne el valor de tipo UProp correspondiente.

  1. (OPCIONAL) Considere la siguiente extensión al lenguaje, en la que se agrega:

    • var: variable proposicional

    Con la siguiente regla de tipado:

    • var x : boolean

    Ahora la interpretación depende de un ambiente de variables en el que se le asocian valores de verdad a las variables.

    • (a) Extender el EDSL definido en 1.
    • (b) Extender el EDSL definido en 2.
    • (c) Extender el tipo definido en 3.a y el parser definido en 3.b.
    • (d) Definir una función typeProp :: Ty t -> UProp -> Prop t donde Prop t es el GADT que definió para el deep embedding y Ty t es el siguiente tipo que representa tipos:
    data Ty :: * -> * where
    TInt :: Ty Int
    TBool :: Ty Bool