类型论，数学、逻辑和电脑科学以下的一个分支，是研究不同类型系统及其表达形式的学科。某些类型系统适合用作数学基础，取代数学家一般使用的集合论，其中最具影响力的有阿隆佐·邱奇的有类型λ演算和佩尔·马丁-洛夫的直觉类型论。许多函式语言和工具都建立在类型论的基础上，如Agda、Coq、Idris、Lean等等。 类型论的核心概念是，每一条合乎语法规则的表达式（或称「项」）都有其所属的「类型」。通过结合多个基础类型，可以定义更加复杂的类型。如此得出的类型可以代表林林总总的数学结构，如自然数、群、拓扑空间等等。在集合论中，这些结构都是含有元素（或称成员）的集合，它的定义纯粹就是指定其所含的所有元素。在类型论中，这些结构的定义并不罗列属于它的所有项，而是指定如何建构它的项的一套规则。 集合论建基于一阶逻辑，有「集合」和「命题」两个主要概念。任何一套集合论公理（如策梅洛-弗兰克尔集合论）和命题都是以一阶逻辑的语言所表达。类型论则只有「类型」的概念，每一条逻辑命题都是一个类型。要证明任何一条命题，就需要建构属于此类型的项，是为命题为类型原理。换言之，证明定理的过程只不过是建构符合指定数学结构的数学物件的过程的一个特例。 概览. 类型论有许多种，底下更细分许多变体，本文只能以直觉类型论为例做基本的入门介绍，而不详细罗列每一种变体。 项与类型. 在类型论中，每一个数学对象都有其所属的类型（笼统地来说，这个类型的独一无二的）。每次加入新的变数时，必须同时指定其所属的类型。举例说，「设"x"为自然数」可写作 formula_1 读作「项"x"的类型是formula_2」。这在形式上似乎和集合论中的formula_3（「"x"是集合formula_2的元素」）无所差异，但后者是一阶逻辑中具备真值的一条「命题」，而前者则是一个纯粹的「断言」，并不是一条有待证明的命题。 类型建构规则. 每一种类型论都指定了如何建构新类型（及其项）的一套规则，通过这些规则所得出的式子都是合理的断言，不须证明。以下归纳每一个新类型定义的组成部分： 以上是类型论的基本规则，可理解为类型论的语法，它并不包含数学公理。这和集合论有所不同：除了一阶逻辑本身的推理规则以外，集合论还加入了一组有关集合的公理（如策梅罗-弗兰克尔公理系统）。最基本的类型论不需公理即可当做逻辑和数学推理使用，但在有需要时，同样也可以加上额外的公理。类型论中的公理是不通过建构规则而接纳的断言，因此有些公理会产生无法通过运算规则简化的式子，从而影响该类型系统的可计算性。 常见类型. 以下列出几种常见的基本类型，除了全类和（依赖）函数类型以外，它们都是最后介绍的的特例。这些类型既可以表达数学结构，又可以表达命题。类型的项可以是某个数学结构的成员，也可以是某条命题的证明。这就是命题为类型原理。 全类. 类型论规定，在介绍新的符号时，必须马上指定它的类型，如「设formula_5」。同样，当我们说「设"A"为类型」的时候也一样要指定"A"自己的类型。然而，"A"本身就已经是一个类型，那么类型的类型是甚么？类型论中有「全类」的概念，每个全类的项都是类型。由于全类本身也是一个类型，如果所有类型都属于同一个全类的话，就不可避免产生（罗素悖论在类型论中的体现）。因此，类型论一般都会假设存在无限层全类，记作0, 1, 2，如此类推。每一层全类都是它上一层全类的项："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")），都可以建构依赖类型 formula_6 要定义依赖类型的某个项（即某个依赖函数），同样有两种方法。直接定义：取名"f"，对于任意项"a" : "A"，将"f"("a")定义为一条可能含有"a"并且类型为"B"("a")的公式Φ。λ抽象化：直接写 formula_7 假如"A"是任意类型而"p" : "A" → 是一族代表命题的类型，那么formula_8就代表了「对于所有"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"是有栖居对象的类型」（类型论区分「有栖居对象」和「非空」这两个概念）。 双值类型. 双值类型记作formula_9或2，它有两条构件式，因此有两个项，记作「02, 12 : 2」。双值类型就是函数式编程中的布林，其两个项可以分别理解为「如果假」和「如果真」两个情况。函数"f" : 2 → "A"可以理解为「如果真，输出"f"(12) : "A"，否则输出"f"(02) : "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"0 : "A" → "C"和"g"1 : "B" → "C"，使得"f"(inl("a"))定义为"g"0(a)，"f"(inr("b"))定义为"g"1(b)。 余积类型可以诠释为逻辑或：假如类型"A", "B", "C"都是命题，则函数"f" : "A" + "B" → "C"可以理解为「假如有"A"的证明，或者有"B"的证明，只需其一就可以用"f"得出"C"的证明」。更简短地说，「"A"或"B"为真时，则"C"为真」。 上文介绍的双值类型可视为余积类型的特例，等同于1 + 1。 依赖对类型. 依赖对类型，又称Σ类型，是积类型的推广，使得每个项("a", "b")中的第二个对象"b"的类型可以依赖于"a"。对于任何类型"A"和一族类型"B" : "A" → ，可以建构依赖对类型 formula_10 它的项的格式是("a", "b")，其中"a" : "A"，而"b" : "B"("a")。 假如"A"是任意类型而"p" : "A" → 是一族代表命题的类型，那么formula_11就代表了「存在"a" : "A"使得"p"("a")为真」这一命题。值得注意的是，这种存在比经典数学中的存在更强，因为类型论要求我们明确提供见证"p"("a")为真的那个项"a"，而经典数学则无此要求（比如可以婉转地证明「不可能不存在这样的"a"」）。这意味著，最纯粹的类型论表达的是一种构成主义数学。通过引入各种公理，如排中律和选择公理，类型论仍然可以灵活地表达非构成主义的经典数学。 自然数. 类型论一般按照皮亚诺算术来定义自然数formula_2。它共有两条建构式： 任何自然数，要么是0，要么是某个自然数的后继（即等于formula_15，其中formula_5）。一、二、三分别表达为formula_17、formula_18、formula_19，如此类推。 要定义某个函数formula_20，须指定一个起始项"g"0 : "A"以及一个「下一步」函数formula_21，使得"f"(0)定义为"g"0，并且对于任何formula_5，formula_23定义为formula_24，也就是以0为起始点利用数学归纳法做一个递归性的定义。比如，以下是「奇偶」函数formula_25的定义： 这里我们也用到了双值类型2的消去式。其他常见函数，例如「双倍」函数formula_32以及加法formula_33等二元运算都有类似的定义。 等同类型. 类型论有至少三种可以理解为「等同」的概念。第一种是「符号等同」，又称「从定义上等同」，例如用1定义为代替formula_17的符号，这记作formula_35。自然数一节中的「定义为」就属于此种等同，也可以用:≡表示。这种等同是为了给符号赋予含义，但它本身不含任何额外的数学意义。 第二种是「断言等同」，即在展开两个符号的定义，并用类型论建构规则运算以后，两者的公式完全吻合，记作「"a" ≡ "b"」。例如，通过oddeven的定义，可做运算： formula_36 若"a" ≡ "b"，则在任何式子中出现的"a"都可以直接替换为"b"。此种等同属于断言，并不是逻辑命题，而是重复应用类型论语法规则后所得的符号等同。在类型论中，不允许说「假设"a" ≡ 1」，因为在设符号formula_37的时候，如果还没有给"n"赋予定义值，那就应该做定义「"a" :≡ 1」；反之如果"n"已经被赋予定义值（比如1），那就轮不到我们假设其数值。假如将类型论的规则视为某种代数系统，那么断言等同就正是该系统中的普通等同关系，类似于一个群的元素之间的等同。 第三种是「命题等同」。有时，两条公式就算在展开定义和运算之后，仍然不完全吻合，但它们具有相同的语义。举例来说，对于所有formula_5，"n" + 1和1 + "n"这两条公式无论如何运算都不会断言等同，因为自然数加法的定义本身就区分先后顺序。故此，我们不能写「对于所有formula_5，"n" + 1 ≡ 1 + "n"」。然而，对于任何特定的自然数"n"，例如2，我们可以通过运算得出「2 + 1 ≡ 1 + 2」。这种从定义上不同但从含义上相同的现象，正正就是内涵和外延之分，逻辑学家戈特洛布·弗雷格称之为之分。 针对这第三种等同关系，类型论有一种意义重大的「等同类型」。对于任何两条类型相同的公式"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"。要证明「对于所有formula_5，"n" + 1 = 1 + "n"」这一命题，就必须给出这样的项： formula_41 要建构这样的项，须展开1和加号的定义，然后结合利用依赖类型、自然数和等同类型的建构和消去式。再举一例，formula_42也是一条合乎语法的等同类型，但它所代表的是一条假命题，所以它不含任何项。 归纳类型. 归纳类型是定义新类型的一套规则，以上介绍的0、1、2、formula_2、"A" × "B"、"a" ="A" "b"等都是其特例。要定义一个归纳类型，必须列出它的建构式。每一条建构式不但可以直接输出该类型的项（如∗ : 1），它的输出项还能依赖于某个变量（如inl : "A" → "A" + "B"），甚至归纳性地依赖于该类型自己的项（如formula_14），从而建构出无限大的数学结构。归纳类型代表了由它的建构式所自由生成的结构，也就是说，它的项正好都是从无开始，通过重复应用任一条建构式后所得的。本文不试图详列归纳类型的严格定义。 举例来说，我们可以用归纳类型来定义整数formula_45。它有两条建构式： 要建构某一个整数，须先指定用哪一条建构式，然后指定一个自然数。 再以幺半群为例，它只有一条比较长的建构式，为方便阅读以文字写出： 要建构某一个幺半群，只须提供这单一条建构式所规定的所有项。 同伦类型论. 同伦类型论是类型论底下一个活跃的研究范畴，它主张从同伦论的角度视每一个类型为（拓扑）空间，并且从范畴论的角度视类型为高维广群。符拉基米尔·弗沃特斯基在研究余调和∞广群的时候，多次遇到某些证明含有错误，但在同行评审的过程中成为了漏网之鱼，这促使他意识到电脑自动验证证明的重要性。另一方面，他发现数学家常年以来普遍使用的策梅洛-弗兰克尔集合论并不能作为满足现代数学论证的日常用途的数学基础。因此他利用Coq证明协助器，在构造演算（类型论的一种）的基础之上研发出基于一价公理上的新数学基础。 基本概念. 在这样的框架下，类型的项可以想象成空间里的点，而两个项之间等同则可以想象成两个点之间有一条路径。假如类型"A"中有两项等同"p" : "a" ="A" "b"，这可以理解为「"p"是始于"a"而终于"b"的路径」。等同类型的对称性意味著存在"p"−1 : "b" ="A" "a"，可以理解为「"p"−1是始于"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"−1 ∘ "p" : "a" ="A" "a"。不过，这一条路径往"b"点跑了一个来回，并不完全等同refl"a"，尽管两者都是同一条命题的证明。这体现了同伦类型论所强调的「证明相关性」。 从拓扑空间的角度来看，由于"p"−1 ∘ "p"沿著同一条线来回跑，所以它可以连续「缩小」至原地不动的refl"a"，而不怕中途被某个「孔」勾住。这种路径与路径之间的连续变换称为同伦，亦可视为始于"p"−1 ∘ "p"而终于refl"a"的一条二维路径，记作 "p"−1 ∘ "p" ="a" ="A" "a" refl"a". 循同样的规律，很自然地有二维路径之间的三维路径（同伦间的同伦），三维路径之间的四维路径，等等。 从抽象代数的角度来看，路径之间的复合可以视为乘法，自反路径refl"a"可以视为单位元，而任何路径"p"的对称"p"−1可以视为反元素。这类似于群的结构，但有两点差异。第一，不是任何两条路径都可以复合，因为其中一条的终点必须是另一条的起点，意味著这只是一个广群而不是群。第二，"p"−1 ∘ "p"只是和refl"a"同伦等价而不是完全等同，因而反元素（结合律同理）只是在同伦意义上得到满足，故此只能说是弱广群。整体来说，这种具有无限层的类型结构形成弱。 任何函数"f" : "A" → "B"都会将命题等同的两个项映射至两个命题等同的项，从范畴论的角度可以说类型论中的函数都是函子，而从拓扑学的角度则可以说每个函数都是连续的。 拓扑学的纤维化和范畴论的等价等等概念同样也有类型论的类比。 一价公理. 在拓扑学中，假如两个空间是同伦等价的，那么它们的许多拓扑性质也会是相同的。因为同伦这一概念在类型论中也有对应的「等价」概念，所以我们可以写下「类型"A", "B" : 是等价的」这样的命题，记作"A" ≃ "B"。 在一般「非形式化」的数学推理当中，也就是不纠结于数学基础细节的时候，数学家往往会滥用符号，随意互换两个等价但严格来说不完全等同的对象。例如，群论所研究的是同构意义上不同的群的性质，而拓扑学所研究的是同胚意义上不同的空间的性质。换言之，数学家一般并不在乎两个等价结构之间定义上的细节差异。例如，实数到底是以戴德金分割还是柯西序列来表示并不重要，更重要的是它的抽象性质，特别是在与另一个等价结构互换以后仍然不变的性质。传统的集合论把所有结构都以层层相叠的集合来表达，无法做这种符合的数学推理。 类型论对类型的定义恰好遵循结构主义，但在「两个等价的类型可以互换」这一问题上，我们只能对于每一对等价类型"A" ≃ "B"逐一证明。弗沃特斯基因此提出在纯粹的类型论上加入一条新的公理，称为一价公理： ("A" = "B") ≃ ("A" ≃ "B"), 可以读成 「等同」等价于「等价」。 一价公理推广了同一个全类以下两个类型之间的等同关系。它要求同伦类型论下的所有定义都不违背类型间的同伦等价。对于任何同伦等价"e" : "A" ≃ "B"和任何项"t" : "P"("A")，其中"P"("A")是利用"A"建构出的类型，都可得出一个对应的项"e"∗"t" : "P"("B")。 以一价公理作为数学基础，终于能够对常用的数学推理手法做严谨的形式化表述。 更高归纳类型. 更高归纳类型是在同伦类型论的框架下对归纳类型的推广。更高归纳类型的建构式不但可以像普通归纳类型一样建构新的项（点），它还能够建构新的等同类型的项（两点之间的路径）。例如，我们可以定义拓扑学意义的圆formula_48，它有两条建构式： 这第二条建构式所建构的是有别于常值路径formula_51的另一条（一维）路径，为这一类型赋予了不平凡的拓扑结构。 再举一例，我们可以定义拓扑学意义的球面formula_52，它同样有两条建构式： 尽管定义里只有基点和一条二维路径，但是可以证明formula_52还有一条非平凡的三维路径，其起点和终点都是reflreflbase。这就是霍普夫纤维化，同时印证了，更高归纳类型的简单定义也可以创造出复杂而不易预见的拓扑结构。 广义地来说，更高归纳类型的建构式可以建构任何更高维度的路径（同伦）。 参阅. 参考文献. 延伸阅读.