5

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

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)
4

2 回答 2

8

例如像这样：

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

注意：这需要ScopedTypeVariables扩展。

于 2012-11-26T00:05:07.973 回答
1

如果您使用扩展名，这将容易得多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。）

于 2012-11-26T16:30:01.247 回答