クライスリトリプルは,計算機科学などの分野で(たとえばHaskellなどの関数型プログラミング言語において)しばしば登場する概念です。クライスリトリプルはモナドと密接に関連しており,ストリング図に慣れればこれらの関係を視覚的にわかりやすい形で表すことができます。
この記事では,クライスリトリプルについて説明した後で,モナドとの関係をストリング図により示します。なお,この記事は圏論に不慣れな方でも大まかな雰囲気がつかめることをめざして書いています。
#1:
圏の定義と具体例
#2:
関手と自然変換
#3:
垂直合成と水平合成
#4:
モノイダル圏
#5:
モナドとは自己関手の圏におけるモノイド対象のこと
#6:
モナドの例
#7:
随伴
#8:
関手を表す線の順序の交換
#9:
普遍射と随伴・極限・カン拡張
#10:
ホム関手のストリング図(前編)
#11:
ホム関手のストリング図(後編)
#12:
米田の補題
番外編1: 視覚的に理解するクライスリトリプルとモナドの同値性(この記事)
番外編2:
線形代数の圏論的な性質(?)を圏論なしで説明する
まず,クライスリトリプルの定義を示します。以降では,圏の定義は知っているものとします。
(a) 写像
(b) 射の集まり
(c) 写像の集まり
各
(1)
(2)
(3)
なお,
Monad
は,return関数とバインド関数により定められます。この Monad
は,クライスリトリプルのことだと考えるとわかりやすいと思います。具体的には,上の定義における単位元>>=
に対応しています(m >>= f
で表されます)。上の三つの条件は,次のように書き換えられます。m >>= (\x -> f x >>= g) == (m >>= f) >>= g
m >>= return == m
(return x) >>= f == f x
クライスリトリプルの定義から,
これらを確認する作業はやや退屈かと思いますので,この作業に興味のない方(または関手・自然変換に不慣れな方)は読み飛ばしても構いません。
各
と定めます。このとき,
が成り立つことからわかります。恒等射を恒等射に写すことは,各
が成り立つことからわかります。
各
が成り立ちます。つまり,
一般的な場合について述べる前に,具体例として
第6回の記事
で述べたリストモナド
四角いブロックが
各集合
青丸が
この図式にある青丸は,
上で述べたリストモナドの図式を一般化して,単位元と持ち上げの図式を導入します。各
図式では,関手
各
持ち上げ
矢印
なお,持ち上げ
持ち上げ
この図式では,点線の枠の中に
以降では,クライスリトリプルとモナドの関係について述べます。
まず,モナドの定義を述べておきます( 第5回の記事 で述べたものと同じです)。
関手
(1')結合律:
結合律
ただし,3本の線がつながった青丸は
(2')単位律:
単位律
ただし,1本の線がつながった青丸は
任意のクライスリトリプルから対応するモナドを構成できて,逆に任意のモナドから対応するクライスリトリプルを構成できることが知られています。このような意味で,クライスリトリプルとモナドは同一視できます。この記事では,このような関係を同値性とよんでいます。
この同値性は,「クライスリトリプルの定義(Kleisli)で述べた三つの条件」が「モナドの定義(Monad)で述べた二つの条件(つまり結合律と単位律)」に対応していることから示せます。また,この対応は,図式を用いれば素直に理解できると思います。以降では,前者の三つの条件を図式で表すことで,このことを示します。
条件(1)は次の図式で表せます。
条件(1)(
この左辺では,補助線で囲まれた領域が
この右辺を変形して青丸の位置を上のほうに動かすと,次の図式が得られます。なお,先ほどの図式に対し,右辺のみを変形しています(補助線はひとまず無視してください)。
条件(1)(
式
結合律
が成り立つことが容易に想像できます。この式は,式
条件(2)は次の図式で表せます。
条件(2)(
この式が任意の
が成り立ちます。この式は,式
条件(3)は次の図式で表せます。
画像の名前
なお,この左辺では
画像の名前
この式が任意の
画像の名前
が成り立つことが容易に想像できます。この式は,式
以上により,条件(1)がモナドの定義(Monad)における結合律と同値であり,条件(2)と条件(3)が単位律と同値であることがわかります。
ストリング図を用いると,クライスリトリプルとモナドの同値性を視覚的に理解できることを示しました。計算機科学などの分野において現れるモナドに関するほかの多くの性質も,このようなストリング図を用いると素直に表せることがわかります。その基本的なものは拙著Nak-2025の4.4節などで述べていますので,興味のある方はご参照ください。また,同じストリング図によりデータの流れを直観的な形で表せますので,ストリング図が描けるようになると便利かと思います。