Catyで使う型定義とスクリプトの構文については、「Jcentric型システムの宣言スタイル・スキーマ構文」と「Catyスクリプトの構文」で述べました。意味論はほとんど述べてません。ここで、意味に関するオオザッパな話を少しだけ書いておきます。
デカルト分配圏
意味論を展開する場としては、順序構造が付いたセットイド（posetoids）の圏を考えています。型（型の台領域）がこの圏の対象に、スクリプトがこの圏の射にほぼ対応します。細部では鬱陶しい議論が必要なんですが、この圏にはデカルト積とデカルト和があり、分配法則が成立しているところがミソです。この性質を持つ圏を、デカルト分配圏（cartesian distributive category）と呼ぶことにします*1。
Cをデカルト分配圏として、特定された和と積を+, ×とします。f, gのデカルトペアを（それが作れるとして）<f, g>、余デカルトペアを [f, g] 、射影をπ1, π2など、入射をι1, ι2などで示します。このとき、次の等式群が成立します。
- <f, g>;π1 = f
- <f, g>;π2 = g
- k;<f, g> = <k;f, k;g>
- h:X→A×B として <h;π1, h;π2> = h
- ι1;[f, g] = f
- ι2;[f, g] = g
- [f, g];k = [f;k, g;k]
- h:A+B→Y として [ι1;h, ι2;h] = h
また、分配法則を与える自然同型δ, δ'が存在します。
- δ :A×(B + C) → A×B + A×C
- δ':(A + B)×C → A×C + B×C
積のモノイド性、和のモノイド性、積の対称性、和の対称性、それと分配法則のあいだには一定の関係がありますが、記述が面倒なので割愛します。
Catyスクリプトの同値性
Catyのモデルの基本的な部分の説明をしたことがないので、先走った話になってしまいますが、デカルト分配圏における等式群の対応物を書いてみます。まず、いくつかの注意を。
- α、βなどは、JSONオブジェクトのキー（プロパティ名）です。
- a, bなどは、JSONデータ（むしろXionデータ）のタグです。明示的なタグだけでなく、暗黙のタグも含まれます。
- getv α は、オブジェクトからキーαの値を取り出すコマンド（get value）、射影に対応します。
- putt a は、データにタグaを付けるコマンド（put tag）、入射に対応します。
- ≡ は、スクリプトの実行結果が同じことを示すメタな記号です。
- 型Aに対して a=>A は、Aがタグ（接頭辞）a を持つことを示します。「a=>」の部分は注釈のようなもので、意味はAとまったく変わりません。
では、デカルト分配圏の等式に対応する、Catyスクリプトの関係を以下に。
- {f >:α, g >:β} | getv α ≡ f
- {f >:α, g >:β} | getv β ≡ g
- k | {f >:α, g >:β} ≡ {(k | f) >:α, (k | g) >:β}
- h:X→object {α:A, β:B} として {(h | getv α) >:α, (h | getv β) >:β} ≡ h
- putt a | {a=>> f, b=>> g} ≡ f
- putt b | {a=>> f, b=>> g} ≡ g
- {a=> f, b=> g} | k ≡ {a=> (f | k), b=> (g | k)} （=>と=>>がどのように混じっても成立する）
- h:(a=>A | b=>B) → Y として {a=> h, b=> h} ≡ h
[追記]以下の記述で、間違いと説明不足がありました。とりあえず、「(b=> object {α: A, β: B} | c=> object {α: A, γ: C})」と書いてあったところを「(object {α: A, β: B} | object {α: A, γ: C})」に直しました。これで理屈の上のツジツマはあいます。が、実際には「(@b object {α: A, β: B} | @c object {α: A, γ: C})」じゃないと、実装上は不都合があります。そのへんの説明は長くなるので別な機会にします。[/追記]
分配法則は、例えば次の2つの型のあいだに同型があることを主張します。
- object {α: A, δ: (b=>B | c=>C)}
- (object {α: A, β: B} | object {α: A, γ: C})
入力を出力にコピーするコマンドを cat、配列として与えられた複数のオブジェクトをマージするコマンドを merge とすると、同型の片側は次のように与えられます。
[
{getv α >: α},
getv δ | {b=> {cat >:β}, c=> {cat >:γ}}
] | merge
逆向きの同型は宿題（誰の？）です。
