notes mizzy.org

検査器が二系統あるのは設計負債である

解釈 出典: explorations/2026-06-10-carina-type-system-type-theory/type-system-analysis.md §8弱み1 / plan-as-compilation.md §6末尾 作成

静的検査器が二系統ある — plan/validate経路とLSP経路 — というのは、機能の重複ではなく理論的な負債である。同じ検査の二重実装であり、意味論の一致(パリティ)を規約と試験で維持している。検査器を一つの定義から導出できていないことのコストがそこに現れている。

LSP診断は静的段階の検査をエディタ上で前倒しに実行するもう一つの実装であり、検査の意味論としてはvalidateと同一であることが要求される。要求されている、というのが問題の核心である。一致が構成から従うのではなく、規約と試験という外部の努力で維持されている限り、ずれは常に入りうる。

現状 — 定義が二つ 検査定義A 検査定義B validate / plan LSP パリティは規約と試験で維持 単一定義化 標準解 — 定義が一つ 検査定義 validate / plan LSP クエリ型コンパイラ基盤。パリティは構成から従う
二重実装は定義が二つあることの症状である。一つの検査定義をバッチとエディタの両方が問い合わせる構造にすれば、パリティは規約ではなく構成から従う。

コンパイラ工学ではこれはフロントエンドの二重実装として知られた問題で、標準解も定まっている。クエリ型(インクリメンタル)コンパイラ基盤 — 一つの検査定義をバッチとエディタの両方が問い合わせる構造 — である。rustcやRoslynが辿った道がこれに当たる。

型システム側の分析が独立に出した改善方向「検査器の単一定義化」は、このコンパイラ工学の標準解と一致する。validateとLSPが同じ検査定義を共有すれば、パリティは規約でなく構成から従う。

この負債の性質は、他の理論的負債と共通の形をしている。「定義を一つにし、区別を型に昇格させる」方向に解がある、という形である。二重実装は定義が二つあることの症状であり、個々のずれを試験で潰し続けるのは症状への対処にとどまる。

#設計負債 #lsp #コンパイラ