平坦レコードのインスティチューション
本編「レコードの型階層を合理的に説明できるか」の設定でインスティチューションを作ってみる。用語や記号は本編記事に従う。
指標圏
フィールド名として許されるすべての名前の集合をName（無限集合と仮定）とする。Nameの有限部分集合を指標と呼ぶ。例えば、{name, age}や{name, age, married}は指標である。2つの指標Σ、Σ'のあいだに包含関係 Σ⊆Σ' があるとき、Σ→Σ'の射があるとみなす。{name, age}⊆{name, age, married}だから、射が存在する。この定義で指標圏Signができる。
別な言い方をすると、Powf(Name)をNameの有限ベキ集合とすると、これは順序集合。順序集合はやせた圏なので、圏とみなしたものが指標圏Sign。Signには始対象があるが、終対象はない。Powfの代わりにPowを使えばNameが終対象となる。
モデル圏
指標Σに対して、Record(Σ)を本編と同じ意味で用いる。Σ={name, age}のときは Record(Σ) = Record({name, age}) = Record{name, age}。Mod(Σ) = Pow(Record(Σ))とする。Mod(Σ)は順序集合なので、やはり圏とみなす。
射σ:Σ→Σ'があるとき、関手σ*:Mod(Σ')→Mod(Σ)を次のように定義する； 定義よりΣ⊆Σ'なので、射影Record(Σ')→Record(Σ)が定義できる。この射影を自然に共変拡張してσ*が得られる。y∈Record(Σ')を射影したΣレコードをy|Σと書くことにして、具体的には：
- Y⊆Record(Σ')に対して、σ*(Y) = { x∈Record(Σ) | x = y|Σ となるy∈Yがある}
- Y⊆Y' のとき、σ*(Y)⊆σ*(Y') である。
以上から、Modが指標圏Sign上のインデックス付き圏であることがわかる。σ*は、インスティチューション用語でリダクト関手である。
文集合と充足関係
値の型（ソート）を S = {Never, Void, Null, Boolean, Number, String, AnyValue}とする。記号と対応する値の集合を同一視（記号の濫用）する。
指標Σに対して、a∈Σ、s∈S による a : s という形を文と呼ぶ。Σに対する文の全体をSen(Σ)とする。Σ⊆Σ'なら、Sen(Σ)⊆Sen(Σ')なので、Senは指標圏から集合（包含）圏への関手となる。
XをMod(Σ)の対象とする。つまり、XはRecord(Σ)の部分集合。このとき、X |= 'a : s' とは：
- すべてのx∈Xに対して、x.a ∈ s （sは集合とみなして）
文の集合は {a : s, b : t}のような形に書ける。これをレコードの仕様またはスキーマと呼ぶ。充足関係は、モデル（レコード集合）とスキーマのあいだにまで自然に拡張することができる。
Σ⊆Σ' 、a∈Σ、Y⊆Record(Σ') のとき、σをΣ→Σ'の包含写像だとして：
- σ*Y |= 'a : s' ⇔ Y |= 'a : s'
これはインスティチューションの充足条件である。
スキーマ／セオリーの圏
ソートs, tなどを集合とみなして（記号の濫用をしている）s⊆tのとき、「a : s ならば a : t」のような推論ができる。適当な方法で“レコード論理”（演繹系）を構成したとして、演繹で閉じている文の集合（無限集合許す）をセオリーと呼ぶ。レコードのスキーマ（文の任意の有限集合）が与えられたとき、演繹閉包としてセオリーが定まる。スキーマαのセオリーを[α]と書くことにする。
2つのスキーマα、βに対して、[α]⊆[β]のとき、α≦β とすると、この順序でSch(Σ)（指標Σ上のスキーマ）はプレ順序集合となる。セオリーの集合Theo(Σ)に関しても同様に（むしろより簡単に）順序を定義できる。
2つの型階層
以上で、指標圏Sign上にMod、Sch、Theoのインデックス付き圏の構造が入った。Sch、Theoは同じようなものなので、MoｄとSchを考える。
インデックス付き圏ModとSchの平坦化により、2つの圏ができるが、これが外延的型階層と内包的型階層を与える。具体的には、X⊆Record(Σ)、Y⊆Record(Σ')、α⊆Sen((Σ)、β⊆Sen(Σ')として：
- (Σ, X)、(Σ', Y)が、Σ⊆Σ' であり、Y|Σ⊆X のとき、(Σ', Y)は(Σ, X)のサブタイプである。
- (Σ, α)、(Σ', β)が、Σ⊆Σ' であり、[α]⊆[β] のとき、(Σ', β)は(Σ, α)のサブタイプ（派生スキーマ）である。
この2つの階層は、内包外延双対性により対応する。
