notes mizzy.org

planはコンパイルである

解釈 出典: explorations/2026-06-10-carina-type-system-type-theory/plan-as-compilation.md §1, §8 作成/ 更新

carina planは、ソース言語(.crn)のプログラムを、検査を通しながら中間言語(Effectのリスト + 依存DAG)へ翻訳するコンパイラである。applyはその中間言語の実行系である。この対応は比喩ではなく、コンパイラの段ごとに具体的な対応物が取れる。

コンパイラの段Carinaでの対応物
字句・構文解析pest文法による.crnのパース
マクロ展開・脱糖letのfixed-point解決、for展開、補間、モジュール展開
意味解析・型検査スキーマ検証(値の所属)+ 参照の代入可能性(エッジの型)
命令選択(lowering)差分計算 — desiredとstateの差を10種の命令(Effect)に落とす
中間表現(IR)plan = Effectのリスト + 依存DAG
オブジェクトファイルplan --outの保存形式
未解決シンボル・再配置情報deferred参照とUnknown
リンク・ロードapply — DAGの位相順に再配置(値の代入)しながら実行
ターゲットアーキテクチャプロバイダ(aws / awscc / mock)
IRダンプplan表示・carina-tui

フロントエンドの読みが最も素直に効く。コンパイラのフロントエンドは、人間向けの構文(糖衣)を中間表現が知らなくてよい形に展開する。Carinaのlet・for・補間・モジュールがこれに当たり、planの時点ではすべて消えて、残るのは型付きノード(リソース定義)とエッジ(依存)だけである。設計上の立場で蒸発条件と呼んだもの — 言語機能は静的段階の終わりまでにグラフへ正規化されて消える糖衣である限りで許容される — は、コンパイラの言葉では「すべての言語機能はフロントエンドでlowering可能でなければならない」というIR中心の言語設計原則そのものである。

この観点で型検査の位置も定まる。Carinaの検査は完全評価された値に対する所属判定であり、コンパイラの語彙では「脱糖後の正規形に対して意味解析を行う」ことに当たる。検査対象が項ではなく値であるという特異性は、フロントエンドが全域的(評価が必ず停止し、脱糖が必ず完了する)だから許される贅沢である。

こう読むと、Carinaの構成要素は一つのコンパイラパイプラインとして整列する。蒸発条件はフロントエンドの設計原則、値ベース検査は脱糖後の意味解析、差分計算は(ソース,世界)を引数とする命令選択、planはSSA的で直列化可能で人間がレビューするIR、applyは再配置しながら実行するリンカ兼ローダ、プロバイダはプラグイン化されたターゲット、WITはABIである。

根拠の確度

コンパイラ各段への対応づけ全体は解釈であり、実装の自己記述ではない。類比は分析の道具として置かれている。個々の事実(Effectが10種であること、plan --outの保存形式、検証と代入の順序)はソースで確認済み(Effectの種類は2026-08-16に再確認。初稿は8種と書き、ReadとDeferredCreate / DeferredReplaceを落として実装に無いReplaceを含めていた)。

#iac #コンパイラ #plan