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 类型添加约束。