依赖类型

在计算机科学和逻辑中，依存类型是依存於值的类型。依存类型在直觉类型论和实验性的函数式编程语言如 Dependent ML 或 Epigram 的设计中扮演了关键性角色。

例如，实数 $n$-元组的类型，可以被稱为 $\mbox{Vec}({\mathbb R},n)$。因为該类型依存于值 $n:{\mathbb N}$，是一種依存類型。

lambda 方塊系统

Henk Barendregt 用 lambda cube 的三個軸，來區分各種類型系統。在 lambda 方塊上的八個頂點各自對應相對的類型系統，而简单类型lambda演算位於表達能力最弱的頂點上，而依存型別在表達能力最強的頂點上。

一阶依存类型

一阶依存类型系统 $\lambda \mbox{P}$，对应于逻辑框架 LF，是通过把简单类型lambda演算的函数空间一般化为依存乘积类型而获得的。

如上述的例子，对实数的 $n$-元组写作 $\mbox{Vec}({\mathbb R},n)$，$\Pi n:{\mathbb N}.\mbox{Vec}({\mathbb R},n)$ 表示為一函數的型別，其輸入為自然数 n 傳回 n 個实数元组的类型。當值域不依存于输入的特殊情況，就是一般的函數空間類型，比如 $\Pi n:{\mathbb N}.\mbox{List}$ 是从自然数到串列的函数类型，在简单类型 lambda 演算中写为 ${\mathbb N}\to \mbox{List}$。

具有依赖类型的语言

• Agda
• Aldor
• ATS
• Cayenne
• Coq
• Dependent ML
• Epigram
• Mizar system
• PVS
• Sage Programming Language
• Twelf
• Xanadu

参见

• Lambda立方
• 有类型lambda演算
• 直觉类型论

外部链接

• Why Dependent Types Matter T. Altenkirch, C. McBride, J. McKinna