このブログは、旧・はてなダイアリー「檜山正幸のキマイラ飼育記 メモ編」（http://d.hatena.ne.jp/m-hiyama-memo/）のデータを移行・保存したものであり、今後（2019年1月以降）更新の予定はありません。

今後の更新は、新しいブログ http://m-hiyama-memo.hatenablog.com/ で行います。

型解析：タグ付きJSONパス

型検査 caty

型解析でもJSONパスは大活躍する。JSONパスでは、配列インデックス（非負整数値）とオブジェクトプロパティ名（文字列）により部分構造にアクセスする。インデックス／プロパティ名によるアクセスには、ブラケット記号（'[', ']'）とドット記号（'.'）が使われるが、ここではドットだけを使う。

ドットオンリーのJSONパス

プロパティ名は、原則として引用符付き文字列リテラルとして表現する。次は、JSONパスの例となる。

  • $."foo"."bar baz".2
  • $.0."foo".3."2"

「.2」と「."2"」が違うことに注意。空白や特殊文字を含まず、数値と誤解されない文字列に関しては引用符を省略できるとする。

  • $.foo."bar baz".2
  • $.0.foo.3."2"

以下では、get(data, path) という関数（メソッドではない）で、データの部分構造を抜き出せるとする。また、exists(data, path) は、パスが指す場所に値が存在するかどうかを調べる述語関数だとする。

JSONパスをgetやexistsに渡すときは、"$.foo.\"bar baz\".2", "$.0.foo.3.\"2\"" のように引用符のエスケープが必要である。シングルクォートやトリプルクォートが使えれば、'$.foo."bar baz".2', '''$.0.foo.3."2"''' のように書ける。

タグチェック

@foo のようなタグをJSONパスに挿入できる。次の例を見てみる。



@secretData 

@person {

  "name" : @personName "檜山",

  "contact" : @contactInfo {

    "mail" : @mail "hiyama@chimaira.org",

    "url" : @url "http://d.hatena.ne.jp/m-hiyama/"

  }

}

このデータに対して、通常のJSONパスはタグを無視してアクセスする。

JSONパス 取り出される値
$.name @personName "檜山"
$.contact.url @url "http://d.hatena.ne.jp/m-hiyama/"

JSONパスにタグが挿入されると、データのタグを確認し、マッチしないとエラーにして、さらにタグを取り除いた値を返す。

JSONパス 取り出される値
$@publicData エラー
$@secretData @person { ...}
$@person エラー
$@secretData@person {"name": ...}
$@secretData.name @personName "檜山"
$@secretData.name@personName "檜山"
$@secretData@person {"name": ...}
$.contact @contactInfo {"mail": ...}
$.contact@contactInfo {"mail": ...}
$.contact@contactInfo.mail @mail "hiyama@chimaira.org"
$.contact@contactInfo.mail@mail "hiyama@chimaira.org"
$.contact@contactInfo.mail@url エラー
$.contact.mail@mail "hiyama@chimaira.org"

次のようなワイルドカードパターンがあると便利そうだが、型解析の文脈では関係しない。

  1. @* -- 任意のタグ
  2. @foo? -- @foo またはタグがない
  3. @*? -- 任意のタグ、またはタグがない
  4. @** -- 任意個のタグの連続
  5. @*+ -- 1個以上のタグの連続

条件付きワイルドカード

「#」を数値ワイルドカード、「*」を文字列ワイルドカードに使える。これを精密化して、次のような条件付きワイルドカードを導入する。nは非負整数定数、αiは名前文字列である。

  • #>n -- nより大きいすべての非負整数にマッチ
  • #>=n -- n以上のすべての非負整数にマッチ
  • [^α1, ..., αk] --- α1, ..., αk 以外のすべての名前にマッチ

