typestateで壊れた状態を書けなくする

確認済み 出典: explorations/2026-06-10-carina-type-system-type-theory/type-system-analysis.md付録 2026-06-10 作成/2026-08-16 更新

Carinaの処理系は「処理が進むと値の型が変わる」typestateパターンを系統的に使っている。狙いは一貫していて、静的段階の内部不変条件を、実装言語の型でコンパイル時に固定することである。

適用例は複数の層に及ぶ。

• 未解決の列挙識別子と解決済み正規形は別の型であり、後者はリゾルバしか生成できない(carina#3438)。DSL綴りのまま比較に持ち込むことが型で書けなくなる。
• μ型の参照を展開した後の型ビューには参照変種が存在しない(carina#3349)。未展開のまま照合する状態がそもそも書けない。
• 効果の部分集合しか受理しない実行器には、絞り込み済みの型を渡す(carina#3164)。
• パーサの段階(パース直後 / 推論後)は型パラメータで区別される。

「覚えている」に依存しないこと

いずれの例も、対応する不変条件は「各消費地点が処理を忘れないこと」でも守れる。列挙値は比較の前に正規化する、μ型の参照は照合の前に展開する、と規約に書くこともできる。

しかし規約に依存する限り、同じバグクラスに未来の呼び出し側が再び到達できる。正規化を経ない比較経路が残っていたために列挙値が永遠に変更扱いされ続けた事故は、まさにその形で起きた。一箇所の消費地点が忘れたことが、差分という中心機能を静かに壊した。

typestateはこれを型の形に変える。壊れた状態を表す値が構成できないなら、忘れることが可能な地点がそもそも存在しない。「呼び出し側が覚えていること」に依存する不変条件は、型の形に作り直すまで根が残っている、という原則の実装である。

適用先の見当

この原則は未解決の問題にも指し示す先を持つ。代入で解決された値がスキーマで再検証されない問題(carina#3448)に対しては、deferredの穴に期待型を持たせ、穴を埋める唯一のAPIが「その型の検証器だけが生成できる検証済み値」を要求するようにすれば、検査を飛ばした代入が実装言語の型レベルで書けなくなる。検査を置くこと(信頼境界での再検証)と、検査を外せなくすること(typestate)は独立の手当てであり、併用が完成形である。

#typestate #型安全 #設計原則