依存タイプ

戻り値の型が引数によって変化する関数（つまり、固定された終域を持たない関数）は従属関数であり、この関数の型は従属積型、π型（Π型）、または従属関数型と呼ばれる。^{[ 4 ]}型のファミリーから${\displaystyle B:A\to {\mathcal {U}}}$依存関数のタイプを構築することができます${\textstyle \prod _{x:A}B(x)}$項は、項を取る関数である。${\displaystyle a:A}$そして、次の項を返します。${\displaystyle B(a)}$この例では、依存関数型は通常次のように記述されます。${\textstyle \prod _{x:A}B(x)}$または${\textstyle \prod {(x:A)}B(x)}$。

もし${\displaystyle B:A\to {\mathcal {U}}}$は定数関数であり、対応する従属積型は通常の関数型と同等です。つまり、${\textstyle \prod _{x:A}B}$判断的に同等である${\displaystyle A\to B}$いつ${\displaystyle B}$依存しない${\displaystyle x}$。

「Π型」という名称は、これらが型のデカルト積として捉えられるという考え方に由来する。Π型は、全称量化子のモデルとしても理解できる。

例えば、次のように書くと${\displaystyle \operatorname {Vec} (\mathbb {R} ,n)}$実数のn組の場合、${\textstyle \prod _{n:\mathbb {N} }\operatorname {Vec} (\mathbb {R} ,n)}$これは、自然数nが与えられたときに、サイズnの実数のタプルを返す関数の型です。通常の関数空間は、範囲の型が実際には入力に依存しない場合の特殊なケースとして発生します。例${\textstyle \prod _{n:\mathbb {N} }{\mathbb {R} }}$これは自然数から実数への関数の一種であり、次のように表されます。$\displaystyle \mathbb {N} \to \mathbb {R} }$型付きラムダ計算において。

より具体的な例として、${\displaystyle A}$0から255までの符号なし整数型（8ビットまたは1バイトに収まるもの）であり、${\displaystyle B(a)=X_{a}}$のために${\displaystyle a:A}$、 それから${\textstyle \prod _{x:A}B(x)}$の産物へと退化する${\displaystyle X_{0}\times X_{1}\times X_{2}\times \ldots \times X_{253}\times X_{254}\times X_{255}}$。

依存積型の双対は、依存ペア型、依存和型、シグマ型、または（紛らわしいことに）依存積型です 。[ 4 ]シグマ型は存在量化子^{としても理解}できます。上記の例を続けると、型の宇宙において、${\displaystyle {\mathcal {U}}}$種類があります${\displaystyle A:{\mathcal {U}}}$そして、タイプのファミリー${\displaystyle B:A\to {\mathcal {U}}}$すると、依存ペア型が存在する。${\textstyle \sum _{x:A}B(x)}$（代替表記法はΠ型の表記法と同様です。）

依存ペア型は、2 番目の項の型が最初の項の値に依存する順序対の概念を捉えています。${\textstyle (a,b):\sum _{x:A}B(x),}$それから${\displaystyle a:A}$そして${\displaystyle b:B(a)}$。 もし${\displaystyle B}$が定数関数である場合、従属ペア型は積型、すなわち通常のデカルト積になります（判断上等になります）。${\displaystyle A\times B}$[ ^{4 ]​}

より具体的な例として、${\displaystyle A}$再び0から255までの符号なし整数型となり、${\displaystyle B(a)}$再び等しくなる${\displaystyle X_{a}}$さらに256個の任意の${\displaystyle X_{a}}$、 それから${\textstyle \sum _{x:A}B(x)}$合計に退化する${\displaystyle X_{0}+X_{1}+X_{2}+\ldots +X_{253}+X_{254}+X_{255}}$。

システム${\displaystyle \lambda \Pi }$論理フレームワークLFに対応する純粋な一階依存型の型は、単純型付きラムダ計算の関数空間型を依存積型に一般化することによって得られる。

システム${\displaystyle \lambda \Pi 2}$2次依存型のものは以下から得られる。${\displaystyle \lambda \Pi }$型コンストラクタに対する量化を可能にすることによって。この理論では、依存積演算子は、${\displaystyle \to }$単純型ラムダ計算の演算子と${\displaystyle \forall }$システムFのバインダー。

高次システム${\displaystyle \lambda \Pi \omega }$拡張${\displaystyle \lambda \Pi 2}$ラムダキューブからの4つの抽象化形式すべてに対応します。すなわち、項から項、型から型、項から型、型から項への関数です。このシステムは構成計算に対応し、その導関数である帰納的構成計算はRocqの基盤となるシステムです。