从功能返回GADT

Question

背景

我正在使用依赖类型在Haskell中编写一个红黑树实现,并且我很难理解为什么下面的代码不起作用.我想做的一种热身练习是找到一个任意值的子树.不幸的是,我在编译代码时遇到了一些麻烦,并最终继续前进.但是,我仍然很困惑为什么这不能编译以及我能做些什么才能使它工作.我无法找到这样的例子,也没有任何显示为什么这不起作用的例子.

代码

data NaturalNum = Z
                | S NaturalNum
                deriving Show


data Color :: * where
  Red :: Color
  Black :: Color
  deriving Show


data Tree :: Color -> NaturalNum -> * -> * where
  Empty :: Tree Black Z a
  RTree :: Tree Black natNum a     -> a -> Tree Black natNum a      -> Tree Red natNum a
  BTree :: Tree leftColor natNum a -> a -> Tree rightColor natNum a -> Tree Black (S natNum) a
deriving instance (Show a) => Show (Tree c n a)


findSubtree :: (Ord a) => Tree c n a -> a -> Tree cc nn a
findSubtree Empty _ = Empty
findSubtree (RTree left curr right) item
  | curr == item = RTree left curr right
  | curr < item  = findSubtree left item
  | otherwise    = findSubtree right item
findSubtree (BTree left curr right) item
  | curr == item = BTree left curr right
  | curr < item  = findSubtree left item
  | otherwise    = findSubtree right item

错误消息

有两个几乎相同的错误消息抱怨其他构造函数.

• Could not deduce: cc ~ 'Black
  from the context: (c ~ 'Black, n ~ 'Z)
    bound by a pattern with constructor:
               Empty :: forall a. Tree 'Black 'Z a,
             in an equation for ‘findSubtree’
    at lib/RedBlackTree.hs:246:13-17
  ‘cc’ is a rigid type variable bound by
    the type signature for:
      findSubtree :: forall (c :: Color) (n :: NaturalNum) a (cc :: Color) (nn :: NaturalNum).
                     Tree c n a -> a -> Tree cc nn a
    at lib/RedBlackTree.hs:245:16
  Expected type: Tree cc nn a
    Actual type: Tree 'Black 'Z a
• In the expression: Empty
  In an equation for ‘findSubtree’: findSubtree Empty _ = Empty
• Relevant bindings include
    findSubtree :: Tree c n a -> a -> Tree cc nn a
      (bound at lib/RedBlackTree.hs:246:1)

我的困惑

根据错误消息,我看到我无法返回由无约束颜色和黑色高度参数化的GADT.但是,我发现这相当不令人满意.我看到如果你有关于findSubtree函数返回类型的这些小信息就很难检查程序其他部分的类型,但找到一个子树似乎是一件非常合理的事情.这是与使用GADT一起出现的限制吗？

最重要的是, 我必须对上面的代码进行哪些更改才能从此数据结构中返回任意子树,以及对于给定代码无法编译的确切原因的解释是什么？

Answer 1

问题在于您的类型签名中的量词findSubtree.

findSubtree :: (Ord a) => Tree c n a -> a -> Tree cc nn a

虽然你显然想要c,n并且a被普遍量化,但不应该存在cc并且nn应该存在量化(发现的子树会有一些颜色).

在Haskell中处理存在性的方法是将它们包装在数据类型中.它并不是很明显,但forall内部数据类型相当于exists(如果它存在于Haskell中).

-- An existential type to represent a tree with _some_ color and depth
data SomeTree a where
  SomeTree :: Tree c n a -> SomeTree a

findSubtree :: (Ord a) => Tree c n a -> a -> SomeTree a
findSubtree Empty _ = SomeTree Empty
findSubtree (RTree left curr right) item
  | curr == item = SomeTree (RTree left curr right)
  | curr < item  = findSubtree left item
  | otherwise    = findSubtree right item
findSubtree (BTree left curr right) item
  | curr == item = SomeTree (BTree left curr right)
  | curr < item  = findSubtree left item
  | otherwise    = findSubtree right item