类型论

类型论有许多种，底下更细分许多变体，本文只能以直觉类型论为例做基本的入门介绍，而不详细罗列每一种变体。

项与类型

在类型论中，每一个数学对象都有其所属的类型（笼统地来说，这个类型的独一无二的）。每次加入新的变量时，必须同时指定其所属的类型。举例说，“设x为自然数”可写作

${\displaystyle x:\mathbb {N} }$ 

读作“项x的类型是${\displaystyle \mathbb {N} }$ ”。这在形式上似乎和集合论中的${\displaystyle x\in \mathbb {N} }$ （“x是集合${\displaystyle \mathbb {N} }$ 的元素”）无所差异，但后者是一阶逻辑中具备真值的一条“命题”，而前者则是一个纯粹的“断言”，并不是一条有待证明的命题。^[1]

类型建构规则

每一种类型论都指定了如何建构新类型（及其项）的一套规则，通过这些规则所得出的式子都是合理的断言，不须证明。以下归纳每一个新类型定义的组成部分：^[1]

1. 建构规则：如何建构符合某种格式的新类型。例如，当A和B分别为类型的时候，可以建构有序对类型A × B，亦可建构函数类型A → B。
2. 建构式，或称引入规则：如何建构属于这一类型的项。例如，从a : A和b : B这两个项，就可以建构A × B的项，记作(a, b)。
3. 消去式，或称消去规则：如何使用属于这一类型的项。例如，设A, B, C为类型，对应于每一个函数g : A → (B → C)，都有一个函数f : A × B → C。这条规则指定了如何使用A × B的项。
4. 运算规则：消去式如何应用在建构式上。例如，设a, b, c分别为A, B, C的项，则f( (a, b) )定义为等同g(a)(b)。
5. 唯一原理（可有可无）：规定指入某个类型或从某个类型指出的函数是唯一的。比如，“A × B的每一个项都可以唯一地表达为(a, b)”。在设计类型论的时候，可以把唯一原理列入类型的建构规则之中，亦可省略之，而视其为有待证明的命题。

以上是类型论的基本规则，可理解为类型论的语法，它并不包含数学公理。这和集合论有所不同：除了一阶逻辑本身的推理规则以外，集合论还加入了一组有关集合的公理（如策梅罗-弗兰克尔公理系统）。最基本的类型论不需公理即可当做逻辑和数学推理使用，但在有需要时，同样也可以加上额外的公理。类型论中的公理是不通过建构规则而接纳的断言，因此有些公理会产生无法通过运算规则简化的式子，从而影响该类型系统的可计算性。

常见类型

以下列出几种常见的基类型，除了全类和（依赖）函数类型以外，它们都是最后介绍的归纳类型（英语：Inductive type）的特例。这些类型既可以表达数学结构，又可以表达命题。类型的项可以是某个数学结构的成员，也可以是某条命题的证明。这就是命题为类型原理。

全类

类型论规定，在介绍新的符号时，必须马上指定它的类型，如“设${\displaystyle n:\mathbb {N} }$ ”。同样，当我们说“设A为类型”的时候也一样要指定A自己的类型。然而，A本身就已经是一个类型，那么类型的类型是什么？类型论中有“全类”的概念，每个全类的项都是类型。由于全类本身也是一个类型，如果所有类型都属于同一个全类的话，就不可避免产生吉拉尔悖论（英语：Girard's paradox）（罗素悖论在类型论中的体现）。因此，类型论一般都会假设存在无限层全类，记作𝒰₀, 𝒰₁, 𝒰₂，如此类推。每一层全类都是它上一层全类的项：𝒰_i : 𝒰_i+1。“设A为类型”的意思其实是“设A : 𝒰_i”，其中层级i可以明确指定，但一般可以从前文后理推断出来，所以下标往往省略不写。同理，当我们说“对于所有类型A”，意思其实是“对于所有第i层全类下的类型A”。有些类型系统规定，𝒰_i下的所有项也是𝒰_i+1的项，这种累积性属性对设计一个类型系统来说有利有弊，在此并不详述。

