hkB*_*Bst 3 haskell types unfold
文档中给出的示例unfoldr :: (b -> Maybe (a, b)) -> b -> [a]:
unfoldr (\b -> if b == 0 then Nothing else Just (b, b-1)) 10
可以使用冗余对轻松编写:
unfoldr (\b -> if b == 1 then Nothing else Just (b-1, b-1)) 11
这对unfoldr需要什么(a,b)？为什么它的类型不是(a -> Maybe a) -> a -> [a]？
Lee*_*Lee 12
具有类型的函数
(a -> Maybe a) -> a -> [a]
将输出列表元素类型限制为与生成过程中的线程相同的状态.unfoldr更通用的是它允许使用独立类型的状态.
利用一点理论，人们可以恢复递归类型的折叠/展开类型，包括列表，理解它们为什么是这样的。
设A为固定类型。类型“list of As”满足同构
List ~~ Either () (A, List)
可以理解为“列表值要么是特殊值（空列表），要么是A后跟列表值的类型值”。
用更简洁的表示法，我们可以写Either为中缀+：
List ~~ () + (A, List)
现在，如果我们让F b = () + (A, b)，我们就有了
List ~~ F List
上面是一个定点方程，在使用递归类型时总会出现。对于由 定义的任何递归类型，T ~~ F T我们可以导出相关折叠/展开的类型（也称为cata/ana归纳/共归纳原理）
fold :: (F b -> b) -> T -> b
unfold :: (b -> F b) -> b -> T
在列表的情况下，我们得到
fold :: ((() + (A, b)) -> b) -> List -> b
unfoldr :: (b -> (() + (A, b))) -> b -> List
展开也可以重写，注意Maybe c ~~ () + c：
unfoldr :: (b -> Maybe (A, b)) -> b -> List
可以使用以下方法重写折叠
((x + y) -> z) ~~ (x -> z, y -> z)
得到
foldr :: (() -> b, (A, b) -> b) -> List -> b
那么，自从() -> b ~~ b,
foldr :: (b, (A, b) -> b) -> List -> b
最后，自从(x, y) -> z ~~ x -> y -> z（柯里化）以来，我们有
foldr :: b -> ((A, b) -> b) -> List -> b
然后再次：
foldr :: b -> (A -> b -> b) -> List -> b
最后翻转x -> y -> z ~~ y -> x -> z：
foldr :: (A -> b -> b) -> b -> List -> b
这些类型如何遵循（共）归纳原理？
域理论指出，当在某个偏序集上单调时，最小不动点F(T)=T( ) 与最小前缀点 ( ) 重合。F(T)<=TF
简单的归纳原理指出，如果T是最小前缀点，并且F(U)<=U，则T<=U。（证明。这是最小的！。QED。）在公式中，
(F(U) <= U) ==> (T <= U)
为了处理类型上的不动点，我们需要从偏序集切换到类别，这使得一切变得更加复杂。非常非常粗略地，每个都<=被某种态射所取代。例如，F(U)<=Unow 意味着存在某种态射F U -> U。“单调F”意味着它F是一个函子（因为a<=b暗示F(a)<=F(b)现在变成了(a->b)暗示F a -> F b）。前缀点是 F 代数 ( F u -> u)。“最少”变成“初始”。等等。
因此折叠的类型：（含义也是->如此）
fold :: (F u -> u) -> (T -> u)
Unfold 源自共归纳原理，该原理处理最大后缀点T（成为余代数）
(U <= F(U)) ==> (U <= T)