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

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

到现在为止还挺好。我的问题是：我不知道我怎么能现在定义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)实例，或者在这种情况下是否推荐其他一些方法？

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。）