gpt4 book ai didi

haskell - 从函数返回 GADT

转载 作者:行者123 更新时间:2023-12-04 22:19:00 26 4
gpt4 key购买 nike

背景

我正在使用 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 带来的限制吗?

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

最佳答案

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

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

尽管您显然希望 cna 被普遍量化,但 ccnn 不应该被存在量化(找到的子树会有一些颜色)。

在 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

关于haskell - 从函数返回 GADT,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/42324889/

26 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com