例：

  • mailAddrs.#>1 -- mailAddrs[2], mailAddrs[3], ... などにマッチ
  • mailAddrs.#>=1 -- mailAddrs[1], mailAddrs[2], ... などにマッチ
  • $@person.[^"name","contact"] -- α≠"name", α≠"contact" である $@person.α にマッチ

注意：ドットの代わりにブラケットを使うと、ブラケットのなかに [^"name","contact"] が入って、ブラケットが二重になる。なんか細工した方がいいかも。

pvalidate関数

Tを型表現として、validate(data, T) が妥当性検証関数とする。validate(get(data, path), T) を pvalidate(data, path, T) とする。ただし、pathにはタグチェックとワイルドカードを含めてよい。

  1. パスのタグチェックに失敗したときは、pvalidateはfalseを返す。
  2. ワイルドカードがあれば、dataに対して有効なパスと、ワイルドカードとのマッチを行い、マッチするすべてのパスに対して検証する。

例えば、pvalidate([0, 1, 2, 3], "$.#>=1", "integer") は次の検証をする。

  1. validate(1, "$.1", "integer")
  2. validate(2, "$.2", "integer")
  3. validate(3, "$.3", "integer")

"$.#>=1" が、"$.1", "$.2", "$.3", "$.4", ... に展開され、実際のデータに対して有効なパス "$.1", "$.2", "$.3" だけがチェックされる。

型解析：細かい注意点

型検査 caty

never型、undefined、型変数の値となる領域

never型はいかなるインスタンスも持たない。never?型の唯一のインスタンスはundefinedと書く。undefinedは意味領域に存在する値だが、表層には出てこない。コマンドの入力にundefinedが入ることはなく、コマンドの出力にundefinedが混じることもあり得ない。undefinedはデータとして受け渡されるものではなく、配列の項目（item）、オブジェクトのプロパティ、タグ付き値のvalの不在の目印となるだけである。存在しない項目／プロパティ／valにアクセスした場合、undefinedが取り出せるわけではなく、例外などのエラーとなる。

型変数は、undefinedを含まない領域を表す。つまり、変数xに対して never⊆x は常に成立する（公理だ）が、never?⊆x は成立しない。変数がそのままでオプショナル型になることはなく、'?'を付けてはじめてオプショナル型になる。よって、T? ⊆ x は、Tが何であっても成立しない。

シングルトン型とnull

単にシングルトン型といえば、シングルトンスカラー型を指す。複合データを1つだけ含むシングルトン型は、シングルトンスカラー型と型構成子から作れる。

シングルトン型はスカラーリテラルによって表現される。つまり、

  1. 数値リテラルはシングルトン型
  2. 文字列リテラルはシングルトン型
  3. true, false, null はシングルトン型

となる。もともと、null値だけからなるシングルトン型がnull型だったので、nullはリテラルと型を同一視する方式に合致している。Catyでは、nullをシングルトンスカラー型として扱う。シングルトンではないスカラー型は、integer, number, string, booleanとなる。

暗黙タグを付与する方法

integer, number, string, boolean, null, array, object は型名として予約されている。arrayとobjectは次の定義を持つと考えてよい。

  • type array = [any*];
  • type array = {*:any?};

一方で、

  • any = (number|string|boolean|null|array|object)

なので、arrayとobjectの定義は再帰的になる（これは余談）。

  • type array = [(number|string|boolean|null|array|object)*];
  • type array = {*:(number|string|boolean|null|array|object)?};

integer, number, string, boolean, null, array, object のインスタンには、型名と同じタグを付けてよい。@integer 3, @number 3.14, @string "hello", @array [1, 2, 3] など。しかし、これらのタグはすぐに消滅してしまい、そのまま維持されることはない。

タグが付いてない値やデータに、どうしてもタグが必要な場合は、予約型名と同じタグ（暗黙タグ）を付与することができる。暗黙タグを付与する作業が必要になるのは、排他的ユニオンの排他性の検査のときだけである。特に、シングルトン型（スカラーリテラル）には次のルールでタグを付ける。

  1. 数値リテラルには、@number を付ける。このとき、@integerは使わない。
  2. 文字列リテラルには、@string を付ける。
  3. true, false には、@boolean を付ける。
  4. null には、@null を付ける。

