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

Question

给定一个静态类型长度的列表（以this 为例）：

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 扩展名。

Answer 2

如果您使用 DataKinds 扩展，这将更容易，这将允许您将 Natural '提升'为一种，这使得（提升）类型 Zero 和 Succ n 更易于处理并消除像Succ Char 这样的废话。有几种方法可以解决，但要紧贴您的文字：

{-#LANGUAGE GADTs, DataKinds, StandaloneDeriving  #-}
data Natural = Zero | Succ Natural deriving (Show,Eq,Ord)

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

deriving instance Show el => Show (List el len)

class HasLength f where len ::  f n -> Natural

instance HasLength (List el) where
    len Nil = Zero
    len (Cons _ xs) = Succ (len xs)

（我也使用了StandaloneDeriving，在这种情况下需要自动派生Show。）