モナドとは何か－私の見方

（プログラミング言語の）モナドについてはいろんな人がいろいろなことを言っていて、チュートリアルも沢山ある。ただ、どうも自分が見聞きした範囲では、そういったものは両極端にわかれているように思う。一つは正確だが難解なもの。去年秋の函数型言語プログラミングの集いでのtanakhさんの講演は多分これで、あまりに難解で笑ってしまった。（悪いという意味じゃないくて、分かっている人には含蓄のある講演だったと思う。）一方で、分かりやすい説明もあって、モナドは「計算」を表すものだ、というアナロジーが使われたりする。これはプログラマにはとっつきやすい説明だけど、よく考えると何を言っているか分からない。「計算」ってなんだ？というわけで（周回遅れかもしれないけど）私なりの理解を書く意味もあるかなと思う。ちなみに分かっている人のために書いておくと、Kleisli圏を使った説明になる。


さて、何か圏$\mathcal C$を考えよう。適当なプログラミング言語の型と関数の成す圏を考えれば良い。すると、関数$f : A \rightarrow B$が$A$から$B$への射となる。ただ、実際プログラミングしていると、この関数の戻り値を拡張したくなることがままある。例えば、関数$f$を$B$の値を返すだけではなくて、エラーも返すように書き換えたくなることがある。つまり $f : A \rightarrow B + E$ ($E$はエラーの型で+は直和）を$A$ から$B$ への射と見たい。もっと一般的に、何か型構築子$M$ について、$f: A \rightarrow M B$を$A$から$B$への射と見たい。

というわけで、オブジェクトが型$A, B,\ldots$でオブジェクト$A, B$間の射が元の圏$\mathcal C$の$A, MB$間の射であるような圏$\mathcal C^M$を新たに考える。これが圏になるためには、恒等射$\eta_A : A \rightarrow MA$と射の合成$\circ^M$があって、任意の$f : A \rightarrow MB, g : B \rightarrow MC, h : C \rightarrow MD$について、次が成り立たなければならない。

1. $\eta_A \circ^M f = f \circ^M \eta_B = f$
2. $(f \circ^M g) \circ^M h = f \circ^M (g \circ^M h)$

さて、$M$がモナドである時、上記のような$\eta$と$\circ^M$を導こう。$\eta$は通常のモナドのreturnそのものである。$ｆ \circ^M g$は>>=から$f \circ (\lambda x. x >>= g)$ (ここで$\circ$は元の圏の合成）と定義できる。モナド則の左恒等則は

return a >>= f　≡ f a

だった。よって左辺を変形して

$$ \eta_A a >>= f = fa $$

よって更に左辺を変形して

$$ (\lambda x. x >>= f) (\eta_A a) = fa$$

よって

$$ \eta_A \circ  (\lambda x. x >>= f) = f$$

よって

$$ \eta_A \circ^M f = f$$.   よって上の1の最初の等式が導かれた。次に右恒等則を考える。

m >>= return　≡ m

これを使って次のような式変形を行う。

$$\begin{align*} f \circ^M \eta_B &= f \circ (\lambda x. x >>= \eta_B) \\ &= f \circ (\lambda x. x >>= \text{return}) \\ &= f \circ (\lambda x. x) \\ &= f \end{align*}$$

よって$\eta$の恒等則が言えた。次に$\circ^M$の結合則だが

$$\begin{align*} f \circ^M (g \circ^M h) (a) &= f \circ (\lambda x. x >>= (g \circ^M h)) (a) \\ &= f(a) >>= (g \circ^M h) \\ &= f(a) >>= (g \circ (\lambda x. x >>= h)) \\ &= f(a) >>= \lambda y. g(y) >>= h \\ &= (f(a) >>= g) >>= h \\ &= (f \circ^M g) \circ^M h (a)  \end{align*}$$

となって結合則が導かれた。よって$\mathcal C^M$が圏をなすことが分かった。(実はいろいろごまかしているけど)

まとめると

1. モナドというのは型AからMBへの関数を型AからBへの「関数」と思う仕掛けである
2. 正確にいうと、型をオブジェクト、型AからMBへの関数をオブジェクトAからBへの射とする圏$\mathcal C^M$がモナドMから構成できる
3. モナド則から、$\mathcal C^M$の恒等則、結合則が導ける

となる。