排他的ユニオンの排他性のチェック

(T1 | ... | Tn) の形をしたユニオンが排他的である条件は：

  • すべての型のタグ（暗黙でもよい）が異なっていること。ただし、@integerと@numberは異なるとは認めない。

成分の型に明示的なタグが付いている必要はない。例えば、次の例は排他的となっている。



type coord = [number, number] 

           | {"x":number, "y":number} 

           | string(remark="座標のテキスト表現");

このcoord では (@array | @object | @string) という3つの暗黙タグが互いに異なる。

新スキーマ構文では、次も許される。



type gender = ("male" | "female");

この例では、(@string | @string) となり、同じタグが含まれる。同じタグを持つシングルトン型をユニオンとして許すため、次の規則を入れる。

  1. ユニオンの成分に同じタグがあってもよい。
  2. ただし、同じタグを持つ型はシングルトン型に限り、それらは互いに排他的（異なる値）でなくてはならない。

シングルトン型またはスカラー型は、次のどれかのタグを持つ； @integer, @number, @string, @boolean, @null。これらのタグを持つ型の排他性は容易に判定できる。例えば、(1|integer), (2|2), (integer|number), (true|boolean) などは排他的ではない例。従来の列挙型、例えば (0|1|2) は、新しい排他性の定義から排他的となる。シングルトン型とスカラー型のあいだに明白な区別はないので、次のようなユニオン型も認める； (integer|false), (0|1|2|null), (number|"+inf"|"-inf")。

型変数が含まれるユニオンは排他性が保証されないので認めない。例えば、(_X|string), (@foo _X | @foo _Y) などは認めない。しかし、(@foo _X | @bar _Y) は排他的だとすぐわかるのでOK。

ユニオンの排他性は、一般の古典論理（∨を含む）を使わず、連言論理だけで型解析を済ませるために必要な条件である。古典論理の計算負担は、∨の多段枝分かれにより、ときに手に負えなくなる。連言論理の範囲内に収めることは効率上重要である。

型解析：雑多な予備知識

型検査 caty

用語法の注意

型検査、型推論、型解析は同義語として使う、特に明確な区別はない。あるCatyスクリプト式（Caty式とも略称）に対する型解析が失敗するとは、否定的な結果を出して解析が成功することである。型解析は、成功する（肯定的な結果を出して終了する）か失敗する（否定的な結果を出して終了する）かのどちらかであり、型解析処理自体が例外を出したり無限走行することはない。（したら困る。）

型解析が“失敗した”場合は、当該のCaty式に、型の不整合があるので、この式は実行されない。型解析は、最初に発見した型不整合の場所と原因を報告することができる。

型解析が成功する場合は、完全に成功するときと条件付きで成功するときがある。条件付きで成功するとは、式内のパイプに実行時型チェック条件が付与されることである。

実行時型チェックを単にチェック、実行時型チェック条件を単に条件と呼ぶことがある。

ほとんどはスキーマ構文領域での話だから、型表現（型項）を単に型、型変数を単に変数とも呼ぶ。値変数はここでは出てこない。

タグ付き値、タグ付き型と言った場合は、暗黙タグのことは考えない。明示タグが付いた値、明示タグが付いた型のことである。暗黙タグに言及するときは、必ずその旨を記す。

記号法と若干の用語

次のようなメタ変数を使う。

  1. a, b など： スカラー定数（リテラル）
  2. x, y, u, v など：型変数
  3. α, β など：プロパティ名、タグ名
  4. E, F など：Catyスクリプト式
  5. A, B など：これもCatyスクリプト式
  6. S, T など：型（の表現、項）
  7. X, Y など：これも型
  8. f, g など：コマンド呼び出し
  9. n, m, i, j など：非負整数
  10. p, q など：JSONパス式

