Haskell计数列表类型

所以，只是为了好玩，我一直在Haskell中使用一个CountedList类型，使用Peano号码和smart constructors。Haskell计数列表类型

型号安全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。

来源

2010-01-14 rampion

我不知道为什么有人会downvote这个题。我保持平衡。 – 2010-01-14 16:00:51

看起来像有人点击downvote错误并修复它：目前没有downvote。 – JaakkoK 2010-01-14 16:02:45

事实上，我点击了我手机上的错误按钮，然后失去了网络连接。我希望堆栈溢出将在不久的将来得到一个移动样式表（带有一些更大的箭头）:-) – 2010-01-14 16:12:57

所有实例来定义你不能写

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

来源

2010-01-14 19:42:36

感谢您指向[GADTs]（http://www.haskell.org/haskellwiki/GADT#Example_with_lists），这就是很有帮助。 – rampion 2010-01-14 20:48:55

您不能这样定义ofList或filter，因为它们与运行时值混淆了类型级别的检查。尤其是，在结果类型中，CountedList n a，类型n必须在编译时确定。暗示的愿望是n应该与第一个参数列表的长度相称。但是直到运行时才能知道。现在

，有可能定义一个类型类，说计数，然后（与适当的哈斯克尔扩展名），定义这些像：

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

但是你有一个困难时期做什么这样的结果，因为CountedListable可以支持的唯一操作是提取计数。你不能，说得到这样一个值的head因为头不能为CountedListable

来源

2010-01-14 16:33:33 MtnViewMark

Haskell计数列表类型

回答

相关问题