¿Cómo crear una función Haskell que introduzca un nuevo tipo?

Question

Actualmente estoy escribiendo un analizador de expresiones. He hecho el análisis léxico y sintáctico y ahora estoy verificando los tipos. Tengo la expresión en un structire de datos como esta (versión simplificada):

data Expr = EBinaryOp String Expr Expr 
      | EInt Int 
      | EFloat Float 

Y ahora necesito una función que convertir esto en un nuevo tipo, responda TypedExpr, que también contendría información de tipo. Y ahora mi principal problema es cómo debería verse este tipo. Tengo dos ideas - con parámetro de tipo:

data TypedExpr t = TEBinaryOp (TBinaryOp a b t) (TExpr a) (TExpr b) 
       | TEConstant t 
addTypes :: (ExprType t) => Expr -> TypedExpr t 

o sin:

data TypedExpr = TEBinaryOp Type BinaryOp TypedExpr TypedExpr 
       | TEConstant Type Dynamic 
addTypes :: Expr -> TypedExpr 

empecé con la primera opción, pero me encontré con problemas, ya que este enfoque supone que sabe tipo de la expresión antes de analizarlo (para mí, es cierto en la mayoría de los casos, pero no siempre). Sin embargo, me gusta, porque me permite usar el sistema de tipos de Haskell y verificar la mayoría de los errores en tiempo de compilación.

¿Es posible hacerlo con la primera opción?
¿Cuál elegirías? ¿Por qué?
¿Qué problemas debo esperar con cada opción?

Answer 1

El tipo de su función

addTypes :: Expr -> TypedExpr t 

es incorrecto, ya que significaría que se obtiene una TypedExpr tpara cualquier t te gusta. Por el contrario, lo que realmente quiere es uno en particulart que está determinado por el argumento del tipo Expr.

Este razonamiento ya demuestra que va más allá de las capacidades del sistema de tipo Hindley-Milner. Después de todo, el tipo de devolución de addTypes debe depender del valor del argumento, pero en Haskell 2010, los tipos pueden no depender de los valores. Por lo tanto, necesita una extensión del sistema de tipo que lo acerque a tipos dependientes. En Haskell, , los tipos de datos algebraicos generalizados (GADT) pueden hacer eso.

Para una primera introducción a las GADT, ver también my video on GADTs.

Sin embargo, después de familiarizarse con las GADT, todavía tiene el problema de analizar una expresión sin tipo en una escrita a máquina, es decirescribir una función

addTypes :: Expr -> (exists t. TypedExpr t) 

Por supuesto, usted tiene que realizar algún tipo de control de sí mismo, pero incluso entonces, no es fácil de convencer al compilador de Haskell que sus controles de tipo (que ocurren en el nivel de valor) pueden ser elevado al nivel de tipo. Afortunadamente, otras personas ya han pensado en ello, véase por ejemplo el siguiente mensaje en la lista de correo Haskell-café:

Edward Kmett.
Re: Tipo-Comprobación manual para proporcionar instancias de lectura para GADT. (fue re: [Haskell-cafe] Leer instancia para GATD)
http://article.gmane.org/gmane.comp.lang.haskell.cafe/76466

(¿Alguien sabe de una referencia publicada formalmente/muy bien redactado?)

Answer 2

Desde que está haciendo el análisis en tiempo de ejecución, no en tiempo de compilación, puede no llevan a cuestas fuera del sistema de tipos de Haskell (a menos de importar los módulos correspondientes y llamar manualmente usted mismo.)

Es posible que desee para ver ejemplos ML de TAPL de verificadores de tipos para un cálculo lambda simple para la inspiración. http://www.cis.upenn.edu/~bcpierce/tapl/ (en implementaciones). Hacen un poco más que tu analizador de expresiones, ya que no soportas lambdas.

Answer 3

recientemente he empezado a utilizar tagless-final syntax de DSL incorporadas, y he encontrado que es mucho más agradable que el método estándar GADT (al que te diriges, y Apfelmus lo describe).

La clave para la sintaxis sin etiqueta final es que en lugar de utilizar un tipo de datos de expresión, representa operaciones con una clase de tipo. Para funciones como el eBinaryOp, he encontrado que es mejor utilizar dos clases:

class Repr repr where 
    eInt :: repr Int 
    eFloat :: repr Float 

class Repr repr => BinaryOp repr a b c where 
    eBinaryOp :: String -> repr a -> repr b -> repr c 

que haría las funciones BinaryOp separadas en lugar de utilizar una cadena sin embargo. Hay mucha más información en Oleg's web page, incluido un analizador sintáctico que usa el sistema de tipos de Haskell.