型Tに含まれる変数をVar(T)と書く。Var(S->T) = Var(S)∪Var(T) として、これをプロファイルS->Tの変数と呼ぶ。プロファイルの右辺Tの側にだけ出現する変数を制御不可変数、左辺Sにだけ出現する変数を制御可能変数、両側に出現する変数を伝搬変数と呼ぶ。read-some-file :: void -> _T の _T は制御不可変数である。length :: list<_T> -> integer(minimum=0) における _T は制御可能変数、 first :: list<_T> -> T throws IndexOutOfRange における _T は伝搬変数である。

左辺型と右辺型

型解析では、通常のスキーマ言語の型と少し違う型も使う。プロファイル S->T の左辺に使える型を左辺型、右辺に使える型を右辺型と呼ぶ。

左辺型は、スキーマ言語の型と同じである。左辺型で使える型演算：

  1. [, ] （配列構成、クリーニスター使用可能）
  2. {, } （オブジェクト構成、ワイルドカード使用可能）
  3. @
  4. ?
  5. | （制限有り、排他的）
  6. &

一方、右辺型で使える型演算は次のとおり。

  1. [, ]
  2. {, }
  3. @
  4. ?
  5. ∪ （制限なし）

制限付きの排他的ユニオン演算'|'の代わりに無制限のユニオン（集合の合併、ジョイン）演算∪が使える。インターセクション&は使えないが、これは消去不可能なインターセクション（次節）が使えないことを意味し、消去可能なインターセクションは自由に使ってよい。

消去不可能なインターセクション

インターセクション演算子&は分配法則を使って、式の内側へと移動することが出来る。この計算によって最終的に消えてしまうインターセクションは消去可能と呼ぶ。消去不可能なインターセクションとは、&の左右どちらか（両方かも）が変数であるものである。&は可換演算なので、左に変数があると仮定して一般性を失わない。つまり、x&T の形が消去不可能なインターセクションである。

次の制約を置く。

  • プロファイルの右辺型には、消去不可能なインターセクションを書けない。

この制約は、コマンドプロファイルに対して検査される。コマンドプロファイルの右辺は、インターセクションを持たないか、消去可能なインターセクションだけを持つことになる。消去可能なインターセクションは前もって消去しておくとする。そして、右辺に出現する記号'|'をすべて∪に置き換えておく。

型の分類

型を次の12種に分類する。

  1. never型
  2. any型
  3. シングルトン型（数値リテラル、文字列リテラル、true, false, null）
  4. スカラー型（integer, number, string, boolean）
  5. 配列型
  6. オブジェクト型
  7. タグ（明示的タグ）付き型
  8. オプショナル型
  9. 排他的ユニオン型
  10. インターセクション型
  11. ジョイン型（無制限ユニオン型）
  12. 変数（不定型）

左辺型は、ジョイン型を除く11種、右辺型は、インターセクション型と排他的ユニオン型を除く10種である。変数はさらに、制御不可変数、制御可能変数、伝搬変数で扱いが少し異なる。

パイプ番号と条件

式Eが与えられたとき、そのなかに出現するパイプ記号に1以上の整数で番号を付けておく。この番号は一意識別できればなんでもよく、番号の大小は意味を持たない。特定の式のなかで、1番パイプ、2番パイプなどで特定パイプを指示できればそれでよい。

Eが与えられた式、Aがダミーの式として、便宜上 A | E という式を考えて、Eの左に出現するパイプ（Eのなかのパイプではない）を0番パイプと呼ぶ。0番パイプは「式の入り口」とまったく同じ意味である。

n番パイプに付与された実行時型チェック条件をn番条件と呼ぶ。特に0番条件は入り口条件である。型解析が完全に成功すると、実行時型チェック条件は不要になるが、0番条件だけは別で、多くの場合は0番条件を省略はできない。