依赖函数类型

普通函数只保证“输入属于 $A$，输出属于固定的 $B$”；Π 类型把许多不同的输出类型 $B(a)$ 绑成一个逐点选择。拥有 $f:\mathrm{\Pi }(x:A).B(x)$，就意味着对每个具体 $a$ 都能产出恰好属于那一纤维 $B(a)$ 的结果。输入不仅参与计算，也参与说明结果应落在哪里。

在命题解释下，$\mathrm{\Pi }(x:A).B(x)$ 对应“对每个 $x:A$，$B(x)$ 成立”，而 λ 抽象把含任意 $x$ 的证明封装为全称证明。这是Curry–Howard 对应理路Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。层面的规则同构，不是把一个运行时函数与一阶逻辑公式宣称为无条件的对象等价；擦除、证明无关性与计算语义仍取决于具体系统。

令 $\mathsf{Vec}(A,n)$ 为长度为 $n$ 的向量族。保持长度的恒等程序具有类型

若 $v_2:\mathsf{Vec}(A,2)$，第一次应用把 $n$ 代为 $2$，所以

第二次应用再由 β-计算给出 $\mathsf{keep}2v_2\equiv v_2$。若误把参数写成 $v_3:\mathsf{Vec}(A,3)$，失败发生在第二次应用的前提判断，而不是等到函数体访问越界元素。与“把长度存在一个整数栏位里”的记录相比，索引替换直接决定调用后的静态类型。

Π 类型本身不会自动比较任意两个函数。点态给出 $\mathrm{\Pi }x.f(x)=g(x)$ 通常只能得到恒等类型中的函数相等，且需要函数外延性；它不必成为判断相等 $f\equiv g$。若允许 $B(x)$ 含有不终止计算，甚至判断 $B(a)$ 与另一个类型可转换都可能不可判定。空定义域上的 Π 类型在逻辑上可居留，也不能据此推出程序已枚举某个运行时集合：构造它只需在假设 $x:A$ 下给出分支。

Π 类型统一表达带索引 API、隐式参数、泛化定理和证明携带函数。例如安全数组索引可取 $i:\mathsf{Fin}(n)$，返回 $A$；矩阵转置可写成 $\mathrm{\Pi }(m,n).\mathsf{Mat}(A,m,n)\to \mathsf{Mat}(A,n,m)$，让维度交换出现在余类型而非文档注释。定理证明中，假设引入与全称引入都由 λ 完成，实例化则由应用完成。

实现上，检查 λ 往往利用期望的 Π 类型，而检查应用先综合函数类型、再核对实参并把实参代入余类型。隐式参数与 metavariable 只改变表面信息如何补全，不改变核心规则中的代入义务。类型检查器若用规范形判定余类型相等，还必须证明该转换过程对所选 Π、η 与宇宙规则可靠且终止。

显式向量连接核心理路依赖类型 elaborationDependent type elaboration · Elaboration of dependent types将表面程序展开为分层Π/Nat/Vec核心，以显式消去子构造向量连接，并由独立核重新检查motive、分支与conversion。把这一应用义务落实到每个参数：先传元素类型与长度，再核对向量，最终用自然数消去子的计算规则验证余类型。其分层宇宙、motive和所有λ参数注解都已写出。