haskell - 使用 GADT 实现类型类

Question

我在 Haskell 中编写了以下线性代数向量

data Natural where
    Zero :: Natural
    Succ :: Natural -> Natural

data Vector n e where
    Nil :: Vector Zero e
    (:|) :: (Show e, Num e) => e -> Vector n e -> Vector (Succ n) e
infixr :|

instance Foldable -- ... Vector ..., but how do I implement this?

当我尝试实现Foldable时，我遇到了具有不同定义的问题（即*和* -> *）Zero。Succ

这个问题有明显的解决方案吗？

Answer 1

只是

instance Foldable (Vector n) where
  fold Nil       = mempty
  fold (a :| as) = a <> fold as

不过，我不建议向e类型添加约束。

Answer 2

您无需在类实例中提及Zero或提及Succ，这就是 GADT 的全部要点：构造函数上的模式匹配为您提供类型信息：

instance F.Foldable (Vector v) where
  foldr _ zero Nil = zero
  foldr f zero (e0 :| v) = f e0 $ F.foldr f zero v