クライスリ圏

スタンダード構成（standard construction；余モナド）の概念はホモロジー代数の分野では早くから現れていたが、随伴概念の発見に伴い、すべてのモナドは関手の随伴対から得られるのではないかという予想がP.J.Hilton その他によって立てられていた^[2]。これに対し二つ解答が寄せられたが、その解答者の一人であるハインリッヒ・クライスリは『Every standard construction is induced by a pair of adjoint functors(1965)』で、

定理

圏 L におけるスタンダード構成 (C,k,p) が与えられたとする。このとき、圏 K が存在し、さらに (C,k,p) を導き随伴を成す二つの共変関手 F ： K → L と G ： L → K が存在する。

を証明して解答したが、ここで新たに随伴対 (F,G) を構成するために必要となるドメインの圏 K はクライスリ圏（Kleisli category）と呼ばれるようになった。クライスリ圏については、イタリアの計算機科学者エウジニオ・モッジによる計算機科学のプログラム意味論における応用がモナドの理論として存在する。

圏 C 上のクライスリトリプル（Kleisli triple）とは、関手 T : C → C、自然変換 η（η_A : A → T A for A ∈ Obj(C)）、射 f : A → T B に対して射 f* : T A → T B を与える拡張演算子（extension operator） _^* からなる三つ組 （T, η, _^*）で、以下

• η_A* = 1_{T A}
• f*・η_A = f ただし、f : A → T B
• g*・f* = (g*・f)* ただし、f : A → T B かつ g : B → T C

を満たすものを言う。

圏 C 上にクライスリトリプル（T, η, _^*）が与えられているとき、クライスリ圏（Kleisli category）C_T とは、対象、射、射の合成規則を以下のとおり定めたものを言う。

• C_T の対象は、C の対象である
• C_T において、対象 A から B への射の集まり Hom_CT(A,B) は、C における射の集まり Hom_C(A, T B) である
• C_T において、射 f ∈ Hom_CT(A,B) と射 g ∈ Hom_CT(B,C) の合成射とは、g*・f : A → T C である

圏 C 上のモナド <T,η,μ> が与えられたとすると、クライスリトリプルの拡張演算子 _^*はモナドを用いて定義することができる。具体的には、任意の射 f : X → T Y に対して、_^* を

${\displaystyle f^{*}=\mu _{Y}\circ Tf.}$

とする。よって、モナド <T,η,μ> を与えることはクライスリトリプル （T,η, _^*） を与えることと同値である。

計算機科学者のエウジニオ・モッジは、クライスリ圏の射をプログラム（program）に対応させる^[3]、すなわち射としてのプログラムが成す圏とはクライスリ圏であるとすることで表示的意味論にモジュール性を持たせることに成功した（モナドの理論）^[4]。

プログラミングの教則として、引数と返り値をもつことからプログラム（program）とは数学の関数、すなわち集合写像（mapping）であると教えられることがある。
しかしながらこの喩えは

• 入出力等をもたらすプログラム
• 例外を返すプログラム
• 引数に対して値を返さない（停止しない）プログラム
• 同じ引数でも返り値が異なる可能性のあるプログラム

などを説明することができない。つまり、プログラムは集合写像ではない（a program is NOT a mapping）^[5]。
プログラム（program）の数学的モデルを見つけ出す過程において、モッジは圏論と表示的意味論の観点からプログラムは圏の射、型は圏の対象とみなすことができ^[6]、さらに直感的解釈として、関数が値を取り値を返すものであるのに対しプログラムが値を取り計算した 値を返す^[7][8]、すなわち引数の型と返り値の型の間にはなにか違いがあり単純な射の合成ができない、と考えた。

集合写像（関数）：値　→　　　　　　　値

プログラム　　　：値　→　"計算した"　値

モッジはこのような射としてのプログラムの数学的モデルとしてクライスリ圏（Kleisli category）の射が妥当であると主張し^[9]実際に副作用、例外処理、非決定計算などの効果^[10]をうまくクライスリ圏の枠組みで統一的に定式化できることを示した。その結果として伝統的な表示的意味論においては欠如していたモジュール性を付与することに成功した^[11]。

