Caty：Jsonic型システムに向けての形式化 - 檜山正幸のキマイラ飼育記 (はてなBlog)

前置きと状況説明を書いたので本題。

JSONベースの型システムは、Catyにとって必須の構成要素です。だいたいのスケッチは出来ていて、実装も進んでいます。それで、細部まで詰めようと思ったら、抜けや矛盾がボロボロ出てきて、…… 今までチンタラ・モンヤリ考えていたのですが、どうもキッチリやらないとダメみたい。

とりあえず形式化（formalize）します。

基本的な記法と構成法

Jsonic型システムは、types as sets の方針で十分なので、型の領域は集合を使います。

集合Aに対して、A^* はクリーネ・スター、つまりAの有限列からなる集合です。長さがnの列の全体は A^[n] と書きます。Aⁿ と書かないのは、列とタプル（直積の要素）を同一視したくないからです。A^[n+1]の要素を、[a₀, a₁, ..., a_n] と書きます。JSON配列と同じ書き方です。

集合Aと集合Bの直積は A×B と書き、その要素は (a, b) と書きます。A² = A×A と A^[2] はまったくの別物と考えます。つまり、A²∩A^[2] = 空集合です。A^[0] は単元集合で、その唯一の要素はです。A⁰ も単元集合ですが、その要素は約束して決めないと不定なので、A⁰ = {null} とします。

なんでnullやねん？ -- Kuwataさんの希望を入れたのです。なんだっていいので、なんかに決めないといけないんですよ。集合Aが何であるかに関係なく、A⁰ は{null}です。したがって、() = null となります。えっ？ nullじゃなくてnilだろう、って？ JSONのなかにnilがないんです。や {} ではどうか？僕はそれでもよかったんですが、Kuwataさんの希望がnullなんで。要するに、ホントになんだっていいいんです！*1

集合Aに⊥（ボトム）を加えた集合をA_⊥とします。つまり、A_⊥ = A + {⊥}、プラス記号は集合の直和。仮に ⊥∈A だったとしても、A_⊥ はAとは異なります。⊥を表すために、unefinedという記号も使います。A_⊥は、オプショナルなAという意味です。A |→ A_⊥ はMaybeモナドで、モナド乗法 (A_⊥)_⊥ |→ A_⊥ があるので、これを使って (A_⊥)_⊥ と A_⊥ を同一視することがあるので注意してください。

集合Aから集合Bへの写像の全体を [A→B] で表します。これは関数集合ですね。[A : B] は、[A→B_⊥] の部分集合で次の性質を満たすものです。

x∈[A : B] ⇔ 有限個のaを除いて、x(a) = ⊥

この有限個のaを a₁, a₂, ..., a_k とすると、x を次の型式で書き表します。



{

 a₁ : x(a₁), 

 a₂ : x(a₂),

  ..., 

 a_k : x(a_k)

}

[A:B] の要素とは、プロパティ名がAに入り、値がBに入るJSONオブジェクトのことです。

今まで出てきた構成法をまとめておきましょう。

A |→ A^* -- 配列を作る
A, B |→ A×B -- タプルを作る
A |→ A_⊥ -- オプショナルを認める
A, B |→ [A : B] -- キーバリュー対のオブジェクトを作る

普遍領域

我々に必要なすべてのデータが入る領域を構成しましょう。

まず、スカラー型データの全体をSとします。それとは別に、プロパティ名の集合をKeyとします。実際のJSONでは、Keyは文字列なので、Key⊆S ですが、この包含関係は仮定しません。シンボル型やアトム型を持つプログラミング言語の型システムににJSONを埋め込むときには、Keyをシンボル／アトムにマップするかも知れません。また、目的によっては、キー（プロパティ名）として使える名前を制限したいことがあります。そこで、KeyとSは独立として話を進めます。

JSONデータ全体からなる領域は、次のように定義できます。

J ::= S | J^* | [Key : J]

