依赖类型

在计算机科学和逻辑中，依赖类型（或依存类型，dependent type）是指依赖于值的类型，其理论同时包含了数学基础中的类型论和计算机编程中用以减少程序错误的类型系统两方面。在 Per Martin-Löf 的直觉类型论中，依赖类型可对应于谓词逻辑中的全称量词和存在量词；在依赖类型函数式编程语言如 ATS、Agda、Dependent ML、Epigram、F* 和 Idris 中，依赖类型系统通过极其丰富的类型表达能力使得程序规范得以借助类型的形式被检查，从而有效减少程序错误。

依赖类型的两个常见实例是依赖函数类型（又称依赖乘积类型、Π-类型）和依赖值对类型（又称依赖总和类型、Σ-类型）。一个依赖类型函数的返回值类型可以依赖于某个参数的具体值，而非仅仅参数的类型，例如，一个输入参数为整型值n的函数可能返回一个长度为n的数组；一个依赖类型值对中的第二个值可以依赖于第一个值，例如，依赖类型可表示这样的类型：它由一对整数组成，其中的第二个数总是大于第一个数。

依赖类型增加了类型系统的复杂度。由于确定两个依赖于值的类型的等价性需要涉及具体的计算，若允许在依赖类型中使用任意值的话，其类型检查将会成为不可判定问题；换言之，无法确保程序的类型检查一定会停机。

由于Curry-Howard同构揭示了程序语言的类型论与证明论的直觉逻辑之间的紧密关联性，以依赖类型系统为基础的编程语言大多同时也作为构造证明与可验证程序的辅助工具而存在，如 Coq 和 Agda（但并非所有证明辅助工具都以类型论为基础）；近年来，一些以通用和系统编程为目的的编程语言被设计出来，如 Idris。

一些以证明辅助为主要目的的编程语言采用强函数式编程（total functional programming），这消除了停机问题，同时也意味着通过它们自身的核心语言无法实现任意无限递归，不是图灵完全的，如 Coq 和 Agda；另外一些依赖类型编程语言则是图灵完全的，如 Idris、由 ML 衍生而来的 ATS 和 由 F# 衍生而来的 F*。

形式化定义

Π-类型

在全类（论域中全部类型构成的类型） ${\displaystyle {\mathcal {U}}}$  中给定一个类型 ${\displaystyle A:{\mathcal {U}}}$ ，存在着类型族 ${\displaystyle B:A\to {\mathcal {U}}}$  为每一项 ${\displaystyle a:A}$  赋予一个类型 ${\displaystyle B(a):{\mathcal {U}}}$ 。一个值域依赖于其参数的函数，称之为一个依赖类型函数，该函数的类型则称之为依赖类型、依赖乘积类型或Π-类型。在此例子中，依赖类型可以写作

${\displaystyle \Pi _{(x:A)}B(x)}$ 

或

${\displaystyle \Pi (x:A),B(x)}$ 

若B为常数，则依赖类型退化成一般形态的函数 ${\displaystyle A\to B}$ 。即 ${\displaystyle \Pi _{(x:A)}B}$  等价于函数类型 ${\displaystyle A\to B}$ 。

被称之为“Π-类型”的原因是它可以被看作是类型的笛卡尔积。Π-类型同时也可被看作是全称量词的模型。

例如，${\displaystyle {\mbox{Vec}}({\mathbb {R} },n)}$ 表示实数的${\displaystyle n}$ -元组类型，则 ${\displaystyle \Pi _{(n:{\mathbb {N} })}{\mbox{Vec}}({\mathbb {R} },n)}$  表示这样的函数类型：给定一个自然数n，该函数返回一个大小为n的实数元组。一般的函数空间可以看作依赖型函数的一个特例，当函数返回值类型实质上并不依赖于输入时，如 ${\displaystyle \Pi _{(n:{\mathbb {N} })}\;{\mathbb {R} }}$  即为从自然数到实数的函数类型，它可以在简单类型lambda演算中被写作 ${\displaystyle {\mathbb {N} }\to {\mathbb {R} }}$ 。

多态是依赖类型函数的一个重要实例。给定一个类型，函数作用于该类型的元素之上。一个返回元素类型为C的多态函数可能拥有如下的多态类型：

${\displaystyle \Pi _{(A:{\mathcal {U}})}A\to C}$ 

Σ-类型

依赖函数类型的对偶是依赖值对类型（或依赖总和类型、Σ-类型）。它与余积或不交并的概念相类似。Σ-类型可以被理解成存在量词的模型。写作：

${\displaystyle \Sigma _{(x:A)}B(x)}$ 

依赖值对类型表示一个值对，其中第二项的类型依赖于第一项的值。若

${\displaystyle (a,b):\Sigma _{(x:A)}B(x)}$ 

则 ${\displaystyle a:A}$  且 ${\displaystyle b:B(a)}$ 。若B为常数，则依赖值对类型退化为一般的乘积类型，即笛卡尔积 ${\displaystyle A\times B}$ 。

Lambda 立方

