モナド則とプログラミング

まずはモナド則を引用します:

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

等号(≡)は置き換え可能であるという意味で読んでください。上から左単位元、右単位元、結合則と呼ばれます。

モナド則が満たされたモナドはプログラマにとって何が嬉しいのでしょうか。

端的に言ったらコードを分割/組み合わせ/抽象化等が出来るため、嬉しいのです。
もう少し言えば、モナド上では自然にプログラミング出来るから嬉しいのです。
もう少し言えば、モナド上でいつも通りエンジニアリング出来るから嬉しいのです。

モナド則のプログラミング上の意義とは、理解してしまうと本当に当たり前になってしまいます。
三日後には嬉しさのことなど忘れてその当たり前のメリットを享受することでしょう。
そうして誰もHaskellのモナド則について語らなくなってしまいました。知らんけど。

モナド則の意義とは、形は違えどプログラマならば本当に誰でも知っています。
つまりは関数による再利用性と同じ嬉しさです。

例えば任意の汎用プログラミング言語[^1]で構わないので、次のシチュエーションを考えます。
プログラミング中に同じことをしているコードを3回書いたとします。特にひねりもなく全く同じことを三回しているとします。
ここで、「じゃあ同じところを関数に括り出して、それぞれの箇所で呼び出すことにしよう」と考え、コードを書き換えます。

この関数定義によって得る嬉しさは再利用性とか保守容易性や抽象化（に伴う恩恵）などです。読者は、昨今のマシンパワーでは関数呼び出しのコストよりも関数定義による保守の容易さの方が多くの場面で重要であることは知っているとします。知らない方は経験が足りないと思われるためもっとプログラミングしてください。

[^1]: 実際には逐次実行処理とサブルーチンの抽象を持つ言語に限ります

さて前述の関数による再利用性の嬉しさに話を戻しますが、モナド上でプログラミングをする際には、暗黙にモナド則の保証を使いまくってます。具体的に見てみましょう。


## モナド上でのプログラミング

(とはいえ具体例を考えることが面倒なので)やる気の感じられない例を出します[^todo1]。
あるモナドインスタンス`M :: * -> *`を考えます[^kind]。型`A`, `B`,...`F`は全て具体的な型とします。

[^kind]: `M :: * -> *`は`M`が型(`*`)を一つとって型(`*`)となる型コンストラクタであることを意味しており、この「型の型のようなもの」をkindsと言いいます。Haskellの型システムを理解するためにはkindsを理解することが重要です。
[^todo1]: 気が向いたらもう少し実プログラムに近い例に置き換えます。

```haskell
f :: A -> M D
f a = do
  b <- special_action_1 a
  c <- special_action_2 b
  action_1 c

g :: A -> M E
g a = do
  b <- special_action_1 a
  c <- special_action_2 b
  action_2 c

h :: A -> M F
h a = do
  b <- special_action_1 a
  c <- special_action_2 b
  action_3 c
```

Haskellに慣れていないかもしれない読者のために一応`f`を解説します。
`f`では`special_action_1 a`の結果`b`を`special_action_2`が受け取り、その結果`c`を`action_1`が受け取っており、その結果が`f`自体の結果となります。
これが`IO`モナドならばアクションが書いた順に上から実行されますが、モナドインスタンスによっては逐次実行されるとは限りません。

さてやる気のない関数名はともかく、ここで押さえて欲しいポイントは`f`, `g`, `h`は同じ箇所が存在するということです。
`special_action_1`と`special_action_2`です。

そこで任意の正直なHaskellプログラマは「じゃあ関数で括り出すか」と思うわけです。それはHaskell以外の言語で、何度も行なっている同じ処理を関数に括り出すかの様なものです。その書き換え結果は以下。

```haskell
f' :: A -> M D
f' a = do
  c <- specials a
  action_1 c

g' :: A -> M E
g' a = do
  c <- specials a
  action_2 c

h' :: A -> M F
h' a = do
  c <- specials a
  action_2 c

specials :: A -> M C
specials x = do
  y <- special_action_1 x
  special_action_2 y
```

`f`, `g`, `h`をそれぞれ`f'`, `g'`, `h'`と名前を変更していますが、説明上の便宜的なものです。
ここでは`specials`という関数を定義し、それぞれの箇所をそれで置き換えたところです。ここまでのプログラム書き換えストーリーなら(Haskellという言語とはいえ)任意のひねくれ者ではないプログラマはなんとなく理解できると思います。

さてここからが本題です。この`specials`を用いた書き換え処理を行うには、実はモナド則による保証が必要です。
do式はシンタックスシュガーなので`>>=`で書き換え可能です。次のdo式は

```haskell
f a = do
  b <- special_action_1 a
  c <- special_action_2 b
  action_1 c
```

次の様に書き換えられます。

```haskell
f a =
  special_action_1 a >>= (\b ->
  special_action_2 b >>= (\c ->
  action_1 c))
```

改行は見やすさのためで他意はありません[^indent]。括弧の位置に注意してください。ここで`special_action_1`と`special_action_2`を別の関数にてまとめることを考えます。

[^indent]: ここのインデントには意味がありません。Haskellはインデントが意味をもつ場所(do, case, whereなど)と持たない場所があります。

```haskell
specials x = special_action_1 x >>= \y -> special_action_2 y
f' a = specials a >>= \b -> act3 b
```

これは`f`を左結合に書き直したことに相当します。

```
f' a = (special_action_1 a >>= \b -> special_action_2 b) >>= \c -> act3 c
```

