型は値の分類器である(意味論的型付け)
Carinaの型付けの様式は、型を「項に付く構文的な札」ではなく「値の集合(値の分類器)」とみなし、型付けを所属判定として与える意味論的型付け(semantic typing)の系譜である。
Γ ⊢ e : T形式の構文的な判断体系はほぼ持たない。代わりに、プログラムを完全評価してから、出てきた値がスキーマ型の表す集合に属するかを判定する。型推論を持つ項ベースの型システムというより、plan生成というコンパイルの最中に全数実行される契約検査(contract checking)に近い、と性格づけるのが正確である。
なぜ値ベースにできるのか
この構成が成り立つのは静的段階が全域的であるためである。評価が必ず停止し、結果がソースとstateだけの関数であるから、「完全評価してから値を検査する」が完全な決定手続きになる。停止しない言語では、そもそも「評価済みの値」が手に入る保証がない。
値ベースであることの配当は篩の述語に現れる。検査はすべて静的段階で評価済みの値に対して行われるため、篩の述語は決定可能性の心配なしに任意の計算を含められる。項レベルで含意を証明しようとすれば決定可能性の壁にぶつかる制約も、値に適用するだけなら走らせれば済む。
完全に値ベースではない
ただし実態はハイブリッドである。静的段階の時点で値が手に入らない参照(他リソースの属性への参照など)に対しては、宣言型どうしの代入可能性を照合する項レベルの検査が補完的に走る。つまり「値がある所では所属判定、ない所では宣言型の判定」という二本立てになっている。
同族
型と値を一つの束に統合したCUEや、スキーマを値の分類器とするJSON Schemaが同族に当たる。Pklも、型注釈に任意の述語を付けて評価済みの値へ適用する方式であり、検査様式だけ見ればこの系譜の中でCarinaに最も近い。
根拠の確度
CUE / JSON Schemaとの同族性の記述はAIの学習データ由来で、一次ソース未確認。意味論的型付けへの対応づけ自体も分析上の主張であり、実装がそう自称しているわけではない。