依存型
ヘンク・バレンドレクト (en:Henk Barendregt) はいくつかの型システムを3つの軸にそって分類するラムダ・キューブを発明した。立方体の形をした図の8個の頂点それぞれが型システムに対応している。単純型付きラムダ計算が最も表現力が低い頂点に配置され、Calculus of constructions (en:Calculus of constructions)が最も表現力が高い頂点に配置されている。立方体の3個の軸はそれぞれ単純型付きラムダ計算に対する3種類の異なる拡張を意味している。それぞれ、依存型の追加、型多相性の追加、高階のカインド (en:Kind (type theory)) を持つ型コンストラクタ (例えば型から型への関数) の追加、である。ラムダ・キューブは純粋型システム (en:Pure type system)によってさらに一般化される。
ラムダ・キューブにおける(狭義の)依存型と多相型は、どちらも(広義の)依存積型の特別な場合と見なせるが、値に関する量化をする場合は(狭義の)依存型、型や型コンストラクタに関する量化をする場合は多相型と呼び、区別される。