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計數列表類型

回答

相關問題