モナド - wpptのブログ

を少々勉強、Haskellとやらは知らぬ。
他にやりたい・やるべきことがあるのに…全くもって現実逃避。
以下、対象、射、関手、自然変換とはいわずに、型、プログラム、型コンストラクタ、多相型関数としてる。

■問題点

型 $A$ 、 $B$ 、 $C$ に関するプログラム $f:\, A\rightarrow B$ と $g:\, B\rightarrow C$ があるとき、プログラムの合成 $g\circ f: A\rightarrow C$ は型 $A$ のデータ $a$ に対して $g\circ f(a)=g(f(a))$ とすれば良い。

ここで $f, g$ にリスト化や外部出力などの何らかの付随計算をさせる場合ことを考える。
そのような計算を付加した時の出力型を $M\langle B\rangle$ 、 $M\langle C\rangle$ とし、出力を拡張したプログラムを $f':\, A\rightarrow M\langle B\rangle$ 、 $g':\, B\rightarrow M\langle C\rangle$ とすると、 $f'$ の出力と $g'$ の入力の型が異なるので、 $g\circ f$ に対応する拡張プログラム $(g\circ f)'$ は $f'$ と $g'$ の単純な合成では表せない。

■解決策

$M$ を型 $X$ に対して型 $M\langle X\rangle$ を生成する型コンストラクタとし、プログラム $f:\, X\rightarrow Y$ が与えられると、 $f$ を元に具体的なプログラム $M\langle f\rangle:\, M\langle X\rangle\rightarrow M\langle Y\rangle$ が生成されるものとする。
そしてこの型コンストラクタ $M$ に対して、2つの多相型関数を用意する。

$\eta_{\tiny X}:\, X\rightarrow M\langle X\rangle$

$\mu_{\tiny X}:\, M\langle M\langle X\rangle\rangle\rightarrow M\langle X\rangle$

次の計算で混乱しないように、幾つかの具体的な $X$ に対して、プログラムの型を明確にしておく。

$\eta_{\tiny M\langle X\rangle}:\, M\langle X\rangle\rightarrow M\langle M\langle X\rangle\rangle$

$M\langle \eta_{\tiny X}\rangle:\, M\langle X\rangle\rightarrow M\langle M\langle X\rangle\rangle$

$\mu_{\tiny M\langle X\rangle}:\, M\langle M\langle M\langle X\rangle\rangle\rangle\rightarrow M\langle M\langle X\rangle\rangle$

$M\langle \mu_{\tiny X}\rangle:\, M\langle M\langle M\langle X\rangle\rangle\rangle\rightarrow M\langle M\langle X\rangle\rangle$

そしてこの2関数が次の性質をもつとき、三つ組 $(X, \eta_{\tiny X}, \mu_{\tiny X})$ をモナドと呼ぶ。

型 $M\langle M\langle M\langle X \rangle\rangle\rangle$ のデータ $x$ に対して、 $\mu_{\tiny X}\big(M\langle\mu_{\tiny X}\rangle (x)\big) = \mu_{\tiny X}\big(\mu_{\tiny M\langle X\rangle} (x)\big)$

型 $M\langle X \rangle$ のデータ $x$ に対して、 $\mu_{\tiny X}\big(\eta_{\tiny M\langle X\rangle} (x)\big) = \mu_{\tiny X}\big(M\langle \eta_{\tiny X}\rangle (x)\big) = x$

プログラム $h: X\rightarrow Y$ と、型 $X$ のデータ $x$ に対して、 $\eta_{\tiny Y}\big( h(x)\big) = M\langle h\rangle\big( \eta_{\tiny X} (x)\big)$

プログラム $h: X\rightarrow Y$ と、型 $M\langle M\langle X\rangle\rangle$ のデータ $x$ に対して、 $\mu_{\tiny Y}\big( M\langle M\langle h\rangle\rangle(x)\big) = M\langle h\rangle\big( \mu_{\tiny X} (x)\big)$

ここで、2つのプログラムを定義する。

$(>>=):\, M\langle X\rangle\rightarrow (X\rightarrow M\langle Y\rangle)\rightarrow M\langle Y\rangle$ を、 $(>>=)(x, h):=\mu_{\tiny Y}\big(M\langle h\rangle (x)\big)$ で定める