8 單子與副作用

8.3 讀取單子

為了進入下一個例子,我們為算式型別加上變數:

data Expr =  Num Int | Neg Expr | Add Expr Expr |
             Var Name | Let Var Expr Expr 

type Name = String 

Name 是變數名稱,Var v 是出現在算式中的變數,Let 則用來宣告新的區域變數。 例如,以下式子表達的是 let x = 3 + 1 in (x+4)+x:

Let "x" (Add (Num 3) (Num 1))
   (Add (Add (Var "x") (Num 4)) (Var "x")) 

變數 x 的值為 3+1, 因此整個算式的值是 ((3+1) + 4) + (3+1) = 12.

8.3.1 變數與環境

有了變數後,我們不能只問「Add (Var "x") (Var "y") 的(整數)值是什麼」了,因為我們不知道 x 和 y 的值。 有自由變數的算式得放在一個環境下才能談它的值。 所謂「環境」是一個變數到值的函數,告訴我們每個變數的值。我們可以用一個串列表示:或著,我們也可以定義 type Env = Name -> Maybe Int, 而 lookup env x = env x.

type Env = [(Name, Int)] 

例如 Add (Var "x") (Num 4) 在環境 [("x", 3), ("y", 6)] 下的值是 7. 我們也假設有一個「查表」函數:

lookup :: Env -> Maybe Int 

例如,當 env = [("x", 3), ("y", 6)],lookup env "x" 是 Just 3, lookup env "z" 則是 Nothing.

提醒一下讀者:Let 是在宣告區域變數,而不是賦值。例如,下式表達 let x = 3 in x + (let x = 4 in x) + (-x):

Let "x" (Num 3)
    (Add (Add "x" (Let "x" (Num 4) (Var "x")))
         (Neg (Var "x")))

它的值是 3 + 4 + (-3),而不是 3 + 4 + (-4) --- 內層宣告的 x 僅是暫時遮蓋到外面的 x。

有了這些鋪陳,我們看看新的 eval 函數該怎麼寫。 既然算式要在環境之下才有值,eval 得把環境也納為參數之一:

eval :: Expr -> Env -> Int

函數 eval 拿一個算式和一個環境,計算該算式的值。 新的 eval 中,最初的三個條款基本上是一樣的,只是多了一個參數 env 得往下傳:

eval (Num n)      env = n
eval (Neg e)      env = - (eval e env)
eval (Add e0 e1)  env = eval e0 env + eval e1 env 

碰到變數時,我們到環境中查變數的值:

eval (Var x) env = case lookup env x of Just v -> return v 

這裡的 case 算式只處理了 Just 的情形。 如果 lookup 傳回的是 Nothing,也就是變數 x 並不在環境 env 中,該怎麼辦呢?我們等下再談。 最後,碰到 Let x e0 e1 時,我們先把 e0 的值在 env 這個環境之下算出,然後算 e1:

eval (Let x e0 e1) env =
  let v = eval e0 env
  in eval e1 ((x, v) : env)

但計算 e1 時須使用新的環境 (x, v) : env,這讓 e1 可以用到 x。變數 x 在新環境中的值是 v.

算式的語意是函數   第 [RefUndefined] 節開頭提及, 算式沒有變數、沒有除法時,eval 的型別是 Expr -> Int --- 此時一個算式的「意思」就是一個整數。 有了除法後,為了表示可能拋出例外的函數,eval 的型別變成 Expr -> Except Int. 此時 Except a 代表一個尚待完成、可能有副作用(拋出例外)的計算。

加上變數、考慮環境後, eval 的型別變成了 Expr -> (Env -> Int):eval 拿一個算式,傳回一個函數;該函數又拿一個環境,才算出一個整數值。 也就是說,一個算式的語意是「拿一個環境,傳回一個整數的函數」。 的確,既然算式算成的那個整數必須由環境決定,算式其實不能看作一個數值,而應該是從環境到整數的函數才對。 算式 eval (Add (Var "x") (Var "y")) 是一個函數,如果給它 [("x", 3), ("y", 2)], 我們得到 5; 如果給 [("x",4), ("y", -3)], 我們得到 1.

如果把「給一個環境,傳回型別為 a 的結果的函數」叫做 Reader a, 也就是說定義 type Reader a = Env -> a, 函數 eval 的型別成了 Expr -> Reader a. 此處,Reader a 也可視為一個尚待完成、可能發生副作用的計算。 此處可能的副作用包括「和環境詢問變數的值」。 習慣上,我們把這種副作用稱作「讀者(reader)」或「讀取」。 「給環境」的動作,就是執行運算,把值算出來。 我們把其中兩個條款改寫成 $\lambda$ 算式:

