Haskell 计数列表类型

Question

所以，只是为了好玩，我一直在使用Peano数在Haskell中玩一个CountedList类型，并使用智能构造函数。

对我来说，类型安全的head和tail似乎非常酷。

我觉得我已经达到了自己知道如何做的极限。

{-# LANGUAGE EmptyDataDecls #-}
module CountedList (
  Zero, Succ, CountedList,
  toList, ofList, 
  empty, cons, uncons, 
  head, tail, 
  fmap, map, foldl, foldr, filter
) where

import qualified List (foldr, foldl, filter)
import Prelude hiding (map, head, foldl, foldr, tail, filter)

data Zero
data Succ n
data CountedList n a = CL [a]

toList :: CountedList n a -> [a]
toList (CL as) = as

ofList :: [a] -> CountedList n a
ofList [] = empty
ofList (a:as) = cons a $ ofList as

empty :: CountedList Zero a
empty = CL []

cons :: a -> CountedList n a -> CountedList (Succ n) a
cons a = CL . (a:) . toList

uncons :: CountedList (Succ n) a -> (a, CountedList n a)
uncons (CL (a:as)) = (a, CL as)

head :: CountedList (Succ n) a -> a
head = fst . uncons

tail :: CountedList (Succ n) a -> CountedList n a
tail = snd . uncons

instance Functor (CountedList n) where
  fmap f = CL . fmap f . toList

map :: (a -> b) -> CountedList n a -> CountedList n b
map = fmap

foldl :: (a -> b -> a) -> a -> CountedList n b -> a
foldl f a = List.foldl f a . toList

foldr :: (a -> b -> b) -> b -> CountedList n a -> b
foldr f b = List.foldr f b . toList

filter :: (a -> Bool) -> CountedList n a -> CountedList m a
filter p = ofList . List.filter p . toList

(抱歉如果有任何转录错误 - 我最初用我的Haskell编译器写的机器目前已经出了问题)

我所做的大部分编译都没有问题，但在使用ofList和filter时会遇到问题。我认为我知道原因 - 当我说ofList :: [a] -> CountedList n a时，我是在说ofList :: forall n . [a] -> CountedList n a - 即创建的列表可以是任何所需的计数类型。我想要编写的等价于伪类型ofList :: exists n . [a] -> CountedList n a，但我不知道该如何实现。

是否有一种解决方法可以让我像想象中那样编写ofList和filter函数，或者我已经达到了使用这个功能的极限？我有一种感觉，我可能漏掉了某些存在类型的技巧。

- rampion

---

我不知道为什么有人会对这个问题投反对票。我为了平衡而投了赞成票。 - Pascal Cuoq

看起来有人误点了踩的按钮，但已经修复了：目前没有踩的选项。 - JaakkoK

的确，我在手机上点击了错误的按钮，然后失去了网络连接。希望 Stack Overflow 在不久的将来能够获得一个移动样式表（带有一些更大的箭头） :-) - Tom Lokhorst

Answer 1

您无法编写

ofList :: [a] -> (exists n. CountedList n a)  -- wrong

但是您可以写下以下内容：

withCountedList :: [a] -> (forall n. CountedList n a -> b) -> b

您需要将一个函数传递给ofList，该函数表示您将如何处理列表的结果，只要其类型与列表的长度无关。

顺便说一下，您可以确保列表的类型与其长度在类型系统中对应，并且不依赖于智能构造函数:

{-# LANGUAGE GADTs #-}

data CountedList n a where
    Empty :: CountedList Zero a
    Cons :: a -> CountedList n a -> CountedList (Succ n) a

- Reid Barton

---

谢谢你指引我去看GADTs，非常有帮助。 - rampion

Answer 2

您不能这样定义ofList或filter，因为它们将类型检查与运行时值混淆在一起。特别地，在结果的类型CountedList n a中，类型n必须在编译时确定。隐含的愿望是，n应该与作为第一个参数的列表的长度相当。但是，这显然直到运行时才能知道。

现在，可能可以定义一个类型类Counted，然后（使用适当的Haskell扩展），像这样定义：

ofList :: [a] -> (forall n. (CountedListable CountedList n) => CountedList n a)

但是，如果只有这样的结果，您将很难进行任何操作，因为 CountedListable 只能支持提取计数的操作。例如，您无法获取这样一个值的 head，因为不能为所有 CountedListable 实例定义 head。

- MtnViewMark