依存型
Π型という名前は、依存積型が型の直積と見なせるという考え方に由来している。依存積型は全称量化のモデルとして理解することもできる。
例えば、実数の n {\displaystyle n} 個の対を Vec ( R , n ) {\displaystyle {\mbox{Vec}}({\mathbb {R} },n)} と表記するとき、 Π ( n : N ) Vec ( R , n ) {\displaystyle \Pi _{(n:{\mathbb {N} })}{\mbox{Vec}}({\mathbb {R} },n)} は、自然数nを受け取りn個の実数の対を返す関数の型である。通常の関数空間は、依存積型で戻り値の型が実際には引数に依存しない特別な場合としてあらわれる。例えば、 Π ( n : N ) R {\displaystyle \Pi _{(n:{\mathbb {N} })}\;{\mathbb {R} }} は自然数から実数への関数の型であり、単純型付きラムダ計算では N → R {\displaystyle {\mathbb {N} }\to {\mathbb {R} }} と表記される。
型多相な関数は依存関数(すなわち、依存積型をもつ関数)の重要な例である。多相関数は、型を与えられると、その型を含む型を持つ値として振る舞う。例えば、恒等関数、すなわち任意の型Aに対し a : A {\displaystyle a:A} を受け取りaをそのまま返す関数、の型は、
Π ( A : U ) A → A {\displaystyle \Pi _{(A:{\mathcal {U}})}A\to A}
と書くことができる。