eval (Num n)      = \env ->  n
eval (Add e1 e2)  = \env -> eval e1 env + eval e2 env

可以理解成:eval (Num n) 傳回一個計算,無論環境為何,該計算都傳回 n; eval (Add e1 e2) 也傳回一個計算,該計算拿到環境後,在同一個環境之下把 eval e1 和 eval e2 算成值,然後傳回他們的和。

然而,手動把 env 傳來傳去是個重複性高、容易出錯、也嫌累贅的動作。在第 8.1 節中,我們把重複性地產生與拆開 Except 型別的動作抽象成 return 和 (>>=), 使得 Except 成為一個單子。 對於本節的 Reader, 我們也能設計出一組 return 和 (>>=), 把重複的動作抽象掉,使得 Reader 成為一個單子嗎?

8.3.2 「讀取」副作用是單子

讀取單子   如第 8.2 節所述, return 製作一個沒有副作用的計算,(>>=) 則用於把兩個計算接起來。 把 m 代換成 Reader, 它們的型別分別是:

return  :: a -> Reader a
(>>=)   :: Reader a -> (a -> Reader b) -> Reader b 

其中 Reader a = Env -> a.

函數 return 比較單純:return x 是一個無論 env 是什麼,都傳回 x 的計算:

return x env = x 

至於 m >>= f 則可定義如下:

(p >>= f) env = f (p env) env 

p >>= f 的型別為 Reader b, 意謂它可以收一個環境 env 當參數,而等號右手邊必須算出一個型別為 b 的結果。 變數 p :: Reader a 是一個尚待完成的計算,p env 把它算出來,得到型別為 a 的結果。 函數 f 的型別為 a -> Reader b, 因此 f (p env) 意謂 f 得到 p env :: a 的結果,並算出一個新的計算. 這個計算又在得到 env 之後才真正被算出來,最後型別為 b.

有了 return 與 (>>=), eval 的前三個條款可改寫如下:

eval :: Expr -> Reader Int
eval (Num n)      =  return n
eval (Neg e)      =  eval e >>= \v -> return (-v) 
eval (Add e0 e1)  =  eval e0  >>= \v0 ->
                     eval e1  >>= \v1 ->
                     return (v0 + v1) 

除了 Except 變成 Reader 之外和第 8.1 節完全相同! 由於使用了單子這個適當的抽象,只要把型別從 Except 變成 Reader,主程式在不需大幅更動的情況下就可以沿用。使用單子,我們能模組化地挑選我們想要的副作用。

讀取單子的特定運算   本節新添加的 Var 與 Let 兩個情況是第 8.1 節沒有的。 要處理它們,需要讀取副作用特有的運算子。

處理 Var x 時,eval 得到環境中查變數 x 的值。 我們姑且先為此專門定義一個函數:

lookupVar :: Var -> Reader Int
lookupVar x env = case lookup env x of Just v -> return v 

之後再考慮更通用的情況。 有了它,eval 遇上 Var x 的條款可寫成:

eval (Var x) = lookupVar x 

計算 Let x e1 e2 時,我們需要更動環境,把「x 的值是 e1 的值」這個資訊加到環境中, 並在新環境內執行 eval e2, 但執行完之後就回到原有的環境 --- 新環境只是局部的。 由於這是常見的模式,我們可定義一個更通用的運算子。 給定一個函數 f :: Env -> Env 用於製作局部的環境, 如果目前的環境是 env, 算式 local f p 在新環境 f env 之下執行 p:

local :: (Env -> Env) -> Reader a -> Reader a
local f p env = p (f env) 

有了 local 的幫忙,eval 遇上 Let 時可寫成:

eval (Let x e0 e1) =  eval e0 >>= \v ->
                      local ((x,v):) (eval e1) 

我們用 ((x,v):) 幫環境增加一筆資料,在這之下計算 eval e2.

練習 8.2

使用本節的定義,將 eval (Add e0 e1) env 與 eval (Let x e0 e1) env 展開,確認它們和第 8.3.1 節的定義一樣。意即:

eval (Add e0 e1)    env = eval e0 env + eval e1 env 
eval (Let x e0 e1)  env = eval e1 ((x, eval e0 env):env)  
答案

考慮 eval (Add e0 e1):

     eval (Add e0 e1) env
===     {- eval 之定義 -}
     (eval e0  >>= \v0 -> eval e1  >>= \v1 -> return (v0 + v1)) env
===     {- (>>=) 之定義 -}
     (\v0 -> eval e1 >>= \v1 -> return (v0 + v1)) (eval e0 env) env
===     {- 函數應用 -}
     (eval e1 >>= \v1 -> return (eval e0 env + v1)) env
===     {- (>>=) 之定義, 函數應用 -}
     return (eval e0 env + eval e1 env) env
