モナドの架け橋：プログラミング言語と圏論の繋がりを俯瞰図で解説

プログラミング言語における『モナド』という概念は、特に関数型プログラミングを学ぶ人々にとってとりわけ興味深いテーマだと思います。

このプログラミング言語における『モナド』ですが、よく知られているように圏論という数学の一分野と深いつながりを持っています。

当記事では、これらプログラミング言語のモナドと圏論の諸概念について、次の俯瞰図を用いてそれぞれの橋渡しを試みます。
私と一緒にモナドの解像度を高めていきましょう！

私は以前もこのようなテーマの記事を書いたことがあります。
今回のように広めのつながりを扱ってはいませんが、個々の説明はこちらの方が詳しいかもしれません。

• 圏論のモナドとPureScriptのモナドの関係性を知ろう
• クライスリ圏とプログラムの関係

前置き

少し前置きをさせてください。

前提知識について

プログラミング言語の知識について

プログラミング言語のモナドに定義されているpureや>>=などの関数は知っている前提で進めます。

圏論の知識について

『圏』は知っている前提で進めます。
『関手』『自然変換』などについては、今回の図に登場するので説明します。
これらについて私の記事でよければ冒頭に載せたここにも説明がありますので、よかったら必要に応じて参照してみてください。

具体的なコードについて

具体的なコードはPureScriptで書きますが、PureScriptが書けなくても知らなくても内容は理解できます。
なぜならこの記事で登場するコードはほぼすべてシンプルなものだからです。

PureScriptを知らない方向けに関数定義の構文を書いておきます。
これだけ覚えておいていただければあとはノリで理解できるので大丈夫です。

関数定義

-- 【意味】
-- 関数名 :: 引数1 -> 引数2 -> 戻り値
function :: String -> String -> Int
function = 関数の実装

関数のシグニチャの定義は::の左側が関数名です。
右側が->で区切られた引数と戻り値の型になっており、区切られた最後の型が戻り値の型です。

プログラミング言語と圏論を繋ぐ俯瞰図

俯瞰図の説明をします。
図の左側がプログラミング言語の世界、右側が圏論の世界で、同じ世界の中で関係しているものは実線、世界をまたいで関係しているものは破線で結ばれています。

大きな図ですが、次の順番で少しずつ説明していきます。

1. 型構築子やmap関数と自己関手の対応
   まずは、型構築子やmap関数と自己関手の関係を説明します。
   これは割とモナドの前提となるような話です。
   

2. 次にプログラミング言語のモナドと、圏論のモナドの対応を説明します。
   

3. 最後にプログラミング言語のモナドに定義されるjoin関数と>>=関数のつながりには理論的な背景があるということを圏論の世界を通して説明します。
   

型構築子/mapと自己関手の対応

まずは図のこの部分のお話をします。

型構築子

型構築子とは、新たな「型」を作り出すための関数のようなもの※です。
※Haskell/PureScriptにおける一般的な関数ではないが、型を別の型に写すという振る舞いは関数に近い
具体例としてMaybeを挙げてみます。
Maybeは次のように定義されています。

data Maybe a = Nothing | Just a

Maybeは型引数aをとり具体的な型を生成します。
Maybe StringとかMaybe Intとかですね。

map

map関数は、PureScriptやHaskellでは型クラスFunctorに定義されている関数です。
（Haskellではfmapという名前になっています）

class Functor f where
  map :: forall a b. (a -> b) -> f a -> f b

他の言語でも色々な型に定義されていますね。
この関数が何をするかの説明は不要でしょう。

関手

圏${\footnotesize \mathbf{C}}$から圏${\footnotesize \mathbf{D}}$への関手${\footnotesize \mathrm{F}}$とは、

• 対象関数: ${\footnotesize \mathbf{C}}$の各対象${\footnotesize X}$を ${\footnotesize \mathbf{D}}$の各対象${\footnotesize \mathrm{F}(X)}$に対応させる
• 射関数: ${\footnotesize \mathbf{C}}$における射${\footnotesize f:X\rightarrow Y}$を ${\footnotesize \mathbf{D}}$における射${\footnotesize \mathrm{F}(f):\mathrm{F}(X)\rightarrow \mathrm{F}(Y)}$に対応させる

からなるものであり以下の性質を満たす。

