类型

依值类型论中, 类型 (或依值函数类型) 是函数类型依值类型论中的推广, 使得函数输出值的类型 可以随输入值 的变化而变化.

具体地说, 给定类型 , 并对每个 给定类型 , 类型是类型构造它的实例的方法是, 对每个 给出 , 这就可以理解为 上的函数, 只是函数的值可以在不同的类型中. 因此, 有时也直接用 “函数” 指代 类型的实例. 如果这些 是不随 而变的类型 , 则相应的类型就是真正的函数类型.

类型论–范畴论–逻辑学类比中, 类型可以类比于一些熟悉的数学对象.

范畴论中, 类型对应于截面范畴. 首先我们将 类型视为底空间上纤维化的全空间. 例如在拓扑空间范畴中, 类型 可以理解为 纤维丛. 此时 类型可以理解为它的截面构成的空间: 对每个 给出纤维 中的元素. 如果 不随 而变化, 类型就是平凡丛 的截面, 也就是映射空间 .

谓词逻辑中, 类型可以类比为含有全称量词的命题: 想象每个 都是命题, 则 类型 可以理解为 “对任意 中的元素 , 均成立”. 事实上如果在类型论的视角下看待命题, 则构造 类型中实例的过程 (也就是证明命题的过程), 就是要对任意的 找到实例 , 也印证了上述全称量词的直观.

1类型规则

本质上是将函数类型中的返回类型 所在的语境从 改到了 .

在考虑变量名时, 也可以写作 , 这样更能体现 类型和函数类型的联系.

以下规则均使用和函数类型相同的语法和名称.

构造规则

消去规则

消去规则满足如下计算规则:

2范畴语义

参见: 依值积

类型的构造过程可以描述如下: 首先有类型 , 然后对于任何类型 , 都可以构造出类型 , 这个过程可以看作一个映射 .

将依值类型论视为一个概括范畴 的话, 可以这么看待: 对于任何代表类型的态射 , 根据纤维范畴的性质, 它能引导出一个反变函子 . 这个函子的伴随函子就是前面提到的 函子, 并且这对伴随的余单位对应 类型的消去规则.