2011/05/07

Term algebra

Jeremy 在昨天的 AoP meeting 重講 maximum segment sum,最後提出一個 datatype-generic version。(他寫在他最新的 blog post Horner's Rule。)中間我們拐到 T-algebras:令 T 是 monad,那麼我們稱 f : T a → aT-algebra 的意思是它滿足 f . μ = f . T ff . η = id。(μ : TT → Tη : Id → T 是伴隨 monad T 來的兩個 natural transformations,在 Haskell 裡面是 joinreturn 這兩個 polymorphic functions。)這時 Nick 問道:他一直看不出這裡說的 algebra 和我們一般講的 algebra(monoids, groups, rings, fields, ...)有什麼關係。Well asked! Jeremy 於是給了下面這一段 monad 循循善誘版介紹。

我們知道一個 monoid 是某個集合上面定義一個 associative binary operator 並且有一個 unit。比方說,List A 是一個 monoid,用的 associative binary operator 是 concatenation "++",unit 則是 empty list []。它們的 type 是

[]   : List A
(++) : List A × List A → List A
稍微複雜一點的例子像是架在某個 field K 上的 vector space V,這時我們有 vector addition、unit、和 scalar product:
0   : V
(+) : V × V → V
(·) : K × V → V
這些 operators 必須滿足某些額外的條件。但無論那些 operators 的 signature 有多複雜,我們發現它們的 result type 都是那個底層的集合。Category theorists 於是用 sum types 把這些 operators 收集起來,list monoid 的話是
1 + List A × List A  →  List A
vector space 則是
1 + V × V + K × V  →  V
最後我們把箭號左邊的東西抽象成某個 "signature" functor F,上述兩個 type 就都能寫成 F X → X 的型式,其中 X 是底層的集合(List AV)。(對於 list monoid 我們讓 F X := 1 + X × X,vector space 則是 F X := 1 + X × X + K × X。)於是 F X → X 這種型式的 arrows 我們就叫它做 F-algebra,只要適當定義 F 就能表現各式各樣的 operators,至於這些 operators 應該滿足的條件就還要另外陳述。以 monoids 為例,令 f : 1 + X × X → X,裡面藏的那個 binary operator (++) = f . inr 的 associativity 是
(x ++ y) ++ z = x ++ (y ++ z)
這可以繼續改寫成 point-free 型式:
(x ++ y) ++ z = x ++ (y ++ z)
≡ ((++) . ((++) × id)) ((x, y), z) = ((++) . (id × (++))) (x, (y, z))
≡   { 令 assoc ((x, y), z) := (x, (y, z)) }
  ((++) . ((++) × id)) ((x, y), z) = ((++) . (id × (++)) . assoc) ((x, y), z)
≡   { extensionality }
  (++) . ((++) × id) = (++) . (id × (++)) . assoc
願意的話可以繼續畫成 commutative diagrams 之類的。如果描述的性質足夠泛化,甚至可以寫成「不須依賴 F 實際定義」的型式。

所以給一個 F-algebra f : F A → A,小學生可以用它列出算式然後求算 normal form。但國中生開始處理未知數的時候,事情就變得複雜一些,因為「列算式」和「求值」這兩個階段更明確地分開了。假設我們考慮整數加法和乘法,小學生看到的算式都是立刻可以求算出值的,在 Haskell 裡面就相當於用 +* 直接列式,比方說 3 + 2 * 5,那直接是個 Int,小學生做的事情只是把它化簡成 normal form 而已。但國中生看到的式子含有未知數,那些式子沒辦法求算得一個整數值,所以更精確的說法是他們先定義一個 datatype

data Expr X = Var X | Add (Expr X) (Expr X) | Mult (Expr X) (Expr X)
其中 X 是未知數 x, y, z, ... 這些符號的集合(請忽略 Haskell 的 naming conventions XD),然後用 Var, Add, Mult 這些 constructors 列式,如 Var 'x' `Add` (Var 'y' `Mult` Var 'z'),另外再有一個求值函式把 X 上的賦值擴充到 Expr X 上:
eval : (X → Int) → Expr X → Int
eval σ (Var x)    = σ x
eval σ (Add a b)  = eval σ a + eval σ b
eval σ (Mult a b) = eval σ a * eval σ b
如果我們要把加法和乘法這兩個 operators 表示成 F-algebra,那麼我們會定義 F Y := Y × Y + Y × Y。顯然 Expr XF 是有關聯的 — 前者乃導自後者,Expr X 其實是 μY. X + F Y!一個算式 Expr X 可能是個未知數,或是一個 F (Expr X),也就是某一個 operator 下繼續裝更多算式。現在有兩件事情應該滿容易能接受:首先,給一個未知數 x : X,我們可以把它變成一個算式 Var x : Expr X。再來,Expr XX 可以是任意的集合,也就是說我們所謂的未知數其實可以是各種奇怪的東西,就像高年級小學生可以寫 "□ + ▵ * ◯" 一樣。而其中一種我們可以當作未知數的東西就是 Expr X,像 "[x + y] + [y * z] * [z + x]",方括號的意思是說括起來的部份其實我們看作是一個「未知數」,這個算式的 type 是 Expr (Expr X)。但絕大部份人看到這個算式都會覺得我們只是寫一個單純的算式,裡面有未知數 x, y, z,也就是說,他們看到的算式型別是 Expr X。因此給一個 Expr (Expr X),我們可以把中括號抹去,讓它變成一個 Expr X。這兩件事情正是 monad 附帶的那兩個 natural transformations return : X → T Xjoin : T (T X) → T X,它們互動的時候會滿足某些看起來很自然的條件,比方說把一個算式看作是未知數(加上中括號)再把中括號抹掉會得到原來的算式(join . return = id)之類的。所以我們剛得知 Expr 是個 monad。再想一想,「抹括號」這件事情其實和 substitution 息息相關。如果我們有一個 Expr Xx + y * z,然後對於每個未知數我們都指定一個要取代它的 Expr Y,也就是說我們有一個 function X → Expr Y,那麼代換後我們會得到 [u + v] + [v * w] * [w + u] 這種東西,其中 u, v, wY 裡的未知數,算式型別是 Expr (Expr Y),抹去括號後我們就得到一個 Expr Y。整個過程的型別是 Expr X → (X → Expr Y) → Expr Y,也就是 bind operator。

List monad 用算式觀點來看應該十分自然(因為正好只是 free monoid),比方說 concat : List (List A) → List A 確實是把第二層的中括號抹掉。IO monad 我相信一樣可以用算式來看,只是它的 operators 複雜一點。想法大概是 IO a 只是一段程式碼(syntax tree — 所以也是某種算式),我們寫 Haskell 程式去產生那些程式碼。至於程式碼的執行是高一層的事情,就好像外界有個 eval 在跑一樣。Expreval 只是把 Add 翻譯成 +,但 IO 的 eval 翻譯出來的東西比較複雜,得把某個 operand 的結果餵給別的 operand 讓那個 operand 算出更多程式碼,所以情況會像是跑一段程式碼把結果丟給 Haskell 程式產出更多程式碼再繼續跑一樣。Haskell 程式負責的永遠只是產出程式碼,那當然都是 pure data/computations 嘍。

--
先還個債,以後想到再寫清楚一點⋯ XD

Labels: ,

Blogger Lin Jen-Shin (godfat)5/08/2011 3:02 pm 說:

未看先感謝,容我慢慢讀.. XDD

 
Blogger XOO5/08/2011 11:32 pm 說:

Well done!

 
Blogger Lin Jen-Shin (godfat)5/15/2011 11:04 am 說:

大抵上看完了,我猜應該有看懂大部份? XD
唯一比較明確不懂的是這條

μY. X + F Y

這邊的 . 是 lambda abstraction 中的 .
還是 composition? 不過不管是哪個,還是
不太懂是什麼意思。然後查到這篇在解釋 μ,
還沒看完,不過相關的東西真的看過無數次了,
希望這次能多搞懂一些 XDD
雖然我後來回頭看,才發現開頭就提過 μ 是haskell
中的 join...

然後我猜,我應該沒有懷疑過 IO monad 是不是 monad
or pure, 純就算式來看,或是說只單純把他當做符號的話,
應該也是滿自然的?我一直覺得很怪的,或許是
總覺得 IO monad 具有比 monad 更多許多的性質?

前一陣子一直在想的是,假使 pattern matching 是
lazy 的,而那個假造的 world state, 實際上我們
並不是真的需要他,那麼我們要怎麼確保 IO monad
本身的運算確實是有相依性的?式子上或許相依,
但依照 haskell laziness 的實作,我們勢必得有個
地方能夠「強迫」他去做某種運算?

現實似乎是,反正 pattern matching 是 strict 的,
因此可以靠 pattern matching 來達成這種強迫,
但這應該不是 monad 本身在描述的?是否有另一種
class/category 可以拿來描述這樣的結果呢?

說不定我得依照這篇:

Unraveling the mystery of the IO monad

看看 IO monad 翻譯出來的運算到底是長啥樣 @@

感謝~

 
Blogger Josh Ko5/15/2011 9:35 pm 說:

> μY. X + F Y

啊,這個是說 G(Y) = X + F(Y) 這個 functor G 的 least fixed point, 不是 monad 的 μ.

> IO monad 具有比 monad 更多許多的性質?

關於 IO monad 我確實沒有明確講,因為我現在有的概念也只停在揮揮手的階段 XD。但要我再多揮一點的話,我會說「算出要執行的 IO expressions」是 Haskell 一般的 evaluation(包括 pattern matching、和 laziness/strictness 之類的性質都在這一層),然後 IO expression 的詮釋(執行)會是另一層,我會猜就是你這裡所謂更多的性質。Monads 只處理 syntax,semantics 要用另外的東西描述,比方說 T-algebras.(但因為 runState 不太像 T-algebras,所以我沒寫這個。) 就好像四則運算算式的「抹括號」是 syntactic operation(所以是用 monad 的 μ operator),但算出那個算式代表的值是用另外的 eval function(這不是 monad 預設帶有的操作)。

 
Blogger Lin Jen-Shin (godfat)5/16/2011 5:10 am 說:

噢!我一直看成:

(μY. X) + F Y

而不是:

μY. (X + F Y)

難怪一直不明白是指什麼 orz
我發覺對這些符號不熟悉對於理解影響真的很大 orz

然後沒搞錯的話,這邊大概都懂了,謝啦~
不過這似乎也意味著,既然 monad 只處理
syntactic operation, 那就還有更多東西要看了 orz

 

<< 回到主頁