Haskell:玩 TypeFamilies；无法推断出问题

Question

我正在玩 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 定义)

我一直在用头撞 table 试图找出我哪里出错了，但没有成功，我真的很想牢牢掌握类型族的来龙去脉，因为它们看起来很棒(上面的例如——能够根据输入期望一些函数类型——会非常酷!)

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

谢谢!

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

编辑 只是说这个例子在某种程度上是受一篇关于类型族的论文的启发，特别是 sprintf 例子 here .也许我在试图从中提炼出我想要的东西时跳过了一些重要的东西!

Answer 1

只是概括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，我们可以在它上面编写详尽的类型族。