あどけない話

インターネットに関する技術的な話など

モナド則三度

モナド則再び」で書いた「モナド則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 62: 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 は不要」です。

モナド則3の意味は、「複数段のモナドは、一段に変更できる」ですね。