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