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

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

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

参照用 記事

Caty:静的型検査の方針と枠組み

型推論」とか「静的型付け」とかいうと若干違うな、という気がするので「静的型検査」という言葉を使うことにします。とはいえ、なりゆきで型推論、静的型付けと言うこともあるでしょうが。

Catyスクリプトの構文と意味は「Catyのインタプリタ=評価関数の表示的意味論」で記述しました。実用上の要求からもう少し機能が拡張されていますが、エッセンスはあれで尽くされています。

スクリプト構文とは別に、Catyのスキーマ言語において型表現(type expression, type term)の構文が定義されています。以下、Eは式(スクリプトコード)、Sは型表現、xはJSONデータとします。

内容:

  1. 安全性と許容可能性
  2. 実行時型検査
  3. 静的型検査と実行時型検査
  4. 常に100%実行時型検査の意義

安全性と許容可能性

まずは、非形式的/直感的な議論から; 型Sに属する任意のデータxに対して、Eval(x, E) が成功することが事前に分かっているとき、式Eは型Sに対して安全である(safe)ということにします。型Sに属するデータxをうまく選べば(あるいは運が良ければ)、Eval(x, E) が成功することが事前に分かっているとき、式Eは型Sに対して許容できる(addmissible; 許容可能)ということにします。

Eが(あるSに対して)安全でないときは、評価が失敗する可能性があります。Eが許容できない(「許容できる」の否定)のときは、評価は必ず失敗します。システムは、安全なEを受け入れ、許容できないEは排除します。安全ではないが許容できる式の扱いは、運用方針とかその場の状況で決めることになるでしょう。

上記の安全性も許容可能性も、まったく曖昧ですが、これをできるだけ厳密に定義して、機械的な証明アルゴリズムを構成/実装するのが目標となります。

実行時型検査

実行時型検査は、静的型検査と性格が異なります。

  1. 式全体に関して検査はできない。検査の対象はコマンド呼び出しである。
  2. 型に対する検査ではなくて、インスタンスデータに対する検査となる。
  3. したがって、安全性、許容可能性の概念は定義できない

xをJSONデータインスタンス、fがコマンド呼び出しのとき、入力xがコマンド呼び出しfに対して適切であるかどうかを判断するのが実行時型検査です。コマンド呼び出しは、プロファイル(入力型と出力型の仕様)を持つので、それを S -> T としたとき、次の検査をします。

  • インスタンスデータxは、型Sに所属するか。(事前検査)
  • Eval(x, f) は、型Tに所属するか。(事後検査、通常はコマンドを信用して省略*1

実行時型検査は、コマンド呼び出し単位の検査なので、式全体を検査するには一般に複数回の検査が必要になります。式に対して何回の実行時型検査が必要になるかは、正確にかつ簡単に評価(estimate)できます。

入力xとコマンド呼び出しfに対して Eval(x, f) が成功することを、呼び出しfはデータxに対して適用できる(applicable; 適用可能)ということにします。実行時型検査は、呼び出しごとに適用可能性を判断する検査です。

データxと式E(閉じた式とする)が与えられれば、最初に実行すべきコマンド呼び出しは決定できるので、それを first(x, E) とします。first(x, E) を実行した後に実行すべき残りの式(文脈とか継続みたいなもの)を rest(x, E) とします。次が成立します。

  • Eval(x, E) = Eval(Eval(x, first(x, E)), rest(x, E))

コマンド呼び出しfに対する Eval(x, f) は、Native(x, f) だったので、

  • Eval(x, E) = Eval(Native(x, first(x, E)), rest(x, E))

Nativ(x, f) の入り口に「fがxに対して適用可能か」を検査するコードを挿入したものをCheckedNativeとします。CheckedNativeを呼び出すように変更したEvalをCheckedEvalとすれば、

  • CheckedEval(x, E) = CheckedEval(CheckedNative(x, first(x, E)), rest(x, E))

これが、実行時型検査の正体です。実装上は、EvalとCheckedEvalを別々に作るより、モードフラグを参照して実行方法を切り替えることになるかもしれません。

静的型検査と実行時型検査

静的型検査は、次の2つの判断を行います。

  1. 式Eは、型Sに対して安全か。
  2. 式Eは、型Sに対して許容可能か。

一方、実行時型検査は、次の判断を行います。

この2つの検査の関係を述べましょう。準備; データ(定数リテラル)xに対して、sing(x) は、xだけを含むシングルトン型だとします。便宜上、sing(x)も型表現として使えるとしておきます。

静的型検査/実行時型検査の使い分けの原則は次のとおりです。

  1. 式Eが、型sing(x)に対して安全なら、Eval(x, E) の実行時型検査は不要である。
  2. 式Eが、型sing(x)に対して許容可能なら、Eval(x, E) の実行時型検査が必要となる。

許容可能でない式は、常に失敗するので実行(評価)する意味がありません。

静的型検査では、安全性/許容可能性の定性的な判断だけでなく、実行時型検査を必要とする場所を完全に特定する必要があります。式Eの静的型検査により、実行時型検査の挿入位置をマークされた(または検査コードが埋め込まれた)式をE'とすると、E'は次の特徴を持ちます。

  • 評価が成功するときは、Eval(x, E) と Eval(x, E') は同じ。
  • Eval(x, E) が失敗するなら Eval(x, E') も失敗する。逆も成立する。([追記 date="翌日"]これが言えるには仮定が必要です。その仮定はそのうち明確にします。[/追記]
  • ただし、E'の失敗は実行時型検査コードによる例外であり、コマンド呼び出しによる型エラーは発生しない

コマンドが、型とは無関係なエラー(例えばIOエラー)を起こせば、式は失敗しますが、これは型検査の範疇外です。ただし、例外も型システム/型検査に含めることにより、宣言された例外の発生を「成功」とみなすことができます。

常に100%実行時型検査の意義

静的型検査の如何<いかん>に関わらず、実行時型検査をフルで行うことも可能ですし、それには次の意義があります。

  • 静的型検査にバグがあっても、二重の検査をすれば安全性が高まる。
  • コマンド(ネイティブコマンド)の間違いを検出できる。

静的型検査にバグはないと仮定して、静的型検査済みのコードが意図せぬ所で実行時型検査に引っかかれば、それはコマンド宣言とコマンド実装が食い違っています。つまり、静的型検査と100%実行時型検査の併用は、コマンド宣言とコマンド実装のテストに使えます。

Catyのポリシーである「人間の間違いをできるだけ検出する」から言えば、運用時であっても100%実行時型検査をオンにしておくのが望ましいと思います。

*1:これはまた、コマンドを信用しないなら事後検査も実施することを意味します。