クライスリ圏

圏論においてクライスリ圏（クライスリけん、英: Kleisli category）とは、『すべてのスタンダード構成は関手の随伴対から得られるか』という予想に対し、ハインリッヒ・クライスリが解答をするにあたって導入した圏である^[1]。

概要

スタンダード構成（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）と呼ばれるようになった。クライスリ圏については、イタリアの計算機科学者エウジニオ・モッジによる計算機科学のプログラム意味論における応用がモナドの理論として存在する。

定義

クライスリトリプル（Kleisli triple）

圏 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

を満たすものを言う。

クライスリ圏（Kleisli category）

圏 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]。

プログラムの圏としてのクライスリ圏（Kleisli category as category of programs）

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

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

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

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

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

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

モッジの原理（Moggi's principle）

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

モナド則（Monad laws）

プログラムの世界におけるクライスリ・トリプルに対応するものは、計算機科学者の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)))

脚注

1. ^ Kleisli(1965)
2. ^ 大熊(1979) pp.205-207
3. ^ Moggi(1991) p.3

   In order to justify the axioms for a Kleisli triple we have first to introduce a category C_T whose morphisms correspond to programs.

   ※ここで圏 C_T はクライスリ圏（定義1.3）

   他 蓮尾(2011)
4. ^ 佐伯(2001) p.11
5. ^ つまり、Set もしくは Ens の普通の射ではない。
6. ^ Moggi(1989)a p.17
7. ^ Moggi(1989)a p.17

   3.2.1 A justification for monads

   In order to justify the use of monads for modelling notions of computations we adopt the following intuitive understanding of programs: a program is a function from values to computations.

8. ^ 圏論の創始者の一人のマックレーンの著作でも、圏Set（もしくは Ens） の普通の射に計算（computation）概念は全く含まれていないことが確認できる。形式と機能(1992) pp.163-173
9. ^ Moggi(1989)a p.18
10. ^ 計算効果（computational effects）と呼ばれる。Filinski(1994)、勝股(2011)
11. ^ 例えば、デイビッド・エスピノーザによる、モナドを用いたモジュラーな意味論を採用することでレゴブロックを組み立てるように言語を組み立てることができることを実証などがある。Espinosa_draft(1995)
12. ^ なお、モッジはプログラミング言語のML（MetaLanguage）のような型システムを持つ言語を前提に理論を展開している。
13. ^ Filinski(1994) p.447
14. ^ 参照

    1 A categorical semantics of computations

    The basic idea behind the categorical semantics below is that, in order to interpret a programming language in a category C, we distinguish the object A of values (of type A) from the object TA of computations (of type A), and take as denotations of programs (of type A) the elements of TA. In particular, we identify the type A with the object of values (of type A) and obtain the object of computations (of type A) by applying an unary type-constructor T to A. We call T a notion of computation, since it abstracts away from the type of values computations may produce. There are many choices for TA corresponding to different notions of computations.

    Moggi(1991) pp.2-3
15. ^ Moggi(1991) p.3
16. ^ Moggi(1989)a pp.17-18
17. ^ Moggi(1991) pp.4-5
18. ^ プログラミング言語のHaskellにおいてはリストモナドとして知られる。
19. ^ HaskellにおいてはMaybeモナドとして知られる。inr(e) = Nothing、inl(a) = Maybe a

参考文献

• 大熊正『圏論（カテゴリー）』槙書店、1979年。 
• Heinrich Kleisli (1965), Every standard construction is induced by a pair of adjoint functors, http://www.ams.org/journals/proc/1965-016-03/S0002-9939-1965-0177024-4/S0002-9939-1965-0177024-4.pdf 
• Eugenio Moggi (1989), An abstract view of programming languages, http://www.disi.unige.it/person/MoggiE/ftp/abs-view.pdf 
• Eugenio Moggi (1989) (PDF), Computational lambda-calculus and monads, http://www.disi.unige.it/person/MoggiE/ftp/lics89.pdf 
  • Moggi, Eugenio (1988) (PDF). Computational lambda-calculus and monads. University of Edinburgh, Department of Computer Science. http://www.lfcs.inf.ed.ac.uk/reports/88/ECS-LFCS-88-66/ECS-LFCS-88-66.pdf 

• Eugenio Moggi (1991), Notions of computation and monads, doi:10.1016/0890-5401(91)90052-4, https://doi.org/10.1016/0890-5401(91)90052-4 
• S. マックレーン (1992). 数学 －その形式と機能－. 赤尾和男, 岡本周一共訳. 森北出版. ISBN 9784627018303 
• David Espinosa (1995), Semantic Lego, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.2885 
• Sheng Liang , Paul Hudak, Modular Monadic Semantics, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.136.1656 
• 佐伯豊『再利用可能な拡張機能を備えた言語処理系』北陸先端科学技術大学院大学〈博士(情報科学) 甲第130号〉、2001年。doi:10.11501/3184128。 NAID 500000205085。https://dl.ndl.go.jp/info:ndljp/pid/3184128。 
• 尾上能之「Haskellプログラミング:自分自身を出力するプログラム」『情報処理』第47巻第3号、情報処理学会、2006年3月、301-309頁、CRID 1050001337897971072、ISSN 04478053。 
• 梅村晃広「モナドに基づく代数仕様の書換え」『情報処理学会研究報告. [プログラミング-言語基礎実践-]』第93巻第97号、情報処理学会、1993年10月、1-8頁、CRID 1573950401960871168、NAID 110002929389。 
• 勝股 審也「圏論の歩き方(第5回)モナドと計算効果」『数学セミナー』第50巻第12号、東京 : 日本評論社、2011年、98-104頁、ISSN 0386-4960。 
• 蓮尾 一郎 (2011), 圏論の歩き方(第6回)モナドのクライスリ圏 
• Philip Wadler, The essence of functional programming, http://www.eliza.ch/doc/wadler92essence_of_FP.pdf 
• Andrzej Filinski (1994), Representing Monads, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.43.8213 
• Simon Peyton Jones, Paul Hudak 他, ed. (2002) (PDF), Haskell 98 Language and Libraries The Revised Report, https://www.haskell.org/definition/haskell98-report.pdf 

関連項目

• モナド (圏論)
• モナド (プログラミング)

表 話 編 歴 圏論
主要項目	圏 射 エピ モニック 図式 可換図式 自然変換 圏同値 反対圏 始対象と終対象 普遍性 米田の補題 双対 極限 帰納極限 射影極限 積 余積 像 余像 等化子 余等化子 トポス 核 余核 引き戻し モナド Kan拡張
関手	加法的 完全 充満 随伴 対角 忠実 導来 表現可能 本質的全射 Hom関手
具体的圏	関手圏 前加法圏 集合の圏 マグマの圏 群の圏 アーベル群の圏 擬環の圏 環の圏 加群の圏 ベクトル空間の圏 多元環の圏 位相空間の圏 距離空間の圏 多様体の圏
圏の類	完備圏 コンマ圏 部分圏 モノイド閉圏 デカルト閉圏 アーベル圏 導来圏 クライスリ圏 デカルトモノイド圏
一般化	豊穣圏 2-圏 圏の圏
人物	ソーンダース・マックレーン サミュエル・アイレンベルグ アレクサンドル・グロタンディーク ウィリアム・ローヴェア ハインリッヒ・クライスリ
関連分野	代数幾何学 普遍代数 ホモロジー代数
関連項目	『圏論の基礎』
カテゴリ