以上解释的是罗素式全类。塔斯基式全类是另一种绕过悖论的方法，它主张每个A : 𝒰要经过一个明确的强制转换函数才能成为一个类型El(A)。

函数类型

类型论将函数视为一种基础类型，而不像集合论一样定义为笛卡尔积的符合某些规定的子集。每一个函数都属于一个类型：假设A, B为类型，可以建构函数类型A → B。要定义这一类型的某个项，共有两种方法。第一种是直接定义：先给函数取名，例如f，然后对于任意项a : A，将f(a)定义为一条可能含有a并且类型为B的公式Φ。f的定义可以读成“给我任何一个a : A，我都可以给你一个Φ : B”。另一种方法是λ抽象化，直接写(λ (a : A), Φ) : A → B，避开给函数取名。

从命题为类型原理的角度来看，函数可以用来表达逻辑蕴涵。假如p, q分别是代表命题的类型，那么p → q就代表了“当p为真，则q为真”这一命题。要证明此命题，对于p的每个项（即证明），须给出q的一个项。

依赖类型

依赖函数类型，又称Π类型，是普通函数类型的推广，使得函数的到达域类型可以依赖于输入值。对于任何类型A和一族类型B : A → 𝒰（即对于任何a : A都有一个可能不同的类型B(a)），都可以建构依赖类型

${\displaystyle \prod _{a:A}B(a).}$ 

要定义依赖类型的某个项（即某个依赖函数），同样有两种方法。直接定义：取名f，对于任意项a : A，将f(a)定义为一条可能含有a并且类型为B(a)的公式Φ。λ抽象化：直接写

${\displaystyle \lambda (a:A),\Phi :\prod _{a:A}B(a).}$ 

假如A是任意类型而p : A → 𝒰是一族代表命题的类型，那么${\displaystyle \prod _{a:A}p(a)}$ 就代表了“对于所有a : A，p(a)为真”这一命题。

空类型

空类型记作⊥或0，它没有任何相应的建构式，也就是说，它没有任何项。空类型的消去规则是，对于任何类型A，都有一个函数false_elim : ⊥ → A。根据命题为类型原理，空类型可以诠释为“假”命题，它不存在任何证明。设p为代表命题的类型，则p → ⊥代表“非p”这一命题，记作¬p。假设⊥有一个项h，而p为任何代表命题的类型，那么通过空类型的消去规则就可以得出false_elim h : p。这意味着无论什么命题都可以证明是真的，是为爆炸原理。

单值类型

单值类型记作⊤或1，它只有一条建构式，因此只含唯一的单个项，记作“∗ : 1”。假如有一个函数f : 1 → A，则可以说A有一个项f(∗)，亦称“A是有栖居对象的类型”（类型论区分“有栖居对象”和“非空”这两个概念）。

双值类型

双值类型记作${\displaystyle \mathbb {B} }$ 或2，它有两条构件式，因此有两个项，记作“0₂, 1₂ : 2”。双值类型就是函数式编程中的布尔，其两个项可以分别理解为“如果假”和“如果真”两个情况。函数f : 2 → A可以理解为“如果真，输出f(1₂) : A，否则输出f(0₂) : A”。

积类型

积类型所表达的是有序对的概念。从两个类型A, B可以建构出它们的积类型A × B。它有一条建构式：从两个项a : A和b : B可以建构出积类型的项(a, b) : A × B。对应于每一个函数g : A → (B → C)，都有一个函数f : A × B → C。

积类型可以诠释为逻辑与：假如类型A, B, C都是命题，则函数f : A × B → C可以理解为“假如同时有A的证明和B的证明，就可以用f得出C的证明”。更简短地说，“A与B为真时，则C为真”。

余积类型

余积类型所表达的是不交并的概念。从两个类型A, B可以建构出它们的余积类型A + B。它有两条建构式：从一个项a : A可以建构出inl(a) : A + B，从一个项b : B则可以建构出inr(b) : A + B。要建构函数f : A + B → C，须指定两个函数g₀ : A → C和g₁ : B → C，使得f(inl(a))定义为g₀(a)，f(inr(b))定义为g₁(b)。

