依存型 (Dependent Types)

依存型は、値に依存して変化する型であり、データの性質を型の中に表現できる。例えば長さnのベクトルの操作結果が長さn+1になることを、型検査の対象にできる。

仕組みと確認

型の形成、値の置換、証明項、消去後の実行を分けて設計する。型が表す不変条件と、実行時に検査すべき条件を列挙し、コンパイラがどの証拠を検査したか確認する。

限界と注意点

依存型がすべての仕様や副作用を表現するわけではない。証明の記述コスト、型推論、実行時表現、外部I/Oとの境界を設計へ含める。