「全数検査」は検証ステップの時点で確定している値に限られる
値ベース検査の売りは「プログラムを完全評価してから、出てきた値を全数検査する」ことである。しかしこの「全数」性には時刻の指標が付く。検査されるのは、検証ステップの時点で値が確定しているものだけである。
「静的段階で確定する値」ではない。静的段階の内部でも、検証ステップより後に代入される値がある。
代入の時刻は二通りある
検証をplanの早い段階で一度だけ走らせると、そのあとに二種類の代入が起きる。
- 上流stateの値は、plan時に代入される。ただし検証ステップの後である。
- リソース出力は、apply時に代入される。
Carinaはしばらくこの形で、代入された値は検査器の視界に入らなかった。参照の宣言型検査が粗い型を通した場合(例えば宣言上はただのStringを、長さ・パターン付きの型が期待される場所へ渡した場合)、代入で解決された値が篩を満たすかを確かめる経路が無く、違反値はplanの表示に現れてさえ検査されず、最終判定はプロバイダAPIのエラーに委ねられていた(carina#3448)。
なぜこの限定が重要か
値ベース検査の全域性は「値が手に入るなら検査できる」を保証するが、「検査の時点で値が手に入っている」ことは保証しない。この二つを混同すると、値ベース検査を採用しただけで全数検査が達成されたと読んでしまう。
実際に必要なのは、検査を一回のステップではなく値が到着した各時点に置くことである。篩の述語は値依存であり、値は代入されて初めて生まれるのだから、値が到着した時点で述語を走らせる以外にない。
今のCarinaはそうしている。planで値が分かればplanで、applyまで分からなければプロバイダに送る直前に検査し、送信用の値は検査を通らないと作れない(再配置後に検証がないのは型検査済みIRの不変条件の破壊である)。それでも残るのは、planを承認する時点で値がまだ無いものである。その値はapplyで初めて検査されるので、承認した人は検査の結果を見ていない(判定できない部分型は、拒否も受理もせず実行時の検査に回す)。
根拠の確度
「全数」性の限定は探索中に二度精密化された。当初の「静的段階で確定する値」という言い方では、検証ステップより後にplan時代入される上流state値を取りこぼす。正しくは「検証ステップの時点で確定している値」である。
今のCarinaが値の到着時点で検査していることは、PR carina#3825とcarina#3846の説明による(2026-11-07時点のmain)。