haskell - 有没有办法在模式匹配期间绑定(bind)存在数据类型的抑制类型变量？

Question

使用 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
  {- ... -}

到目前为止一切顺利。我的问题是:我不知道现在如何在 T 上定义 Eq。

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

我不知道如何/是否可以在模式匹配中绑定(bind)类型变量。一旦拿到它们，我也不确定如何比较它们。(我怀疑 Data.Type.Equality 就是为了这个，但我还没有看到任何使用它的例子。)

那么，有没有办法实现 Eq (T a) 实例，或者在这种情况下是否有其他推荐的方法？

Answer 1

您应该编写一个与深度无关的相等运算符，它能够比较两棵树，即使它们具有不同的深度 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。)