从属类型

在计算机科学和逻辑学中，从属类型是一种类型，其定义取决于一个值。

它是类型理论和类型系统的一个重叠的特征。在直觉类型理论中，从属类型被用来编码逻辑的量词，如forall和thereexists。在Agda、ATS、Coq、F*、Epigram和Idris等函数式编程语言中，从属类型通过让程序员分配类型来进一步限制可能的实现集，从而帮助减少错误。依赖类型的两个常见例子是依赖函数和依赖对。

从属函数的返回类型可能取决于它的一个参数的值（不仅仅是类型）。

例如，一个函数取一个正整数，其中数组的长度是数组类型的一部分。(注意，这与多态性和泛型编程不同，两者都将类型作为一个参数）。一个依赖对可能有第二个值，其类型取决于xxx个值。坚持以数组为例，依赖对可以用来以类型安全的方式将一个数组与它的长度配对。

从属类型增加了类型系统的复杂性。在一个程序中决定从属类型的平等性可能需要进行计算。

如果在从属类型中允许任意的值，那么决定类型平等可能涉及到决定两个任意程序是否产生相同的结果；因此类型检查可能变得不可判定。

历史在1934年，HaskellCurry注意到，在类型化lambdacalculus中使用的类型，以及在它的组合逻辑对应物中使用的类型，遵循着与命题逻辑中公理相同的模式。

进一步说，对于逻辑中的每个证明，在编程语言中都有一个匹配的函数（术语）。库里的例子之一是简单类型的λ微积分和直觉逻辑之间的对应关系。谓词逻辑是命题逻辑的扩展，增加了量词。

Howard和deBruijn扩展了lambdacalculus以匹配这种更强大的逻辑，他们为依赖函数和依赖对创建了类型，前者对应于forall，后者对应于thereexists。(由于霍华德的这项工作和其他工作，命题即类型被称为库里-霍华德的对应关系）。

Π类型宽泛地说，依赖类型类似于集合的索引族的类型。更正式地说，给定一个类型一个函数的返回值类型随其参数的变化而变化（即没有固定的模域），是一个依赖函数，这个函数的类型被称为依赖积类型、π类型（Π类型）或依赖函数类型。

从一个类型的家族中{displaystyleB:Ato{mathcal{U}}是一个常数函数。｝是一个常数函数，相应的依存积类型就等同于一个普通的函数类型。

就是说Π型"这个名字来自于这样的想法：这些类型可以被看作是类型的笛卡尔乘积。Π-类型也可以被理解为通用量词的模型。

例如，如果我们写表示实数的n个元组，那么{textstyleprod_{n:mathbb{N}}operatorname{Vec}(mathbb{R},n)}。}/operatorname{Vec}(`mathbb{R},n)}将是一个函数的类型，该函数给定自然数n，返回实数元组。

这将是一个函数的类型，给定一个自然数n，返回一个大小为n的实数元组。

例如{displaystyle}{mathbb{N}}是自然数到实数的函数类型，写成N→Rto`mathbb{R}}。在类型化的lambda计算中。