notes mizzy.org

良い類比は実バグを予言する

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

類比の価値は、記述が整うことにあるのではない。対応から実装上の予言が導け、その予言が実際のバグや改善方向を当てることにある。当たらない類比は装飾であり、当たる類比は分析の道具である。

「planはコンパイルである」という読みは、この基準を満たした。導かれた予言は少なくとも三つある。

第一の予言 — 再配置後の検証の欠如。IRの性質として「well-typedなIRだけがバックエンドに渡る」と置き、applyの性質として「再配置はIRに新しい値を書き込む」と置くと、リンカの類比から自動的に問いが出る:「再配置後のオブジェクトを誰かベリファイするのか」。答えは否で、これは確認済みの実バグ(carina#3448)だった。実装を眺めて見つけたのではなく、対応表から演繹して見つかっている。しかも修正の縫い目まで類比が指す — 各再配置点の直後に、書き込んだ値をその穴の型で検証する。

第二の予言 — 検査器の単一定義化。検査器が二系統ある問題(validateとLSPのパリティ維持)は、コンパイラ工学ではフロントエンドの二重実装として知られ、標準解はクエリ型(インクリメンタル)コンパイラ基盤 — 一つの検査定義をバッチとエディタの両方が問い合わせる構造 — である。型システム側の分析が独立に出した「検査器の単一定義化」という改善方向と一致する。

第三の予言 — 最適化パスの置き場。IRを持つコンパイラには最適化パスの置き場が自然に生まれる。効果の併合(同一プロバイダへのバッチ発行)、無効果の削除、並列スケジューリングの強化などは、planというIRが既にあるからこそ「パスを足す」形で議論できる将来余地である。

類比が予言力を持つのは、対応が構造レベルで取れているときだけである。だからこそ、類比がどこで切れるかも同じ精度で押さえておく必要がある。切れ目を明示しない類比は、当たらない場所でも当てにされてしまう。

#方法論 #類比 #設計