TL;DR
定義が値に依存する型。たとえば「長さ n のベクトル」の型 Vector α n は、要素の型 α だけでなく、値 n にも依存する。Lean、Agda、Idris、Rocq（旧 Coq）などが依存型を備える。
なぜ必要か
Wikipedia によると、依存型を使うと、型によって許される実装を絞り込める。長さを型に含めれば、「ちょうど n 個の要素を返す関数」を型で表せる。
カリー＝ハワード対応のもとでは、命題が型に、証明がプログラムに対応する。依存関数型は「すべての〜について」に、依存ペア型は「〜が存在する」に対応するので、依存型を持つ言語は定理証明支援系と深く関係する。
仕組み
Theorem Proving in Lean 4 によると、依存型理論の「依存」とは、型がパラメータに依存できることを指す。
- 依存関数型:
(a : α) → β aの形の型で、返り値の型が引数の値によって変わる。βがaに依存しなければ、通常の関数型α → βになる。 - 依存ペア型:
(a : α) × β a（Σ a : α, β a）の形の型で、2 つ目の要素の型が 1 つ目の要素の値によって変わる。βがaに依存しなければ、通常の直積型になる。
例
リストの先頭に要素を足す cons は、要素の型 α を最初の引数として受け取ると、(α : Type) → α → List α → List α という依存関数型で書ける。返り値の型 List α が、引数 α の値で決まる。
注意点
発表「多段階計算によるコンパイル時テンソル形状検査」では、Idris のような依存型と手動の証明を使う方法は、プログラムを直すたびに証明を書き直す必要があり、継続的なソフトウェア開発との相性に課題があるとしている。