形式陈述

依赖类型允许类型包含项。依赖函数类型

$$ \Pi(x:A).B(x) $$$$\mathrm{\Pi }(x:A).B(x)$$

表示对每个 $a:A$$a:A$ 返回 $B(a)$$B(a)$ 值的函数；依赖对类型 $\Sigma(x:A).B(x)$$\mathrm{\Sigma }(x:A).B(x)$ 同时包含 $a:A$$a:A$ 与 $b:B(a)$$b:B(a)$。普通函数类型是 $x$$x$ 不在 $B$$B$ 中自由出现的特例。类型检查需要比较含计算的类型，因此依赖一个可判定的定义等价或归约关系；为保持逻辑一致性和可判定性，核心理论通常限制一般递归并要求类型良构。

直觉

类型可以精确记住值的索引和性质，使“长度为 $n$$n$ 的向量”与“长度为 $m$$m$ 的向量”成为不同类型，程序接口由此携带可机器检查的证明。

例子与边界

向量类型 $\operatorname{Vec}(A,n)$$\mathrm{Vec}(A,n)$ 以长度索引；安全的头函数可取类型 $\Pi n.\operatorname{Vec}(A,n+1)\to A$$\mathrm{\Pi }n.\mathrm{Vec}(A,n+1)\to A$，从类型上排除空向量。等式证明也是类型的值。依赖类型不意味着编译器自动证明任意数学命题；用户仍需构造证明项，且自动化受可判定性和搜索复杂度限制。把不终止计算无约束地放入类型等价会使检查失去终止保证。

推论与应用

依赖类型用于证明助手、认证程序、协议状态、维度安全和精确 API。Curry–Howard 对应下，$\Pi$$\mathrm{\Pi }$ 对应全称量化/蕴涵，$\Sigma$$\mathrm{\Sigma }$ 对应存在量化/合取式证据。

参考资料

• Per Martin-Löf, Intuitionistic Type Theory, Bibliopolis, 1984，Full monograph, dependent function, pair, and identity types。
• Bengt Nordström, Kent Petersson, and Jan M. Smith, Programming in Martin-Löf’s Type Theory, Oxford University Press, 1990，Chs. 2–7, Martin-Löf type theory and programming。