问题描述
我使用GADT定义了深度索引树数据类型(2–3 tree)。深度可以静态确保树木平衡。
-- Natural numbers
data Nat = Z | S Nat
-- Depth-indexed 2-3 tree
data DT :: Nat -> Type -> Type where
-- Pattern of node names: N{#subtrees}_{#containedValues}
N0_0 :: DT Z a
N2_1 :: DT n a -> a -> DT n a
-> DT (S n) a
N3_2 :: DT n a -> a -> DT n a -> a -> DT n a
-> DT (S n) a
deriving instance Eq a => Eq (DT n a)
现在,某些操作(例如插入)可能会或可能不会更改树的深度。所以我想从类型签名中隐藏它。我使用存在数据类型来做到这一点。
-- 2-3 tree
data T :: Type -> Type where
T :: {unT :: DT n a} -> T a
insert :: a -> T a -> T a
insert x (T dt) = case dt of
N0_0 -> T $ N2_1 N0_0 x N0_0
{- ... -}
到目前为止一切顺利。我的问题是:
我现在看不到如何在Eq
上定义T
。
instance Eq a => Eq (T a) where
(T x) == (T y) = _what
很明显,我想做这样的事情:
(T {n = nx} x) == (T {n = ny} y)
| nx == ny = x == y
| otherwise = False
我不知道如何/是否可以在模式匹配中绑定类型变量。我也不确定一旦获得它们后如何比较它们。
(我怀疑Data.Type.Equality
是为此使用的,但是我还没有看到使用它的任何示例。)
因此,有没有一种方法可以实现Eq (T a)
实例,或者在这种情况下是否建议采用其他方法?
解决方法
您应该编写一个与深度无关的等式运算符,该运算符可以比较两棵树,即使它们的深度n
和m
不同。
dtEq :: Eq a => DT n a -> DT m a -> Bool
dtEq N0_0 N0_0 = True
dtEq (N2_1 l1 x1 r1) (N2_1 l2 x2 r2) =
dtEq l1 l2 && x1 == x2 && dtEq r1 r2
dtEq (N3_2 a1 x1 b1 y1 c1) (N3_2 a2 x2 b2 y2 c2) =
dtEq a1 a2 && x1 == x2 && dtEq b1 b2 && y1 == y2 && dtEq c1 c2
dtEq _ _ = False
然后,针对您的存在类型:
instance Eq a => Eq (T a) where
(T x) == (T y) = dtEq x y
即使在最后一行中深度是未知的(由于存在),dtEq
也无所谓,因为它可以接受任何深度。
次要注意事项:dtEq
利用了多态递归,因为递归调用可以使用与原始调用中不同的深度。 Haskell允许多态递归,只要提供显式类型签名即可。 (因为我们正在使用GADT,所以还是需要一个。)
您可以使用Data.Coerce.coerce来比较树的内容:只要将depth参数标记为phantom,它就应该愿意给您coerce :: DT n a -> DT m a
。
但是,这当然并不能真正解决问题:您想知道它们的类型是否相同。好吧,也许Typeable有一些解决方案,但是听起来并不那么有趣。缺少Typeable,对我来说似乎是不可能的,因为您想要两个矛盾的东西。
首先,您希望不同深度的树应该是单独的类型,而不能相互混合。这意味着处理它们的每个人都必须知道它们是什么类型。
其次,您希望您可以将这样一棵树送给某人,而不必告诉他们它有多深,让他们随意地四处张望,然后将其还给您。如果您需要打字知识来对它们进行操作,他们怎么办?
存在项不会“禁止”类型信息:它们会将其丢弃。像所有类型信息一样,它在运行时消失了。并且在编译时也使它不可见。
我也不确定您的问题仅在于Eq
:您将如何实现insert
之类的功能? N0_0
很容易,因为已知类型为DT Z a
,但是在其他情况下,我看不到如何构造DT (S n) a
来包装{{1} },当您不知道T
是什么时。