部分写像の圏、単元例外処理とか
集合圏、部分写像の圏、関係圏は一緒に考えて互いに比較するといいようだ。今の焦点は部分写像の圏。
まずは、モナド、つうか随伴関手対と共に考える。Set上のモナドAugを考える。Augはaugmentation（増加、増強、増大、添加物、拡大）のことで、付点モナドとする。これは次のようにも呼ばれる。
Aug:Set→Setのクライスリ圏は、
- 部分写像（partial function/mapping）の圏
- 例外（エラー）付き写像の圏
- 無限走行（非停止 non-terminating）するかもしれない手続きの圏
- 特定特殊な値を出すかもしれない関数の圏
などの解釈を持つ。ここでは、部分写像または例外付きの手続きの圏とみなす。
J:Set→Partialを自然な埋め込みとして、J(Set) = Tot ⊆Partial とする。部分圏Totの射は、
- 厳密射 strict morphism
- 全域射 total morphism
- 純射 pure morphism
- 無例外射 noexcept morphism
などと呼ばれる。
Totz（totalize）を Partial→Set という写像とすると、
- Set(A, Totz(Y))
Partial(J(A), Y)
なので、J -| Totz 。この随伴対によるSet上のモナドが Aug := J;Totz、そのクライスリ圏がPartial。Totz;J :Partial→Partial はPartial上のコモナドの台関手となる。これをLiftとする。Lift:Partial→Partialの対象部分は、Augの対象部分と同じで、集合への付点操作となる。AugとLiftは極めて類似しているので、混同や同一視がされるが、ここではちゃんと区別する！
J:Set→Partial はクライスリ圏のクライスリ埋め込みとなるが、Setがデカルト圏なのでフレイド圏となる。通常のフレイド圏よりは強くて、外側の圏Partialが直積（圏的直積に非ず）に対してモノイド圏になっており、さらに共通の直和（圏的直和）を持つ。
- Jは、フレイド圏の構造関手である。
- 基礎圏Setは、直積に関してデカルト圏で、直和と共に半環圏である。
- 外の圏Partialは、直積に関してモノイド圏で、直和と共に半環圏である。
- Jは、半環圏の準同型関手になっている。
- Jは、随伴の相方Augを持つ。
η::Id⇒Aug:Set→Set を付点モナドの単位とする。埋め込みJでηを成分ごとに移した族をη'とする。Jは対象上で恒等なので、n'::Id⇒Lift となる。
f:A→B in Partial に対して、Try(f) := η'A;Lift(f) とする。
- Try(f):A→Lift(B) in Partial
となる。これは、Partialを単元例外付き手続きの圏とみてのtryブロックとなる。Try(f)はfがなんであってもTotに入るので、Try(f)∈Tot。
h:Lift(B)→B を例外ハンドラと呼ぶ。Try(f);h がtry-catch構造に対応する。h∈Totなら、Try(f);h もTotに入る。Lift(B) = B + {⊥} であることから、h = [hnormal, hexcept];∇B と書ける。ここで、hnormal:B→B、hexcept:{⊥}→B、∇Bは余対角。
h:Lift(B)→C in Partialを一般化例外ハンドラと呼ぶ。tryブロックと一般化例外ハンドラを組み合わせると、(f:A→B)|→(g:A→C) という圏的操作を定義できる。これを（一般化）例外ハンドリングと呼ぶ。
2 = 1 + 1 として、直和の標準入射を使って、false:1→2, true:1→2 を定義して、(2, false, true) を二値真偽構造だとする。述語 p:A→1 in Partial に対して、+p := try(f);[true, false] ; A→2、-p := try(f);[false, true] ; A→2 として、一値の述語を二値の正論理項と負論理項に対応付けることが出来る。論理演算は、2→2 として定義できる。
等式的論理は、対角の双対であるコンパレーター γA:A×A→A in Partial を使って展開できる。コンパレーターは例外を出す（部分性を持つ、値がないかも）が、例外ハンドリングを使って二値真偽値2への射に調整可能。
注意すべき点：
