値ベースの全数検査は停止性の配当である
Carinaの型検査は、項(構文)にラベルを付ける体系ではなく、評価済みの値がその型に属するかを判定する様式を取る。これができるのは静的段階が全域的だからで、値ベースの検査様式は停止性の配当として読める。
型理論の分類でいえば、これは型を「項に付く構文的な札」ではなく「値の集合(値の分類器)」とみなし、型付けを所属判定として与える意味論的型付け(semantic typing)の系譜である。型と値を一つの束に統合したCUEや、スキーマを値の分類器とするJSON Schemaが同族に当たる。Γ ⊢ e : T形式の構文的な判断体系はほぼ持たない。
配当が最もはっきり出るのは篩型(refinement types)である。Carinaに「カスタム型」という独立した型構成子はなく、代わりにString / Int / Floatの各変種が
- 正規表現パターン(
pattern) - 長さ・値域の区間(
length/range、両端の省略で開区間を表現) - 任意の検証関数
を持ち運ぶ。これは{ x: String | P(x) }のように基底型を述語で絞り込んだ篩型に相当する。検査はすべて静的段階で評価済みの値に対して行われるため、篩の述語は決定可能性の心配なしに任意の計算を含められる。項ベースの篩型システムなら述語の含意判定が決定可能かを常に気にしなければならないところを、完全評価できる言語はその問題を丸ごと回避する。
ただし完全に値ベースというわけでもない。静的段階の時点で値が手に入らない参照(他リソースの属性への参照など)に対しては、宣言型どうしの代入可能性を照合する項レベルの検査が補完的に走る。つまり実態は「値がある所では所属判定、ない所では宣言型の判定」というハイブリッドである。
配当には限界もある。篩の述語のうち構造的な表現を持つのは区間とパターンだけで、それを超える部分は不透明な関数に逃がしている。述語が一階の表現を持つか否かは、型を直列化してプラグイン境界を越えられるかを分ける線でもある。