2020-04-18 | 研究与探索 | UNLOCK

《The Little Typer》笔记:0≠1

前置知识

自然数

自然数类型是 Nat,有两种构造器 zeroadd1,其中 add1 接受一个 Nat 参数。因此 0 就是 zero1 就是 (add1 zero),2 就是 (add1 (add1 zero)),等等。Nat 有一个归纳析构器 ind-Nat,这样就可以不用递归写 Nat 的依赖函数啦。

相等类型

Pie 的内置类型 (= E e1 e2) 表达“类型为 Ee1e2 相等” 这一命题,唯一的构造器(也就是证明)是 (same e),产生一个类型为 (= E e e) 的值;当 e1e2 不相等时,没有 (= E e1 e2) 类型的值。

反命题、归缪

直觉主义逻辑表达假命题的方式是“推出谬”,在 Pie 中就是 (→ X Absurd) 类型,Absurd 类型没有值,却有一个可以导出任意类型的析构器(eliminator)ind-Absurd,因此命题 a ≠ b 对应的类型是 (→ (= E a b) Abusrd)

0≠1

在 Agda 里以上都可以自定义,0 ≠ 1 这种命题也可以用谬模式(absurd pattern)轻易地写出来:

1
2
3
4
5
6
7
8
9
10
11
data ≡ {A : Set} (x : A) : A → Set where
refl : (≡ x x)

data Nat : Set where
zero : Nat
add1 : Nat → Nat

data Absurd : Set where

0≠1 : (≡ zero (add1 zero)) → Absurd
0≠1 ()

最后一个 () 就是谬模式,意思就是编译器和你都知道那玩意是根本构造不出来的,所以以谬推谬,返回啥都行。

但 Pie 可没有这么聪明,它能做到的事更多是“检查”而非“推导”。看起来想写出 (→ (= zero (add1 zero)) Absurd) 很困难,怎样才能从一个不存在的东西((= zero (add1 zero)))得到另一个不存在的东西(Absurd)呢?

我们可以用依赖类型(dependent type)的精髓——从值到类型来解决这个问题。首先定义 =consequence,它把两个自然数映射到一个类型上,其中 zerozero 结果是 Trival,它们显然相等;zero(add1 n) 或者 (add1 n)zero 结果是 Absurd,它们显然不相等;(add1 m)(add1 n) 的结果则是 (= Nat m n)——它们的相等性可由 mn 的相等性归纳给出。=consequence 的完整定义:

1
2
3
4
5
6
7
8
9
10
11
(claim =consequence (→ Nat Nat U))
(define =consequence
(λ (m n)
(which-Nat m
(which-Nat n
Trivial
(λ (_) Absurd))
(λ (m-1)
(which-Nat n
Absurd
(λ (n-1) (= Nat m-1 n-1)))))))

《The Little Typer》最后两章可以说以 =consequence 为基础。=consequence 是类型生成器,我们还需要构造对应的值:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
(claim =consequence-same
(Π ((n Nat)) (=consequence n n)))
(define =consequence-same
(λ (n)
(ind-Nat n
(λ (k) (=consequence k k))
sole
(λ (n-1 _) (same n-1)))))

(claim use-Nat=
(Π ((m Nat)(n Nat)) (→ (= Nat m n) (=consequence m n))))
(define use-Nat=
(λ (m n m=n)
(replace m=n
(λ (k) (=consequence m k))
(=consequence-same m))))

=consequence-same 很简单,同一个数和自己肯定是相等的,分类讨论 zeroadd1 即可;有意思的是 use-Nat=,它把一个 (= Nat m n),也就是 m 等于 n 的证明映射为一个 (=consequence m n)!其思路比 =consequence-same 还简单,用 replace(=consequence m n) 转换为 (=consequence m m),再用 (=consequence-same m) 证明之。

注意到了吗,如果 mn 并不相等,此时 (=consequence m n) 就是 Absurd,我们成功完成了“从无到无”的构造!而 use-Nat= 内部并没有什么矛盾——从类型上看,传入的 (= Nat m n) 就意味着 mn 相等。

事实上我们可以把 =consequence 定义中的 Absurd 换成其它类型,比如 Atom,则 Atom 就会成为 use-Natmn 不等时返回的类型,而实际上我们并没有构造任何一个 Atom,此时就有了 ind-Absurd 的类似物,可以看出 Absurd 类型在系统中的作用可以由 (= Nat 0 1) 或者 (= Nat 1 2) 及无数个其它表达不成立相等命题的类型来取代。

于是我们就能愉快地证明 0 ≠ 1 啦:

1
2
3
4
(claim 01 (→ (= Nat zero (add1 zero)) Absurd))
(define 01
(λ (0=1)
(use-Nat= zero (add1 zero) 0=1)))