Haskell 计数列表类型

Question

所以，只是为了好玩，我一直在玩 Haskell 中的 CountedList 类型，使用 Peano 数 和smart constructors。

类型安全的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 函数，或者我已经达到了我能做的极限？我有一种感觉，existential types 缺少一些技巧。

Answer 1

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

现在，可以定义一个类型类，比如 Counted，然后（使用适当的 Haskell 扩展）定义如下：

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

但是你很难对这样的结果做任何事情，因为CountedListable 可以支持的唯一操作就是提取计数。你不能说得到这样一个值的head，因为无法为CountedListable的所有实例定义head

Answer 2

你不会写

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