依赖类型

维基百科,自由的百科全书
跳转至: 导航搜索

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

例如,实数 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}

具有依赖类型的语言[编辑]

参见[编辑]

外部链接[编辑]