notes mizzy.org

検査対象はノード上の値とエッジ両端の型の二種に還元できる

解釈 出典: explorations/2026-06-10-carina-type-system-type-theory/design-position.md §2 作成

IaC言語の型検査が項ベースの型体系をほぼ必要としないのは、実装上の手抜きではなく、意味的本体がグラフだけであることの帰結である。型を付けるべき「プログラム」が実質存在しないので、検査対象はグラフそのものになる

グラフを検査するとは、次の二種を検査することである。

リソース定義(ノード) 属性値 宣言された型・制約に属するか 検査1:ノード上の値の所属(スキーマ検証) 参照(エッジ) 検査2:代入可能性 他ノードの属性 参照先の型 参照元の要求型に代入可能か 蒸発条件 糖衣が消えて この二種に閉じる 蒸発しない機能を一つ入れるたび、この二種に収まらない検査対象が言語に混入する。
let・for・補間・モジュールが静的段階の終わりまでに消え、残るのが型付きノードとエッジだけになるからこそ、検査対象が二種に閉じる。

型システム分析レポートで記述された検査機構は、すべてこの二種に還元できる。意味論的型付けも、篩の任意述語も、型主導の等価性も、Unknownの一貫した意味論も、「ノード上の値」か「エッジ両端の型」のどちらかに属する検査として位置づけられる。

この還元が成り立つ前提が蒸発条件である。let・for・補間・モジュールといった糖衣が静的段階の終わりまでに消え、残るのが型付きノードとエッジだけになるからこそ、検査対象が二種に閉じる。逆に言えば、蒸発しない言語機能を一つ入れるたびに、この二種に収まらない検査対象 — つまり項ベースの型付けを必要とする「プログラム」 — が言語に混入する。

#型システム #設計原則 #グラフ