理論的には、ある計算方式で"計算した"ことを示す印は、次のモッジの原理から型構築子として導入される^[12]。

モッジの原理（Moggi's principle）^[13][14]

計算によって得られた型 A の値（computations of type A）は、型 T A の値に対応する

（Computations of type A correspond to values of type T A.）

特に、この計算方式を表す型構築子 T を計算概念（a notion of computation）と呼ぶ^[15]。

また、必然的に計算した値を返すプログラム概念は次のようになる。

モッジが（暗黙的に）主張するプログラムの概念

型 A の引数を取り T の計算効果を伴いつつ計算をした型 B の値を返すプログラム（program）とは、

A → T B

の型を持つものである。

この特徴付けによって、計算効果 T を伴うプログラムとなんら計算効果を持たない単なる集合写像（関数）は区別できるようになる。ただし、その代わりに２つのプログラムの合成を関数のように単純に行うことができなくなるのである。

例えば、program1 :: A → T B と program2 :: B → T C が与えられたとき、その合成を行おうと思っても、型 B というデータの型としての共通性はあっても計算概念の分だけ型に違いがあるため、実際にプログラムの合成を行うことはできない。

program2 :: B → T C × program1 :: A → T B （合成不可）

この致命的な問題点を解消するために導入されるのがクライスリトリプル（Kleisli triple）である。 直感的な記法となるが、クライスリトリプル（T,η, _^*）が与えられれば、「_^*」演算子の機能からprogram2* :: T B → T C となり

program2* . program1 :: A → T C （合成可能）

という形でプログラムの合成が可能となる。おおよそこのような理由からモッジはプログラムはクライスリ圏をなすとした^[16]。

プログラムの世界におけるクライスリ・トリプルに対応するものは、計算機科学者のPhillip Wadlerによって命名された次のモナド則（Monad laws）である。

{-                     モナド則（Monad laws）                     -}
{-  1.右単位則（Right unit）　-}
  T a `bindT` unitT == T a
{- 2.左単位則（Left unit）　 -}
  (unitT a) `bindT` f == f
{- 3.結合規則（Associative）-}
  T a `bindT` (\ x → (f x) `bindT` (\ y → g y) ) == (T a `bindT` (\x → f x) ) `bindT` (\y → g y)

これに直接対応するのは次の合成順序を逆にしたのときのクライスリトリプルである。

合成順序が逆のときのクライスリトリプル

圏 C 上に定義された関手 T、自然変換 η、T への射に対する操作 _^* が以下

1. T A ; η_A*＝ T A（モナド則との明白な対応関係をつけるため、元々の定義よりも冗長にしてある。）
2. η_A ; f* ＝ f ただし、f : A → T B
3. f* ; g* ＝ (f ; g*)* ただし、f : A → T B かつ g : B → T C

を満たすとき、三つ組（T, η, _^*）をクライスリトリプルと呼ぶ。

クライスリ圏をなす計算概念としては以下の計算効果が挙げられる^[17]。

部分性（partiality）

T A = A_⊥（= A + { ⊥ }）

η_A は A から A_⊥ の中への包含（inclusion）

f : A -> T B であれば、f^*(⊥) = ⊥ 、f^*(a) = f(a) ただし、a ∈ A

非決定性（nondeterminism）^[18]

T A = P_fin(A)

η_A は単要素（singleton）写像 a ↦ {a}

f : A -> T B かつ c ∈ T A であれば、f^*(c) = ∪_{x ∈ c}f(x)

副作用（side-effects）

T A = (A × S)^S

η_A は写像 a ↦ (λs: S.<a,s>)

f : A -> T B かつ c ∈ T A であれば、λs:S.(let <a, s'> = c(s) in f(a)(s'))

例外（exceptions）^[19]

T A = A + E

η_A は入射（injection）写像 a ↦ inl(a)

f : A -> T B であれば、f^*(inr(e)) = e (ただし、e ∈ E) かつ f^*(inl(a)) = f(a) (ただし、a ∈ A)

継続（continuations）

T A = R^(RA)

η_A は写像 a ↦ (λk: R^A. k(a))

f : A -> T B かつ c ∈ T A であれば、f^*(c) = (λk: R^B .c(λa: A.f(a)(k)))