Henk Barendregt 提出了 Lambda 立方模型，用于对不同的类型系统的表达能力加以区分。Lambda 立方的八个顶点分别对应各自的类型系统，简单类型lambda演算位于表达能力最低的顶点上，而构造演算（calculus of constructions）则位于表达能力最强的顶点上。

一阶依赖类型

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

二阶依赖类型

二阶依赖类型 ${\displaystyle \lambda \Pi 2}$ ，通过允许对 ${\displaystyle \lambda \Pi }$  类型构造子的量化得到。此时，依赖乘积类型涵括了简单类型lambda演算中的${\displaystyle \to }$ 与 系统F 中的${\displaystyle \forall }$ 。

高阶依赖类型多态 lambda 演算

高阶类型系统 ${\displaystyle \lambda \Pi \omega }$  扩充了 ${\displaystyle \lambda \Pi 2}$ ，使之支持 Lambda 立方中的全部四种表达形式：从项到项的函数、从类型到类型的函数、从项到类型的函数、以及从类型到项的函数。这对应于构造演算（calculus of constructions），而构造演算则是证明辅助器 Coq 所基于的构造归纳演算^[1]理论的基础。

依赖类型编程语言

语言	是否活跃开发中	范式^[脚注 1]	策略（tactics）	证明项	终止检查	类型允许依赖于^[脚注 2]	全类	证明无关性	是否支持程序抽取	程序抽取是否消除无关项
Agda	是^[2]	纯函数式	少且有限^[脚注 3]	是	是（可选）	任意项	是（可选）^[脚注 4]	证明无关性参数^[4]	Haskell、JavaScript	是^[4]
ATS	是^[5]	函数式 / 命令式	否^[6]	是	是	?	?	?	是	?
Cayenne	否	纯函数式	否	是	否	任意项	否	否	?	?
Coq	是^[7]	纯函数式	是	是	是	任意项	是^[脚注 5]	否	Haskell、Scheme、OCaml	是
Dependent ML	否^[脚注 6]	?	?	是	?	自然数	?	?	?	?
Guru （页面存档备份，存于互联网档案馆）	否^[8]	纯函数式^[9]	hypjoin^[10]	是^[9]	是	任意项	否	是	Carraway	是
Idris	是^[11]	纯函数式^[12]	是^[13]	是	是（可选）	任意项	是	否	是	是^[13]
Matita	是^[14]	纯函数式	是	是	是	任意项	是	是	OCaml	是
NuPRL	是	纯函数式	是	是	是	任意项	是	?	是	?
F*	是	函数式 / 命令式	?	?	?	?	?	?	?	?
PVS（Prototype Verification System）	是	?	是	?	?	?	?	?	?	?
Sage （页面存档备份，存于互联网档案馆）	?	混合类型检查	?	?	?	?	?	?	?	?
Twelf	是	逻辑式	?	是	是（可选）	任意（LF）项	否	否	?	?
（[//web.archive.org/web/20200221043405/http://www.cs.bu.edu/~hwxi/Xanadu/Xanadu.html 页面存档备份，存于互联网档案馆） Xanadu]]	否^[15]	命令式	?	?	?	?	?	?	?	?

脚注

1. 这里专指核心语言之编程范式，而非任何 tactic 或代码生成子语言的范式。
2. 受到语义约束，诸如全类（universe）的约束。
3. 环求解器。^[3]
4. 可选的全类、可选的全类多态、可选的显式全类指定。
5. 全类，由全类约束自动推导（不同于 Agda 的全类多态）和可选的全类约束回显。
6. 已由 ATS 取代。

参见

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

参考文献

1. Announce:Calculus of Inductive Constructions. [2019-04-12]. （原始内容于2020-11-11）. 
2. Agda download page. [2014-08-24]. （原始内容于2019-06-27）. 
3. Agda Ring Solver. [2014-08-24]. （原始内容于2009-04-17）. 
4. . [2014-08-24]. （原始内容存档于2011-07-18）. 
5. . [2014-08-24]. （原始内容存档于2012-03-02）. 
6. email from ATS inventor Hongwei Xi. [2014-08-24]. （原始内容于2013-02-04）. 
7. Coq CHANGES in Subversion repository. [2014-08-24]. （原始内容于2018-09-29）. 
8. Guru SVN. [2014-08-24]. （原始内容于2015-11-18）. 
9. Aaron Stump. (PDF). 6 April 2009 [28 September 2010]. （原始内容 (PDF)存档于2009年12月29日）. 
10. Adam Petcher. Deciding Joinability Modulo Ground Equations in Operational Type Theory (PDF). 1 April 2008 [14 October 2010]. （原始内容 (PDF)于2010-07-19）. 
11. Idris git repository. ^{[永久失效連結]}
12. (PDF). [2014-08-24]. （原始内容 (PDF)存档于2011-07-16）. 
13. Edwin Brady. How does Idris compare to other dependently-typed programming languages?. 
14. . [2014-08-24]. （原始内容存档于2006-05-08）. 
15. Xanadu home page. [2007-11-05]. （原始内容于2020-02-21）. 

延伸阅读

• Why Dependent Types Matter （页面存档备份，存于互联网档案馆） T. Altenkirch, C. McBride, J. McKinna