类型论

类型论不是一张数据类别清单，而是一组研究表达式、类型及其推导关系的形式理论。典型判断写作Γ⊢t:A，表示在上下文Γ给出的变量假设下，项t具有类型A。上下文的作用不可省略：同一个变量名称离开其声明，不会自动具有固定含义。

类型形成规则规定哪些写法是合法类型，项的规则规定怎样构造表达式并推出其类型。例如已知A、B是类型，可形成函数类型A→B；若f:A→B且a:A，则应用f(a)具有类型B。规则把一项复杂判断拆成能够逐层检查的前提，而不是靠名称相似或程序员直觉决定。

参考：[1]

简单类型系统可以从基本类型出发，用函数类型等构造建立更复杂类型。自然数到自然数的函数与自然数本身不是同一类型；要求自然数参数的函数不能任意接受布尔值。在带类型的λ演算中，函数抽象与函数应用对应相应的推导规则，计算则可由把参数代入函数体来描述。

这些限制也与逻辑基础有关。罗素为处理悖论发展了类型思想，丘奇在1940年给出了以λ演算表达简单类型论的形式。不能由此把所有现代类型系统视为同一个体系：允许哪些基本类型、递归、公理和等同性规则，会改变系统的表达能力与性质。

参考：[1]

依赖类型允许一个类型随某个项的值变化。例如Vector A n不仅记住元素类型A，也记住长度n；长度3与长度4的向量因而可在类型层面区别。把一个元素放到长度n的向量前端，结果类型能表达长度变成n＋1，而不只是笼统地说结果仍是向量。

依赖函数类型可写为(x:A)→B(x)，函数对每个输入x返回B(x)类型的值。若B实际不依赖x，就退化为普通A→B。这样的表达力让规格信息进入类型，也让检查过程需要比较计算后的类型表达式；具体能否自动完成、需要多少辅助证明，取决于所采用的理论和实现。

参考：[2]

在程序语言中，类型系统用于组织接口、限制不合适的运算，并为类型检查和类型推断提供依据。类型标注是某种语言呈现这些信息的语法，不是类型论的全部。一个程序满足类型规则，不能自动推出它符合用户的全部需求；只有进入规格与规则的性质，才可能得到对应保障。

在数学基础的语境中，类型论还可表达数学对象、命题和证明，依赖类型尤其便于把构造与性质联系起来。它与集合论可以相互研究和解释，却不宜简单把t:A等同于集合论公式t∈A：前者通常是规定表达式合法归属的判断，后者是理论内部可讨论真假的成员关系命题。两种框架的组织方式及具体公理都需要分别说明。

参考：[1] [2]