作者joshs (Josh Ko)
看板PLT
标题Re: [问题] Free Monad 是怎麽来的？
时间Wed Oct 30 22:10:49 2013
※ 引述《suhorng ( )》之铭言：
: 不过那个结构[aka. data Free f a = Pure a | Impure (f (Free f a))]
: 到底要怎麽推出来呢...?
我觉得若能用 "monad is monoid in the category of endofunctors"
这个观点把 free monoid 和 free monad 类比起来，应该会比较直觉。
（警告：本文论述和正式理论有显着差距。）
先从 monoid 和 monad 的类比开始。我们知道 monoid 是有单位元素和
二元乘法（具结合律）的集合。对应到 monad 时，我们得问这个「集合」
是什麽，以及这「集合」里的「元素」如何「相乘」。（单位元素请自行脑补。）
这里需要一点想像力的飞跃：给定 monadic functor M, 我们可以把 M
想成一个 type, 里面的元素是「一层 M-结构」。例如，定义
data Expr a = Var a | Add (Expr a) (Expr a)
Expr 是个 monad. 什麽是「一层 Expr-结构」？考虑 Expr Int:
这是在整数上加一层「Expr-结构」 —— 整数并非赤裸裸地出现，
而是包在某个树形里。这个树形可能是 Var -（减号代表为了包东西留的洞），
可能是 Add (Var -) (Var -), 或更复杂的东西。这些用来包东西的树形
可直观视为 Expr 这个 "type" 的元素。（如果你觉得这个说法有漏洞，
你大概懂了...）
那麽「Expr-结构」相乘是什麽意思？是两层树形整并成一层树形，即
join :: Expr (Expr a) -> Expr a
join (Var e) = e
join (Add es es') = Add (join es) (join es')
若树形里面包的东西（都）是树形，那麽整个形状可「视为」一个更大的树形。
「整并」有结合律：若树形里包树形，後者里面再包树形，那麽把这三层整并成
一层时，先整并外两层或内两层，结果都一样。
至此我们已可对照 monoid 和 monad —— 我们把 join 的型态写成
"point-free style"
join :: (Expr . Expr) ~> Expr -- natural transformation
以便和 monoid（以固定大小的方阵为例；无特别意义）做类比：
monoid（固定大小的方阵） monad (Expr)
元素 方阵 用来包东西的树形
两个元素 一对方阵 树形里包树形
(cartesian product) (functor composition)
乘法 矩阵乘法 嵌套的树形整并为一
（型态为 方阵 × 方阵 -> 方阵） （形态为 Expr . Expr ~> Expr）
这类比完整且精确地写下来，就是有名的那句 "All told, a monad X is just
a monoid in the category of endofunctors of X".
回到 free monoid 和 free monad. 前者的构造可想成对乘法封闭性的追求：
给一集合 S, 我们当然没办法把任两个 S 的元素合成一个 S 的元素，但如果
我们把「一对元素」也视为合法元素，那现在任两个 S 的元素确实可以合成一个
合法元素。但我们要的是任意合法元素的合成，所以我们又必须考虑 S 的元素
如何和「一对元素」合成，以及「一对元素」和「一对元素」如何合成，因此
我们只能把合法元素的定义推广到「一个、两个、三个、或四个元素排成一排」。
依此类推以至无穷（并将乘法单位元素纳入考量），我们得到的合法元素定义
就变成「任意有穷个元素排成一排」，在这个定义上乘法才终於封闭了。
Functor F 上的 free monad 也是一样，不过现在「一排元素」指的是任意
有穷层的嵌套「F-结构」，即「零层或一层或两层或 ... 的 F-结构」。
这可以很随性（全无理论基础）地写成
F* ~= 1 + F + F^2 + ...
我们可以弄点高中数学，左右同乘 F 再加 1 (identify functor):
F . F* ~= F + F^2 + ...
1 + F . F* ~= 1 + F + F^2 + ... ~= F*
最後一式左右翻转、逐点 (pointwise) 展开就得到
F* a ~= a + F (F* a)
对应於 Free f 的定义。
--
※ 发信站: 批踢踢实业坊(ptt.cc)
◆ From: 163.1.130.189
※ 编辑: joshs 来自: 163.1.130.189 (10/30 22:47)
1F：→ scwg:查一下 IP (xcycl 和 joshs) 就知道, 药学好 category 就要去 10/30 22:58
2F：→ scwg:英国 (误) 10/30 22:58
3F：→ joshs:我 category theory 不好啦.. 像刚刚 xcycl 才骂我太随便 XD 10/30 23:20
※ 编辑: joshs 来自: 163.1.130.189 (10/31 00:49)
4F：→ xcycl:我才是太随便的人啦 QQ 10/31 00:56
5F：→ CindyLinz:後面这段无穷级数求极限太过份了 XD 10/31 16:29
xcycl 也是当我这里，因为
1 + F + F^2 + ... 和 1 + F(1 + F(1 + ...))
不一样。现在我知道为何左式（真的）不对了 XD。
两个问题：
(1) 为何左式不对？
(2) 为何胡乱操作无穷级数竟变得出真的 free monad?
※ 编辑: joshs 来自: 163.1.130.189 (11/01 01:46)
6F：→ suhorng:大惊XD 11/01 10:39