「=」は代入演算子だとして、次のような関数呼び出しを考えてみます。
- f(y = x + 1, x + y)
変数xの値が2, 変数yの値が5の状況を例とします。引数を左から右の順で評価するなら、関数に渡る実引数は f(3, 5) となり、f(x + 1, x + x + 1) と変わりません。最初のyの値は破壊されます。一方、引数の評価が逆順、右から左なら、f(3, 7)、つまり、f(x + 1, x + y) となります。
(y = x + 1, x + y) を式のタプルと見ると、タプル成分の評価順序を決めないと値が確定しません。このような状況も含めて、圏論により計算をモデル化をする試みが次の論文に載っています。
- Title: Cartesian effect categories are Freyd-categories
- Authors: Jean-Guillaume Dumas, Dominique Duval, Jean-Claude Reynaud (2009)
- URL: http://hal.archives-ouvertes.fr/docs/00/39/48/54/PDF/seqArxivV3.pdf
- Pages: 23
[追記]arXivにもあります。http://arxiv.org/abs/0903.3311[/追記]
いつものごとく、ザッと斜め読みしただけでろくに理解してないのですが、僕の問題意識の観点から、内容の一部を紹介をします。原論文の忠実な解説にはなってないし、誤解しているおそれもあることはご了承ください。一度に紹介するのは無理なので、今回は実例を1つだけ。続きがあると思います、たぶん。
内容：
はじめに
これは使える
僕は不純な計算が好きだし、必要性があると思っています（「不純な計算科学」を参照）。部分性、例外、状態遷移、ストレージとのIO、非決定性、無限走行などを排除して、実用的な計算が出来るとは思えないのです。
冒頭に挙げた例のように、F、Gが何らかの式だとしてペア (F, G) を考えると、FとGが純関数型の式（項）なら、FとGのどちらを先に評価するかを気にする必要はありません。しかし、F, Gの評価の最中にメモリ状態を書き換えたりファイルIOをすると、評価順序が結果に影響します。このような評価順序依存性は、たいていの不純計算では避けられません。
"Cartesian effect categories are Freyd-categories" で述べられている方法は、不純計算を扱うのに使いやすい枠組みだと思います。圏論としては珍しい概念や記法が多いのですが、これらの概念・記法は実際のプログラムと直接的に対応するものです。まだ十分に洗練されてない印象もありますが、実用性は高いし、僕はすぐ実用に使うつもりです。
「これは使える」「いいものみっけた」という感じ*1。
作用圏を使う方法を一言でいえば
作用圏（effec category）とは、圏Kとその部分圏Cの組 (K, C) で、ある条件を満たすものです。外側の圏Kによりプログラム（による計算）をモデル化します。部分圏Cに含まれる射は、取り扱いやすいプログラムを意味します。典型的な状況としては、Kの射は副作用を持つかもしれないプログラムで、Cの射は純関数型プログラムというのがあります。
「副作用」（side effect）はよく使われる言葉ですが、副作用が主たる目的であることも多いので、「副」を取り払って単に「作用」としましょう。作用圏 -- これは、計算作用（computational effect）を圏論的に定式化する枠組みとして命名されたのでしょう。作用を定式化するには、相対的に「作用を持たない射」を明確にする必要があります。その作用を持たない射を集めた部分圏がCです*2。
単一の圏ではなくて圏の組を考えるのは最近の傾向のようです。"Cartesian effect categories are Freyd-categories"でも言及されているフレイド圏（Freyd category）、Arrowsは、外側の圏と部分圏を考えるので、圏の埋め込み J:C→K を使っています。ニック・ベントン（Nick Benton）の線形非線形圏（linear non-linear category； http://hal.archives-ouvertes.fr/docs/00/15/42/29/PDF/catmodels.pdf などを参照）では、随伴で結ばれたデカルト圏と対称モノイド閉圏を使っています。フォックス（Fox）の定理（http://d.hatena.ne.jp/m-hiyama-memo/20080823/1219466252 に断片的記述）の文脈では、対称モノイド圏とその内部コモノイドの圏を一緒に考えます。
非可換代数（非可換多元環）を考えるときでも、係数域（スカラー）には可換環／可換体を取るのと似たような感じもします。一般性がある圏Kをモデルに使いますが、それだけだと扱いにくいので、なんらかの“可換性”を持った圏Cを基礎として採用するという構図のようです。
部分関数の例
基礎概念はこんなもの
部分関数（partial function, partial mapping）の圏を例として作用圏の基礎概念を紹介します。それらは次に挙げるものです。
- 純射（pure morphism）
- 純終対称（pure terminal object） 1
- 射の作用（effect） Eff(f)
- 同作用関係（same-effect relation） 〜
- 両立関係（consistency relation） ◇
- 制約関係（constraint relation） ＜|
- 作用圏の基本条件
原論文とわずかに用語・記法を変えたので、それを注意しておきます。
- 射fの作用は、花文字のEを使ってますが、ここでは Eff(f) とします。
- 同作用関係は、イコールをニョロンにした形ですが、ここでは一本棒のニョロン 〜 にします。
- 両立関係と制約関係は、どちらも同じ言葉 consistency を使ってますが、分かりにくかったので、制約と両立に分けました。
- 制約関係（もとは両立関係の一種）の記号は左がとんがった三角形です。代用に ＜| を使います。|＞ は右がとんがった三角形の代用。
- 両立関係は、2つの三角形を並べた形状でしたが、◇ で代用します。
以下で述べる部分関数の例では、「作用」「同作用」という言葉に違和感があるかもしれません。次に述べる（であろう予定の）状態遷移の例ではピンと来ると思います。作用圏は、非常に広い範囲の実例を持つので、一般的な用語法がいつでもピッタリ当てはまるとは限らないのです*3。
部分関数と全域関数
では、実例紹介に入りましょう。
部分関数（部分写像）は、(X, Y, D, f) の4つ組で決まるものです。X, Y, Dは集合で、D⊆X、fはDからYへの関数（写像）です。記号の乱用ですが、f = (X, Y, D, f) とも書きます。集合Dはfの定義域（domain of definition）なので D = DD(f) と書くことにします。dom(f) = X, cod(f) = Y、その他適切に定義して、部分関数の圏を作ります。
こうして作った、「集合を対象、部分関数を射とする圏」をKと置きます。f = (X, Y, D, f) が全域的であるとは、D = X のことです。全域関数は部分関数の特殊なもので、全域関数どうしの結合もまた全域関数なので、集合と全域関数の全体はKの部分圏となります。これをCと置きます。Cは集合圏Setと同じ圏です*4。
作用圏の用語を先走って使って、とりあえず、Cの射を純射と呼びます。Cは純射からなる部分圏なので純部分圏、あるいは純圏と呼んでもいいでしょう。特定の単元集合を1つ選んで1とします。1は、純部分圏Cの終対象となります。注意すべきは； 1はKの終対象とはならないことです。例えば、1→1であるKの射、つまり部分関数は2つあります。Cの射、つまり全域関数に限定すれば、1→1 である射は1つだけです。1は純終対象と呼びます。
ここらで、状況を中間的にまとめておくと：
- 圏Kとその部分圏Cがある。Cに属する射は純射と呼ぶ。
- 部分圏Cは、Kの広い部分圏（{broad, wide} category）である。つまり、|C| = |K| 。広い部分圏の話は「包含付き圏：対象を集合っぽく扱うために」とか「骨格的な圏と圏の骨格」にもあります。
- 部分圏Cには終対象1が存在する。ただし、1がKの終対象である必要はない。1を純終対象と呼ぶ。
部分関数の作用＝定義域
作用圏の枠組みで、射fの作用 Eff(f) を定義します。ですが、部分関数の例では、Eff(f) は DD(f) と事実上同じです。あんまり「作用」という感じはしないのですが、一般的に Eff(f) は、fが純射と違っている度合いを示すものです。DD(f) を見れば「fが純射かどうか、純射とどの程度へだたっているか」がわかるので、「純射と違っている度合い」にはなっています。
XをKの対象とします。Cは広い部分圏なので、XはCの対象でもあります。純終対象1はCの終対象なので、X→1 という純射は一意的に定まります。これを !X:X→1 と書きます。（!X はよく使われる記法ですが、原論文では <>X でした。）
f:X→Y がKの射（任意の部分関数）だとして、f に !Y を後結合（post-compose）した f;!Y:X→1 をfの作用と呼び、Eff(f) と書きます。この定義 Eff(f) := f;!Y:X→1 は作用圏一般で通用するものです（まだ、作用圏の定義が完了してませんが）。
全域関数 f:X→Y に !Yを後結合すると、関数値の区別がなくなってしまいます。つまり、f≠g でも Eff(f) = Eff(g) = !X となります。しかし、fが部分関数の時は、Eff(f) に情報が残っています。一般に、X→1 である部分関数はイッパイあるので、Eff(f) には、X→1 で識別できる特性が含まれます。
Eff(f) に残るfの特性とは、つまりは定義域（または未定義域）の情報です。なんでそうなるかは、自分で具体的に確認してみてください。
ここで、作用圏一般で通用する定義を2つ導入しておきます。f, g:X→Y in K だとして：
- Eff(f) = Eff(idX) のとき、fは無作用（effect-free）という。
- Eff(f) = Eff(g) のとき、fとｇは同作用だといい、f 〜 g と書く。
部分関数の例では、無作用な射は全域関数になり、純射と同じことです。2つの部分関数が同作用だとは定義域が一致することに他なりません。
両立関係と制約関係
圏の射fとｇが共端（parallel）であるとは、dom(f) = dom(g) かつ cod(f) = cod(g) のことです。両立関係と制約関係は、共端な射のあいだにだけ定義される関係（ホムセットごとに定義される関係）です。以下では、いちいちこの事に言及しないこともあるので注意してください。
f, g:X→Y が圏Kの射、つまり部分関数だとして、定義域の共通分 DD(f)∩DD(g) では一致するとき、fとgは両立するといい、f ◇ g と書きます。fとgが両立するなら、定義域の合併 DD(f)∪DD(g) まで自然に延長した部分関数を定義可能です。
u:X→Y が純射、つまり全域関数で、f:X→Y が射（一般の部分関数）のとき、fが、uの定義域Xを制限した形をしているとき f ＜| u と書き、fはuで制約されているということにします。
定義から、f ＜| u は、f ◇ u と同じ関係だとわかります。ですが、制約関係を先に導入して、両立関係を制約関係を使って定義することもできます。次のような定義を採用するのです。
- f ◇ g とは、f ＜| u かつ g ＜| u となる u が存在すること
論理記号を使えば、次のとおり。
- f ◇ g ⇔ ∃u.( (f ＜| u) ∧ (g ＜| u) )
一般の射と純射のあいだの制約関係 ＜| があれば、それを使って両立関係 ◇ を定義できます。制約関係をより基本的なものとして扱うことにしましょう。
基本条件と作用圏の定義
圏Kと純射からなる部分圏Cがあり、純終対象1と制約関係 ＜| が存在するような状況を考えます（部分関数の実例はそのような状況を与えます。）この状況では、同作用関係 〜 と両立関係 ◇ が定義できます。この2つの関係によって、射の同一性（equality）が導出されると好都合です。この要請は、次の形で述べることができます。
- 任意の共端なf, gに対して、(f 〜 g) ∧ (f ◇ g) ⇒ f = g 。
この条件*5が、作用圏の定義に含まれる基本的な公理となっています。これは、純射との隔たりが同じであり、同一の純射で制約されるなら、同じ射だということです。純射を基準にして、射の同定ができることを表しています。
部分関数の例では、f 〜 g とは、fとgの定義域が同じことです。f ◇ g とは、fとgの共通定義域では一致する関数になっていることです。この2つが成立するなら、確かに f = g です。
ここで一般の作用圏の定義を述べます。部分関数の例を思い起こせば、唐突な定義ではないでしょう。
- 圏Kとその部分圏Cがある。
- CはKの広い部分圏となっている。
- Cには終対象1が存在する。
- 一般の射（Kの射）と純射（Cの射）のあいだに制約関係 ＜| が定義されている。
制約関係の公理がありますが、今は割愛します（特に難しくはありません）。(K, C, 1, ＜|) が作用圏であるとは、純終対象1と制約関係 ＜| を使って定義された 〜、◇ に関して次の条件を満たすことです。
- 任意の共端なf, gに対して、(f 〜 g) ∧ (f ◇ g) ⇒ f = g 。
基本条件に関する重要な注意
作用圏の基本条件は、「(f 〜 g) ∧ (f ◇ g) ⇒ f = g」であり、逆向きの「f = g ⇒ (f 〜 g) ∧ (f ◇ g) 」は含まれません。「f = g ⇒ (f 〜 g)」は言えるので、「f = g ⇒ (f ◇ g) 」が必ずしも要求されないことになります。特に、「f = f ⇒ (f ◇ f) 」が保証されず、両立関係◇は反射性を持ちません（持たなくても許されます）。
f◇f の定義は、∃u.(f ＜| u) なので、fを制約する純射が存在することと同じです。作用圏の公理には ∀f.∃u.(f ＜| u) が入ってません。そのため、f◇f の導出はできないのです。
部分関数の圏から作った作用圏では、∀f.∃u.(f ＜| u) が成立します。これが成立しない例を挙げましょう； 部分関数 (X, Y, D, f)を位相空間の圏で考えます。D⊆X で、DはXの開集合とします。fはD上の連続関数だとします。(R, R, {x|x > 0}, f = λx.(1/x)) とすると、この部分関数を制約する純射（全域連続関数）はありません。計算可能関数の圏でも同様の現象があります。
∀f.∃u.(f ＜| u) は純射が十分たくさんあることを意味していて、成立していればとても助かります。しかし、多くの事例をカバーするにはきつすぎる条件ということなのでしょう。
デカルト作用圏とプログラムのモデル
プログラムのモデルを作る際に、タプルデータがないのは辛いですよね。タプルを導入するということは、デカルト圏で考えることです。作用圏(K, C)の純部分圏Cをデカルト圏としたものがデカルト作用圏（Cartesian effect category）です。ただし、Cだけにデカルト構造を入れても整合性が取れないので、外側の圏Kにも弱いデカルト構造（デカルトもどき構造）を入れます。
外の圏Kに入るデカルト積に類似した積が順次積（sequential product）です。冒頭で例に出した (y = x + 1, x + y) というタプルは順次積*6として解釈できます。順次積の定義は圏論的になされますが、順次積の性質はプログラマにはお馴染みであり、直感的に理解可能なように思えます。プログラミングで実行順序に気を使うのは当たり前のことですから。
作用圏を使う方法は、道具立ては若干大げさですが、現実のプログラム、日常のプログラミングとの対応が取りやすいのがメリットでしょう。今回は部分関数の例を紹介しましたが、状態遷移の例では、さらに現実のプログラムとの対応が鮮明です。
順次積は、より基本的な“積”から定義されるのが普通です。"Cartesian effect categories are Freyd-categories"では、半純積（semi-pure product）、バイノイド積（binoidal product）、クライスリ積（Kleisli product）などのさまざまな“積”を導入しています。デカルト積や一般のモノイド積が、非対称であっても可換なフレーバーを持っていたのに対して、これらの新しい積は本質的な非可換さを持っています。プログラムによる作用は多くの場合に非可換なので、プログラムのモデルに非可換性を取り入れるのは当然だと思います。
デカルト作用圏によるモデルは、非可換なモデルとしては初等的なのでしょうが、今までうまく定式化できなかったプログラムの挙動を（ある程度は）表現してくれそうです。これ、面白いですね。
