类型

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

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

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

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

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

规定什么样的表达式对应某类型的实例, 相当于给出类型的生成元, 这对应构造规则;

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

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

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

1例子

圆周

函数类型

自然数类型

宇宙

类型 类型

2相关概念

集合

类型论

术语翻译

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