「厳密分離指向テンプレートエンジン：6月3週」にて、次のように述べました。
- データ構造と実行モデルは固定されている
- どんなテンプレート構文も同じ式言語（Expression Language）を使うことになります
- 計算セマンティクスはひとつしかありません
データ構造とはJSONデータのことです。許される式は、JSONデータの各部にアクセスするパス式に過ぎません。非常に簡単な式なので、型を計算したり、型の立場から“式の正しさ”を検証するのも容易です。実際にどうやるのかを以下に述べます。
内容：
型に関する基本的なこと
データ型はJSONスキーマの型なので、次の型が基本となります。
- スカラー型
- integer
- number
- string
- boolean
- 複合型
- array
- object
- 特殊な型
- null
- any
JSONスキーマで書いたユーザー定義型も認めます。ここでは、types as sets の立場を採るので*1、「XがYの部分型」とは、Xの値の集合が、Yの値の集合に含まれることです。これを、X⊆Y と書きましょう。例えば、integer⊆number、boolean⊆any 。
xが定数でも変数でも、typeof(x) で型（の名前）が返ってくるとします。typeof が返す型は、事前に与えられた型システムのなかで可能な限り狭い（条件がきつい）ものだとします。どうしても型が不明なら、typeof(x) = any です。
パス式の構文と補助的メタ関数
- 数値、文字列、真偽値を表現する定数リテラル： 2, 3.14, "hello", true など
- 単なる変数 ： count, PI, greeting など
- ドット「.」を使ったプロパティ（メンバー、フィールド）参照：item.count, math.const.PI, user.name.given など
- ブラケットと番号「[0], [1], [2]など」を使った配列要素の参照：members[12], weeks[1][3], order.cancelled[0] など
- ドットとブラケットの組み合わせ：company.people[3].hobbies[0] など。
Eが既に得られた式だとして、構文的には次の形が許されます。
- E.x
- 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 の正しさは次のように記述できます。
- typeof(E) ⊆ object
- typeof(x) ⊆ string
- StrValues(x) ⊆ Keys(E)
この3つの条件が判断できるなら、式 E.x の正しさを主張（または否定）できます。
E[x] の正しさは、場合分けして次のように記述できます。
- typeof(E) ⊆ object のとき
- typeof(x) ⊆ string
- StrValues(x) ⊆ Keys(E)
- typeof(E) ⊆ arrayt のとき
- typeof(x) ⊆ integer
- IntValues(x) ⊆ Index(E)
以上に述べた条件が静的に分かれば、式の正しさを静的に決定できます（アルゴリズムは再帰的になります）。完全に決定できないとしても、どこが不明かを指摘できるので、最低限の動的チェックを付け加えることができます。
これは、「ものごとを単純にすれば、正しさの検証が容易になる」事例です。僕がJSONに肩入れする最大の理由は、この「単純だから容易」という特性を持つからです。
*1:ここだけの話です。一般的には、types as sets では素朴すぎてうまくいきません。
