[Haskell]結局、モナド則は何を要求しているのか

Qiita 初投稿です。仲良くしてね　(*´σｰ｀)ｴﾍﾍ
モナド則の解釈に悩む Haskell 初心者の方向けの記事です。

はじめに

Haskellに入門すると、すぐにモナドという概念に向き合うことになります。

モナドは純粋関数型言語であるHaskellの中で手続きを扱うための概念であり、モナドを使うと

• 手続きを記述できる
• 入出力を伴う処理が書ける
• 例外処理が書ける
• 書き換え可能なグローバル変数をエミュレートできる
• パーサが簡単に書ける

などなど、なんだか便利そうです。

そしてモナドを解説する記事や本を読むと、必ず モナド則 という、3つの式からなるモナドの条件が説明されています。
また、自分でモナドを作るときにはこれらのモナド則を満たさなければいけない、とも書かれています。

この記事の目的は、

「これらの式が自作モナドにどんな性質を要求しているのか」
「モナド則を満たすとどんなメリットがあるのか（満たさないと何が問題なのか）」

について説明することです。

（圏論における意味については誰か俺に優しく教えてください……）

準備

本題に入る前にモナド則と、do構文についておさらいしておきます。

準備：モナド則　3つの式

モナド則は以下の3つの式から成ります。

1. (return x) >>= f ≡ f x
2. m >>= return ≡ m
3. (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)

ここで、≡は、両辺のHaskellのコードが等価であることを示します。

モナド則の書き換え