===     {- return 之定義 -}
     eval e0 env + eval e1 env 

考慮 eval (Let x e0 e1) env:

     eval (Let x e0 e1) env
===     {- eval 之定義 -}
     (eval e0 >>= \v -> local ((x,v):) (eval e1)) env
===     {- (>>=) 之定義, 函數應用 -}
     local ((x,eval e0 env):) (eval e1) env
===     {- local 之定義 -}
     eval e1 ((x, eval e0 env):env)  

更通用的環境單子   為了說明方便,目前為止我們假設「環境」是某個固定的型別: Env. 我們當然可以把這部份也抽象掉:

type Reader e a = e -> a  

現在 Reader 多吃一個參數 e, 代表環境的型別。 對任意的 e, Reader e 都是一個單子, 函數 local 更通用的型別是 (e -> e) -> Reader e a -> Reader e a. 本節之前的每個 Reader 都需代換成 Reader Env. 例如 eval 的型別是 Expr -> Reader Env Int. 但改變的都只有型別,程式不需變動。

函數 lookupVar :: Var -> Reader Env Int 只能在 e 為 Env 的情況下運作。 更一般來說,讀取單子通常會有一個運算子 ask, 把整個環境傳出來供我們使用:

ask :: Reader e e
ask env = env 

函數 lookupVar 則可改用 ask 定義為:

lookupVar :: Var -> Reader Int
lookupVar x =  ask >>= \env ->
               case lookup env x of Just v -> return v 

最後,本節之中讓 Reader e 與前一節的 Except 共用 return, (>>=) 等符號。 若需在 Haskell 中如此,我們得將 Reader e 宣告為 type class Monad 的一個特例。 但由於一些型別檢查的技術問題, Haskell 不允許用 type 宣告的別名成為 type class 特例。 我們得把 Reader 用 data 宣告成一個資料型別:更普遍的做法是用 newtype 宣告:newtype Reader e a = Reader { runReader :: (e -> a) }. 但本書不談 newtype.

data Reader e a = Reader (e -> a) 

instance Monad (Reader e) where
    return a        = Reader (\e -> a)
    Reader r >>= f  = Reader (\e -> f (r e) e) 

8.3.3 推論讀取單子程式的性質

給一個單子程式,如何討論它的性質? 比如說,對某一個 e, 如何得知 eval (Let "x" (Num 3) (Let "y" (Num 4) e)) 的值是什麼? 它和 eval (Let "y" (Num 4) (Let "x" (Num 3) e)) 的值是否總是相等?

由於 eval 是用 return, (>>=), local ... 等等運算子定義出來的,而這幾個運算子的定義也都已經有了, 我們總是可以把他們的定義都展開, 回到最基礎的層次證明任何我們想確認的性質。 但一來如此的證明可能非常瑣碎,二來 return, (>>=) 等運算子的定義可能還會改變。 我們是否能在稍微抽象一點的層次運作,假裝我們不知道這些單子運算子的定義,只討論它們具有什麼性質,並用這些性質來做證明?

我們應可以合理要求一個「正確」的讀取單子實作應該要滿足下列的性質。 首先,假設 e 是一個不含變數 v 的算式:

ask >>= \v -> return e = return e  \mbox{如果 v 不出現在 e 之中。}    (8.1 )

等號兩邊都只是傳回 e 的值,而 e 的值不受 v 影響,因此 ask 是可以省略掉的。 其次,連續使用 ask 兩次可以縮減為一次就好:

ask >>= \v0 -> ask >>= \v1 -> f v0 v1 {-"~~"-}={-"~~"-} ask >>= \v -> f v v     (8.2 )

在等號左手邊,我們把問了環境兩次之後的計算抽象為一個函數呼叫 f v0 v1. 在右手邊我們則讓 f 的兩個參數都是 v --- 詢問環境一次的結果。

下面兩個式子討論當 local 遇上 return 與 (>>=) 時會如何:

  • local g (return e) = return e

  • local g (p >>= f) = local g p >>= (local g . f)

在 ([RefUndefined]) 的左手邊,改變環境之後立刻 return e, 其實和單純做 return e 一樣。 性質 ([RefUndefined]) 則告訴我們 local g 可以分配到 (>>=) 的兩側。由於型別之故,(>>=) 的左邊是 local g p, 右邊則得用函數合成 (.).

最後,下列性質將 local 與 ask 關聯在一起:

local g ask = ask >>= (return . g)     (8.3 )

在 local g 的環境之下做 ask, 相當於先做 ask, 然後把得到的環境交給 g 加工。 我們可說算式 ([RefUndefined]) 藉由這兩個運算子的互動定義出了 local 的「意思」。

