简介

直觉类型论 (Intuitionistic type theory, 或 Martin-Löf's type theory) 中, 定义了一些于经典类型论中没有的高阶类型: \(\Pi\)-类型 (依赖函数类型, Dependent function types) 以及 \(\Sigma\)-类型 (依赖乘积类型, Dependent pair types), 该种类型系统可被对应到 \(\lambda\)立方体 中的 \(\lambda P\) 上. 本篇章大部分内容均来自于对 Hott Book 的理解与翻译, 再稍加改动并引入 Agda 作举例用途. 在此推荐读者配合其中 第一章 Foundations 的 1.4 ~ 1.7 节 进行阅读. 由于篇幅过长, 文章将会分为上下两节, 而本篇将先行介绍 全类, \(\Pi\)-类型 以及 乘积类型 的概念.

全类 (Universes)

全类多态 (Universe polymorphism)

于经典类型论中, 一般会非形式化地称 "\(A\) 是一个类型", 但为了更准确的形式化地定义出这种关系, 以及描述类型与项之间的关系, 我们需要引入一个全新的概念: 全类 (Universes). 全类的意思就相当于 "整个宇宙" 一般, 其是这个宇宙中所有类型的类型, 一般地会写为 \(U_\infty\). 而当我们试着从集合论出发去定义全类时, 由于 \(U_\infty\) 能够包含自身, 即 \(U_\infty : U_\infty\), 但此处将会引发一个非常严重的问题, 即集合论上这么定义是 不可靠的 (Unsound) , 这将直接导致罗素悖论 (Russell's paradox) 的出现. 为了避免这种情况的发生, 我们需要独立且不依赖集合论的情况下重新定义出全类的层级:

\[ U_0 : U_1 : U_1 :\ ... \]

一般地我们会写为 \(U_i\) (这里的 \(i\) 为全类的层级), 而每个 \(U_i\) 都是 \(U_{i+1}\) 的元素 (也就是一个大宇宙内包含着一个小宇宙). 而我们称这种分层是 可累加的 (Cumulative), 即对于所有于 \(i^{th}\) 全类内的元素亦都是 \((i + 1)^{st}\) 内的元素, 例如有 \(A : U_i\), 即亦有 \(A : U_{i+1}\), 而这种概念可被称为 全类多态 (Universe polymorphism) .

隐式层级 (Implicit level)

而于大部分的情况下, 并不需要显式地标记出全类的层级 \(i\), 而亦可将其隐藏起来, 因此可以写成 \(U : U\) (其含义与 \(U_i : U_{i+1}\) 等价), 这种写法称之为 Typical ambiguity. 这种写法虽然较为便捷, 但还是会略带点危险性, 因为其将允许我们写出看似合法的, 但实质可能会诱发各种自引用悖论的证明. 不过在这里其实也无需太过担心, 于 Agda 或者 Coq 这些语言上, 其全类层级都是可以自动推导得出的.

小类型 (Small types)

由于全类多态的出现, 允许了我们编写出表达能力极强的类型系统, 除了类型本身外, 不仅仅可以定义出 "类型的类型", 即 \(Kind\) (类型构造器), 还可以定义出类型的类型的类型, 类型的类型的类型的类型, 即 $Type_1 : Type_2 : Type_3 : ... $ 等等. 然后假设现在有 \(U\), 而所有归属于该 \(U\) 的元素 (类型) 均可被称之为 \(U\)小类型 (Small types).

类型族 (Families of types)

为了使类型也能够被参数化, 把一个类型当作函数看待是被允许的. 例如设有类型 \(A\), 然后有一函数 \(B : A \to U\), 其接受 \(A\) 作为参数, 返回 \(B\) 这个类型, 而陪域上则是 \(U\). 这种函数我们一般称为 类型族 (有时候可被视为依赖类型).

例如当我们想要模拟出模数取模时, 定义出有限集合 \(\{ m\ |\ m < n \}\) 有利于以循环群的形式进行运算, 而该集合则可定义为 Fin : \(\Bbb{N} \to U\), Fin(\(n\)) 的 \(n\) 则表示了其集合的边界位置, 对应到 Agda 中 Data.Fin.Base 的定义如下:

1
2
3
data Fin : ℕ → Set where
zero : {n : ℕ} → Fin (suc n)
suc : {n : ℕ} (i : Fin n) → Fin (suc n)

而最直观的且非常重要的例子就非 Constant type 莫属了, 其定义如 \((\lambda (x : A). B) : A \to U\), 由于这个类型族无论参数如何变化, 其永远返回的都将是 \(B\), 则其可被视为为 \(B : U\) .

Agda 上的定义

于 Agda 上, Set 类型对应的就是全类的概念, 而 Set \(\ell\) 中的 \(\ell\) 则是全类的层级. 而全类层级于 module Agda.Primitive 中的定义如下:

1
2
3
4
5
6
7
8
9
10
11
12
13
...

infixl 6 _⊔_

postulate
Level : Set

postulate
lzero : Level
lsuc : (ℓ : Level) → Level
_⊔_ : (ℓ₁ ℓ₂ : Level) → Level

...

该层级的定义实际上是个内置于 Agda 中的自然数, 并非直接使用的 Data.Nat (\(\Bbb{N}\)) 类型.

\(\Pi\)-类型 (\(\Pi\)-Type)

\(\Pi\)-类型, 又称为 依赖函数类型 (Dependent function type), 是依赖类型的一种. 其于陪域的类型将依赖于传入的值, 即到达域的值而作出改变. 而之所以称为 \(\Pi\)-类型 是因为这种类型可以被视为是在类型之上的笛卡儿积.

定义

形式化地, 假设现在有类型 \(A : U\) 以及类型族 \(B : A \to U\), 我们便能够构造一个依赖函数类型 \(\Pi_{(x : A)} B(x) : U\). 当然还有许多种不同的写法可供选择, 例如以下这些:

\[ \Pi_{(x : A)} B(x) \qquad \underset{(x : A)}{\Pi} B(x) \qquad \Pi (x : A), B(x) \]

而对应到 Agda 中的类型标签则如下:

1
_ : ∀ (A : Set) {x : A} {B : A → Set} → B x

而在一个特殊情况下, 当 \(B\) 是一个 Constant family 时, 即 \(B\) 并没有依赖于 \(x : A\), 则依赖函数类型将 "坍塌" 成一普通函数:

\[ \Pi_{(x : A)} B \equiv (A \to B) \]

1
_ : ∀ (A : Set) {x : A} {B : Set} → B

在上面给到的例子以及定义中, 类型标签本身是没有名字的 (即 Agda 中的 _), 实际上我们无论于形式化的定义上, 还是 Agda 中, 都可以给予相应的名字, 如: \(f : \Pi_{(x : A)} B(x)\), 即 \(f\) 是为一依赖函数的名字, 使得他们是 显式定义 (Explicit definitions) 的. 而除了类型外, 一个依赖函数若果带有诸如表达式 \(\Phi : B(x)\) 而涉及到 \(x : A\) 的话, 可被描述为:

\[ f(x) :\equiv \Phi \qquad 对于 x : A \]

当然亦可替代成使用 \(\lambda\)-abstraction 的形式进行定义:

\[ \lambda x. \Phi : \underset{x : A}{\Pi} B(x) \]

全类上的多态

多态能够应用于给定的全类上, 这是又一依赖函数类型至关重要的特性. 用通俗的话来说即是假设现在有 \(id : \Pi_{(A : U)} A \to A\) 这么一个依赖函数类型, 而此处则可以像类型族一般, 接受一个类型作为参数, 然后作用于类型 \(A\) 的表达式上, 就如同 \(id :\equiv \lambda (A : U). \lambda (x : A). x\) 一样.

而另一个多态函数的例子 swap (或 flip) 函数, 相信大家都非常熟悉的了, 我们可以观察一下它是怎么定义的:

\[ swap : \underset{(A : U)}{\Pi} \underset{(B : U)}{\Pi} \underset{(C : U)}{\Pi} (A \to B \to C) \to (B \to A \to C) \]

且其表达式为:

\[ swap(A, B, C, g) :\equiv \lambda b. \lambda a. g(a)(b) \]

当然地, 我们在表达式上并无需要使用到 \(A\), \(B\), \(C\) 时, 则可以将其隐藏起来, 如:

\[ swap_{A, B, C}(g)(b, a) :\equiv g(a)(b) \]

但不要忘记, swap 仅仅还只是个普通的多态函数而已! 我们现在需要做的是定义出一个基于依赖函数类型的多态函数 swap', 例如:

\[ swap' : \underset{(A : U)}{\Pi} \underset{(B : U)}{\Pi} \underset{(C : A \to B \to U)}{\Pi} (\underset{(x : A)}{\Pi} \underset{(y : B)}{\Pi} C(x, y)) \to (\underset{(y : B)}{\Pi} \underset{(x : A)}{\Pi} C(x, y)) \]

而对于上面的 \(C(x, y)\), 实际上等同于 \(C(x)(y)\), 即相当于柯里化. 下面则为 Agda 于 Function.Core 下的对照版本:

1
2
3
flip : ∀ {A : Set a} {B : Set b} {C : A → B → Set c} →
((x : A) (y : B) → C x y) → ((y : B) (x : A) → C x y)
flip f = λ y x → f x y

再来一个 _∘_ (Compose) 的例子:

非依赖类型的情况下是:

\[ comp : \underset{(A, B, C : U)}{\Pi} (B \to C) \to (A \to B) \to (A \to C) \]

而使用了依赖函数类型定义的则是:

\[ comp : \underset{(A, B, C : U)}{\Pi} \underset{(B : A \to U)}{\Pi} \underset{(C : \underset{(x : A)}{\Pi} B(x) \to U)}{\Pi} (\underset{(x : A)}{\Pi} \underset{(y : B(x))}{\Pi} C(y)) \to \underset{(g : \underset{(x : A)}{\Pi} B(x))}{\Pi} (\underset{(x : A)}{\Pi} C(g(x))) \]

Agda 上的定义则是:

1
2
3
4
_∘_ : ∀ {A : Set a} {B : A → Set b} {C : {x : A} → B x → Set c} →
(∀ {x} (y : B x) → C y) → (g : (x : A) → B x) →
((x : A) → C (g x))
f ∘ g = λ x → f (g x)