「モナド則再び」で書いた「モナド則1」は何の訳に立つのかという問題ですが、"Monads for functional programming" に答えが載っていました。
以下のような加算機を考えます。
data Term = Con Int | Add Term Term data M a = M a deriving Show instance Monad M where return x = M x M x >>= f = f x eval :: Term -> M Int eval (Con a) = return a eval (Add t u) = do a <- eval t b <- eval u return (a + b)
論文には、M の実装が載っていないので、適当に作りました。Maybe でもいいでしょう。
こういう風に動きます。
式1: eval (Add (Con 1) (Add (Con 2) (Con 3))) → M 6 式2: eval (Add (Add (Con 1) (Con 2)) (Con 3)) → M 6
上記の二つの式が、同じ値を返すことを、モナド則を使って証明します。
モナド則は、こうです。
モナド則1: return x >>= f == f x モナド則2: m >>= return == m モナド則3: m >>= (\x -> f x >>= g) == (m >>= f) >>= g
do 表記に変えてみると、こうなります。
do y <- return x == do f x f y do x <- m == do m return x do y <- do x <- m == do x <- m f x y <- f x g y g y
式1をモナド則を利用して変形すると、こうなります。
eval (Add t (Add u v)) -- eval の定義 = do a <- eval t x <- eval (Add u v) return (a + x) -- eval の定義 = do a <- eval t x <- do b <- eval u c <- eval v return (b + c) return (a + x) -- モナド則3 = do a <- eval t b <- eval u c <- eval v x <- return (b + c) return (a + x) -- モナド則1 = do a <- eval t b <- eval u c <- eval v return (a + (b + c))
式2をモナド則を利用して変形すると、こうなります。
eval (Add (Add t u) v) -- eval の定義 = do x <- eval (Add t u) c <- eval v return (x + c) -- eval の定義 = do x <- do a <- eval t b <- eval u return (a + b) c <- eval v return (x + c) -- モナド則3 = do a <- eval t b <- eval u x <- return (a + b) c <- eval v return (x + c) -- モナド則1 = do a <- eval t b <- eval u c <- eval v return ((a + b) + c)
めでたく、モナド則1が利用されました。パチ、パチ、パチ。
モナド則1の意味は、「単に return された値を保持する変数は、なくすことができる」という意味なんですね。
ちなみに、モナド則2の意味は、「最後の式が return されるので、明示的な return は不要」です。
