このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

Jsonic型システムのコア

雑記／備忘

JSONをベースとした型システムとスキーマ定義を整備しようと思ってます。具体的なスキーマ定義構文の第一候補としては、パス式を基本とした構文を考えています。

他にもスキーマ定義構文は考えられるし、用途によって色々な構文があっていいでしょう。しかし、型システムのセマンティクスが揺らぐのはマズイので、型システムのコアの部分を記述しておきます。「コアの部分」とは、ユーザー定義の型を含まない部分のことです。また、JSONスキーマ属性を使った制限や修飾は、ここでは触れません。

内容：

基本型

基本のスカラー型は次のとおり。（nullもスカラーとみなすことにします。）

  1. integer
  2. number
  3. string
  4. boolean
  5. null

型Sのインスタンスが、必ず型Tのインスタンスであるとき、S ⊆ T と書くことにします。関係「⊆」により、型の全体に階層構造がはいります。

integer ⊆ number は成立しますが、基本スカラー型のあいだにそれ以外の包含関係はありません。null ⊆ string であるプログラミング言語がありますが、JSON仕様のstringにnull（インスタンスとしてのnull）は含まれません。

JSON仕様の構文定義を見ればわかるように、データ表現（リテラル）の最初の1文字から型を決定できます。

最初の1文字 データ型
数字またはマイナス '-' number
二重引用符 '"' string
't' または 'f' boolean
'n' null

numberデータがintegerかどうかを確定するにはさらなる解析が必要です -- これは、integer ⊆ number であることに起因します。

型システムの要件

これから記述する型システムでは、次の2つの判断が確実に出来ることを目標にします。

  1. 与えられたJSONデータxが、特定の型Tのインスタンスである（x∈T）かどうかを判断
  2. 与えられた2つの型S, Tのあいだに、包含関係 S ⊆ T があるかどうかを判断

JSONデータの型式／構文は、既にJSON仕様で与えられているので再論しません。型を書き表すための型表現（type expression）と、上の2つの判断の根拠について述べていきます。既に述べた基本スカラー型（の名前）は一番簡単な型表現であり、所属（インスタンス）関係と包含関係もハッキリと決まっています。

オプショナル型

型Tのオプショナル型は、「値が型Tであるか、または値が出現しない」ことを意味します。配列の項目またはオブジェクトのプロパティの記述では、オプショナル型が必須です。型Tのオプショナル型を正規表現で書くなら T? となります。ここでは、optional [T] という型表現を使うことにします（T? のほうが簡潔でいいですけどね）。optional<T> としない理由は … 特にありませんけど、&lt; って書くのがイヤだから^^; 。

「出現しない」という事態を値undefinedで表すなら、optional [T] の値の領域は T∪{undefined} となります。型（値の領域）T から optional [T] を作る操作（型構成子）は、未定義値を追加することで、いわゆるMaybeモナドになっています。理論的な話では、undefined を表すのに⊥（ボトム）がよく使われます*1。

次のルールがあります。

  1. x∈T ならば、x∈(optional [T])
  2. T ⊆ (optional [T])
  3. S ⊆ T ならば、(optional [S]) ⊆ (optional [T])

値undefinedだけからなる型を、同じ名前undefinedで表すなら、次も成立します。

  • undefined ⊆ (optional [T])

しかし、型undefined が表舞台に現れることはありません（裏では使います）。

配列型

配列型の型表現は次の形を採用します。これが実際のスキーマ定義構文になるかどうかはともかく、説明にはこの型式を使います。

  • array [T0, T1, ..., Tn; T]

T0, T1, ..., Tn, T は既に知られている型表現で、配列の各項目（items）の型を記述します。最後のTは、（0番目から数えて）n番目より先の要素の型をまとめて記述しています。ちょうど(n + 1)個の項目を要求するときは：

  • array [T0, T1, ..., Tn]

長さ0の配列も許すときは：

  • array [; T]

完全な空配列は：

  • array []

上の4つの配列型表現を正規表現で書くなら次のようです。

  • T0 T1 ... Tn T*
  • T0 T1 ... Tn
  • T*
  • ε （εは空列を表す）

与えられたインスタンスが、配列型に属するかどうかの判断は明らかでしょうから述べません。

配列型に関する包含を判断する基準を列挙します。

  1. 配列型と他の型のあいだに包含関係はない（包含関係があるなら、配列型どうし）。
  2. 配列型Sのi番目項目の型をSiとして、Siが定義されているすべてのiに関して Si ⊆ Ti のとき、そのときに限り S ⊆ T である。

