8.2 單子與單子律
第 0 章提及,「抽象化」意指抽取出一個問題中最關鍵的元素。 一個成功的抽象化能抓到同類問題的共通本質,因此可以推廣到其他相關的情境、問題,用同一套方法表達這些情境、解決這些問題。 我們在第 8.1 節發現的便是一個關於計算與副作用的成功抽象化。
我們可以把第 8.1 節中的 Except a 理解成一個 尚待完成的計算,或是一個尚待執行的程式。
用 case 去配對它便是把這個計算算出來、把程式執行出來。
如果順利執行,計算結果的型別為 a, 但也可能產生副作用。
而由其型別建構子 Except 可看出此處可能的副作用是「可能拋出例外」。
運算子 (>>=) 的功用是將小計算/程式串接起來,組成較大的計算/程式。
推廣出去,Except 其實可以是任意一個型別建構元 m: 一個型別為 m a 的值表示一個尚待完成的計算,或是一個尚待執行的程式。如果順利執行,計算結果的型別為 a, 但執行過程中可能產生副作用。
至於究竟是什麼副作用,則看 m 是什麼而定。
此外,每個 m 附帶兩個運算子:
return :: a -> m a;(>>=) :: m a -> (a -> m b) -> m b.
它們三者合稱為一個單子(monad).
給任一個值 x :: a, 運算子 return x 代表一個純粹傳回 x, 沒有副作用的計算。以 m = Except 為例,自然的選擇是令 return = Return. 我們之後會看到其他例子。
運算子 (>>=) 將小計算串接在一起。
在 p >>= f 之中,p :: m a 是一個回傳型別將為 a, 但可能有副作用的計算。
如果 p 被算出來,其結果會被傳給 f.
函數 f :: a -> m b 是一個拿到 p 的結果後算出一個計算的計算.
整個式子 p >>= f 的型別也是 m b.
這是理解單子程式的一個重點:函數本身沒有副作用,但函數可以算出含有副作用的程式。
如果我們把 f 寫成 $\lambda$ 表示式,
在 p >>= \x -> e 之中,p 的結果被取名為 x,而 e :: m b 之中可以使用 x.
此處 (>>=) 可理解成由兩個小計算 p 與 e 組出一個大計算的接著劑,兩個小計算用 x 來溝通。
運算子 return 與 (>>=) 是用來組合出含有副作用的程式的元件,因此得滿足一些該有的性質。正式說來,
定義 8.1 單子
一個單子(monad)包含一個型別建構子 m,
以及兩個運算子 return :: a -> m a 與 (>>=) :: m a -> (a -> m b) -> m b. 它們須滿足以下三條單子律:
右單位律(right identity):
p >>= return= p左單位律(left identity):
return x >>= f= f x結合律(associativity):
(p >>= f) >>= g= p >>= (\x -> f x >>= g)
右單位律若寫成 p >>= \x -> return x 也許更好理解。計算 p 的結果 x 被傳到 (>>=) 的右邊,但後者只是單純地把 x 再傳出。這和只寫 p 得是一樣的。
在左單位律的左手邊 return x >>= f 之中,函數 f 接收 return x 的結果 --- 而 return x 的結果就是 x! 因此這和 f x 得是一樣的。
最後一條是 (>>=) 的結合律:「用 p 與 f 串接出一個程式,再把 g 串接到右邊」與「把 f 與 g 串接在一起,並把 p 串接在它們左邊」得到的必須是一樣的程式。
但由於型別的問題,在後者的情況我們需要一個 x 表示 p 的結果,前者則不用。
每定義一個新的單子,我們需選定一個型別 m,定義 return 與 (>>=) 兩個運算子,然後證明它們滿足單子律。需要推論含單子的程式的性質與正確性時,這三條單子律也是我們會用到的性質。
最後一提:定義 8.1 並不是單子的唯一定義方式。其他等價的定義詳見 \todo{where}.
單子 class 既然 Haskell 有 type class 機制,我們可以把單子定義為一個 class:
class Monad m where
return :: a -> m a
(>>=) :: m a -> (a -> m b) -> m b
如此明確規定一個屬於 Monad 的型別建構子必須有 return 與 (>>=).
Except 型別則是其中的一個特例:
instance Monad Except where
return = Return
Expt msg >>= f = Expt msg
Return x >>= f = f x
之後我們討論其他的 m 時,也將把它們宣告為 Monad 的特例。
但這麼做只是為了兩個方便性:1. 讓不同的 m 可以共用 return 與 (>>=) 兩個符號,不用重新取名;2. 看到使用 return 與 (>>=) 的程式時,可以暫時不指定它們到底使用那一個特例。
若非為了這些小方便,單子與 type class 不一定得有關聯。
此外,Haskell 中的 type class 宣告也只保證 return 與 (>>=) 的型別是正確的。
目前 Haskell 並無法保證使用者定義的 return 與 (>>=) 滿足前述的單子律。
副作用特定的運算子
不知讀者是否想起:那麼 throw 與 catch 呢?
他們也應該滿足一些性質,例如,throw msg >>= f = throw msg (拋出例外後,後面的 f 不會執行)和 catch (throw msg) hdl = hdl msg (throw 拋出的例外由 hdl 處理)應該都是合理以及必要的性質。
另一方面,它們是屬於「例外」這個副作用的運算子,其他的副作用並不見得會有它們。
反之,別的副作用可能會有該副作用的特定運算子。例如,要談可變變數,可能會有個賦值運算子,這是 Except 沒有的。
由此得知,用於表達副作用時,單子的運算子可分為兩大類:1. return 與 (>>=) 是各個副作用共通的,
每個單子都必須定義 return 與 (>>=), 並確保它們滿足單子律。2. 此外,每個副作用還可能擁有特有的運算子,它們可能也有些該滿足的性質。
我們將在介紹各個副作用的小節中看到更多例子。