依存型
値に依存する型。型システムで不変条件を表現できる。Vec n Int は「ちょうどn個の整数のベクトル」を意味し、コンパイラが長さの整合性を検証する。Coq、Agda、Leanなどの証明支援系では標準である。
主流に近いのはIdris、F*（Microsoft Research）、現代的なLean 4。ErlangやElixirの「spec」は弱い依存型のようなものだ。用途は、認証済みソフトウェア（CompCert Cコンパイラ）、暗号の証明、ブロックチェーンのスマートコントラクトなど。トレードオフとして、非常に強力な反面、コンパイルに数分かかることがあり、頭への負荷も高い。主流のオブジェクト指向言語には依存型がなく、Rust、Java、Goは「値制限」と境界付きジェネリクスの範囲にとどまる。Lean 4はMITやCMUの形式手法の講義で教えられている。Leanの数学ライブラリMathlibは、学部レベルの数学の大半を形式化している。