依赖类型

定义

依赖类型（dependent type）是指可以依赖于「值」的类型。普通泛型只能让类型依赖类型（如 List<T>），依赖类型则允许写出「长度为 n 的向量 Vec n」「小于 m 的自然数 Fin m」这类由运行值参数化的类型。

理论基础

依赖类型源于 Martin-Löf 直觉主义类型论。依据 Curry-Howard 同构，依赖函数类型（Π 类型）对应全称量词，依赖对类型（Σ 类型）对应存在量词，因此依赖类型语言可以把数学命题写成类型、把证明写成程序。

代表语言

Agda、Coq/Rocq、Idris、Lean、F* 是主要的依赖类型语言；Haskell、Scala 通过扩展支持部分依赖类型特性。

优缺点

依赖类型能在编译期证明数组不越界、协议状态正确等强性质，但类型检查可能需要人工提供证明，学习与工程成本高，目前主要用于形式化验证与研究领域。