ここでモナド則を思い出して欲しいのですが、
この書き換え(`f` -> `f'`)はモナド則の結合則そのままの例であり、つまりは同じ挙動であることが保証されています。


## モナド則とプログラミング

この書き換えで重要なことは、ここで仮定していることが「`M`はモナド則を満たしたモナドインスタンスである」ことだけということです。
つまり任意のモナドインスタンスにおいて、それがどんな具体的なモナドであるかを考慮することなく、僕らはこの書き換えを行うことが出来ます。実際任意のHaskellerは計算がモナド則を満たすことが分かった時点で、そのモナドの具体的な構成を知ることなく（例えばStateモナドが実質`s -> (s, a)`とかいう関数だとかその時の`(>>=)`の実装がどんなものかとか、扱っているモナドがモナド変換子が5つくらい咬んでいる複雑なモナドであるだとか、Effectモナドの具体的な構成がどうなっているとかいうことを忘れたとしても）そのモナドインスタンス上での計算をこなすことができます。

ここでようやくモナド則がプログラミングに与える影響が明らかになりました。
僕らはモナド上でなら関数の書き換えをいつも通り（他の言語で行なっている様に）自然に行うことが出来ることが保証されているのです。

この性質は非常に重要で基礎的であるため、モナドインスタンスとなっているけどモナド則を満たさないものは役に立ちません。なのでそう言ったものはコミュニティの中で議論され、除外されているかWARNINGが表示されています。例えば`ListT`[^listt]や`STT`[^stt]があります[^transformerlaw]。

[^listt]: http://hackage.haskell.org/package/transformers-0.5.5.0/docs/Control-Monad-Trans-List.html
[^stt]: http://hackage.haskell.org/package/STMonadTrans-0.4.3/docs/Control-Monad-ST-Trans.html
[^transformerlaw]: `listT`, `STT`はモナド変換子ですが、これはmonad transformer lawと呼ぶべき則があり、それを満たしていれば、任意のモナド`m`に対してモナド変換子`t`を適用した結果`t m`はモナド則を満たします。


モナド則の残り二つ、左単位元と右単位元は外部の値をそのモナド上に導入するための`return`の性質ですが、これらは`return`がプログラムに影響を与えないことの性質です。ここでは結合則がメイントピックであるためこの程度の記述にしておきます。


## 他の言語でのモナドインスタンス

このモナド則は非常に重要で基礎的であると書きましたが、自明ではありません。
例えばjavascriptの`Promise`を考えます。あれはモナドインスタンスです[^promise]。

[^promise]: コメントにて指摘があるように、javascriptのPromiseはネストしたPromiseは扱えない様なので正確にはモナドではないかもしれません。

次の`then`で単にチェーンしたPromiseと、`then`をネストさせていくPromiseを考えます。

```js
Promise.resolve(3)
  .then( (n) => {
    console.log(n);
    return Promise.resolve(4);
  })
  .then( (n) => {
    console.log(n);
    return Promise.resolve(5);
  })
  .then( (m) => {
    console.log(m);
    return Promise.resolve(6);
  });
```

```js
Promise.resolve(3)
  .then( (n) => {
    console.log(n);
    return Promise.resolve(4)
      .then( (n) => {
        console.log(n);
        return Promise.resolve(5)
          .then( (m) => {
            console.log(m);
            return Promise.resolve(6);
          });
      })
```

いちいち`return Promise.resolve(n)`と冗長に書いているのはMonadの`(>>=)`の型に合わせているだけです。
これらが同じ様に動くことは、ブラウザ開発者がモナド則を満たす様にPromiseを実装したからでしょうが、この二つの構造が同じ様に動くことは自明には見えません。ただ、`then`という名前が「きっと同じ様に動いてくれるだろう」、という直感は与えてくれます。
Haskellerがこれを見ると、「Promiseがモナドインスタンスであるためにはこれらは同様に動くべきである」などと考えます。そうして色々試したり調べたりしてちゃんとモナド則を満たしたことを確認した後、その実装を忘れて単純にモナドインスタンスとして扱います。モナドインスタンスであることが確認出来たということは、その上で自由にエンジニアリング出来ることの保証を得られたということだからです。

最近の言語は非同期モナドを一つくらい持っていることが多く、Scalaには`Future`, Rustにも`Future`が存在します。僕は仕事でScalaを使っていますが、非同期モナドがあるとその言語で非同期プログラミングがまともに出来る、という感触があり非常に助かっています。javascriptはあまり書きませんが、Promiseが入ったことで非常に書きやすくなったと認識しています。


## まとめ

非常に大雑把な例を用いて説明しましたが、モナド則が実際のプログラミングでどの様に関わっているのか、という話はあまり世間に出回っていないかもしれなかったので書きました。Haskellerは全員分かった上で基礎的すぎるからそこを説明するということを思いつかないだけです多分。

そしてこのエントリ書いてて思いましたが、もしかしたらこれはモナドを学習する上で納得するために必要なことかもしれません[^notcomprehension]。そういえばモナドの記事に当たって「モナド則というものの存在は分かった、だから一体何？？？」と考える時期が確か僕にもありました。
このエントリは元々モナドの嬉しさという題のはずでしたがちょっとずれている（と指摘された）のでモナド則の話としています。

他ここが分からない等ありましたらコメントなどにどうぞ。わかる範囲で答えます。

[^notcomprehension]: 納得は全てに優先するぜッ、と鉄球を回す人も言っています