検査は素通し、等価性は不成立 — Unknownの一貫した保守性
Unknownの扱いは、検査では楽観的に、等価性では悲観的に振る舞う。方向が逆に見えるが、どちらも「インフラを壊さない側」に倒すという一つの原則の現れである。
(1)所属検査は素通しする
値の所属検査はUnknownを素通しする。「動的段階で解決されるはずの値」に偽の型エラーを出さない楽観的な扱いで、漸進的型付け(gradual typing)における動的型?と既知型の整合(consistency)関係と同型の判断である。ただしCarinaの場合これは検査を実行時へ先送りするのではなく、静的近似の精度限界を受け入れるという意味を持つ。gradual typingが実行時キャストで埋め合わせるところを、Carinaは埋め合わせない。
素通しの粒度も重要である。素通しはUnknownが現れた葉の位置単位であり、リストは具体値と未解決値の混在が許されて要素ごとに個別に判定される。したがって兄弟要素の所属検査やコンテナの形状・必須フィールドの検査は通常どおり走る。実装上は、検証器の最上位で値を具体軸へ射影し、射影できない値だけを受理する一点に、この素通しの判断が集約されている。
(2)等価性は成立しない
等価性においてUnknownは何とも等しくない。差分計算は「不明な値は変化したとみなす」方向に倒れるため、健全(変化の見逃しを出さない)だが完全ではない(実際には変化しない差分を表示しうる)。三値論理の「不明」を二値の判定に埋め込む際の保守的な選択である。
二つを合わせた意味
検査は素通し、等価性は不成立という組み合わせは、「偽の型エラーを出さず、怪しい差分は出す」方向に揃っている。偽陽性の型エラーはユーザーが正しいコードを書けなくする一方、余分な差分表示はレビューで捨てられる。コストの非対称に合わせて楽観と悲観を使い分けた結果が、Unknownの一貫した保守性である。