依赖类型 在计算机科学和逻辑中依赖类型或依值类型dependent type是指依赖于值的类型其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面在 Per MartinLöf 的直觉类型论中依赖类型可对应于谓词逻辑中的全称量词和存在量词在依赖类型函数式编程语言如ATS英语ATS programming languageAgdaDependent ML英语Dependent MLEpigram英语Epigram programming languageF和Idris中依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查从而有效减少程序错误 依赖类型的两个常见实例是依赖函数类型又称依赖乘积类型Π类型和依赖值对类型又称依赖总和类型Σ类型一个依赖类型函数的返回值类型可以依赖于某个参数的具体值而非仅仅参数的类型例如一个输入参数为整型值n的函数可能返回一个长度为n的数组一个依赖类型值对中的第二个值可以依赖于第一个值例如依赖类型可表示这样的类型它由一对整数组成其中的第二个数总是大于第一个数 依赖类型增加了类型系统的复杂度由于确定两个依赖于值的类型的等价性需要涉及具体的计算若允许在依赖类型中使用任意值的话其类型检查将会成为不可判定问题换言之无法确保程序的类型检查一定会停机 由于CurryHoward同构揭示了程序语言的类型论与证明论的直觉逻辑之间的紧密关联性以依赖类型系统为基础的编程语言大多同时也作为构造证明与可验证程序的辅助工具而存在如 Coq 和 Agda但并非所有证明辅助工具都以类型论为基础近年来一些以通用和系统编程为目的的编程语言被设计出来如 Idris 一些以证明辅助为主要目的的编程语言采用强函数式编程total functional programming这消除了停机问题同时也意味着通过它们自身的核心语言无法实现任意无限递归不是图灵完全的如 Coq 和 Agda另外一些依赖类型编程语言则是图灵完全的如 Idris由 ML 衍生而来的 ATS 和 由 F 衍生而来的 F