Haskell: jouer avec TypeFamilies; Je n'ai pas pu en déduire le numéro

Question

Je joue avec TypeFamilies et comme dans Haskell. J'essaye de créer un exemple simple par lequel j'ai une fonction qui prend dans un certain type (Parsers ty) ci-dessous, et une fonction qui prend un certain nombre d'arguments dépendant de cela ty, et produit un certain résultat.

est ici l'ensemble du code à l'avant:

{-# LANGUAGE UndecidableInstances, TypeFamilies,GADTs #-} 


data V a --"variable" 
data S a --"static" 
data C a b --combination 

--define data type: 
data Parsers ty where 
    ParVar :: a -> Parsers (V a) 
    ParStatic :: a -> Parsers (S a) 
    ParCombine :: Parsers ty1 -> Parsers ty2 -> Parsers (C ty1 ty2) 

--basic type alias to below, output set to Bool 
type ExtractVars parsers = GetVars parsers Bool 

--we want to convert some combination of C/S/V 
--types into a function taking, from left to right, 
--each type inside S as parameter 
type family GetVars parsers output where 
    GetVars (S a) output = output 
    GetVars (V a) output = a -> output 
    GetVars (C a b) output = GetVars a (GetVars b output) 

--this function uses the above such that, hopefully, 
--the second argument to be provided will be a function 
--that will take each S type as an argument and return 
--a bool. We then return that bool from the whole thing 
getVars :: Parsers p -> ExtractVars p -> Bool 
getVars (ParVar s) fn = fn s 
getVars (ParStatic _) fn = fn 
-- this is the offending line: 
getVars (ParCombine a b) fn = getVars b (getVars a fn) 

Mon type Parsers ty semble faire la bonne chose; construire des choses avec elle conduit à des types j'attendre par exemple:

ParVar "hi" 
    :: Parsers (V [Char]) 
ParCombine (ParVar "hi") (ParStatic "woop") 
    :: Parsers (C (V [Char]) (S [Char])) 
ParCombine (ParVar 'h') (ParCombine (ParStatic True) (ParVar "hello")) 
    :: Parsers (C (V Char) (C (S Bool) (V [Char]))) 

De même, mon type de famille GetVars semble faire la bonne chose, effectuer des conversions telles que:

(C (V a) (V b)) out => a -> b -> out 
(V a) out   => a -> out 
(S a) out   => out 
(C (S a) (V b) out => b -> out 

Fondamentalement, la cueillette correctement la choses étiquetés avec V dans le bon ordre et en ignorant les S s

Ma fonction getVars utilise alors ceci dans sa signature de type:

getVars :: Parsers p -> ExtractVars p -> Bool 

Dire que tout est p, attendez-vous une fonction correspondant à mon alias de type ExtractVars p, et le retour d'un Bool.

de ma fonction getVars, ces deux définitions ne causent pas de problème:

getVars (ParVar s) fn = fn s 
getVars (ParStatic _) fn = fn 

mais le dernier:

getVars (ParCombine a b) fn = getVars b (getVars a fn) 

ne réussit pas à typer, avec les erreurs:

test.hs:74:42: 
    Could not deduce (GetVars ty2 Bool ~ Bool) 
    from the context (p ~ C ty1 ty2) 
     bound by a pattern with constructor 
       ParCombine :: forall ty1 ty2. 
           Parsers ty1 -> Parsers ty2 -> Parsers (C ty1 ty2), 
       in an equation for ‘getVars’ 
     at test.hs:74:10-23 
    Expected type: ExtractVars ty2 
     Actual type: Bool 
    Relevant bindings include b :: Parsers ty2 (bound at test.hs:74:23) 
    In the second argument of ‘getVars’, namely ‘(getVars a fn)’ 
    In the expression: getVars b (getVars a fn) 

test.hs:74:52: 
    Could not deduce (GetVars ty1 Bool 
         ~ GetVars ty1 (GetVars ty2 Bool)) 
    from the context (p ~ C ty1 ty2) 
     bound by a pattern with constructor 
       ParCombine :: forall ty1 ty2. 
           Parsers ty1 -> Parsers ty2 -> Parsers (C ty1 ty2), 
       in an equation for ‘getVars’ 
     at test.hs:74:10-23 
    NB: ‘GetVars’ is a type function, and may not be injective 
    Expected type: ExtractVars ty1 
     Actual type: ExtractVars p 
    Relevant bindings include 
     b :: Parsers ty2 (bound at test.hs:74:23) 
     a :: Parsers ty1 (bound at test.hs:74:21) 
    In the second argument of ‘getVars’, namely ‘fn’ 
    In the second argument of ‘getVars’, namely ‘(getVars a fn)’ 
Failed, modules loaded: none. 

(la ligne 74 est la définition de ParCombine échouée de getVars)

Je me suis cogné la tête contre le bureau en essayant de comprendre où je me trompe en vain, et je veux vraiment avoir une prise ferme sur les tenants et les aboutissants des familles de types car ils semblent impressionnants (ci-dessus exemple: être capable d'attendre un certain type de fonction en fonction de l'entrée - serait incroyablement cool!)

Est-ce que quelqu'un pourrait me pointer dans la bonne direction ou corriger mon éventuelle erreur?

Merci!

(PS J'utilise GHC 7.10.1 et dans l'exécution de ce ghci)

Modifier Juste pour dire que cet exemple a été quelque peu motivé par un document sur les familles de type, en particulier l'exemple de sprintf here. Peut-être ai-je sauté quelque chose d'important en essayant de distiller ce que je voulais!

Answer 1

Tout généralisent getVars:

getVars :: Parsers p -> GetVars p out -> out 
getVars (ParVar s)  fn = fn s 
getVars (ParStatic _) fn = fn 
getVars (ParCombine a b) fn = getVars b (getVars a fn) 

Avec le type original, getVars a fn :: Bool, mais nous avons besoin getVars a fn :: ExtractVars ty2. En général, si nous voulons faire un calcul substantiel sur GADTs, nous devons nous assurer que nous avons un type assez général pour que nous puissions réellement faire les appels récursifs (puisque les types ou indices de type pourraient changer pendant que nous recurse).

Comme une note de côté, le chemin idiomatiques pour représenter les indices de GADT est d'utiliser DataKinds et types: levés

{-# LANGUAGE DataKinds #-} 

data ParserTy a = V a | S a | C (ParserTy a) (ParserTy a) 

data Parsers (ty :: ParserTy *) where 
    ParVar :: a -> Parsers (V a) 
    ParStatic :: a -> Parsers (S a) 
    ParCombine :: Parsers ty1 -> Parsers ty2 -> Parsers (C ty1 ty2) 

Le reste du code reste le même. De cette façon, nous ne pouvons pas polluer ParserTy avec des types arbitraires qui n'y appartiennent pas vraiment, et nous pouvons écrire des familles de types exhaustives dessus.