ここで多少の注意が必要です。T = array [integer, boolean; string] のとき、すべてのi（i = 0, 1, 2, ...）に関してTiが定義できますが、セミコロンより後に書いてある型はオプショナル型だと解釈します。この例で具体的に書き下すと：

  1. T0 = integer
  2. T1 = boolean
  3. T2 = optional [string]
  4. T3 = optional [string]
  5. 以下同様

下付き添字は書くのが面倒なので、以下では、配列型Tのi番目項目の型を T[i] とします。各iに関してT[i]の型を（undefinedも含めて）指定すれば配列の型が確定します。ただし、次の例のような指定はダメです。

  1. T[0] = integer
  2. T[1] = undefined
  3. T[2] = string
  4. i≧3 なら T[i] = optional [any]

この定義を満たすには、第1（実際には2番目）項目が抜けた配列が必要になります。JavaScriptでは、[5, ,"hello"] のような書き方がOKなのですが、JSONでは「歯抜け配列」は禁止です。（「もう一度、ちゃんとJSON入門」を参照。）

歯抜けはダメ（写真は次男）

タプル型、リスト型

array [T0, T1, ..., Tn] を tuple [T0, T1, ..., Tn] と書いて、タプル型とも呼びます。array [; T] を list [T] と書いてリスト型とも呼びます。

タプル型とリスト型を導入したのは、そう呼んだほうが気持ちが落ち着く人がいるかと思って。それと、プログラミング言語が備えているネイティブのタプル型とリスト型にマッピングするときに便利かも知れません。オリジナルJSONとの互換性を気にしないなら、配列型を廃止して、タプル型とリスト型にしたほうがスッキリすると僕は思ってます。

列挙型

列挙型とは、基本スカラー型、ユーザー定義スカラー型から、値の範囲を有限個に制限した型です。今はユーザー定義スカラー型を考えてないので、スカラー型は integer, number, boolean, null だけです。booleanやnullから列挙型を作っても面白くないですが、（一応用途があるので）特に禁止はしません。値がスカラーでない列挙型は、説得的な導入理由が見いだせないので禁止します。

列挙型を表現するには、enum {1, 2, 3 : integer} のように、値のリテラルと、もとになったスカラー型を書きます（この書き方も、説明に使うだけです）。各リテラルは、元になったスカラー型のインスタンスでなくてはなりません。

与えられたインスタンスが列挙型に所属するかどうかの判断は明らかです。列挙型に関する包含を判断する基準は次のとおり。

  • どのiについても ai∈S ならば、enum {a1, ..., an : T} ⊆ S である。

特に、enum {a1, ..., an : T} ⊆ T は常に成立します。T ⊆ S でなくても、enum {a1, ..., an : T} ⊆ S である例があります。

  • enum {1, 2, 3 : number} ⊆ integer

有限集合型と複数選択型

有限集合型は、オリジナルのJSONスキーマ仕様にはありません。HTMLフォームから送られるデータを記述・処理する都合から導入しました。

型Tの有限集合型*2は、型Tのインスタンスの任意有限個（0個でもよい）からなる集合の型です。値が有限集合なのであって、領域が有限集合である列挙型とはまったく別です。型Tの有限集合型を set [T] と表すことにします。

特に、Tが列挙型のときの有限集合型を複数選択型と呼ぶことにします。複数選択型は頻繁に使われるので、set [enum {1, 2, 3 : integer}] を multi {1, 2, 3 : integer} と略記していいことにします。

有限集合型（もちろん、複数選択型を含む）のインスタンスは、JSON配列で表現されます。ただし、解釈の際には次のルールが適用されます。

  1. 同じ値が2回以上出現しても1回の出現と同じ。[1, 2, 1]と[1, 2]は同じとみなす。
  2. 値の出現順序は無視する。[2, 1]と[1, 2]は同じとみなす。

配列インスタンスに上のルールを適用すれば、有限集合型への所属関係が定義できます。

有限集合型の包含関係には次のルールがあります。

  • S ⊆ T ならば、(set [S]) ⊆ (set [T])

これ以外のルールはないので、S ⊆ T を確認できないなら (set [S]) ⊆ (set [T]) を主張できません。

オブジェクト型 -- 次の機会

残るはオブジェクト型だけだ。

… … 疲れたので次回にします。

*1:⊥の用法はいろいろで、「出現しない」「未定義」以外の意味で使われることもあるので注意してください。

*2:コンピュータで扱える集合はすべて有限だと言えますが、形容詞「有限」を付けておくことにします。