余积类型可以诠释为逻辑或：假如类型A, B, C都是命题，则函数f : A + B → C可以理解为“假如有A的证明，或者有B的证明，只需其一就可以用f得出C的证明”。更简短地说，“A或B为真时，则C为真”。

上文介绍的双值类型可视为余积类型的特例，等同于1 + 1。

依赖对类型

依赖对类型，又称Σ类型，是积类型的推广，使得每个项(a, b)中的第二个对象b的类型可以依赖于a。对于任何类型A和一族类型B : A → 𝒰，可以建构依赖对类型

${\displaystyle \sum _{a:A}B(a).}$ 

它的项的格式是(a, b)，其中a : A，而b : B(a)。

假如A是任意类型而p : A → 𝒰是一族代表命题的类型，那么${\displaystyle \sum _{a:A}p(a)}$ 就代表了“存在a : A使得p(a)为真”这一命题。值得注意的是，这种存在比经典数学中的存在更强，因为类型论要求我们明确提供见证p(a)为真的那个项a，而经典数学则无此要求（比如可以婉转地证明“不可能不存在这样的a”）。这意味着，最纯粹的类型论表达的是一种构成主义数学。通过引入各种公理，如排中律和选择公理，类型论仍然可以灵活地表达非构成主义的经典数学。

自然数

类型论一般按照皮亚诺算术来定义自然数${\displaystyle \mathbb {N} }$ 。它共有两条建构式：

• ${\displaystyle 0:\mathbb {N} }$ ，自然数的起始点
• ${\displaystyle {\mathsf {succ}}:\mathbb {N} \to \mathbb {N} }$ ，自然数的后继函数

任何自然数，要么是0，要么是某个自然数的后继（即等于${\displaystyle {\mathsf {succ}}(n)}$ ，其中${\displaystyle n:\mathbb {N} }$ ）。一、二、三分别表达为${\displaystyle {\mathsf {succ}}(0)}$ 、${\displaystyle {\mathsf {succ}}({\mathsf {succ}}(0))}$ 、${\displaystyle {\mathsf {succ}}({\mathsf {succ}}({\mathsf {succ}}(0)))}$ ，如此类推。

要定义某个函数${\displaystyle f:\mathbb {N} \to A}$ ，须指定一个起始项g₀ : A以及一个“下一步”函数${\displaystyle g_{\mathsf {succ}}:\mathbb {N} \to A\to A}$ ，使得f(0)定义为g₀，并且对于任何${\displaystyle n:\mathbb {N} }$ ，${\displaystyle f({\mathsf {succ}}(n))}$ 定义为${\displaystyle g_{\mathsf {succ}}(n)(f(n))}$ ，也就是以0为起始点利用数学归纳法做一个递归性的定义。比如，以下是“奇偶”函数${\displaystyle {\mathsf {oddeven}}:\mathbb {N} \to {\boldsymbol {2}}}$ 的定义：

• g₀定义为0₂
• ${\displaystyle g_{\mathsf {succ}}:\mathbb {N} \to {\boldsymbol {2}}\to {\boldsymbol {2}}}$ 的定义：对于所有${\displaystyle n:\mathbb {N} }$ ，
  • ${\displaystyle g_{\mathsf {succ}}(n)(0_{\boldsymbol {2}})}$ 定义为${\displaystyle 1_{\boldsymbol {2}}}$ 
  • ${\displaystyle g_{\mathsf {succ}}(n)(1_{\boldsymbol {2}})}$ 定义为${\displaystyle 0_{\boldsymbol {2}}}$ 

这里我们也用到了双值类型2的消去式。其他常见函数，例如“双倍”函数${\displaystyle {\mathsf {double}}:\mathbb {N} \to \mathbb {N} }$ 以及加法${\displaystyle +:\mathbb {N} \to \mathbb {N} \to \mathbb {N} }$ 等二元运算都有类似的定义。

等同类型

类型论有至少三种可以理解为“等同”的概念。第一种是“符号等同”，又称“从定义上等同”，例如用1定义为代替${\displaystyle {\mathsf {succ}}(0)}$ 的符号，这记作${\displaystyle 1:\equiv {\mathsf {succ}}(0)}$ 。自然数一节中的“定义为”就属于此种等同，也可以用:≡表示。这种等同是为了给符号赋予含义，但它本身不含任何额外的数学意义。

