GADT pour la liste

Question

polymorphes J'analyse pas quelques déclarations de la forme

v1 = expression1 
v2 = expression2 
... 

J'utilise l'État Monade et mon état devrait être une paire de (String, Expr a), je tiens vraiment à avoir la expressions typées. J'ai essayé de mettre en œuvre l'État comme [PPair] où je définis PPair par le GADT:

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

Une fois que cette ligne a passé le compilateur, je sentais que je suis en train de faire quelque chose de vraiment vraiment mal. J'ai supprimé la pensée et j'ai continué à coder. Quand je suis venu à écrire le code qui extraire la valeur de la variable de l'Etat, je me suis rendu le problème:

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

Je reçois:

Inferred type is less polymorphic than expected 

qui est très attendue. Comment puis-je contourner ce problème? Je sais que je peux le résoudre en divisant le type sur tous les types de candidats, mais n'y a-t-il pas de façon plus nette?

Answer 1

Le problème est qu'il n'y a pas de type possible evalVar peut avoir:

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

Vous ne pouvez pas dire ? est a, parce que vous affirmez votre valeur de retour fonctionne pour une valeur de a. Ce que vous pouvez faire, cependant, est envelopper "un Expr avec un type inconnu" dans son propre type de données:

data SomeExpr where 
    SomeExpr :: Expr a -> SomeExpr 

ou, ce qui revient, avec RankNTypes plutôt que GADTs:

data SomeExpr = forall a. SomeExpr (Expr a) 

C'est appelé quantification existentielle. Vous pouvez ensuite réécrire PPair en utilisant SomeExpr:

data PPair = PPair String SomeExpr 

et evalVar fonctionne sur: (. Bien sûr, vous pouvez simplement utiliser une place [(String,SomeExpr)] et la fonction standard lookup)

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

En général, cependant, essayer de garder des expressions complètement typées au niveau Haskell comme ceci est probablement un exercice futile; un langage typé de manière indépendante comme Agda n'aurait aucun problème, mais vous finirez probablement par rencontrer quelque chose que Haskell ne peut pas faire assez rapidement, ou affaiblir les choses au point où la sécurité à la compilation que vous vouliez sortir de l'effort est perdu. Cela ne veut pas dire que ça ne marche jamais, bien sûr; Les langues typées étaient l'un des exemples de motivation pour les GADT. Mais cela peut ne pas fonctionner aussi bien que vous le souhaitez, et vous aurez probablement des problèmes si votre langage a des caractéristiques de système de type non-trivial comme le polymorphisme.

Si vous voulez vraiment garder la saisie, j'utiliserais une structure plus riche que les chaînes pour nommer les variables; ont un type Var a qui porte explicitement le type, comme ceci:

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

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

Une bonne façon d'obtenir quelque chose de semblable à ce serait d'utiliser le paquet vault; vous pouvez construire Key depuis ST et IO, et utiliser Vault comme un conteneur hétérogène. C'est fondamentalement comme un Map où les clés tiennent le type de la valeur correspondante. Plus précisément, je suggère de définir Var a comme Key (Expr a) et en utilisant un Vault au lieu de votre [PPair]. (Divulgation complète: Je travaille sur le paquet de voûte.)

Bien sûr, vous aurez encore à cartographier les noms de variables aux Key valeurs, mais vous pouvez créer tout droit le Key après l'analyse syntaxique, et porter ceux qui sont autour au lieu des cordes. (Ce serait un peu de travail d'aller d'un Var à son nom de variable correspondant avec cette stratégie, cependant, vous pouvez le faire avec une liste d'existentiels, mais la solution est trop longue pour mettre dans cette réponse.)

(En passant, vous pouvez avoir plusieurs arguments à un constructeur de données avec GADTs, tout comme les types réguliers: data PPair where PPair :: String -> Expr a -> PPair.)