• 恒等射を保存する: 各対象${\footnotesize X\in \mathbf{C}}$に対して${\footnotesize \mathrm{F}(\mathrm{id}_X) = \mathrm{id}_{\mathrm{F}(X)}}$
• 射の合成を保存する: 任意の射${\footnotesize f:X\rightarrow Y}$および${\footnotesize g:Y\rightarrow Z}$に対して${\footnotesize \mathrm{F}(g\circ f) = \mathrm{F}(g)\circ \mathrm{F}(f)}$

---

視覚化するとこのようなイメージでしょうか。

対象関数と射関数のイメージ

恒等射/合成射を保存するイメージ
(Wikipediaに書かれていた定義がカジュアルで良さそうだったので拝借させてもらいました(ちょっと改変してますが))

自己関手

同じ圏${\footnotesize \mathbf{C}}$から圏${\footnotesize \mathbf{C}}$への関手${\footnotesize \mathrm{F}}$を自己関手${\footnotesize \mathrm{F}}$という。

自己関手のイメージ

関手がわかっていればこれは簡単ですね。

対応

ここで、プログラミング言語側の『型構築子』『map』の関係性と圏論側の『自己関手』『対象関数』『射関数』の関係性を並べてみてみましょう。
プログラミング言語側の方は具体的な型を当てはめてみました。

両者に対応関係があることがわかると思います。

最初お見せした図の意味がおわかりいただけたでしょうか。

ちなみに、関手の『恒等射/合成射を保存する』という条件は、プログラミング言語においてはFunctor則と呼ばれるものに対応しています。

次はPureScriptで表現したFunctor則です。

• map identity a == identity a
• map (f <<< g) a == (map f <<< map g) a

関手の条件と比べてみるとこれらが対応関係にあるのがわかると思います。

• ${\footnotesize \mathrm{F}(\mathrm{id}_X) = \mathrm{id}_{\mathrm{F}(X)}}$
• ${\footnotesize \mathrm{F}(g\circ f) = \mathrm{F}(g)\circ \mathrm{F}(f)}$

プログラミング言語のモナドと圏論のモナドの関係

まず図のこの部分を見てください。

圏論のモナド側から見ると、
自然変換 ${\footnotesize \eta}$とpureが対応しており、
自然変換 ${\footnotesize \mu}$とjoinが対応しています。
（アルファベットは異なりますが、形が一致していることがわかるはずです）

プログラミング言語のモナドに馴染みがある方は「おや？」と思われなかったでしょうか？
「>>=はどこにいったんだ？」
と。

そう、プログラミング言語側のモナドでpureの他に一般的に定義される関数は>>=なのですが、>>=と圏論のモナドは直接の対応がありません。
対応しているのはjoinです。

更に圏論のモナドの定義には「可換図式」という条件があり、その条件に対応するのがプログラミング言語側のモナドにおける「pureとjoinによるモナド則」なのです。

pureとjoinによるモナド則

みなさんがよく見かけるモナド則は次のような形をしていると思いますが、このモナド則は>>=ではなくjoinを使って書くこともできます。

1. 左単位律: pure a >>= f == f a
2. 右単位律: m >>= pure == m
3. 結合律:　 (m >>= g) >>= h == m >>= (\x -> g x >>= h)

joinを使って書くとこうなります。
(単位律のmはモナドの値、結合律のmはネストされたモナドの値です)

1. 左単位律: join (map pure m) == m
2. 右単位律: join (pure m) == m
3. 結合律:　 join (join m) == join (map join m)

このあたりの対応を詳しくみていきたいのですが、それにはまず圏論のモナドの定義を知る必要があります。

モナド

圏${\footnotesize \mathbf{X}}$におけるモナド${\footnotesize \langle \mathrm{T},\eta,\mu\rangle}$ は自己関手${\footnotesize \mathrm{T}:\mathbf{X}\rightarrow \mathbf{X}}$ と二つの自然変換

$${\footnotesize \eta:\mathrm{id}_{\mathbf{X}}\Rightarrow \mathrm{T}, \mu:\mathrm{T}^{2}\Rightarrow \mathrm{T}}$$

からなり、次の図式を可換にするものである。

---

自然変換とか可換について一応補足しておきます。

補足:自然変換

${\footnotesize \mathbf{C} ,\mathbf{D}}$ を圏とし、${\footnotesize \mathrm{F}:\mathbf{C}\rightarrow \mathbf{D} ,\ \mathrm{G}:\mathbf{C}\rightarrow \mathbf{D}}$を関手としたとき
自然変換 ${\footnotesize \alpha :\mathrm{F}\Rightarrow \mathrm{G}}$ とは、${\footnotesize \mathbf{D}}$ の射の族 ${\footnotesize \{ \alpha_{X}:\mathrm{F}( X)\rightarrow \mathrm{G}(X)\}_{X\in \mathbf{C}} }$ である。