有了這些性質,我們不需引用 local, ask, (>>=) ... 等等的定義,也可論證讀取單子程式的性質了。例如,我們來看看 let x = 4 in x + x 的值會是什麼:

     eval (Let "x" (Num 4) (Add (Var "x") (Var "x")))
===    {- eval 之定義 -}
     eval (Num 4) >>= \v -> local (("x",v):) (eval (Add (Var "x") (Var "x")))
===    {- eval 之定義 -}
     return 4 >>= \v -> local (("x",v):) (eval (Add (Var "x") (Var "x")))
===    {- 單子律:左單位律 \eqref{eq:monad-left-id} -}
     local (("x",4):) (eval (Add (Var "x") (Var "x")))
===    {- eval 之定義 -}
     local (("x",4):) (  eval (Var "x") >>= \v0 ->
                         eval (Var "x") >>= \v1 -> return (v0 + v1))
===    {- \eqref{eq:reader-local-bind} -}
     local (("x",4):) (eval (Var "x")) >>= \v0 ->
     local (("x",4):) (eval (Var "x")) >>= \v1 ->
     local (("x",4):) (return (v0 + v1))

我們將 local (("x",4):) (eval (Var "x")) 抽出來化簡:

    local (("x",4):) (eval (Var "x"))
===   {- eval 與 lookupVar 之定義 -}
    local (("x",4):) (ask >>= \env -> case lookup env "x" of Just v -> return v)
===   {- \eqref{eq:reader-local-bind} -}
    local (("x",4):) ask >>= \env ->
    local (("x",4):) (case lookup env "x" of Just v -> return v)
===   {- \eqref{eq:reader-local-ask}, 左單位律 \eqref{eq:monad-left-id} -}
    local (("x",4):) (case lookup (("x",4):env) "x" of Just v -> return v)
===   {- lookup (("x",4):env) "x" = Just 4 -}
    local (("x",4):) (return 4)
===   {- \eqref{eq:reader-local-return} -}
    return 4 

由此我們得知 local (("x",4):) (eval (Var "x")) 就是 return 4. 將它放回原式中:

     local (("x",4):) (eval (Var "x")) >>= \v0 ->
     local (("x",4):) (eval (Var "x")) >>= \v1 ->
     local (("x",4):) (return (v0 + v1))
===   {- 前述計算 -}
     return 4 >>= \v0 -> return 4 >>= \v1 -> return (v0 + v1)
===   {- 單子律:左單位律 \eqref{eq:monad-left-id} -}
     return (4 + 4) 

因此,eval (Let "x" (Num 4) (Add (Var "x") (Var "x"))) 就是 return 8.

提醒讀者注意一點:eval (Let "x" (Num 4) (Add (Var "x") (Var "x"))) 和 return 8 都不是基礎型別,而是「尚待完成的計算」。 論證單子程式時我們常常不是在基礎型別的層次上運作,而是證明一個計算與另一個計算是等價的。 這意味著它們傳回同樣的值,也發生同樣的副作用。 我們日後會看到更多此類的例子。

練習 8.3

證明對所有 e :: Expr,

  eval (Let "x" (Num 3) (Let "y" (Num 4) e)) =
    eval (Let "y" (Num 4) (Let "x" (Num 3) e)) 

如果 (("x",3):) . (("y",4):) = (("y",4):) . (("x",3):) 成立。

練習 8.4

然而,(("x",3):) . (("y",4):) = (("y",4):) . (("x",3):) 並不成立。

我們稍早曾遇到這個問題:如果給這樣的式子 eval (Var "x") [("y",0)], 變數 x 並不在環境中,lookup 將傳回 Nothing,這時該怎麼辦?

我們可以再擴充 Reader 的型別,讓 eval 也可以傳回一個 Except 結果:

type ReaderExcept e a = e -> Except a

而 return 和 (>>=) 也得隨之擴充:

return a = \env -> Just a
rm >>= f = \env -> case rm env of
                    Just v -> f v env
                    Nothing -> Nothing

這個 ReaderExcept 型別綜合了讀取單子與例外單子的功能,其 return 與 (>>=) 定義也像是兩個單子定義的混合。 但這並不是令人相當滿意的做法。ReaderExcept 比起 Reader 又更複雜了一點。日後我們也許會想要有更多功能,例如狀態、輸出入等。ReaderExcept 已經夠抽象難解了,我們並不希望設計、維護越來越龐大的單子。

既然 Maybe 單子讓一個程式加上「例外」的副作用,讀取單子讓一個程式加上可存取環境的功能,我們能否把這兩項功能分別模組化地加入呢?

也就是說,給了兩個單子 M1 和 M2, 能否把他們的功能加在一起,產生另一個新單子呢?