不知道我理解這種類型在Haskell

Question

好，所以繼續my previousquestions，我有一個名爲Enumeration類型，現在描述爲

，枚舉是有限桶的無限序列， 索引由自然數

並定義爲這樣：

> type Nat = Int 
> type Enumeration a = Nat -> Finite a 

日是是Finite Bucket

> type Finite a = [a] 

所以，如果我理解正確的，一個Enumeration是一樣的東西列出清單？它是一個從Int到列表的函數，它應該像索引那樣取int，並返回一個列表。

但我不明白的是，如果它確實是一個列表清單，它在哪裏存儲它「列表」，以便稍後可以使用我提供的index返回它們。

我已經定義了這個Enumeration類型的一些函數，但我不確定它們是否正確，因爲我不確定是否理解Enumeration的真實含義。

例如：

定義一個函數來進行單例枚舉。 我建議你把唯一的項目在水桶0

> singleE' :: a -> Enumeration a 
> singleE' a 0 = singleF a 

定義映射過枚舉簡單：

> imapE :: (a -> b) -> Enumeration a -> Enumeration b 
> imapE f g = (imapF f) . g 

定義枚舉不交：

爲了簡單起見，可以通過存儲桶執行此操作：結果枚舉的存儲桶i中的項目應該從 的存儲桶i中抽取兩個參數枚舉。

> plusE :: Enumeration a -> Enumeration b -> Enumeration (Either a b) 
> plusE f g = \n -> [Left x | x <- f n] ++ [Right y | y <- g n] 

定義枚舉

這是棘手的笛卡爾積，因爲你不能用水桶做任何桶以上， 像你一樣的時脈（爲什麼不呢？）。最簡單的技術是執行 一種卷積：結果枚舉 的桶i中的項目應該從第一個參數 的桶j中的項目和第二個桶的k中構建，其中j + k =一世。

> timesE :: Enumeration a -> Enumeration b -> Enumeration (a,b) 
> timesE f g = \n -> timesF (f n) (g n) 

所以我的問題是：

1. 我才明白的Enumeration正確

2. 如果我做的類型，是我定義正確的功能？

Answer 1

我們可以證明Enumeration a（主要）是同構列表的列表。 的「同構」是通過以下功能給定：

enumerationToLists :: Enumeration a -> [[a]] 
enumerationToLists f = map f [0..] 

listsToEnumeration :: [[a]] -> Enumeration a 
listsToEnumeration xss i = head $ drop i (xss++empties) 

其中：

empties :: [[a]] 
empties = []:empties 

由於引用透明，我們可以使用「方程式推理」在數學完成，以證明他們確實是形成「同構」

證明listsToEnumeration . enumerationToLists = id：

(listsToEnumeration . enumerationToLists) f 
by definition of . 
    = listsToEnumeration (enumerationToLists f) 
by definition of enumerationToLists 
    = listsToEnumeration (map f [0..]) 
by definition of map 
    = listsToEnumeration [f 0, f 1, f 2, ...] 
by definition of listsToEnumeration 
    = \i -> head $ drop i ([f 0, f 1, f 2, ...]++empties) 
concatenation of infinite lists 
    = \i -> head $ drop i [f 0, f 1, f 2, ...] 
by definition of drop and of the argument 
    = \i -> head $ [f i, f (i+1), f (i+2), ...] 
by definition of head 
    = \i -> f i 
eta reduction (i.e. \x -> f x = f) 
    = f 

而現在，鑑於xss = [xs1, xs2, ..., xsN]和empties = []:empties，我們有(enumerationToLists . listsToEnumeration) (xss++empties) = xss++empties

(enumerationToLists . listsToEnumeration) (xss++empties) 
by definition of . 
    = enumerationToLists (listsToEnumeration (xss++empties)) 
by definition of listsToEnumeration 
    = enumerationToLists (\i -> head $ drop i (xss++empties++empties)) 
concatenation of infinite lists 
    = enumerationToLists (\i -> head $ drop i (xss++empties)) 
by definition of empties 
    = enumerationToLists (\i -> head $ drop i [xs1, xs2, ..., xsN, [], [], ...]) 
by definition of enumerationToLists 
    = map (\i -> head $ drop i [xs1, xs2, ..., xsN, [], [], ...]) [0..] 
by definition of map 
    = let f = (\i -> head $ drop i [xs1, xs2, ..., xsN, [], [], ...]) in [f 0, f 1, ...] 
by definition of f 
    = [head $ drop 0 [xs1, xs2, ..., xsN, [], ...], head $ drop 1 [xs1, xs2, ..., xsN, [], ...], ...] 
by definition of drop 
    = [head [xs1, xs2, xsN, [], ...], head [xs2, ... xsN, [], ..], ..., head [xsN, [],...], head [[], ...], ..] 
by definition of head 
    = [xs1, xs2, ..., xsN, [], [], ...] 
by definition of xss, empties and ++ 
    = xss ++ empties 

顯然我們假設Enumeration a是總（應爲「非定義的索引」迴歸[]）。上面的兩個函數是一個同構，如果我們限制爲無限列表的列表，否則它只能保持「高達++empties」（如果xss是無限的，我們有xss = xss++empties，因爲我們將永遠無法訪問空容器部分）。所以如果你在乎保持這個「同構」，你應該確保你的所有功能都是全部的（看着singleE' ...），但除了這個，它們看起來不錯。

我希望上面的例子給出了關於如何推斷你定義的函數是否正確的提示。