また ${\footnotesize \alpha_{X}}$ や ${\footnotesize \alpha_{Y}}$ を自然変換${\footnotesize \alpha}$の成分と呼ぶ。

ざっくりいうと、自然変換とは、関手から関手への射みたいなものですね。
視覚化したものが以下です。

自然変換のイメージ

補足:可換

図式が可換であるとは、異なる経路を辿っても結果が同じになることをいいます。
可換である図式を可換図式といいます。

モナドの図式は可換なのですが、これは次が成り立つことを意味しています。

• 左の図式: ${\footnotesize \mu\circ \mathrm{T}\mu = \footnotesize \mu\circ \mu\mathrm{T}}$
• 右の図式: ${\footnotesize \mu\circ \mathrm{T}\eta = \footnotesize \mu\circ \eta\mathrm{T}}$
  

対応

関数と自然変換の対応

プログラミング言語側のモナドの関数と圏論側のモナドの自然変換の対応を見てみましょう。

そのために自然変換${\footnotesize \eta}$と${\footnotesize \mu}$の${\footnotesize A}$成分を書いてみます。

• ${\footnotesize \eta_{A}:A\rightarrow \mathrm{T}(A)}$
• ${\footnotesize \mu_{A}:\mathrm{T}(\mathrm{T}(A)) \rightarrow \mathrm{T}(A)}$

これを用いて比較したものが次になります。

プログラミング言語側	圏論側
pure :: a -> m a	${\footnotesize \eta_{A}:A\rightarrow \mathrm{T}(A)}$
join :: m (m a) -> m a	${\footnotesize \mu_{A}:\mathrm{T}(\mathrm{T}(A)) \rightarrow \mathrm{T}(A)}$

どうでしょうか。形が一致していますね。
これで図の赤枠のところがわかりました。

モナド則と可換図式の対応

あらためて可換図式を見てみましょう。

まず可換図式に出てくる${\footnotesize \mathrm{T}_{\eta}}$や${\footnotesize \eta \mathrm{T}}$といった自然変換の${\footnotesize A}$成分と、それをプログラミング言語で表したものを表にしてみます。

自然変換	${\footnotesize A}$成分	意味	プログラミング言語で表したもの
${\footnotesize \mathrm{T}_{\eta}}$	${\footnotesize \mathrm{T}(\eta_A):\mathrm{T}(A)\rightarrow \mathrm{T}(\mathrm{T}(A))}$	${\footnotesize \eta_A}$を${\footnotesize \mathrm{T}}$で写す	map pure m
${\footnotesize \eta \mathrm{T}}$	${\footnotesize \eta_{\mathrm{T}(A)}:\mathrm{T}(A)\rightarrow \mathrm{T}(\mathrm{T}(A))}$	${\footnotesize \mathrm{T}(A)}$を${\footnotesize \eta}$で写す	pure m
${\footnotesize \mathrm{T}_{\mu}}$	${\footnotesize \mathrm{T}(\mu_A):\mathrm{T}(\mathrm{T}(\mathrm{T}(A)))\rightarrow \mathrm{T}(\mathrm{T}(A))}$	${\footnotesize \mu_A}$を${\footnotesize \mathrm{T}}$で写す	map join m
${\footnotesize \mu \mathrm{T}}$	${\footnotesize \mu_{\mathrm{T}(A)}:\mathrm{T}(\mathrm{T}(\mathrm{T}(A)))\rightarrow \mathrm{T}(\mathrm{T}(A))}$	${\footnotesize \mathrm{T}(A)}$を${\footnotesize \mu}$で写す	join m

上記の表をベースに、図式の経路と、その経路をプログラミング言語で表したものの表を作ってみます。

経路	プログラミング言語で表したもの
${\footnotesize \mu_A \circ \mathrm{T}(\eta_A)}$	join (map pure m)
${\footnotesize \mu_A \circ \eta_{\mathrm{T}(A)}}$	join (pure m)
${\footnotesize \mu_A \circ \mathrm{T}(\mu_A)}$	join (map join m)
${\footnotesize \mu_A \circ \mu_{\mathrm{T}(A)}}$	join (join m)

