notes mizzy.org

IaC言語は二段階の言語である

解釈 出典: explorations/2026-06-10-carina-type-system-type-theory/type-system-analysis.md §1 / totality-comparison.md §1 作成/ 更新

Carinaのようなインフラ記述言語は「実行時に型を検査する動的型付き言語」ではないし、古典的な静的型付き言語でもない。静的段階と動的段階という二つの段階を持つ言語として読むのが正確である。

この読みの起点は「何を実行と呼ぶか」の定義にある。Carinaプログラムの実行とは、apply段階でEffectが実際のインフラに作用することである。validateとplanはそれに先立つ段階であり、そこで行われるのは式の評価(let束縛、補間、for展開)、スキーマ型に対する検査、そして実行すべき操作(Create / Update / DeleteなどのEffect)のリスト、つまりplanの生成である。型エラーはどの操作も実行される前に報告される。

静的段階 — validate / plan 評価・型検査・planの生成 外界には一切触れない エラーはここで報告される plan 検査と実行の境界 動的段階 — apply 効果の実行(外界への作用) ここで初めてインフラが変わる この線の左で検査が完結する
段階の分離が効くのは、検査が実行に先立って完結するからである。静的段階の成果物であるplanが、検査と実行の境界そのものになっている。
段階行われること型理論上の対応
静的段階(validate / plan)評価・型検査・plan(実行する操作のリスト)の生成型検査しながらの中間表現へのコンパイル
動的段階(apply)効果の実行(外界への作用)実行

段階の分離が効いているのは、検査が実行に先立って完結するからである。静的段階の成果物であるplanが、検査と実行の境界そのものになっている。エラーは外界に一切触れる前に報告される。

この二段階構成が可能なのは静的段階が全域的であるためで、検査の対象が原則として項(構文)ではなく評価済みの値になっているのもそれが理由である。プログラムを完全評価してから値をスキーマ型と照合する、という構成が成り立つ。したがって型付けの様式は、型推論を持つ項ベースの型システムというより、plan生成というコンパイルの最中に全数実行される契約検査(contract checking)に近い。

段階の分離は「どこに窓が開くか」も決める。静的段階では値が決まらないもの(上流スタックのapply結果への参照、まだ作られていないリソースの属性)が必ず残り、それが二つの段階の間に開いた窓になる。planは動的段階の挙動の静的近似であり、近似で確定できなかった箇所を明示する装置が要る。

なおLSP診断は、この静的段階の検査をエディタ上で前倒しに実行するもう一つの実装であり、検査の意味論としてはvalidateと同一であること(パリティ)が要求されている。

根拠の確度

二段階言語という読みそのものは分析上の枠組みであり、実装がそう自称しているわけではない。段階ごとに何が起きるか(評価・検査・plan生成の順序、applyでの効果実行)はソース・実行で確認済み。

#iac #型システム #段階分離