Unknownは二段階の間に開いた窓である
静的段階では値が決まらないものがある。上流スタックのapply結果への参照、まだ作られていないリソースの属性、for展開の変数などで、Terraformの「(known after apply)」に相当する。CarinaはこれをValue::Unknown(理由)として値の一級表現にしている。
型理論的に見ると、これは二つの段階の間に開いた窓の扱いの問題である。planは動的段階の挙動の静的近似であり、Unknownはその近似で確定できなかった箇所を明示する装置と言える。窓が開くこと自体は二段階言語の構造から必然で、問うべきは「窓をどう扱うか」の意味論である。
Carinaの扱いは二点に整理できる。
- 値の所属検査はUnknownを素通しする。 「動的段階で解決されるはずの値」に偽の型エラーを出さない楽観的な扱いである。
- 等価性においてUnknownは何とも等しくない。 差分計算は「不明な値は変化したとみなす」方向に倒れる。
この二点の組み合わせは「偽の型エラーを出さず、怪しい差分は出す」方向に揃っており、インフラツールとして健全側に倒れている。
Unknownは⊥ではない
Unknownが単なる⊥(情報なしの底値)ではなく、理由を持ち運ぶ点は実務的に優れている。上流参照、for変数、編集途中の補間など10種の理由が区別されており、近似が確定できなかった箇所の診断品質を支えている。「値が不明である」だけを伝える表現なら、なぜ不明なのか・いつ確定するのかをユーザーに示せない。理由付きのUnknownは、静的近似の失敗を診断可能な形で持ち運ぶ設計である。この理由の集合は診断のための注釈にとどまらず、解決経路の分類になっている — Unknownの理由は診断文言ではなく「誰がいつ埋めるか」の分類である
この設計は、未知値をホスト言語のstringに偽装するCDKのTokenや、型付きコンテナに包むPulumiのOutput<T>とは別の位置にある。未知値をどう扱うかが言語の意味論として固定されている、という点が要である。