（ここは読み飛ばしてつぎのdo構文の説明に行ってもらっても構いません）
これらの式は [Control.Monad] (http://hackage.haskell.org/package/base-4.10.0.0/docs/Control-Monad.html#v:-62--61--62-) に定義されている (>=>) という中置演算子を使うと、もっとスッキリとした見た目になります。

(>=>)が何をする演算子なのか理解するため、(>=>) の型と(>>=)の型を見比べてみましょう。

Control.Monad

(>=>)       :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
f >=> g     = \x -> f x >>= g

ghci

class Applicative m => Monad (m :: * -> *) where
  (>>=) :: m a -> (a -> m b) -> m b
  ...

この型から、(>=>) は (>>=) の右項になるような、「値を受け取って、モナドに包まれた値を返す」ような関数同士をつなげることができる演算子であることが予想でき、実際に実装を見るとそのように定義されていることがわかります。

この演算子を使うとモナド則は以下のように書き換えることができます。

1. return >=> f ≡ f
2. f >=> return ≡ f
3. (f >=> g) >=> h ≡ f >=> (g >=> h)

随分と見やすくなりましたね。
これは、return, f, g, h の型が全て同じ型、Monad m => a -> m a であるときモノイド則と同等になります。

わけのわからない数式のように見えていたモナド則が、こう書くとちょっと身近に感じられるようになったのではないでしょうか。

準備：do構文

Haskellには、 do構文 と呼ばれるモナドに関する糖衣構文があります。
例として、

do構文

hoge x = do
    foo <- m
    bar <- mFunction x
    m''
    return $ foo + bar

というdo構文は

do構文の展開形

hoge x = (
    m >>= (\foo ->
    mFunction x >>= (\bar ->
    m'' >>= (\_ ->
    return $ foo + bar
    ))))

という風に脱糖されます。
つまり、各行についてそれ以降の行をラムダ式で包んで、それに(>>=)で値を渡すことで手続き的な書き方が実現されているということです。

m'' の部分は

do構文の展開形

hoge x = (
    m >>= (\foo ->
    mFunction x >>= (\bar ->
    m'' >>
    return $ foo + bar
    )))

という風に解釈することもできますが、個人的には前者のほうが統一感があって好きです。

本題：モナド則は自作モナドにどのような性質を要求しているか

以降、簡単のため

1. (return x) >>= f ≡ f x
2. m >>= return ≡ m
3. (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)

をそれぞれ、モナド則(1),(2),(3) と表記します。

1. (return x) >>= f ≡ f x

(return x) >>= f ≡ f x （モナド則(1)）が何を要求しているのかを理解するのは簡単です。
この式はつまり、以下のようなコードが自然に書けることを要求しています。

MonadLaw1.hs

foo x = do
    return $ 10 * x

ultimateAnswer = do
    one <- Just 2
    ten <- foo 4
    return $ ten + one

ここで注目すべきは、foo関数の中のreturnの部分です。
ultimateAnswer内でfoo 4と呼び出しているので、その返り値はreturn 40になることがわかります。

つまり、ten <- foo 4 は ten <- return 40 と同等であり、それはdo構文によって
return 40 >>= (\ten -> ...)
と脱糖されます。

モナド則(1)が満たされていれば、これは
(\ten -> ...) 40
と同等であり、これはつまり、ラムダ式内のtenという変数は、 return の引数であった 40 に束縛されることを示しています。

もし、モナド則(1)が満たされていなかった場合、40を戻り値にしたつもりが、別の値がtenに束縛されてしまう可能性があることをしめしています。

つまりモナド則(1)は、関数内でreturnを使って返した値が、暗黙に書き換わることなく呼び出し元の変数に束縛されることを要求しています。

これで、なぜ自作のモナドにおいてもモナド則(1)を満たす必要があるのかが理解できたと思います。

2. m >>= return ≡ m

つぎに、m >>= return ≡ m （モナド則(2)）ですが、これの理解もそれほど難しくないでしょう。
以下のコードを見てください。

MonadLaw2.hs

ultimateAnswer = do
    ans <- Just $ 7 * 6
    return ans

ultimateAnswer' = do
    Just $ 7 * 6

ここで、 ultimateAnswer はdo構文によって
(Just $ 7 * 6) >>= (\ans -> return ans)
と脱糖されます。

このラムダ式は return に値を渡しているだけなので以下のように書き換えられます
(Just $ 7 * 6) >>= return

ここでモナド則(2)が満たされていれば、これは
(Just $ 7 * 6)
と同じになります。

つまり、 ultimateAnswer は ultimateAnswer' と同等になります。

まとめると、モナド則(2)は <- によって変数に値を束縛してから return しても、 <- を使わずに直接 return するのと同じ結果になることを要求しています。

モナド則(2)が満たされないと、 <- によって一度値を束縛するかどうかで結果が変わってしまう可能性があることになるので、モナド則(2)もモナド則(1)と同様に、自作のモナドをつくるときに必ず満たしていなければいけません。

3. (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)

最後に、 (m >>= f) >>= g ≡ m >>= (\x -> f x >>= g) （モナド則(3)）について説明します。
モナド則(3)はモナド則(1),(2)に比べてややこしく、少し理解が難しいです。

結論を先に言うと、モナド則(3)はブロックや関数を自由に作って、手続きを小分けにできることを要求しています。

do構文の中で if による分岐を行っている以下のコードを見てください。

MonadLaw3_if.hs

import Control.Monad.Writer

ultimateAnswer :: Writer (Sum Int) ()
ultimateAnswer = do
    x <- return $ 5 * 4
    tell x
    if True
      then do
        y <- retrun $ 7 - 5
        tell y
      else
        return ()
    tell 20
    return ()

main = print $ getSum $ execWriter ultimateAnswer

output

42

このコードのdo構文を全て展開すると、以下のような形になります

展開後

import Control.Monad.Writer

ultimateAnswer :: Writer (Sum Int) ()
ultimateAnswer = 
    (return $ 5 * 4) >>= (\x ->
    tell x >>= (\_ ->
    (
      if True
        then 
          retrun $ 7 - 5 >>= (\y ->
          tell y)
        else
          return ()
    ) >>= (\_ ->
    tell 20 >>= (\_ ->
    return () ))))

main = print $ getSum $ execWriter ultimateAnswer

ここで、if True のelse節は実行されないので、このコードは以下のコードと同等になります。

展開後にifを消去

import Control.Monad.Writer

ultimateAnswer :: Writer (Sum Int) ()
ultimateAnswer = 
    (return $ 5 * 4) >>= (\x ->
    tell x >>= (\_ ->
    (
        retrun $ 7 - 5 >>= (\y ->
        tell y)
    ) >>= (\_ ->
    tell 20 >>= (\_ ->
    return () ))))

main = print $ getSum $ execWriter ultimateAnswer

ところで、この章の最初に示したMonadLaw3_if.hsは、以下のように書いても同じ動きをすることが期待されます。

ifを消去

import Control.Monad.Writer

ultimateAnswer :: Writer (Sum Int) ()
ultimateAnswer = do
    x <- return $ 5 * 4
    tell x
    -- if True を消去
    y <- retrun $ 7 - 5
    tell y

    tell 20
    return ()

main = print $ getSum $ execWriter ultimateAnswer

これのdo構文は以下のように展開されます。

ifを消去後にdoを展開

import Control.Monad.Writer

ultimateAnswer :: Writer (Sum Int) ()
ultimateAnswer = 
    (return $ 5 * 4) >>= (\x ->
    tell x >>= (\_ ->

    (retrun $ 7 - 5) >>= (\y ->
    tell y >>= (\_ ->

    tell 20 >>= (\_ ->
    return () )))))

main = print $ getSum $ execWriter ultimateAnswer

さて、ここで 展開後にifを消去 したコードと、 ifを消去後にdoを展開 したコードを比較してみると、 (\y -> ... の括弧など、いくつかの括弧の閉じる位置が異なっていることがわかります。
if によってブロックができることによって、括弧の閉じる位置が変わってしまうのです。

この括弧の閉じる位置の差が 全体の結果に影響を与えない ことを要求しているのがモナド則(3)、つまり
(m >>= f) >>= g ≡ m >>= (\x -> f x >>= g)
という式になります。

この式は括弧がどこについていても問題ないことを示しています。

直感的にわかりづらい場合は、「モナド則の書き換え」の章で示した、(>=>)演算子で考えてみると、モナド則(3)が括弧がどこについていても問題ないことを示しているとわかりやすいと思います。

今回の例では if によってできるブロックについて説明しましたが、関数についても同じように、関数を頭の中でインライン化して考えてみるときにできる括弧の位置のズレを無視できることがモナド則(3)によって保障されます。

まとめると、モナド則(3)はブロックや関数を作って手続きを小分けにしても、直接、呼び出し元の位置に処理を書くのと同じように処理されるようにモナドを作ることを要求しています。

まとめ

長々と書きましたが、結論としてはモナド則は

1. returnした値が暗黙に書き換わらないこと
2. 自由に<-を使って代入していいこと
3. 手続きの一部をブロックにしたり関数にして小分けしても意味が変わらないこと

といった、ある意味では手続きを記述するうえで「当たり前のこと」を自作モナドに要求していることがわかりました。

あとがき

変な所とか、お手柔らかに突っ込んでね　(*´σｰ｀)ｴﾍﾍ