※ 引述《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)