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

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

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

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

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

1 类型规则

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

Γ ⊢ ∏ x : A ​ B Γ ⊢ A Γ , x : A ⊢ B ​

在考虑变量名时, 也可以写作 ( x : A ) → B ( x ) , 这样更能体现 Π 类型和函数类型的联系.

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

构造规则

Γ ⊢ λ x . u : ∏ x : A ​ B Γ , x : A ⊢ u : B ​

消去规则

Γ ⊢ ap ( u , v ) : B [ x ↦ v ] Γ ⊢ u : ∏ x : A ​ B Γ ⊢ v : A ​

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

Γ ⊢ ap ( λ x . u , v ) = u [ x ↦ v ] : B [ x ↦ v ] Γ , x : A ⊢ u : B Γ ⊢ v : A ​

2 范畴语义

参见: 依值积

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

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

3 相关概念