クライスリ圏
圏論における重要な概念の一つであるクライスリ圏は、1965年に数学者ハインリッヒ・クライスリによって導入されました。その背景には、「スタンダード構成と呼ばれるあらゆる構成は、常に二つの
関手の随伴対から導き出されるのではないか?」という当時の予想に対する解答を与えるという目的がありました。スタンダード構成は、もともとホモロジー代数などの分野で古くから知られていましたが、随伴概念の発見により、その
普遍性が問われるようになったのです。
クライスリによる導入
クライスリはこの予想に対し、「Every standard construction is induced by a pair of adjoint functors」(1965年)と題された論文で肯定的な解答を示しました。そこで証明された定理は、以下のような内容です。
定理
ある圏 `L` 上にスタンダード構成 `(C, k, p)` が与えられているとき、新たな圏 `K` と、このスタンダード構成を導き出し、随伴の関係を成す二つの共変
関手 `F: K → L` および `G: L → K` が存在します。
この定理において、随伴対 `(F, G)` を具体的に構成する際に必要となる、元の圏 `L` とは異なる新しい圏 `K` が導入されました。この圏 `K` こそが「クライスリ圏(Kleisli category)」と名付けられたものです。
クライスリ圏の形式的な定義
クライスリ圏を定義するためには、「クライスリトリプル(Kleisli triple)」と呼ばれる概念が必要です。圏 `C` 上のクライスリトリプル `(T, η, _)` とは、以下の要素からなる三つ組です。
圏 `C` から `C` 自身への
関手 `T: C → C`
各対象 `A` に対して `ηA: A → T A` という射を与える自然変換 `η`
任意の射 `f: A → T B` に対して、射 `f: T A → T B` を与える拡張演算子 `_`
これらの要素は、以下の3つの条件(法則)を満たす必要があります。
1. `ηA = 1TA` (対象 `A` における単位射 `ηA` を拡張演算子で変換すると、`TA` 上の恒等射になる)
2. `f ∘ ηA = f` (`A` から `T B` への射 `f` に対して、`ηA` に `f` を合成すると元の `f` に戻る)
3. `g ∘ f = (g ∘ f)` (合成 `f` してから `g` を適用するのと、`f` の拡張 `f` と `g` の拡張 `g` を合成するのとが等しい)
圏 `C` 上にクライスリトリプル `(T, η, _)` が与えられているとき、クライスリ圏 `CT` は以下のように定義されます。
対象: 圏 `CT` の対象は、元の圏 `C` の対象と全く同じです。
射: 圏 `CT` において、対象 `A` から `B` への射 `f: A → B` は、元の圏 `C` における `A` から `T B` への射 `f: A → T B` として定義されます。すなわち、`HomCT(A, B) = HomC(A, T B)` です。
射の合成: 圏 `CT` において、射 `f: A → B` (これは `C` では `A → T B`) と 射 `g: B → C` (これは `C` では `B → T C`) の合成 `g ∘ f: A → C` は、`C` における射 `g ∘ f: A → T C` によって定義されます。
モナドとの関係
圏論におけるモナド `
` は、クライスリトリプル `(T, η, _)` と密接に関連しており、実質的に等価な概念です。モナド `` が与えられている場合、拡張演算子 `_` はモナドの結合律子 `μ` と関手 `T` を用いて、任意の射 `f: X → T Y` に対して `f = μY ∘ T f` と定義することができます。このように、モナドからクライスリトリプルを導くことができ、またその逆も可能であるため、どちらの概念も同じ数学的構造を記述していると言えます。
計算機科学における応用
クライスリ圏は、理論数学だけでなく計算機科学の分野、特にプログラムの意味論において重要な役割を果たしています。イタリアの計算機科学者エウジニオ・モッジは、プログラムが単なる数学的な関数(集合写像)では捉えきれない多様な性質(入出力、状態変化、例外、非決定性、非停止など、これらを「計算効果」と呼びます)を持つことに着目しました。
単純な集合写像が「値 → 値」という変換であるのに対し、プログラムは「値 → 『計算した』値」という、計算効果を伴う変換であると考えられます。モッジは、このような計算効果を伴うプログラムをモデル化するために圏論を適用しました。彼は、プログラムの「型」を圏の「対象」に対応させ、「プログラム」自身を圏の「射」に対応させることができると考えました。
モッジの重要な発見は、「計算効果を伴う型 `B` の値を返す、型 `A` の引数を取るプログラム」は、クライスリ圏における `A` から `B` への射、すなわち元の圏 `C` における `A` から `T B` への射として捉えることができる、という点です。ここで `T` は計算効果を表す型構築子(関手)です。これを「モッジの原理」と呼びます。
しかし、このモデル化には問題がありました。 `A → T B` というプログラム `p1` と、 `B → T C` というプログラム `p2` があった場合、単なる関数の合成のように `p2 ∘ p1` と合成しようとしても、型の不整合(`T B` と `B`)のため直接合成ができませんでした。
この合成の問題を解決するために、クライスリトリプルの拡張演算子 `_` が重要な役割を果たします。プログラム `p2: B → T C` に対して、その拡張 `p2: T B → T C` を考えます。すると、`p1: A → T B` と `p2: T B → T C` は型が整合するため、通常の圏の合成 `p2 ∘ p1: A → T C` が可能となります。この `A → T C` という射が、プログラム `p1` と `p2` を順に実行した結果得られる合成プログラムに対応します。このように、クライスリ圏の射の合成規則が、計算効果を伴うプログラムの自然な合成を与えることが示されました。
計算機科学でよく知られている「モナド則」は、このようなプログラム合成の規則に対応しており、これは圏論的なクライスリトリプルの法則と等価です。
クライスリ圏で扱える計算効果の例
クライスリ圏の枠組みは、様々な計算効果を統一的に扱うための強力なツールとなります。代表的な計算効果の例と、それに対応する型構築子 `T` の直感的な説明を以下に示します。
部分性 (Partiality): 結果が未定義になる可能性を表します。`T A` は `A` の値に「未定義」を表す特別な要素 `⊥` を加えた型 `A + {⊥}` のように考えられます。
非決定性 (Nondeterminism): 一つの入力から複数の結果が得られる可能性を表します。`T A` は `A` の要素の(空でない)有限集合全体の型 `Pfin(A)` のように考えられます。
副作用 (Side-effects): 計算がプログラムの状態を変化させる可能性を表します。`T A` は、状態 `S` を受け取って `A` の値と新しい状態 `S` のペアを返す関数の型 `S → (A × S)` のように考えられます。
例外 (Exceptions): 計算が正常な結果ではなく例外を発生させる可能性を表します。`T A` は `A` の値か、例外 `E` のどちらかを含む型 `A + E` のように考えられます。
* 継続 (Continuations): 計算の残りの部分(継続)を引数として受け取ることで、計算の流れを制御する可能性を表します。`T A` は、ある結果型 `R` への関数を受け取って `R` を返す関数の型 `(A → R) → R` のように考えられます。
これらの例のように、クライスリ圏は抽象的な構造を提供することで、一見異なる様々な計算の性質を統一的に理解し、モデル化することを可能にしています。
圏論におけるクライスリ圏は、純粋数学的な構造としてのみならず、プログラムの意味論におけるモナド理論の基盤としても、現代の情報科学において重要な概念となっています。