Haskell计算列表类型

2018-06-28 22:17:05

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

类型安全的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

（抱歉，任何转录错误 - 我最初编写的这个机器上的W /我的Haskell编译器目前已停机）。

我所做的大部分工作都是针对某个问题编译的，但我遇到了使用ofList和filter问题。我想我理解为什么 - 当我说ofList :: [a] -> CountedList na ，我说的是ofList :: forall n . [a] -> CountedList na ofList :: forall n . [a] -> CountedList na - 创建的列表可以是任何需要的计数类型。我想写的是相当于伪类型的ofList :: exists n . [a] -> CountedList na ofList :: exists n . [a] -> CountedList na ，但我不知道如何。

有没有一种解决方法可以让我编写像我想象的ofList和filter函数，或者我已经达到了我可以用这个做的极限？我有一种感觉，那就是我缺少存在类型的一些技巧。

你不能写

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

但你可以写

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

并向它传递一个函数，该函数表示您将使用ofList的结果完成的ofList ，只要它的类型与列表的长度无关。

顺便说一下，可以确保列表类型与类型系统中的长度相对应的不变量，而不依赖于智能构造函数：

{-# LANGUAGE GADTs #-}

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

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

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

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

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

链接地址: http://www.djcxy.com/p/80771.html

上一篇: Haskell counted list type

下一篇: Haskell unit testing