1
Il y a plusieurs semaines, j'ai lu Writing an interpreter using fold. J'ai essayé d'appliquer cette méthode au projet sur lequel je travaille, mais il y a eu des erreurs à cause des GADT. Voici le code du jouet qui génère le même problème.Utilisation de fold-interpreter sur GADT
{-# LANGUAGE GADTs, KindSignatures #-}
data Expr :: * -> * where
Val :: n -> Expr n
Plus :: Expr n -> Expr n -> Expr n
data Alg :: * -> * where
Alg :: (n -> a)
-> (a -> a -> a)
-> Alg a
fold :: Alg a -> Expr n -> a
fold [email protected](Alg val _) (Val n) = val n
fold [email protected](Alg _ plus) (Plus n1 n2) = plus (fold alg n1) (fold alg n2)
Voici le message d'erreur.
/home/mossid/Code/Temforai/src/Temforai/Example.hs:16:36: error:
• Couldn't match expected type ‘n1’ with actual type ‘n’
‘n’ is a rigid type variable bound by
the type signature for:
fold :: forall a n. Alg a -> Expr n -> a
at /home/mossid/Code/Temforai/src/Temforai/Example.hs:15:9
‘n1’ is a rigid type variable bound by
a pattern with constructor:
Alg :: forall a n. (n -> a) -> (a -> a -> a) -> Alg a,
in an equation for ‘fold’
at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:11
• In the first argument of ‘val’, namely ‘n’
In the expression: val n
In an equation for ‘fold’: fold [email protected](Alg val _) (Val n) = val n
• Relevant bindings include
n :: n
(bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:27)
val :: n1 -> a
(bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:15)
fold :: Alg a -> Expr n -> a
(bound at /home/mossid/Code/Temforai/src/Temforai/Example.hs:16:1)
Je pense que le compilateur ne peut pas en déduire que le n et n1 sont les mêmes types, de sorte que la réponse pourrait être levée variables intérieure à la signature du type de données. Cependant, contrairement à cet exemple, il ne peut pas être utilisé sur le code d'origine. Le code d'origine a une variable de type forall-quantifié dans Expr, et la signature de type doit gérer des informations spécifiques.
+ Voici le code original
data Form :: * -> * where
Var :: Form s
Prim :: (Sat s r) => Pred s -> Marker r -> Form s
Simple :: (Sat s r) => Pred s -> Marker r -> Form s
Derived :: Form r -> Suffix r s -> Form s
Complex :: (Sat s r, Sat t P) =>
Form s -> Infix r -> Form t -> Form s
data FormA a where
FormA :: (Pred s -> Marker t -> a)
-> (Pred u -> Marker v -> a)
-> (a -> Suffix w x -> a)
-> (a -> y -> a -> a)
-> FormA a
foldForm :: FormA a -> Form s -> a
foldForm [email protected](FormA prim _ _ _) (Prim p m) = prim p m
foldForm [email protected](FormA _ simple _ _) (Simple p m) = simple p m
foldForm [email protected](FormA _ _ derived _) (Derived f s) =
derived (foldForm alg f) s
foldForm [email protected](FormA _ _ _ complex) (Complex f1 i f2) =
complex (foldForm alg f1) i (foldForm alg f2)
La définition correcte est 'Alg :: (n -> a) -> ... -> Alg n a' - le type' existe n. n -> a' est isomorphe à 'a' puisque la seule chose que vous pouvez faire avec une fonction est de l'appliquer, mais vous ne connaissez rien au type' n', donc vous ne pouvez appliquer cette fonction qu'à 'undefined'. Mais il semble que vous en soyez conscient - "la réponse pourrait être de soulever la variable interne à la signature du type de données". "Cependant, pas comme dans cet exemple, il ne peut pas être utilisé sur le code original" - alors c'est le code original que vous devriez publier. – user2407038