判定できない部分型は、拒否も受理もせず実行時の検査に回す(hybrid type checking)
{x: Int | x > 0}のような篩型(refinement type)に任意の述語を許すと、部分型判定{x: B | p} <: {x: B | q}は「pならばq」という任意の述語の含意判定になり、決定不能になる。普通の型検査器は部分型を「証明できた → 受理」「反証できた → 拒否」の二値で扱うが、表現力の高い型ではどちらも言えない場合が残る。
Flanaganのhybrid type checkingは、この3つ目の場合の扱い方についての提案である。
3つの結果と、「分からない」の3つの扱い
含意判定のアルゴリズムは、√ 証明できた、× 反証できた、? 時間内にどちらも言えなかった、のどれかを返すと仮定する。?の扱いには3つの選択肢があり、論文は前の2つを退けている。
?を | 起きること |
|---|---|
| 拒否する | 深く調べれば正しいプログラムも落ちる。どれが通るか予測できず脆い |
| 楽観的に受理する | 仕様違反が実行時に素通りする |
| キャストを入れて受理する | 違反は実行時に必ず止まる。元のプログラムが正しければキャストは失敗しない |
関数適用t1 t2でS <: Tが?なら、t1 (⟨S ▷ T⟩ t2)に変換する。キャストは「t2の値がTに属するか」を実行時に調べる。実行時にS <: Tそのものを調べるのではない(相の区別を壊すので)。Tが「素数だけを受け付ける」なら、キャストは素数判定を走らせる。
何が嬉しいのか
純粋な動的検査(契約)と比べると、確実に間違っているものはコンパイル時に落とせる。純粋な静的検査と比べると、決定可能な述語に制限せずに済む。論文のTheorem 14は、どんな計算可能な抽象化γで述語を決定可能な断片に落としても、静的検査器は「正しいプログラムを拒否する」か「hybridなら静的に見つけた誤りを見逃す」のどちらかになることを示している。
静的解析が強くなるほど?は減り、√と×に吸収されていく。?の範囲は言語仕様ではなく実装の能力で決まる。
Sageはこれを言語にしたもので、型Dynamic(全ての型の上位型)、第一級の型、任意の篩型を持ち、?の判定に自動定理証明器と「反証済みの部分型判定のデータベース」を使う。型注釈を省くとDynamicになるので、動的型付けの書き方から始めて少しずつ精密な仕様にしていける。
Carinaの値制約の検査は同じ形をしている
Carinaの値制約(pattern / length / rangeを持つ篩型、プロバイダが宣言する入力ルール)の検査は、同じ3値で組まれている。ただし?の原因が違う。
Flanaganの?は論理の限界、Carinaの?は世界の限界である。 Flanaganでは値はいつか具体的になり、決められないのは型どうしの含意だけである。Carinaでは型の含意(正規表現の包含など)が決められないことに加えて、値そのものがapplyまで存在しないことがある。
型の段: キャスト相当を選ぶ場所と、選ばない場所
代入可能性(is_assignable_to)の規則は、?の扱いを場合ごとに選んでいる。
- 篩の付いていない
Stringから、識別を持たない篩付きString(長さだけ等)へは受理し、値の検査に回す(規則10)。識別を持つ型の値(aws.Arn等)からも同じく受理する(carina#4230)。キャストを挿入する選択に当たる。 - 識別を持たない篩付き型どうしは拒否する。パターンは文字列として一致しなければ認めず、長さは区間の包含を要求する(規則8)。
?を×に倒す選択で、カスタム型は独立の構成子ではなく篩型であるに書いた保守的な近似はここに残っている。 - 識別を持つ受け側へは、識別の証拠が無い限り拒否する(公称軸ごとの幅部分型付け)。
#4230に至った経緯が、論文の「?を拒否すると脆い」の実例になっている。プロバイダが属性をStringからString(len: 1..=1024)に締めると、そこへaws.Arnの参照を渡していた既存の設定が型エラーになった。ARNは実際にはその長さに収まるのに、型の上では証明できなかった。
値の段: Proven / Violation / Undecided
プロバイダが宣言する入力ルール(carina#4267)は、判定結果をInputVerdict::{Proven, Violation, Undecided}で返す。
- plan — 値が分かっていればそのまま判定する。値がまだ無くても、書かれた式と宣言型から長さの区間や文字種を健全に見積もり、決められる分は決める。Violationはplanエラー、Undecidedは対象のeffectに「未決の義務」として結び付けて持ち越す。
- apply — プロバイダに送る正確なリクエストに対してもう一度判定する。送信用の型はこの判定を通らないと作れない。置換のdeleteは、対になるcreateがこの判定を通ったという許可が無いと実行できないので、createが拒否されれば古いリソースは残る。
- apply時にもUndecidedなら失敗させる(fail-closed)。
schemaのpattern / lengthと、モジュール引数のvalidationも、参照の値が分かった時点で検査する(carina#3805)。planで分かればplanで、applyまで分からなければプロバイダへの送信直前に、それでも決まらない複数引数の条件はapply終了時の一掃で判定する。
対応と違い
| Flanagan | Carina | |
|---|---|---|
| √ | そのまま受理 | Proven: 何もしない |
| × | 静的に拒否 | 型エラー、またはplanエラー |
| ? の原因 | 含意の証明が時間内に終わらない | 正規表現の包含が決められない / 値がapplyまで無い |
| キャストの位置 | 適用箇所のコード | 対象effectに結び付けた義務。送信直前に解消 |
| キャストの失敗 | 元が正しければ起きない | 起きうる。同じapplyの先行effectは実行済みでありうる |
| 実行時にも決まらない | 起きない(値は具体的) | 起きうる。失敗にする |
最後の2行が一番大きな違いである。プログラムの実行時エラーはプロセスを止めれば済むが、applyの途中の失敗は、既に作ったリソースを外部世界に残す。Carinaが置換のdeleteにcreate側の許可を要求しているのは、この部分適用の害のうち最悪のもの(古いリソースを消したのに新しいものが作れない)を型で塞いでいる。
planは予測であり、真実はapplyが確立するの言い方をすれば、hybrid type checkingの「コンパイル時」と「実行時」はplanとapplyに対応し、Undecidedはその間に開いた窓(Unknownは二段階の間に開いた窓である)である。
根拠の確度
3つの結果、?の3つの扱いと退ける理由、キャストへの変換、Theorem 14、元のプログラムが正しければキャストは失敗しないことは、POPL論文の本文で確認した。{x : B | t}の構文と、篩型どうしの部分型が述語の含意判定に帰着して決定不能になることは、FOOL/WOOD論文で確認した。Sageの構成要素(Dynamic、第一級の型、任意の篩型、定理証明器、反証済み判定のデータベース)はSage論文の要旨による。
Carinaの規則8・規則10の内容はcarina-core/src/schema/mod.rsのis_assignable_toのdocコメント、3値の判定とapply時の扱いはcarina-core/src/input_rules.rsとcarina-core/src/executor/input_discharge.rsを読んで確認した。schema制約の参照値への再検査とapply終了時の一掃は、PR carina#3825の説明による。いずれも2026-11-07時点のmainで、入力ルールの一連の変更はその日に入ったばかりである。
Carinaの機構をhybrid type checkingとして読むのは解釈で、実装がそう名乗っているわけではない。「先行effectは実行済みでありうる」は、送信直前の判定とPR #3825のKnown limits(複数引数のrequireが、片方の値を使う側が走った後に決まる)からの推論である。