---

※ 引述《suhorng ( )》之銘言：
: 最近看code時, 看到好幾個的地方都出現 free monad:
: http://www.haskellforall.com/2013/06/
: from-zero-to-cooperative-threads-in-33.html
: Data types `a la carte 最後考慮結合monad也只考慮free monad (因為結構最少?)
: Extensible Effects推到後來他拿來包 effect 的 monad 型別
:     data VE r w = Val w | E (Union r (VE r w))
: 看起來也有幾分像 free monad (Union是某個由 r indexed 的 coproduct)
: 而且後來舉的 coroutine 例子
:     type CoT a m = ContT (Y m a) m
:     data Y m a = Done | Y a (() -> m (Y m a))
: 雖然前面 Done 那項不太一樣, 但後面 Y 那裡一樣有遞迴, 也是丟進 m 裡面
: 我只知道 free monad 是當我們想要給一個 functor F 多加上
: monad 的結構時所自然衍生出來的東西,
: 不過那個結構[aka. data Free f a = Pure a | Impure (f (Free f a))]
: 到底要怎麼推出來呢...?
用特例來說的話，其實看 free monoid 就好
要構造 free monoid (FA, e, .) over A

第零層 X0  只有 A
第一層 X1 有 A, e 跟  x . y 其中 x, y 在 X0，並且將該有的等式加上去
第二層 X2 有 A, e 跟  x . y 其中 x, y 在 X1
.. 依此類推
因為 . 只取兩個元素出來，我們可以保證取 X0 + X1 + ... + Xn + ...
可數無窮多個的聯集之後就得到 free monoid FA，也就是 fixpoint。

在 Haskell 恰好是 ([A], [], ++)

那麼 unit :: A -> [A] 就是定義成

unit a = [a]

而 mul :: [[A]] -> [A] 定義成 concat

這也恰好是 list monad 的定義。或許跟 Haskell 的 monad 定義稍微不同，
數學上 Haskell 的定義稱為 Kleisli triple，與以上用 A -> [A] 與 [[A]]-> A
定義的是等價的。

如果讓 FX 代表將 e 跟 x . y 加進去的集合，
得出 A -> A + FA -> A + F(A + FA) -> ... 這樣的序列。
一般的情況下，對任意 functor F，
假若上面的序列收斂的話，我們就會得到 (algebraically) free monad，
其中 mul 對應到 monad 的 muplication (mu) 而 unit 就對應到 unit (eta) 。
同時從 functor 到 monad 的 left adjoint 也很自然地得到。

嚴格的數學證明在

J. Adamek, "Free algebras and automata realizations
in the language of categories", Comment. Math. Univ. Carolin. 15(1974), issue 4,
589-602

G. M. Kelly, "A unified treatment of transfinite constructions for
free algebras, free monoids, colimits, associated sheaves, and so on",
Bull. of the Austral. Math. Soc, 22(1980), 1-83

這兩篇論文都找得到，可能要熟悉 category theory 比較好讀
: 這個定出來以後 instance 怎麼寫就比較好猜了..雖然還是很神奇QQ
: [1]關於free monad http://stackoverflow.com/questions/13352205/
: -
: 另外有人聽過 codensity monad 嗎?
: 查不太到什麼資料orz...
Tom Leinster 在 arXiv 有一篇比較一般性的討論，可參考
http://golem.ph.utexas.edu/category/2012/09/where_do_monads_come_from.html

--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 78.151.174.221
※ 編輯: xcycl           來自: 78.151.174.221       (10/30 09:26)

--