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