図式が可換であるとは、異なる経路を辿っても結果が同じになることでしたので、条件の形にしてみましょう。

図式の条件	プログラミング言語で表したもの
${\footnotesize \mu_A \circ \mathrm{T}(\eta_A) = \mu_A \circ \eta_{\mathrm{T}(A)}}$	join (map pure m) == join (pure m)
${\footnotesize \mu_A \circ \mathrm{T}(\mu_A) = \mu_A \circ \mu_{\mathrm{T}(A)}}$	join (map join m) == join (join m)

すると、これはモナド則と一致します。

1. 左単位律: join (map pure m) == m
2. 右単位律: join (pure m) == m
3. 結合律:　 join (join m) == join (map join m)

可換図式とモナド則の対応がわかりました。

これで次の図の意味がおわかりいただけたかと思います。

クライスリ圏を通してつながるjoinと>>=

最後はこの図のこの部分の説明をします。

クライスリ圏とクライスリトリプル

クライスリ圏とは、クライスリトリプルと呼ばれる3つ組${\footnotesize \langle \mathrm{T},\mu,-^{*}\rangle}$をもとに構成される圏です。

上記の3つ組を見ると、ほとんどモナドと共通の要素をもっていることがわかるかと思います。
違いといえば

• モナドには自然変換${\footnotesize \mu}$があるがクライスリトリプルにはない。
• クライスリトリプルには拡張演算子${\footnotesize -^{*}}$ があるがモナドにはない。

ということです。
そして、${\footnotesize \mu}$と拡張演算子には、「どちらか一方を使ってもう一方を定義することができる」という関係があります。
${\footnotesize \mu}$を使って拡張演算子を定義でき、逆に拡張演算子を使って${\footnotesize \mu}$を定義できるということです。

つまりモナドからクライスリトリプルを構成することができ、クライスリトリプルからモナドを構成することができるわけです。

どういうことか見ていきましょう。

拡張演算子

まずはこの意味を理解しましょう。
拡張演算子は、いってみれば射をもとに別の射をつくる射（関数から別の関数を作る関数みたいなやつ）です。

クライスリ圏の射は${\footnotesize f:A\rightarrow \mathrm{T}(B)}$という形をしているのですが、拡張演算子にこの射を適用した${\footnotesize f^{*}}$は
${\footnotesize f^{*}:\mathrm{T}(A)\rightarrow \mathrm{T}(B)}$
という射になります。

図にするまでもないかもしれませんが、こんなイメージです。

拡張演算子と=<<の対応

このような拡張演算子を、プログラミング言語で表すとしたらa -> t bという関数をt a -> t bという関数に変換する関数になるので、このようになるのではないでしょうか。

拡張演算子 :: (a -> t b) -> (t a -> t b)

というかこれは=<<そのものです。
PureScriptでは次のように定義されています。

bindFlipped :: forall m a b. Bind m => (a -> m b) -> m a -> m b
bindFlipped = flip bind

infixr 1 bindFlipped as =<<

=<<は>>=の引数の順序を入れ替えたものなので、実質同じ関数だと考えてよいでしょう。

ここまでで、図の次の部分のつながりがわかりました。

---

続いて赤枠の部分を見ていきます。

拡張演算子を使ってμを定義する

まず ${\footnotesize \mathrm{id}_{\mathrm{T}(A)}:\mathrm{T}(A)\rightarrow \mathrm{T}(A)}$ という${\footnotesize \mathrm{T}(A)}$の恒等射を考えます。

拡張演算子にこの恒等射を適用した${\footnotesize \mathrm{id}_{\mathrm{T}(A)}^{*}}$がどうなるかというと

$${\footnotesize \mathrm{id}_{\mathrm{T}(A)}^{*}:\mathrm{T}(\mathrm{T}(A))\rightarrow \mathrm{T}(A)}$$

となります。

どこかで見た形をしていますね？
そう、${\footnotesize \mu}$です。
${\footnotesize \mathrm{id}_{\mathrm{T}(A)}^{*} = \footnotesize \mu}$と定めれば、拡張演算子を使って${\footnotesize \mu}$が定義できるのです。

μを使って拡張演算子を定義する

射${\footnotesize f:A\rightarrow \mathrm{T}(B)}$があるとします。
この${\footnotesize f}$をもとに${\footnotesize \mu_{B} \circ \mathrm{T}(f)}$を生成する操作が拡張演算子になります。

