具有静态类型长度的列表的写长度函数

Question

给定一个静态类型长度的列表(以此为例):

data Zero

data Succ nat

data List el len where
    Nil  ::                      List el Zero
    Cons :: el -> List el len -> List el (Succ len)

是否可以编写一个长度函数,使用静态类型而不是通常的递归来计算长度？

到目前为止,我的努力使我得出的结论是,这是不可能的,因为它需要"解除"类型信息才能重现:

class HasLength a where
    length :: a -> Natural

instance HasLength (List el Zero) where
    length _ = 0

instance HasLength (List el (Succ len)) where
    length _ = 1 + *how to recur on type of len*

然而,我只是刚刚开始了解所有类型的魔法,所以我知道我无法想象一个解决方案并不意味着没有一个.

更新

由于长度返回自然,我写错了length _ = 1 + ....正确的实例(使用下面给出的答案)是

instance HasLength (List el len) => HasLength (List el (Succ len)) where
    length _ = succ $ length (undefined :: List el len)

Answer 1

例如这样:

instance HasLength (List el len) => HasLength (List el (Succ len)) where
    length _ = 1 + length (undefined :: List el len)

注意:这需要ScopedTypeVariables扩展.