すぐ上の書き方は、ひどくイイカゲンな（でも割と使われる）書き方なんで、もう少し詳しく言うと：

スカラー型データはJSONデータである。
JSONデータからなる、任意の長さ（0でもよい）の配列はJSONデータである。
値（バリュー）がJSONデータであるキーバリュー対の集まり（オブジェクト）はJSONデータである。

領域Jは、最初に与えたSとKeyに依存します。ですから、正確には J(S, Key) と書くべきです。Jが2つのパラメータを持つ構成法であることは、後で非常に重要な意味を持つことになります。

さて、Catyの目的からすると、普遍領域Jは狭すぎます。少し拡張します。

Nameを名前シンボルからなる集合とします。とりあえず、Nameは、SともKeyとも独立です。Nameを使って、新しい普遍領域Uを次のように定義します。

U ::= S | U^* | [Key : U] | Name×U

Uの要素を拡張JSONデータと呼ぶと：

スカラー型データは拡張JSONデータである。
拡張JSONデータからなる、任意の長さ（0でもよい）の配列は拡張JSONデータである。
値（バリュー）が拡張JSONデータであるキーバリュー対の集まり（オブジェクト）は拡張JSONデータである。
名前シンボルと拡張JSONデータからなるタプルは拡張JSONデータである。

Jが2つのパラメータを持ったのと同じ事情で、Uは3つのパラメータを持ち、U(S, Key, Name) と書くべきです。特に、Nameが空集合のときはJと一致するので、次のように書けます。

J(S, Key) = U(S, Key, 0) （0は空集合）

Name×U の要素は、a∈Name, v∈U として (a, v) の形をしています。名前シンボルaをこのデータのタグと呼びます。また、Name×U に含まれるデータをタグ付きデータ（タグ付き値）と呼びます。

Xion記法

今、拡張JSONデータと呼んだものは、実は以前に僕がXionと呼んでいたデータ構造とまったく同じものです（Xion関連記事へのリンク集）。

Xionは、スカラーを含むすべてのJSONデータにタグを前置することを許した構文です。



EmployeeList [

 Person {

  "name" : PersonNameJa "板東 トン吉",

  "tel" : TelNo "03-0000-9999",

  "age" : Age 26

 },

 Person {

  "name" : PersonNameJa "園部 ハナ子",

  "tel" : TelNo "04-1111-1111",

  "age" : Age 22

 }

]

タグを単純に前置する構文でもいいのですが、視認性とパージングの容易性を考慮して、タグを丸括弧で囲むことにします。



(EmployeeList) [

 (Person) {

  "name" : (PersonNameJa)"板東 トン吉",

  "tel" : (TelNo)"03-0000-9999",

  "age" : (Age)26

 },

 (Person) {

  "name" : (PersonNameJa)"園部 ハナ子",

  "tel" : (TelNo)"04-1111-1111",

  "age" : (Age)22

 }

]

(PersonNameJa)"板東トン吉" や (Age)26 のような書き方は、プログラミング言語のキャストに似ているので具合がいいという理由もあります。「日本語の名前としての "板東トン吉"」とか「年齢としての 26」と読むことができます。

このXion記法をソフトウェア的にサポートするかどうかは未定ですが、説明用には便利な記法なので、その目的では使います。

これから

これで、最も基本的な枠組みはできました。この枠組みをもとに次のような事項を扱いたいと思います。

パス式
スキーマ定義
バリデーション、コンバージョン
ユーザー定義型
型推論

ただ、ユーザー定義型を扱うためには、今までとは少し別な観点から型システムを議論しなくてはなりません。それは、JSONとは別の（例えばプログラミング言語に備え付けの）型システムとJsonic型システムとの対応をどうやって取るかという話です。

細かい点も含めれば、山のように問題があるんですが、それらのことは次の機会に。

*1:圏論でも、終対象やモノイド単位をdistinguishしなきゃいけないのだけど、なにを選んでも同型になるので、具体的な選択は理論に影響を与えません。