依存型
カリー=ハワード同型対応により、どんなに複雑な数学的な性質も型によって表現できる。もしユーザーが、型が非空である (つまり、その型を持つ値が存在する) ことの構成的な証明を与えることができれば、コンパイラは証明の正当性を検査し、証明の構成を追うことにより、実際にその値を計算できる実行可能なプログラムコードを出力することができる。このように証明を検査できるという性質により、依存型を持つプログラミング言語は定理証明支援系と近い関係にある。コードを生成できるという視点からは、機械的に検証された数学の証明からプログラムコードを直接導出することができるため、形式手法によるプログラム検証や証明つきコード(英語版)へのアプローチが考えられる。
依存積型の双対は、依存ペア型、依存和型、あるいはΣ型と呼ばれる型である。これは余積や直和、非交和などのアナロジーである。依存和型は存在量化のモデルとして理解することもできる。依存和型は
Σ ( x : A ) B ( x ) {\displaystyle \Sigma _{(x:A)}B(x)}
と表記される。
依存和型は、2番目の型が1番目の値に応じて変化するペアの型を表している。したがって、もし
( a , b ) : Σ ( x : A ) B ( x ) {\displaystyle (a,b):\Sigma _{(x:A)}B(x)}
ならば、 a : A {\displaystyle a:A} であり、 b : B ( a ) {\displaystyle b:B(a)} である。Bが定数関数 B ( x ) = C {\displaystyle B(x)=C} のときは、依存和型は直積型、すなわち通常の直積 A × C {\displaystyle A\times C} と一致する(型判定において一致する)。
ラムダ・キューブにおけるカインド(通常の型を集めた特別な型)を ∗ {\displaystyle *} , 超カインド(カインドを集めた特別な型)を ◻ {\displaystyle \square } と表記する。このとき、(狭義の)依存型とは、 A : ∗ {\displaystyle A:*} および B : A → ∗ {\displaystyle B:A\to *} を用いて構成される、 Π ( x : A ) B ( x ) {\displaystyle \Pi _{(x:A)}B(x)} という型のことである。一方、多相型は、 A : ◻ {\displaystyle A:\square } および B : A → ∗ {\displaystyle B:A\to *} を用いて構成される、 Π ( x : A ) B ( x ) {\displaystyle \Pi _{(x:A)}B(x)} という型のことである。例えば、 ∗ : ◻ {\displaystyle *:\square } であることを用いて Π ( x : ∗ ) B ( x ) {\displaystyle \Pi _{(x:*)}B(x)} と書いたものは、型に関する量化をしている多相型となる。