昨日の記事「集合の添字族とユニオン型とコタプル構成」に少し補足説明を追加します。「指数法則に類似のセクション公式」で説明した、バンドルとセクションなどの概念も関係する話です。
内容：
スキーマと集合の添字族
スキーマとは、「データ型を記述するデータ」だと言えるでしょう。「集合の添字族とユニオン型とコタプル構成」で述べた集合の添字族（以下、「集合族」と表記）は、この意味でのスキーマです。つまり、集合族はデータ型を記述します。ただし、どのようなデータ型を記述するかの解釈は一通りではないのです。
おそらく「集合族は名前付きタプル型を記述する」という解釈が多数派だと思いますが、「集合族は弁別子付きユニオン型を記述する」という解釈もあります。この2つの解釈は双対になっていて、対等な関係にあります。名前付きタプル型と弁別子付きユニオン型の両方を同時に考えることにより、データ型の世界の構造（例えばデカルト半環圏構造）が見えてきます。
集合族の具体例
具体例を出すために、3つの集合（の固有名詞）を定義しておきます。
- Int -- 整数の全体
- Str -- 文字列の全体（文字列が何であるかは前もって定義されているとする）
- NNInt -- 非負整数（non-negative integer）の全体、NNInt = {0, 1, 2, ...}
これら以外の有限集合は列挙により書き下すとします。例えば、Boolean = {true, false}、Undef = {undefined}。
集合族Aは、A:I→Pow(U) の形で与えるとします。ここでU（universal set）は、Int⊆U、Str⊆U、Boolean⊆U、Undef⊆U などとなるように十分大きく取って固定しておくとします。また、集合Xに対して、X? := X∪Undef = X∪{undefined} と書くことにします。undefinedは未定義／非存在を表す特殊な値だとして、x∈X? は「xはXの要素、または、xは未定義」という意味で使います。
さて、集合族の具体例を挙げましょう。添字の集合Iを、I = {"name", "age", "gender"} とします。Iの要素に集合を割り当てるのですが、それは次のように定義します。
- "name" |→ Str
- "age" |→ NNInt?
- "gender" |→ {"male", "female"}?
疑問符（'?'）の意味は先に説明したとおりです。
バンドルのセクションとデータインスタンス
この集合族からバンドルを作ります。E := ({"name"}×Str)∪({"age"}×NNInt?)∪({"gender"}×{"male", "female"}?) として、p:E→I をペアの第1成分を対応させる関数とします。例えば、p(("age", 25)) = "age"。このEとpの組 (E, p) がI上のバンドルを定義します*1。
s:I→E は、"name", "age", "gender" のそれぞれに値を対応させる関数とします。s;p = idI という制限を付けると、それは次の条件となります。
- s("name") は、{"name"}×Str に入る。
- s("age") は、{"age"}×NNInt? に入る。
- s("gender") は、{"gender"}×{"male", "female"}? に入る。
このような条件を満たすsがバンドル(E, p)のセクションです。セクションの例を1つ挙げましょう。
- s("name") = ("name", "坂東トン吉")
- s("age") = ("age", undefined)
- s("gender") = ("gender", "male")
このsは、名前・値ペアの集まりとして、{("name", "坂東トン吉"), ("age", undefined), ("gender", "male")} と書き表してもいいでしょう。あるいは、JSONオブジェクト形式を使って、{"name": "坂東トン吉", "age": undefined, "gender": "male"} とも書けます。undefinedをプロパティの不在として表現するなら、{"name": "坂東トン吉", "gender": "male"} です。
以上のことから、集合族から作られたバンドルのセクションが、名前付きタプル型のインスタンスとなることが分かりました。
配列の場合
集合族 A:I→Pow(U) があるとき、Iは添字の集合と呼んでいました。「添字」は"index"の訳語ですが、インデックスというと、“配列のインデックス”を思い起こす人が多いでしょう。I = {0, 1, 2, 3} と置いて、次のような集合族を考えてみましょう。
- 0 |→ Int
- 1 |→ Int
- 2 |→ Str
- 3 |→ Boolean?
この集合族からバンドルを作ると、E := ({0}×Int)∪({1}×Int)∪({2}×Str) ∪({3}×Boolean?) となります。p:E→I はペアの第1成分を対応させる関数です。このバンドルのセクションsの一例を挙げると：
- s(0) = (0, 32)
- s(1) = (1, -99)
- s(2) = (2, "hello")
- s(3) = (3, undefined)
JSONオブジェクト風に表現するなら、{0: 32, 1: -99, 2: "hello"} です。undefinedに対するプロパティは不在としています。もっと普通の書き方をすれば、[32, -99, "hello"] です。添字（インデックス）を明示しないで並び順の位置を使ってインデックスを暗示します。
この例を見ると、配列、タプル、リスト、名前付きタプル、ハッシュマップ、辞書（ディクショナリ）、レコード、構造体、オブジェクトなどと様々な名前で呼ばれるデータ構造が、適当なバンドルのセクションとして与えられることが分かります。ゴーン（S. Gorn）の定式化を使うとツリー構造もセクションで表現できます。
Iの要素を添字と呼びましたが、データ構造では、インデックス、キー、名前（フィールド名、プロパティ名、フィーチャ名、属性名など）、パスなどと呼ばれます。呼び名が変わっても同じ概念です。用語の多様さよりは、概念の共通性のほうに注目しましょう。
バンドルとしてのユニオン型
バンドルのセクションが名前付きタプル型のインスタンスを与えることがわかりました。そのバンドルは集合族（集合の添字族）から作られます。セクションを考えずに、バンドルの段階でもデータ構造を定義します。これが弁別子付きユニオン型です。
集合族を、名前・集合ペアの集まりで表現しましょう。例えば、先に例示した集合族は {("name", Str), ("age", NNInt?), ("gender",{"male", "female"}?)} と書けます。これから作るバンドルの集合 ({"name"}×Str)∪({"age"}×NNInt?)∪({"gender"}×{"male", "female"}?)、これがまさに弁別子付きユニオン型です。
より現実的な別な例として、{("name", Str), ("userNumber", NNInt), ("email", Str)} という集合族を考えましょう。これから作られる弁別子付きユニオン型は次のようです。
- {({"name"}×Str)∪({"userNumber"}×NNInt)∪({"email"}×Str)
このデータ型の現実的な意味は「ユーザー識別子の型」です。名前の文字列、ユーザー番号の非負整数値、メールアドレスのどれか／どれでもユーザー識別子として使えるという意味です。
Caty（動画）のデータ表現形式（XJSON）では、("name", "坂東トン吉") のように、第1成分が弁別子であるペアを @name "坂東トン吉" の形で書きます。型定義のスキーマでも @name string のような表現を使います。{({"name"}×Str)∪({"userNumber"}×NNInt)∪({"email"}×Str) をCatyの型定義構文で書くと次のようになります。
- (@name string) | (@userNumber integer(minimum=0)) | (@email string)
演算子の優先順位があるので丸括弧を省略しても大丈夫です。
- @name string | @userNumber integer(minimum=0) | @email string
集合論的記法に比べると随分と可読性が向上してるでしょ。でも、意味論は集合論的な表示的意味論、Sets-as-Typesを採用しています。