これは図にしてみると意味がわかると思います。

---

ここまでで

拡張演算子を使ってμを定義することと、=<<を使ってjoinを定義することの対応

拡張演算子を使って${\footnotesize \mu}$を定義するには、${\footnotesize \mathrm{T}(A)}$の恒等射を拡張演算子に適用させればよいのでした。
そして拡張演算子はプログラミング言語のモナドにおいては=<<なのでした。
恒等射がプログラミング言語のモナドにおいてidentityだとすると、identityを=<<に適用すればよさそうです。

実際、PureScriptのjoinは次のように定義されています。=<<ではなく引数の順序を入れ替えた>>=を使っていますが、もうそのまんまといってもいいでしょう。

join m = m >>= identity

μを使って拡張演算子を定義することと、joinを使って>>=を定義することの対応

${\footnotesize f}$をもとに${\footnotesize \mu_{B} \circ \mathrm{T}(f)}$を生成する操作をプログラミング言語で考えてみましょう。
まずこの場合の${\footnotesize \mathrm{T}}$は射関数になるので対応するのはmapです。
${\footnotesize \mu}$はjoinに対応していますね。
ということは、mapしてjoinすればよさそうです。

実際このように実装することができます。

bind m f = join (f <$> m) -- <$>はmapの中置演算子

infixl 1 bind as >>=

まとめ

>>=とjoinがお互いを使って定義可能であるということは、モナドとクライスリトリプルはお互いに構成可能という理論的背景でもってつながっていました。
このような背景をコードレベルでも確認できるのが面白いところです。

ということで図の次の部分の説明が終わりました。

クライスリ射の合成と>=>の対応

ここまでで正直私が書きたかったことはもう書けてしまっているのですが、クライスリ射の合成についても触れておきます。
図のこの部分です。

クライスリ射の合成

クライスリ圏の射とは${\footnotesize f:A\rightarrow \mathrm T (B)}$のような射でした。
ここで

$${\footnotesize f:A\rightarrow \mathrm T (B), g:B\rightarrow \mathrm T (C)}$$

という二つの射があるとして、これらの合成射は拡張演算子を用いて

$${\footnotesize g^{*}\circ f:A \rightarrow \mathrm T (C)}$$

と定義されます。

${\footnotesize f}$と${\footnotesize g}$はそのままでは合成できませんが、拡張演算子によって${\footnotesize g^{*}}$とすることで${\footnotesize B}$が${\footnotesize \mathrm T (B)}$になり合成できるようになります。

>=>との対応

拡張演算子はプログラミング言語のモナドにおいては=<<で引数の順序を入れ替えれば>>=なので、
クライスリ射に対応するa -> m bという関数と>>=を組み合わせれば、${\footnotesize g^{*}\circ f:A \rightarrow \mathrm T (C)}$を表現できそうです。

実際PureScriptでは>=>は次のように定義されています。これもそのまんま一緒ですね。

composeKleisli :: forall a b c m. Bind m => (a -> m b) -> (b -> m c) -> a -> m c
composeKleisli f g a = f a >>= g

infixr 1 composeKleisli as >=>

おわりに

以上で冒頭にお見せした馬鹿でかい図のすべての説明が終わりました。
あらためて俯瞰してみていかがでしょうか。
自分は全体像を最初に見たいタイプなので、こういうものはまさに自分がほしかったものなのですが、みなさんはいかがでしたでしょうか。

あとがき (なぜ書いたか)

私は最初『圏論のモナドとPureScriptのモナドの関係性を知ろう』という記事を書いたとき、クライスリ圏のことはよく知らなかったんです。
それゆえ、そのときは${\footnotesize \mu}$joinの対応については書いたものの、joinと>>=のつながりについての説明が、「一方を使ってもう一方を実装することができます」程度のものになってしまっていました。
一方で『クライスリ圏とプログラムの関係』という記事では、圏論側と>>=の対応については言及したものの、記事のテーマ的にjoinとのつながりには言及しませんでした。

ということで「こんな感じにつながっているのか」という図はずっと頭の中にあったのですが、「書かなくてもええか」とアウトプットはしてきませんでした。
が、喉に何かが詰まった感じではあったため、「やっぱ書くか」と11月くらいからちょとずつ書いてきて年末にようやく書き終わりました。

一日のうち自由に使える時間が非常に少ないため、終わるまでやけに時間が掛かってしまいました。
あー、自由時間がほしい。