第二种是“断言等同”，即在展开两个符号的定义，并用类型论建构规则运算以后，两者的公式完全吻合，记作“a ≡ b”。例如，通过oddeven的定义，可做运算：

${\displaystyle {\mathsf {oddeven}}(1)\equiv g_{\mathsf {succ}}(0)({\mathsf {oddeven}}(0))\equiv g_{\mathsf {succ}}(0)(g_{0})\equiv g_{\mathsf {succ}}(0)(0_{\boldsymbol {2}})\equiv 1_{\boldsymbol {2}}.}$ 

若a ≡ b，则在任何式子中出现的a都可以直接替换为b。此种等同属于断言，并不是逻辑命题，而是重复应用类型论语法规则后所得的符号等同。在类型论中，不允许说“假设a ≡ 1”，因为在设符号${\displaystyle a:\mathbb {N} }$ 的时候，如果还没有给n赋予定义值，那就应该做定义“a :≡ 1”；反之如果n已经被赋予定义值（比如1），那就轮不到我们假设其数值。假如将类型论的规则视为某种代数系统，那么断言等同就正是该系统中的普通等同关系，类似于一个群的元素之间的等同。

第三种是“命题等同”。有时，两条公式就算在展开定义和运算之后，仍然不完全吻合，但它们具有相同的语义。举例来说，对于所有${\displaystyle n:\mathbb {N} }$ ，n + 1和1 + n这两条公式无论如何运算都不会断言等同，因为自然数加法的定义本身就区分先后顺序。故此，我们不能写“对于所有${\displaystyle n:\mathbb {N} }$ ，n + 1 ≡ 1 + n”。然而，对于任何特定的自然数n，例如2，我们可以通过运算得出“2 + 1 ≡ 1 + 2”。这种从定义上不同但从含义上相同的现象，正正就是内涵和外延之分，逻辑学家戈特洛布·弗雷格称之为意涵与指称（英语：Sense and reference）之分。

针对这第三种等同关系，类型论有一种意义重大的“等同类型”。对于任何两条类型相同的公式p, q : A，都有一个类型Id_A(p, q)，指的是“p等于q”这一命题。在不怕混淆的情况下，可以使用更熟悉的写法“p =_A q”，其中类型下标A往往可以省略。根据命题为类型原理，要证明此命题，就必须提供它的项（此命题为真的见证物）。等同类型只有一条建构式：对于任何项a : A，可以建构refl_a : a =_A a，称为“自反”。由于断言等同的公式都可以随意互换，所以只要有a ≡ b，那就自动有a =_A b。要证明“对于所有${\displaystyle n:\mathbb {N} }$ ，n + 1 = 1 + n”这一命题，就必须给出这样的项：

${\displaystyle {\mathsf {add\_one\_eq\_one\_add}}:\prod _{n:\mathbb {N} }(n+1=_{\mathbb {N} }1+n).}$ 

要建构这样的项，须展开1和加号的定义，然后结合利用依赖类型、自然数和等同类型的建构和消去式。再举一例，${\displaystyle 0=_{\mathbb {N} }1}$ 也是一条合乎语法的等同类型，但它所代表的是一条假命题，所以它不含任何项。

归纳类型

归纳类型是定义新类型的一套规则，以上介绍的0、1、2、${\displaystyle \mathbb {N} }$ 、A × B、a =_A b等都是其特例。要定义一个归纳类型，必须列出它的建构式。每一条建构式不但可以直接输出该类型的项（如∗ : 1），它的输出项还能依赖于某个变量（如inl : A → A + B），甚至归纳性地依赖于该类型自己的项（如${\displaystyle {\mathsf {succ}}:\mathbb {N} \to \mathbb {N} }$ ），从而建构出无限大的数学结构。归纳类型代表了由它的建构式所自由生成的结构，也就是说，它的项正好都是从无开始，通过重复应用任一条建构式后所得的。本文不试图详列归纳类型的严格定义。

