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

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

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

参照用 記事

JSONデータにアクセスするパス式の正しさについて

「厳密分離指向テンプレートエンジン:6月3週」にて、次のように述べました。

  • データ構造と実行モデルは固定されている
  • どんなテンプレート構文も同じ式言語(Expression Language)を使うことになります
  • 計算セマンティクスはひとつしかありません

データ構造とはJSONデータのことです。許される式は、JSONデータの各部にアクセスするパス式に過ぎません。非常に簡単な式なので、型を計算したり、型の立場から“式の正しさ”を検証するのも容易です。実際にどうやるのかを以下に述べます。

内容:

  1. 型に関する基本的なこと
  2. パス式の構文と補助的メタ関数
  3. パス式の正しさ

型に関する基本的なこと

データ型はJSONスキーマの型なので、次の型が基本となります。

  • スカラー
    1. integer
    2. number
    3. string
    4. boolean
  • 複合型
    1. array
    2. object
  • 特殊な型
    1. null
    2. any

JSONスキーマで書いたユーザー定義型も認めます。ここでは、types as sets の立場を採るので*1、「XがYの部分型」とは、Xの値の集合が、Yの値の集合に含まれることです。これを、X⊆Y と書きましょう。例えば、integer⊆number、boolean⊆any 。

xが定数でも変数でも、typeof(x) で型(の名前)が返ってくるとします。typeof が返す型は、事前に与えられた型システムのなかで可能な限り狭い(条件がきつい)ものだとします。どうしても型が不明なら、typeof(x) = any です。

パス式の構文と補助的メタ関数

「厳密分離指向テンプレートエンジン:6月3週」にて:

  1. 数値、文字列、真偽値を表現する定数リテラル: 2, 3.14, "hello", true など
  2. 単なる変数 : count, PI, greeting など
  3. ドット「.」を使ったプロパティ(メンバー、フィールド)参照:item.count, math.const.PI, user.name.given など
  4. ブラケットと番号「[0], [1], [2]など」を使った配列要素の参照:members[12], weeks[1][3], order.cancelled[0] など
  5. ドットとブラケットの組み合わせ:company.people[3].hobbies[0] など。

Eが既に得られた式だとして、構文的には次の形が許されます。

  1. E.x
  2. E[x]

E.x という形を許すのは、xがオブジェクトのキー(プロパティ、フィールド、メンバーの名前)のときです。E[x] は、xが配列の番号インデックスのときです。さらに、JavaScriptのように、Eがオブジェクトでxが名前のときも E[x] を許すとしましょう。

ここで、補助的なメタ関数(説明に使うための関数)を導入しておきます。

  • typeof(x) ⊆ object のとき、Keys(x) は、xのキーの集合
  • typeof(x) ⊆ array のとき、Index(x) は、xのインデックスの集合(整数区間
  • typeof(x) ⊆ integer のとき、IntValues(x)は、xが取り得る値の集合
  • typeof(x) ⊆ string のとき、StrValues(x)は、xが取り得る値の集合

Kyes, Index, IntValues, StrValues は、いずれも集合値の関数です。

パス式の正しさ

E.x の正しさは次のように記述できます。

  1. typeof(E) ⊆ object
  2. typeof(x) ⊆ string
  3. StrValues(x) ⊆ Keys(E)

この3つの条件が判断できるなら、式 E.x の正しさを主張(または否定)できます。

E[x] の正しさは、場合分けして次のように記述できます。

  • typeof(E) ⊆ object のとき
    1. typeof(x) ⊆ string
    2. StrValues(x) ⊆ Keys(E)
  • typeof(E) ⊆ arrayt のとき
    1. typeof(x) ⊆ integer
    2. IntValues(x) ⊆ Index(E)

以上に述べた条件が静的に分かれば、式の正しさを静的に決定できます(アルゴリズム再帰的になります)。完全に決定できないとしても、どこが不明かを指摘できるので、最低限の動的チェックを付け加えることができます。

これは、「ものごとを単純にすれば、正しさの検証が容易になる」事例です。僕がJSONに肩入れする最大の理由は、この「単純だから容易」という特性を持つからです。

*1:ここだけの話です。一般的には、types as sets では素朴すぎてうまくいきません。