Re: [問題] Free Monad 是怎麼來的？

看板PLT (程式語言與理論)作者xcycl (XOO)時間11年前 (2013/10/30 08:50)推噓2(2推 0噓 4→)

留言6則, 2人參與討論串2/5 (看更多)

※ 引述《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 不同於傳統用 term algebra 取 quotient 的方式，我們可以層層迭代，第 n 層恰好有 n 個 dot 運算第零層 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)