この記事はOPTIMIND x Acompany Advent Calendar 2021の22日目の記事となります。
こんにちは。株式会社オプティマインドの伊豆原(イズハラ)と申します。
モナドといえば単なる自己函手の成す圏のモノイド対象だよ。ということで何の問題も無ければ良かったのですが、いっちょHaskellのモナドをかじってみようとHaskellWikiのMonadのページを見ますと以下のような記述が確認できます。
class Monad m where
(>>=) :: m a -> ( a -> m b) -> m b
(>>) :: m a -> m b -> m b
return :: a -> m a
- モナド則
return a >>= k = k a
m >>= return = m
m >>= (\x -> k x >>= h) = (m >>= k) >>= h
これの何が「自己函手の成す圏のモノイド対象」なのか？という話はとても非自明に思いますので、その簡単な橋渡しをする記事を書きたいと思います。想定する読者像は"日常生活で使用する範囲で圏論の言葉は知ってるけど、たまたまモナドは知らなかったプログラマ"です(いますか？)。
まぁだいたいのところ、Kleisli圏というものを紹介をする感じの記事になります。
参考 : https://en.wikipedia.org/wiki/Kleisli_category
圏論のモナドとその分解
まず$T \in \text{End}(\mathcal{C})$を圏$\mathcal{C}$のモナドとします。すなわち函手と自然変換による次のような3つ組$(T,\eta,\mu)$で、
\begin{align}
T &: \mathcal{C} \to \mathcal{C} \\
\eta &: \text{id}_\mathcal{C} \Rightarrow T \ (単位元に対応)\\
\mu &: T^2 \Rightarrow T \ (積に対応)\\
\end{align}
次の等式を満たすものになります。
\begin{align}
\mu \circ T \mu &= \mu \circ \mu T : T^3 \Rightarrow T \ (結合則に対応) \\
\mu \circ T \eta &= \mu \circ \eta T = \text{id}_T : T \Rightarrow T \ (単位元則に対応)
\end{align}
参考 : https://en.wikipedia.org/wiki/Monad_(category_theory)#Introduction_and_definition
(等式の条件が少し分かりにくいと思いますので対象$X$を補いますと、それぞれ等式$ \mu_{X} \circ T \mu_X = \mu_{X} \circ \mu_{TX} : T^3X \to TX$および$\mu_X \circ T \eta_X = \mu_{X}\circ \eta_{TX} : TX \to TX$になります)
肝となるのは次の定理です(名前あるんでしょうか？)。
任意のモナド$T\in \text{End}(\mathcal{C})$に対し、ある随伴函手対$F : \mathcal{C} \rightleftarrows \mathcal{D} : G$が存在して$T=G \circ F$
この定理における随伴函手対$(F,G)$と圏$\mathcal{D}$は具体的に構成することができまして、特徴的なものにKleisli圏$\mathcal{C}_T$とEilenberg-Moor圏$\mathcal{C}^T$があります(実際、与えられたモナドを分解する随伴関手全体は圏を構成しまして、Kleisli圏はその始対象、Eilenberg-Moore圏は終対象になります1)。このうちKleisli圏$\mathcal{C}_T$のほうは以下のように構成されます。
-
$\text{Obj}(\mathcal{C}_T): = \text{Obj}(\mathcal{C})$
-
$\text{Hom}_{\mathcal{C}_T}(A,B):=\text{Hom}_{\mathcal{C}}(A,TB)$
-
$\tilde{f} \in \text{Hom}_{\mathcal{C}_T} (A,B)$と$\tilde{g} \in \text{Hom}_{C_T}(B,C)$の合成を、それぞれに対応する$f \in \text{Hom}_{\mathcal{C}}(A,TB), g \in \text{Hom}_{\mathcal{C}}(B,TC)$を用いて
$$ \tilde{g} \circ \tilde{f} := \mu_C \circ Tg \circ f: A \to TB \to T^2C \to TC: $$
Kleisli圏に対応する随伴関手対$F_T : \mathcal{C} \rightleftarrows \mathcal{C}_T : G_T$は以下のように定義されます。
\begin{align}
F_T X &:= X \\
F_T f &:= \eta_B \circ f : A \xrightarrow{f} B \xrightarrow{\eta_B} TB \ \ \ ( \ f \in \text{Hom}_\mathcal{C} (A,B))\\
G_T X &:= TX \\
G_T \tilde{f} &:= \mu_B \circ Tf: TA \to T^2B \to TB \ \ \ (\ \tilde{f} \in \text{Hom}_{\mathcal{C}_T}(A,B))
\end{align}
このように構成された$F_T,G_T$に対して、確かに$G_T \circ F_T = T$となることが確認できます(射の方の等式はモナドの定義$\mu \circ T \eta = \text{id}_T$を使っています)。
\begin{align}
(G_T \circ F_T) X &= G_T X = TX \\
(G_T \circ F_T) \ f &= G_T (\eta_B \circ f) = \mu_B \circ T \eta_B \circ Tf = \text{id}_{TB} \circ Tf = Tf
\end{align}
以上により、モナド$T$は随伴関手対の合成に分解されることが確認できました。
Haskellのモナド
では改めてHaskell側の記述を確認します。
class Monad m where
(>>=) :: m a -> ( a -> m b) -> m b
(>>) :: m a -> m b -> m b
return :: a -> m a
先程のKleisli圏に出てきた言葉を用いれば、次のように対応付けることができます(変数a,bの型をそれぞれ$A$,$B$とします)。
- m $\Leftrightarrow$ $T$の(あるいは$G_T$の)対象における対応
- return $\Leftrightarrow \eta : id_\mathcal{C} \to T$ (対象$A$が与えられれば$\eta_A : A \to TA$)
- (>>=) $\Leftrightarrow G_T$の射における対応 ($\ f:A\to TB$から$TA \to TB$を作り出す)
- (>>) $\Leftrightarrow$
m >> k = m >>= \_ -> kらしいので(>>=)と同様 (\_ -> kはラムダ式)
ついでにモナド則のほうも確認しておきます。
return a >>= k = k a
m >>= return = m
m >>= (\x -> k x >>= h) = (m >>= k) >>= h
return a >>= k = k aではreturn aの意味するところが$\eta_A (a)$となり、等式は$k:A\to TB$に対して$\mu_B \circ Tk(\eta_A(a)) = k(a)$を意味します。これは自然変換の定義から$Tk\circ \eta_A = \eta_{TB}\circ k$であることと、モナドの定義から$\mu \circ \eta T = \text{id}_T$であることから導かれます。
m >>= return = mに関しては左辺が$\mu \circ T \eta$になるため、これもモナドの定義$\mu \circ T \eta = id_T$から導かれます。
m >>= (\x -> k x >>= h) = (m >>= k) >>= hは$k : A \to TB$、$h:B \to TC$とすれば等式$\mu_C \circ T \mu_C \circ T^2 h \circ Tk= \mu_C \circ Th \circ \mu_B \circ Tk$となります。これまた自然変換の定義から$Th \circ \mu_B = \mu_{TC} \circ T^2 h$であることと、モナドの定義から$\mu \circ T \mu = \mu \circ \mu T$であることから導かれます。
つまりモナド則は上から順に右単位則・左単位則・結合則に対応してることが分かります。
以上により、自己函手の圏のモノイド対象であるモナドから、Haskellで定義されているモナドを理解できることが分かりました。2
まとめ
「モナドは単なる自己函手の圏のモノイド対象だよ。そういうものは常に随伴関手対の合成に分解できるのだけど、その時の相方となる圏の例としてKleisli圏というのがあって、その構成の仕方がHaskellのモナドに対応するんだよ。何か問題でも？」
宣伝
株式会社オプティマインドでは、一緒に働く仲間を大募集中です。
カジュアル面談も大歓迎ですので、気軽にお声がけください。
【エンジニア領域の募集職種】
●ソフトウェアエンジニア
●QAエンジニア
●Androidアプリエンジニア
●組合せ最適化アルゴリズムエンジニア
●経路探索アルゴリズムエンジニア
●バックエンドエンジニア
●インフラエンジニア
●UXUIデザイナー
【ビジネス領域の募集職種】
●セールスコンサルタント
●採用・人事
『オプティマインドってどんな会社？』については、こちらから
Wantedlyでもこちらで募集中