haskell - Haskell:与TypeFamilies一起玩；无法推断问题

我在Haskell和TypeFamilies等玩。我正在尝试创建一个简单的示例，在该示例中，我下面有一个采用某种类型(Parsers ty)的函数，以及一个采用许多依赖于ty的参数并输出一些结果的函数。

这是前面的整个代码片段:

{-# 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)

我的Parsers ty类型似乎做对了；用它构造事物会导致我期望的类型，例如:

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])))

同样，我的类型族GetVars似乎做正确的事情，执行如下转换:

(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

基本上，以正确的顺序正确地选择用V标记的内容，并忽略S
然后，我的getVars函数在其类型签名中使用它:

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

要说什么p是什么，需要一个与我的类型别名ExtractVars p匹配的函数，然后返回Bool。

在我的getVars函数中，这两个定义没有问题:

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

但最后一个:

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

无法进行类型检查，并显示以下错误:

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.

(第74行是getVars失败的ParCombine定义)

我一直把头撞在桌子上，试图弄清楚哪里出了问题，但无济于事，真的想牢牢抓住类型家庭的来龙去脉，因为它们看起来很棒(例如，上面的例子-能够根据输入期望某些功能类型-太酷了!)

谁能指出我的正确方向或纠正我可能非常愚蠢的错误？

谢谢!

(PS我正在使用GHC 7.10.1并在ghci中运行它)

编辑只是说这个例子是出于有关类型族的论文的启发，特别是sprintf例子here。也许我在尝试从中提取想要的东西时已经跳过了一些重要的事情!

最佳答案

只是概括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)

原始类型为getVars a fn :: Bool，但我们需要getVars a fn :: ExtractVars ty2。通常，如果我们想对GADT进行大量计算，则必须确保我们具有足够通用的类型，这样我们才能进行递归调用(因为在递归时类型或类型索引可能会发生变化)。

附带说明一下，代表GADT索引的惯用方式是使用DataKinds和提升类型:

{-# 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)

其余代码保持不变。这样，我们就不会用真正不属于该类型的任意类型污染ParserTy，并且可以在其上编写详尽的类型族。