作者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