依赖类型

普通类型只能说“这是一个整数列表”，依赖类型还能把长度、维度或协议状态写进类型。函数的返回类型可随输入值变化，于是接口本身精确描述输入与输出之间的关系。最有效的心智模型是“类型也能提到程序数据”，而不是“运行时随便计算一个类型”；为了让类型检查可执行，出现在类型中的计算通常受纯度和终止性约束。精确规格带来更强保证，也把原本的测试义务转化为构造证明项的义务。

长度索引向量是按自然数索引的归纳族公理库归纳类型Inductive type · Inductive datatype由有限构造步骤生成的最小递归数据类型，并以严格正性保障其递归结构良好。，可写作 $\mathrm{Vec}(A,n)$；nil 只构造 $\mathrm{Vec}(A,0)$，cons 则把长度索引从 $n$ 推进到 $n+1$。连接函数的类型

保证结果长度由输入长度相加得到。矩阵乘法可把内维相等写进参数类型，从而使维度不匹配无法通过检查。

边界是值相等问题。若类型检查必须判断任意一般递归程序是否返回相同自然数，就会遇到不可判定性；实际系统通过强正规化核心、结构递归、用户提供证明或把复杂相等推迟为命题来控制。依赖类型也不会自动证明实现正确，程序员仍须给出能通过这些精确类型的项。

依赖类型支撑 Lean、Coq、Agda 等证明助理与高度验证的程序库。通过Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。，命题可作为依赖类型、证明可作为其居民；依赖消去子公理库消去子、递归子与归纳原理Eliminator · Recursor · Induction principle由归纳类型的构造器导出消费数据、定义递归函数和证明依赖性质的规则。让 motive 随数据与索引变化，从同一规则得到递归程序和归纳证明。本页只说明这种依赖关系，不重写归纳类型的构造与正性条件。

它扩展类型判断公理库类型判断Typing judgment由类型规则推导的上下文判断，记录项在给定变量假设下具有的静态类型。的同时，也依赖严格的正规化性质公理库正规化性质Normalization property每个良构或良类型项能否经有限归约到正规形的性质。来保持转换检查可判定。协议状态、数组边界、序列化格式和密码实现都可把关键不变量提升到类型层。