モナド

圏論勉強会 @ ワークスアプリケーションズのモナドの説明をもとにまとめた

モナドの定義

圏$C$におけるモナドとは、

• 自己関手 $T:C\to C$
• 自然変換 $\eta :1_C\to T$
• 自然変換 $\mu :T^2\to T$ からなり、等式
• $\mu \circ {\mu }_T=\mu \circ T(\mu )$
• $\mu \circ {\eta }_T=\mu \circ T(\eta )=1_T$ が成り立つものである。

$\eta$をモナドの単位元、$\mu$をモナドの積などと呼ぶ。

理論計算機科学でのモナド

$C$を型と関数の圏とした場合、計算作用を自己関手$T:C\to C$によって表現する。 この計算作用の表示が$T$であり、計算の表示が射$f:A\to T(B)$ということになる。(クライスリ圏とクライスリ射)

計算作用

モナドで扱うような計算作用

• 値を返さない場合がある(partiality)
  • $T(B)=T+1$
• 複数の計算結果がある(nondeterminism)
  • $T(B)=P_{fin}(B)$
• 副作用がある(side-effects)
  • $T(B)=(S\times B{)}^S$
• エラーが発生する(exception)
  • $T(B)=B+E$
• 継続(計算機科学)を返す(continuations)
  • $T(B)=R^{R^B}$

元記事へのリンク

計算$f:A\to T(B)$と$g:B\to T(C)$を単純に合成すると、計算作用が2回発生するため、出力が$T^2(C)$という型になってしまう。例えば、$T$が副作用を表しているならば、$T^2$は「副作用が2度発生する」という計算作用を表す。

graph LR
  A --f--> 2["T(B)"] --g--> 3["T²(C)"]

しかし、「副作用のある計算」をいくつ合成しても、単に「副作用のある計算」と認識することが多い。そこで、自然変換$\mu :T^2\to T$をつかって畳み込みをすることで、複数の副作用をまとめることにする。この計算作用の畳み込みは結合的である。

graph LR
  A --f--> 2["T(B)"] --g--> 3["T²(C)"] --μ--> 4["T(C)"]

また、「何もしない」という計算を表現する必要がある。これは自然変換$\eta :1_C\to T$で表すことにする。この「何もしない」計算は単位的である。

do構文とモナド

圏論がわからない場合は、モナドは単にdo構文だとおもって捉えるのが良さそう。

モナドの資料

• プログラマのためのモナド(圏論) - Speaker Deck
• 「圏論とプログラミング」発表スライドメモ - Qiita
  • Lensについても載ってた