子类型

类型论中, 子类型集合之间子集概念的类比.

集合论中的子集有两种观点, 集合 的子集 一方面可以视作 的幂集中的元素 , 另一方面可以视作集合 到集合 的嵌入 . 与之相对应, 类型论也有两种子类型的概念, 被称为质料子类型结构子类型.

1定义

质料子类型

定义 1.1.命题宇宙 (或将其视作子对象分类子的真值对象), 定义 幂类型为从 函数类型:

定义 1.2. 定义 质料子类型为其幂类型中的元素 .

定义 1.3. 定义 中元素 和质料子类型 之间的局部属于关系 为:

结构子类型

定义 1.4. 对于函数 , 我们称 嵌入, 当且仅当对任意 , 函数等价.

定义 1.5. 结构子类型是二元组 , 其中 是类型, 的嵌入 .

质料子类型与结构子类型的比较

质料子类型和结构子类型之间有一一对应的关系.

给定质料子类型 , 其对应的结构子类型可以表达为:

反之, 给定结构子类型 , 相应质料子类型可以表达为:

另外, 定义函数 , 那么可将其视作一种子类型分类子. 具体来说, 质料子类型 与其对应的结构子类型 可构成如下的拉回图表:

外延子类型

警告. 本定义不被主流数学界所采用.

定义 1.6. 若对于任意 满足 , 都有 , 那么 子类型, 记作 .

该定义可以写作类型规则: 该性质又叫 Liskov 替换原则.

这种子类型的定义存在明显的问题. 若 , 那么 的实例就是 的实例, 这使得一个值可以对应多个不等价的类型, 违背了类型论中的内涵性思想.

术语翻译

子类型英文 subtype

质料子类型英文 material subtype

结构子类型英文 structural subtype

局部属于关系英文 local membership relation

Liskov 替换原则英文 Liskov substitution principle (LSP)