依存型とは？

依存型（dependent type）とは、プログラミング言語の型理論における概念で、型の内容・構造が値（実行時の具体的なデータ）に依存して変化する型のことをいいます。通常の型システムでは「整数の配列」のように型と値は明確に分離されていますが、依存型では「長さが5の整数の配列」のように、値の情報が型に含まれます。

依存型の代表的な例として、長さ情報を型に持つベクター型があります。たとえばAgda・Idris・Coqなどの言語では、Vec A nのように「要素型Aで長さnのリスト」という型を定義でき、長さが異なるリストを誤って連結しようとするとコンパイル時にエラーとなります。これにより実行時エラーの原因となるバグをコンパイル段階で防ぐことができます。

依存型が活用される主な場面は次のとおりです。

• 境界外アクセスなどの安全性保証
• 数学的証明をプログラムとして記述する「定理証明支援系」
• プロトコルや状態遷移の仕様をコードで直接表現する形式検証
• 型レベルでの不変条件（invariant）の強制

依存型を採用した代表的な言語・システムにはCoq・Agda・Idris・Lean・F*などがあります。型検査が非常に強力である一方、型の記述や証明の負担が大きく、実用的な汎用プログラミング言語への完全な統合はまだ発展途上の分野です。関数型プログラミングや形式手法の研究において中心的なトピックのひとつとなっています。