GADT para la lista polimórfica

Question

estoy analizar un par de enunciados de la forma

v1 = expression1 
v2 = expression2 
... 

estoy usando la Mónada Estado y de mi estado debe ser un par de (String, Expr a), realmente insisten en tener la expresiones escritas. Traté de poner en práctica el Estado como [PPair] donde defino PPair por el GADT:

data PPair where 
    PPair :: (String, Expr a) -> PPair 

vez que esta línea pasa al compilador, sentí que estoy haciendo algo muy, muy mal. Reprimí la idea y seguí codificando. Cuando llegué a escribir el código que permita, mediante el valor de la variable del Estado, me di cuenta del problema:

evalVar k ((PPair (kk, v)):s) = if k == kk then v else evalVar k s 

me sale:

Inferred type is less polymorphic than expected 

que es bastante esperado. ¿Cómo puedo solucionar este problema? Sé que puedo resolverlo dividiendo el tipo sobre todos los tipos de candidatos, pero ¿no hay una manera más ordenada?

Answer 1

El problema es que no hay ningún tipo posible evalVar puede tener:

evalVar :: String -> [PPair] -> Expr ? 

no se puede decir ? es a, porque entonces usted está reclamando su valor de retorno funciona para cualquier valor de a. Lo que puede hacer, sin embargo, es envuelva "un Expr con un tipo desconocido" en su propio tipo de datos:

data SomeExpr where 
    SomeExpr :: Expr a -> SomeExpr 

o, equivalentemente, con RankNTypes en lugar de GADTs:

data SomeExpr = forall a. SomeExpr (Expr a) 

Esto es llamado cuantificación existencial. A continuación, puede volver a escribir PPair usando SomeExpr:

data PPair = PPair String SomeExpr 

y evalVar se resuelve: (. Por supuesto, es posible que utilices una [(String,SomeExpr)] lugar y la función estándar lookup)

evalVar k (PPair kk v : xs) 
    | k == kk = v 
    | otherwise = evalVar k xs 

En general, sin embargo, tratar de mantener las expresiones escritas completamente en el nivel de Haskell de esta manera es probablemente un ejercicio inútil; un lenguaje de tipo dependiente como Agda no tendría problemas con eso, pero probablemente terminarás tropezando con algo que Haskell no puede hacer bastante rápido, o debilitando las cosas hasta el punto en que la seguridad en tiempo de compilación que querías fuera del esfuerzo está perdido.

Eso no quiere decir que nunca funciona, por supuesto; los tipeados fueron uno de los ejemplos motivadores para GADTs. Pero puede que no funcione tan bien como desee, y probablemente tenga problemas si su lenguaje tiene características del sistema tipo no triviales como el polimorfismo.

Si realmente desea mantener el tipado, entonces usaría una estructura más rica que las cadenas para nombrar variables; tener un tipo Var a que lleva explícitamente el tipo, así:

data PPair where 
    PPair :: Var a -> Expr a -> PPair 

evalVar :: Var a -> [PPair] -> Maybe (Expr a) 

Una buena manera de lograr algo similar a esto sería usar el paquete vault; puede construir Key s desde ST y IO, y usar Vault como un contenedor heterogéneo. Es básicamente como Map donde las teclas tienen el tipo del valor correspondiente. Específicamente, sugeriría definir Var a como Key (Expr a) y usar Vault en lugar de su [PPair]. (La revelación completa: He trabajado en el paquete de bóveda.)

Por supuesto, usted todavía tiene que asignar los nombres de las variables a los valores Key, pero se puede crear todo el Key s justo después de analizar, y realizar aquellos alrededor en lugar de las cuerdas. (Sería un poco difícil pasar de Var a su nombre de variable correspondiente con esta estrategia, sin embargo, puede hacerlo con una lista de existenciales, pero la solución es demasiado larga para ponerla en esta respuesta.)

(Por cierto, puede tener múltiples argumentos para un constructor de datos con GADT, al igual que los tipos normales: data PPair where PPair :: String -> Expr a -> PPair.)