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

看板PLT (程式語言與理論)作者 (Josh Ko)時間10年前 (2013/10/30 22:10), 編輯推噓0(006)
留言6則, 5人參與, 最新討論串4/5 (看更多)
※ 引述《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)

10/30 22:58, , 1F
查一下 IP (xcycl 和 joshs) 就知道, 藥學好 category 就要去
10/30 22:58, 1F

10/30 22:58, , 2F
英國 (誤)
10/30 22:58, 2F

10/30 23:20, , 3F
我 category theory 不好啦.. 像剛剛 xcycl 才罵我太隨便 XD
10/30 23:20, 3F
※ 編輯: joshs 來自: 163.1.130.189 (10/31 00:49)

10/31 00:56, , 4F
我才是太隨便的人啦 QQ
10/31 00:56, 4F

10/31 16:29, , 5F
後面這段無窮級數求極限太過份了 XD
10/31 16:29, 5F
xcycl 也是噹我這裡,因為 1 + F + F^2 + ... 和 1 + F(1 + F(1 + ...)) 不一樣。現在我知道為何左式(真的)不對了 XD。 兩個問題: (1) 為何左式不對? (2) 為何胡亂操作無窮級數竟變得出真的 free monad? ※ 編輯: joshs 來自: 163.1.130.189 (11/01 01:46)

11/01 10:39, , 6F
大驚XD
11/01 10:39, 6F
文章代碼(AID): #1ISHDhbW (PLT)
文章代碼(AID): #1ISHDhbW (PLT)