类型

类型是类型论研究的基本对象之一, 类似于集合论中的集合. 定义集合时一般给出集合所有的元素, 这可能会引来若干问题:

•	无限集有时难以描述, 比如自然数集定义为包含 $0$ 和任意元素后继的最小集合, 而没有更直接的描述.

•	在集合论中, 所有数学对象全是集合, 而在我们直观中, 不同的数学对象应该属于不同的类型. 有时, 属于不同类型的数学对象可能恰好是相等的集合.

•	Russell 悖论: 所有集合的集合并不能存在.

另一方面, 类型则直接通过规则来定义:

•	规定什么样的表达式对应某类型的实例, 相当于给出类型的生成元, 这对应构造规则;
•	规定什么样的表达式能使用某类型的实例, 相当于给出它满足的万有性质, 这对应消去规则.

这样就绕开了集合的概念, 而定义出的每个实例都只属于各自的类型.

大部分数学都能以类型论为基础而重新表述.

1例子

术语翻译

类型 • 英文 type • 德文 Typ (m) • 法文 type (m) • 拉丁文 typus (m) • 古希腊文 τύπος (m)