プログラミングの解説で「関手」や「モナド」という言葉に出会い、なぜ数学の圏論が突然現れるのか戸惑うことがあります。一方、証明支援系では命題を型、証明をプログラムのように扱います。数学、計算、論理という三つの領域が、同じ用語を偶然借りているわけではありません。
接点にあるのは、複雑なものを小さな変換へ分け、それらを合成して全体を作るという発想です。圏論は、変換の中身よりも接続と合成の規則を取り出します。そのため、関数をつなぐプログラム、推論をつなぐ証明、効果を伴う計算の順序を、共通の構造として比較できます。ただし、圏論があらゆるプログラムを自動的に説明するわけではありません。どこまでが厳密な対応で、どこからが実装上の比喩なのかを分ける必要があります。
型を対象、関数を射として捉える計算の圏
まず、型A、B、Cを対象とし、A型の値を受け取ってB型の値を返す全関数 f: A → B を射とする世界を考えてみましょう。B → Cという関数gがあれば、fのあとにgを実行する合成 g ∘ f: A → C が得られます。各型Aには、値を変えず返す恒等関数idAも備わっています。
関数合成は結合律を満たすため、三つの関数のどこから二つずつまとめても、入力から出力までの結果は変わりません。さらに恒等関数が合成の単位となる。この二つが、圏の公理そのものです。
この見方の利点は、プログラムの内部実装を開かずに接続を議論できる点にあります。焦点となるのは、fがどのアルゴリズムを使うかではなく、Aを受け取ってBを返し、gへ接続できるかどうか。型が接続面となり、関数合成は部品から大きな計算を作る規則になります。
実在するプログラミング言語と全関数の理想化
ただし、現実のプログラミング言語をそのまま「型と全関数の圏」だと断定することはできません。停止しない計算、例外、可変状態、入出力、遅延評価などがあるため、A型の入力が必ずB型の値へ到達するとは限らないからです。プログラムの等しさを何で判定するかという問題も残ります。
たとえば、同じ入力に同じ値を返す二つのプログラムでも、片方だけが途中で出力を行うなら、観測できる振る舞いは異なります。実行時間やメモリ消費まで意味に含めるかによっても同値関係は変わります。圏を作るには、対象、射、合成だけでなく、どの計算を同じ射とみなすかを明らかにしなければなりません。
そこで表示的意味論では、対象となる言語の特徴に合った数学的な圏を選び、プログラムをその圏の射として解釈します。圏論は現実のコードを無条件で関数へ置き換える道具ではなく、どの性質を保存した意味モデルが必要かを整理する言語として働きます。
型構築子を関手にするmapの二法則
プログラミングでは、型Aからリスト型List(A)や省略可能な値Maybe(A)を作る操作を型構築子と呼びます。圏論的な関手として扱うには、型だけでなく関数も移さなければなりません。関数f: A → BからList(f): List(A) → List(B)を作るmapが、その役割を担います。
関手であるためには、恒等関数をmapしても何も変わらず、合成関数を一度にmapした結果が、二つのmapを順に適用した結果と一致する必要があります。式では map(id) = id と map(g ∘ f) = map(g) ∘ map(f) です。この二法則によって、リストという文脈へ移しても元の関数合成が崩れません。
Maybeなら、値がある場合だけfを適用し、値がない状態はそのまま保ちます。重要なのは容器という比喩ではなく、恒等射と合成を保存するという一点。Haskellなどの`Functor`はこの発想を型クラスとして表しますが、法則は型だけから自動的に証明されるとは限らず、実装者が守るべき契約として扱われます。
値から計算を分けたモナドの出発点
普通の関数f: A → Bは、Aの値からBの値を得る純粋な変換として解釈できます。しかし失敗する、状態を更新する、複数の候補を返すといった計算は、Bの値だけでは振る舞いを表せません。そこで、結果Bではなく「何らかの計算効果を伴ってBを返す計算」T(B)を終域に置きます。
例外Eを伴う計算ならT(B)をBまたはE、状態Sを扱う計算ならSを受け取って(B, S)を返す関数、非決定的計算ならBの候補の集まりとしてモデル化できます。Tは型を計算の型へ移し、関数をその計算の文脈へ持ち上げる関手です。
エウジェニオ・モッジは1989年と1991年の研究で、値と計算を分け、さまざまな計算効果をモナドによって統一的に意味づける枠組みを示しました。ここでモナドは「副作用」という一種類の機能名ではありません。どの効果を扱うかはTの選択で変わり、モナドが与えるのは、効果を伴う計算を一貫して合成する構造です。
Kleisli合成が定める効果付き計算の順序
効果付き関数 f: A → T(B) のあとに g: B → T(C) を実行したくても、通常の関数合成は使えません。fが返すのはBではなくT(B)なので、gの入力型とつながらないためです。モナドは、T(B)の中の結果を受けて次の計算gへ進み、全体をA → T(C)へまとめる合成を提供します。
g ∘ f : A → C
g ⋆ f : A → T(C)
この合成はKleisli合成と呼ばれます。純粋な値aを効果のない計算T(A)へ入れるunitと組み合わせ、満たすべき法則は恒等律と結合律。どこで括弧を付けて二つずつ合成しても、計算全体の意味が変わらないことが結合律です。
Haskellの`>>=`、いわゆるbindは、`m a`型の計算結果を受け取り、値aを次の関数`a -> m b`へ渡します。`do`記法は、この接続を手続きのような順序で書く構文。モナドの法則は、前後に何もしない計算を置いても結果が変わらず、計算列の括り方にも意味が依存しないことを要求します。
失敗・状態・入出力で異なる「効果」の意味
Maybe型の計算では、途中で値がなくなれば、その後の関数を実行せず失敗を引き継ぎます。状態モナドなら、前の計算が返した新しい状態を次へ渡し、リストを使う非決定的計算なら、前段の複数候補それぞれに次の処理を適用して結果をまとめます。同じbindという形を使っても、効果の結合方法がTごとに異なる点を見落としてはいけません。
IOもHaskellではモナドとして扱われます。`IO A`は、実行されると入出力を行いながらA型の結果を生むアクションで、bindが前の結果を後続アクションへ渡します。純粋な式の評価と、外界とのやり取りを伴うアクションを型で分ける設計といえるでしょう。
ただし、「モナドさえ使えば副作用が消える」わけではありません。効果は型と合成規則の中へ明示されますが、入出力そのものは実行時に起こります。複数の効果をどう組み合わせるか、並行性や資源使用をどう表すかには、モナド変換子、代数的効果、そのほかの意味論が必要になる場合もあります。
数学上のモナドとプログラミング上のMonad
圏論のモナドは、ある圏C上の自己関手T、恒等関手からTへの自然変換η、Tを二重に適用したT²からTへの自然変換μから成り、単位律と結合律を満たします。プログラミングでは、ηに相当する`return`や`pure`と、μを使った合成に相当するbindで表す形がよく使われます。
両者は確かな数学的関係を持ちますが、実用言語の`Monad`型クラスを見ただけで、厳密な圏論モデルがすべて確定するわけではありません。どの型と関数を圏の対象・射にするか、非停止計算をどう扱うか、プログラムの等しさを何にするかが別途必要です。また、Haskellの型クラスはモナド則そのものをコンパイラで一般に強制しません。
モナドはプログラミングへ持ち込まれた神秘的な数学用語ではなく、合成できなかったA → T(B)型の計算を、法則に従って合成可能にする方法です。圏論から得られる価値は名称ではなく、実装が満たすべき等式と、別の効果にも再利用できる構造にあります。
命題を型、証明を項とみなすCurry–Howard対応
論理側では、命題Pを型、Pの証明をその型の項p: Pとみなす対応があります。命題Pが証明可能であることに対応するのは、型Pに項が存在すること、すなわち型が値を持つ状態にほかなりません。これがCurry–Howard対応、または「命題は型である」という見方として知られています。
含意P → Qの証明は、Pの証明を受け取ってQの証明を返す関数にほかなりません。P → Qの証明fとQ → Rの証明gがあれば、関数合成g ∘ fによってP → Rの証明が得られます。仮定から結論へ進む推論が、型付き関数の合成と同じ形になるわけです。
ここで圏を作るなら、命題または型を対象、証明またはプログラムを射として扱います。恒等射は「Pを仮定してPを得る」証明であり、射の合成は推論の接続。同じ結論へ至る証明をどの等式で同一視するかを定めれば、論理体系の構造を圏として表現できるのです。
論理積・論理和・含意を映す型の構成
命題PかつQは、Pの証明とQの証明を組にした積型P×Qへ対応します。一方、PまたはQに対応するのは、どちら側の証明かを印付きで保持する和型P+Q。常に真である命題は一つの自明な項を持つ単位型、偽は項を持たない空型として表せます。
含意P → Qは関数型です。P×Qの証明からPを得る第一投影、Pから「Qを仮定すればP×Qを得る関数」を作る操作など、自然演繹の導入則と除去則が、積や関数の構成規則として現れます。似ているのは論理記号と型構築子の見た目ではありません。作り方と使い方の規則まで対応しているのです。
ただし、最も直接に対応するのは直観主義論理です。排中律のような古典論理の原理を使うには、追加の公理や制御演算など、それに相当する構造が必要になります。「あらゆる論理がそのまま普通のプログラムになる」という主張ではありません。
直観主義論理とラムダ計算を結ぶデカルト閉圏
有限積と関数空間に相当する指数対象を備えた構造が、デカルト閉圏です。対象AとBに対して積A×Bがあり、AからBへの射を内部の対象BAとして表せる構造。随伴の言葉で書けば、Aとの積を取る関手−×Aと指数関手(−)Aの間に −×A ⊣ (−)A という関係があります。
この随伴は、二変数関数X×A → Bと、一変数を固定して関数を返すX → BAの対応、つまりカリー化を表します。複数の引数を受け取る関数と、引数を一つ受け取って次の関数を返す表現が往復できる理由が、普遍性として定式化されます。
ヨアヒム・ランベックらの研究によって、単純型付きラムダ計算とデカルト閉圏、直観主義命題論理の間に深い対応が整理されました。項の計算規則、証明の簡約、圏の射の等式が結び付くため、プログラム変換の正しさと証明変換を同じ構造から調べられます。
証明支援系で現実の操作になる命題と型の対応
Lean、Coq、Agdaなどの証明支援系では、命題と型の対応が実際の入力形式になります。たとえばLeanでは、命題Pは`Prop`に属する型として表され、その証明は型Pを持つ項です。ではP → Qの証明には何が必要でしょうか。Pの証明を仮定として受け取り、Qの証明を返す項を構成します。
カーネルが検査するのは、提出された項が宣言された型を持つかどうかです。証明手続きを人が書く場合も、自動化されたタクティクが項を組み立てる場合も、最後の確認を担うのは小さな検査器。証明とプログラムの対応は、数学的な連想にとどまらず、機械検証の仕組みとして実際に働いているのです。
もっとも、これらのシステムが内部で常に「圏」「関手」「自然変換」というオブジェクトを操作しているわけではありません。実装の直接の基盤は依存型理論や帰納型、簡約規則などです。圏論は、それらの型理論に意味を与え、異なる論理体系やモデルの関係を比較する側で重要な役割を果たします。
圏論が与えるのはコード生成ではなく合成の法則
圏論を学んでも、個々のアルゴリズムが自動的に速くなったり、バグのないプログラムが生成されたりするわけではありません。データ構造、計算量、実行環境、ユーザーインターフェースといった問題には、それぞれ固有の知識が要ります。
圏論が力を発揮するのは、異なる構成に共通する合成法則を見つける場面です。mapが合成を保つこと、効果付き計算が結合的に接続できること、証明の接続が関数合成に対応すること。こうした法則が明示されると、部品の交換や式変形を、実装の細部に立ち入らず議論できます。
プログラミングと論理で圏論が語られる理由は、世界中のあらゆる事柄を矢印で表せるからではありません。型の間の関数、計算の順序、仮定から結論への推論が、恒等射と合成という同じ規律を持つからです。共通する範囲を厳密に取り出し、異なる部分は型や効果や論理体系の選択として残す。この節度ある抽象化が、圏論を計算と証明の双方で役立つ言語にしています。