Term algebra

Jeremy 在昨天的 AoP meeting 重講 maximum segment sum，最後提出一個 datatype-generic version。（他寫在他最新的 blog post Horner's Rule。）中間我們拐到 T-algebras：令 T 是 monad，那麼我們稱 f : T a → a 是 T-algebra 的意思是它滿足 f . μ = f . T f 和 f . η = id。（μ : TT → T 和 η : Id → T 是伴隨 monad T 來的兩個 natural transformations，在 Haskell 裡面是 join 和 return 這兩個 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 A 或 V）。（對於 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 X 和 F 是有關聯的 — 前者乃導自後者，Expr X 其實是 μY. X + F Y！一個算式 Expr X 可能是個未知數，或是一個 F (Expr X)，也就是某一個 operator 下繼續裝更多算式。現在有兩件事情應該滿容易能接受：首先，給一個未知數 x : X，我們可以把它變成一個算式 Var x : Expr X。再來，Expr X 的 X 可以是任意的集合，也就是說我們所謂的未知數其實可以是各種奇怪的東西，就像高年級小學生可以寫 "□ + ▵ * ◯" 一樣。而其中一種我們可以當作未知數的東西就是 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 X 和 join : T (T X) → T X，它們互動的時候會滿足某些看起來很自然的條件，比方說把一個算式看作是未知數（加上中括號）再把中括號抹掉會得到原來的算式（join . return = id）之類的。所以我們剛得知 Expr 是個 monad。再想一想，「抹括號」這件事情其實和 substitution 息息相關。如果我們有一個 Expr X 如 x + y * z，然後對於每個未知數我們都指定一個要取代它的 Expr Y，也就是說我們有一個 function X → Expr Y，那麼代換後我們會得到 [u + v] + [v * w] * [w + u] 這種東西，其中 u, v, w 是 Y 裡的未知數，算式型別是 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 在跑一樣。Expr 的 eval 只是把 Add 翻譯成 +，但 IO 的 eval 翻譯出來的東西比較複雜，得把某個 operand 的結果餵給別的 operand 讓那個 operand 算出更多程式碼，所以情況會像是跑一段程式碼把結果丟給 Haskell 程式產出更多程式碼再繼續跑一樣。Haskell 程式負責的永遠只是產出程式碼，那當然都是 pure data/computations 嘍。

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