举例来说，我们可以用归纳类型来定义整数${\displaystyle \mathbb {Z} }$ 。它有两条建构式：

• ${\displaystyle {\mathsf {ofNat}}:\mathbb {N} \to \mathbb {Z} }$ ，从每一个自然数可建构一个对应的非负整数
• ${\displaystyle {\mathsf {negSucc}}:\mathbb {N} \to \mathbb {Z} }$ ，从每一个自然数可建构一个对应的负整数（理解为−(n + 1)）

要建构某一个整数，须先指定用哪一条建构式，然后指定一个自然数。

再以幺半群为例，它只有一条比较长的建构式，为方便阅读以文字写出：

• 一个类型G，一个乘法函数G × G → G（记作(a, b) ↦ a * b），一个单比特e : G，以及以下两项条件的证明：
  • 对于任何x : G，x * e = x且e * x = x
  • 对于任何x, y, z : G，x * (y * z) = (x * y) * z

要建构某一个幺半群，只须提供这单一条建构式所规定的所有项。

同伦类型论是类型论底下一个活跃的研究范畴，它主张从同伦论的角度视每一个类型为（拓扑）空间，并且从范畴论的角度视类型为高维广群。符拉基米尔·弗沃特斯基在研究余调和∞广群的时候，多次遇到某些证明含有错误，但在同行评审的过程中成为了漏网之鱼，这促使他意识到电脑自动验证证明的重要性。另一方面，他发现数学家常年以来普遍使用的策梅洛-弗兰克尔集合论并不能作为满足现代数学论证的日常用途的数学基础。因此他利用Coq证明协助器，在构造演算（类型论的一种）的基础之上研发出基于一价公理上的新数学基础。

基本概念

在这样的框架下，类型的项可以想象成空间里的点，而两个项之间等同则可以想象成两个点之间有一条路径。假如类型A中有两项等同p : a =_A b，这可以理解为“p是始于a而终于b的路径”。等同类型的对称性意味着存在p⁻¹ : b =_A a，可以理解为“p⁻¹是始于b且终于a的路径”。当然，每个项都有自己的自反路径refl_a : a =_A a，可以理解为停留在a上不动的路径。

利用等同类型的递移关系，可以从p : a =_A b和q : b =_A c得出p ∘ q : a =_A c。理解为路径的话，路径p和路径q可以复合（串联）起来形成一条始于a而终于c的路径p ∘ q。假如我们复合p和它的对称，就会得出p⁻¹ ∘ p : a =_A a。不过，这一条路径往b点跑了一个来回，并不完全等同refl_a，尽管两者都是同一条命题的证明。这体现了同伦类型论所强调的“证明相关性”。

从拓扑空间的角度来看，由于p⁻¹ ∘ p沿着同一条线来回跑，所以它可以连续“缩小”至原地不动的refl_a，而不怕中途被某个“孔”勾住。这种路径与路径之间的连续变换称为同伦，亦可视为始于p⁻¹ ∘ p而终于refl_a的一条二维路径，记作

p⁻¹ ∘ p =_{a =A a} refl_a.

循同样的规律，很自然地有二维路径之间的三维路径（同伦间的同伦），三维路径之间的四维路径，等等。

从抽象代数的角度来看，路径之间的复合可以视为乘法，自反路径refl_a可以视为单比特，而任何路径p的对称p⁻¹可以视为反元素。这类似于群的结构，但有两点差异。第一，不是任何两条路径都可以复合，因为其中一条的终点必须是另一条的起点，意味着这只是一个广群而不是群。第二，p⁻¹ ∘ p只是和refl_a同伦等价而不是完全等同，因而反元素（结合律同理）只是在同伦意义上得到满足，故此只能说是弱广群。整体来说，这种具有无限层的类型结构形成弱∞广群（英语：∞-groupoid）。

任何函数f : A → B都会将命题等同的两个项映射至两个命题等同的项，从范畴论的角度可以说类型论中的函数都是函子，而从拓扑学的角度则可以说每个函数都是连续的。

拓扑学的纤维化和范畴论的等价等等概念同样也有类型论的模拟。

一价公理

