Catyの型システムの背景とアルゴリズム
http://twitter.com/#!/hiyama_on_caty/status/67728585816948736 とか http://twitter.com/#!/hiyama_on_caty/status/68582156598910976 とかつぶやいてるだけだと後で分からなくなる。
型の代数はブール半環層を係数とする多元環圏
型の表現を台集合Aとその上の述語pの組で表す。(A, p)でもいいが、{x∈A|p(s)} だから {A|p} と略記するといい。さらにはpを係数として p・A、pA と書いてもいいだろう。
台集合の全体、正確には台集合を表現する記号の全体は帰納的な可算集合で：
- neverを含むスカラー型（の記号）が基本記号
- 直積×と∩、∪から作られる式
×、∩、∪に関する代数法則から同値関係が入る。+ を導入すると、×と＋で半環になる（と思ってよい）。型変数を考えない具体型（の表現）なら順序が判定可能で、順序を射と思って圏となる。各台集合（の表現）にスキーマ属性を付けると、スキーマ属性の全体がブール半環（否定のないブール代数）となるから、台集合の包含の圏からブール半環の圏への関手ができる。この関手は貼りあわせ条件を満たすから層になる。
もともと半環だったのだが、ブール半環の層を係数にしたスカラー乗法を入れると、この可換半環（の層）係数の多元環となる。包含順序を射とみなせば多元環圏。
総称型は関手だが、掛け算と足し算から構成されるから多項式関手。複線形関手と定数との足し算で構成されるアフィン複線形関手に対角を組み合わせた形が多項式関手。
型グラフをプログラムと解釈する
型定義モジュール（の一部）を有向グラフとして描いて型グラフと呼ぶことにする。そのノードは：
- define {name, body}
- never 末端
- any 末端
- null, boolean, number, string, binary, tagName 末端
- array {items}
- object {properties}
- tagged {name, val}
- union {choices}
- option {base}
- reference 末端
グラフ構造にとって特に重要なのは、unionによる場合分けとdefine/refereceによる接続。
次の解釈で、型グラフをプログラム（の表現）と考える。
- union → 非決定性の選択だが、タグと値がガード
- option → if-exists-then
- referece → goto
- any → ある種の暴走（乱数選択でもいい）
以上を制御ノードと呼ぶ。それ以外はデータノードでコンストラクタとなる。
型グラフで表現できるプログラムの関して、プログラムAが生成可能なデータ集合をD(A)と書く。プログラムAの任意の挙動をプログラムBが模倣できるなら、Aが生成するデータは必ずBでも生成できる。したがって、D(A)⊆D(B) 。これは受理オートマトンとみなすのとは逆（双対）で、生成装置とみなしている。が、どっちでも同じだろう。
データ集合の包含関係を、プログラムの生成能力の順序に置き換える。生成能力を模倣関係に還元し、最大の模倣関係を「単一化＋ダイクストラ法」で具体的に構成する。というストーリー。
