使用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类型添加约束.