在拓扑学中，假如两个空间是同伦等价的，那么它们的许多拓扑性质也会是相同的。因为同伦这一概念在类型论中也有对应的“等价”概念，所以我们可以写下“类型A, B : 𝒰是等价的”这样的命题，记作A ≃ B。

在一般“非形式化”的数学推理当中，也就是不纠结于数学基础细节的时候，数学家往往会滥用符号，随意互换两个等价但严格来说不完全等同的对象。例如，群论所研究的是同构意义上不同的群的性质，而拓扑学所研究的是同胚意义上不同的空间的性质。换言之，数学家一般并不在乎两个等价结构之间定义上的细节差异。例如，实数到底是以戴德金分割还是柯西序列来表示并不重要，更重要的是它的抽象性质，特别是在与另一个等价结构互换以后仍然不变的性质。传统的集合论把所有结构都以层层相叠的集合来表达，无法做这种符合结构主义（英语：Structuralism (philosophy of mathematics)）的数学推理。

类型论对类型的定义恰好遵循结构主义，但在“两个等价的类型可以互换”这一问题上，我们只能对于每一点对点价类型A ≃ B逐一证明。弗沃特斯基因此提出在纯粹的类型论上加入一条新的公理，称为一价公理：

(A =_𝒰 B) ≃ (A ≃ B),

可以读成

“等同”等价于“等价”。

一价公理推广了同一个全类以下两个类型之间的等同关系。它要求同伦类型论下的所有定义都不违背类型间的同伦等价。对于任何同伦等价e : A ≃ B和任何项t : P(A)，其中P(A)是利用A建构出的类型，都可得出一个对应的项e^∗t : P(B)。

以一价公理作为数学基础，终于能够对常用的数学推理手法做严谨的形式化表述。

更高归纳类型

更高归纳类型是在同伦类型论的框架下对归纳类型的推广。更高归纳类型的建构式不但可以像普通归纳类型一样建构新的项（点），它还能够建构新的等同类型的项（两点之间的路径）。例如，我们可以定义拓扑学意义的圆${\displaystyle \mathbb {S} ^{1}}$ ，它有两条建构式：

• ${\displaystyle {\mathsf {base}}:\mathbb {S} ^{1}}$ ，圆的基点
• ${\displaystyle {\mathsf {loop}}:{\mathsf {base}}=_{\mathbb {S} ^{1}}{\mathsf {base}}}$ ，从基点至基点的路径

这第二条建构式所建构的是有别于常值路径${\displaystyle {\mathsf {refl}}_{\mathsf {base}}:{\mathsf {base}}=_{\mathbb {S} ^{1}}{\mathsf {base}}}$ 的另一条（一维）路径，为这一类型赋予了不平凡的拓扑结构。

再举一例，我们可以定义拓扑学意义的球面${\displaystyle \mathbb {S} ^{2}}$ ，它同样有两条建构式：

• ${\displaystyle {\mathsf {base}}:\mathbb {S} ^{2}}$ ，球面的基点
• ${\displaystyle {\mathsf {surf}}:{\mathsf {refl}}_{\mathsf {base}}=_{{\mathsf {base}}=_{\mathbb {S} ^{2}}{\mathsf {base}}}{\mathsf {refl}}_{\mathsf {base}}}$ ，非平凡的二维路径

尽管定义里只有基点和一条二维路径，但是可以证明${\displaystyle \mathbb {S} ^{2}}$ 还有一条非平凡的三维路径，其起点和终点都是refl_reflbase。这就是霍普夫纤维化，同时印证了，更高归纳类型的简单定义也可以创造出复杂而不易预见的拓扑结构。

广义地来说，更高归纳类型的建构式可以建构任何更高维度的路径（同伦）。

主要

• 简单类型λ演算，一种高阶逻辑；
• 直觉类型论；
• 系统F;
• LF经常用来定义其他类型论；
• 构造演算及其派生理论。

次要

• Automath（英语：Automath）；
• ST类型论;
• 组合逻辑的一些形式；
• λ立方体中定义的其他；
• 其他有类型λ演算;
• 其他纯类型系统（英语：pure type system）。

活跃

• 正在研究中的同伦类型论