久々にモナドの話でも。気が散って基本を疎かにするのも考えものなので、今日は地味な話です。あんまり厳密な記述じゃないですが、気分は伝わるでしょう。
内容：
付点モナドあるいはMaybeモナド
集合Aに、Aには含まれない要素⊥（ボトム、実際には何でもいい）を付け足す操作を考えます。Pt(A) := (A∪{⊥}) と置きましょう。⊥はAに含まれてないので、A∪{⊥} は A + {⊥} とも書きます（「+」は直和の記号）。ときに、A + ⊥ と略記することもあります。
正確に言えば、どんな集合Aをとっても ⊥∈A であってはいけないので、Aごとに⊥Aを選んで、Pt(A) := (A∪{⊥A}) とします。例えば、⊥A = A として、Pt(A) := (A∪{A}) とすれば、A∈A は成立しないことが保証されているので安心です。あるいは、集合 ({1}×A + {2}×{0}) を作れば、(1, a) と (2, 0)（←これがボトム）は異なる要素となります。まー、ボトムの付け足し方は何でもいいのです。
f:A→B に対して、f(⊥A) = ⊥B として拡張した f:Pt(A)→Pt(B) を作ることができるので、拡張したfを Pt(f) とすれば、Ptは集合圏Set上で定義された自己関手になります。これに、A⊆Pt(A) という埋め込みを ηA、それと Pt(Pt(A))→Pt(A) という2個のボトムを1個に潰す写像を μA とすると：
- 関手 Pt:Set→Set
- 自然変換 η::Id⇒Pt:Set→Set
- 自然変換 μ::Pt;Pt⇒Pt:Set→Set
素材が揃いました。これらを組み合わせた Pt = (Pt, η, μ) はSet上のモナドになります。点を1個付加するモナドなので付点モナドと呼ぶことにします。そう、Maybeモナドと同じものです。このモナドのクライスリ圏を Kl(Set, Pt) と書きましょう。
Kl(Set, Pt) の射は（集合圏で考えると）、A→Pt(B) という形の写像です。Pt(B) を開いた形で書けば、A→(B + ⊥B) です。ここで、直和の記号「+」を「:+」という変わった記号に置き換えます； A→(B :+ ⊥)。その理由は、Bと⊥（⊥Bの下付きBは省略）は扱いがまったく異なるからです*1。
f:A→(B :+ ⊥) と g:B→(C :+ ⊥) があったとき、集合圏Setのなかで普通に結合することはできません。f#g := f;Pt(g);μC のような新しい結合 # を定義することによって圏としての性質を回復する、それがモナドに伴うクライスリ構成でした。
例外モナド
付点モナド（Maybeモナド）のボトムは、異常値と解釈できます。異常事態の発生を伝える値なので、例外と捉えることもできます。ただし、「異常事態が起きた」という以外の情報は何も持ちません。これでは不便なので、単元（シングルトン）とは限らない集合Eを使って A :+ E という集合を構成しましょう。記号「:+」は先程と同じで、扱いが異なる2つの集合の直和です。「:+」の左側は正常値、右側は（様々な）異常値です。
集合Eを固定した上で Ex(A) := (A :+ E) とします。f:A→B に対して、E上では恒等として拡張した f:(A :+ E)→(B :+ E) を定義できるので、ExはSet上の自己関手となります。付点モナドのときと同様に、A⊆Ex(A) という埋め込み ηA と、Ex(Ex(A))→Ext(A) というEのコピーを同一視する写像 μA により、モナド Ex = (Ex, η, μ) が作れます。これが、例外の集合をEとした例外モナドです。E = {⊥} とすれば付点モナドになります。
例外モナドは、例外集合Eをパラメータに持つので、正確に書けば ExE のようになります。モナド ExE のクライスリ圏 Kl(Set, ExE) をE（Eのイタリック）と略記します。
例外を含んだ集合 A :+ E は、正常値の集合Aを部分集合として持つので、A⊆(A :+ E) と考えられます。f:A→B in Set は f:A→(B :+ E） in E とみなせるので、Set→E という自然な埋め込み関手があります。この埋め込み関手を J:Set→E とします。J(A) = A です。
随伴の解釈
定義より、E(A, B) = Set(A, ExE(B)) でした。J(A) = A を代入してみると E(J(A), B) = Set(A, ExE(B))。固有名詞Setの個性を消すために、SetをCで置き換えると E(J(A), B) = C(A, ExE(B)) となり、これは、埋め込み関手Jと例外モナドの台関手ExEが随伴となっていることを示します。
しかし、上記の推論は抽象的かつ大雑把（けっこう杜撰）なので、ソフトウエア的な解釈がしにくいですね。インフォーマルではありますが、ソフトウエア的な解釈をしてみましょう。
圏Cは、必ず成功する計算の世界です。Cの射 f:A→B は、型Aの入力（引数）をもらえば必ず型Bの値を正常な計算結果として出力します。一方、圏Eは失敗するかも知れない計算の世界です。Eの射 g:A→B は、成功すれば型Bの値を出力しますが、失敗のときはEに属する異常値により例外を報告します。計算のベースとなる型システムは同じ（と仮定する）ので、|C| = |E| です。
Eの射は必ず失敗するわけではなくて、失敗するかもしれない計算です。よって、Cの射である成功する計算 f:A→B はEの射とみなしてよく、CはEの部分圏（C ⊆ E）です。この「みなし」を J:C→E という埋め込み関手で表しています。一方で、失敗するかもしれない計算 g:A→B はそのままCの射とみなすことはできません。g:A→B は、集合Eに属する異常値（例外）を返す可能性があるからです。
正常値Bと異常値Eの組み合わせを A :+ E と書いたのでした。g:A→B in E は、g:A→(B :+ E) です。「:+」の右が異常値の集合です。さて、正常・異常の区別をなくした単なる直和集合を B + E と書くことにして、B :+ E を B + E に変換すれば、異常終了したEの計算もCの射とみなせます。
Eの対象としてのB（暗黙に例外を含む）を、Cの対象としての (B + E) に変換する操作をCatchとすると、
- E(A, B) = C(A, Catch(B))
というホムセットの同型が成立します。g∈E(A, B) は失敗する（例外を起こす）かも知れない計算です。そういう計算gをtryブロックに入れて保護すると、try{g}:A→Catch(B) という失敗しない計算になります。g |→ try{g} という対応が、E(A, B) → C(A, Catch(B)) のホムセット同型を与えるものだったのです。
一般の場合
前節の説明では、埋め込み関手 J:C→E に対する右随伴関手を、“Catch”というプログラム的な連想が働く名前で表しました。J(A) = A ですが、Jも明示するなら、
- E(J(A), B) → C(A, Catch(B)) （ホムセット同型）
となります。
より一般的に、Q:C→E、P:E→C が随伴対 Q -| P なら、ホムセット同型写像 E(Q(A), B) → C(A, P(B)) が存在します。この同型写像を φA,B とすると、φA,B(g:Q(A)→B in E):A→P(B) in C となります。
例外モナドのときは、φA,B(-) がtryブロック tryA,B{-}:A→Catch(B) で表現できたわけです。一般的なモナドのときも、特殊なブロック構文 specialA,B{-}:A→P(B) により、別な（しかし関係する）圏Eの射をCに持ち込むことができます。このようなブロックは、役に立つプログラム構成素になるように思えます*2。Cから見れば、ブロック special{-} の内部には別な世界Eの射が入ります。ブロックの入り口と出口で型のズレが発生しますが、そのズレは随伴関手で統制されているものですからキチンと処理可能です。さらに、special{-} をもう一度Eに埋め込むことも可能です。
今日は、例外モナドから誘導される随伴関手以外の例を出しませんが、目をこらしてみると、随伴関手はたくさんります。
