《The Little Typer》笔记：0≠1

前置知识

自然数

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

相等类型

Pie 的内置类型 (= E e1 e2) 表达“类型为 E 的 e1 和 e2 相等” 这一命题，唯一的构造器（也就是证明）是 (same e)，产生一个类型为 (= E e e) 的值；当 e1 和 e2 不相等时，没有 (= 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，它把两个自然数映射到一个类型上，其中 zero 和 zero 结果是 Trival，它们显然相等；zero 和 (add1 n) 或者 (add1 n) 和 zero 结果是 Absurd，它们显然不相等；(add1 m) 和 (add1 n) 的结果则是 (= Nat m n)——它们的相等性可由 m 和 n 的相等性归纳给出。=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 很简单，同一个数和自己肯定是相等的，分类讨论 zero 和 add1 即可；有意思的是 use-Nat=，它把一个 (= Nat m n)，也就是 m 等于 n 的证明映射为一个 (=consequence m n)！其思路比 =consequence-same 还简单，用 replace 把 (=consequence m n) 转换为 (=consequence m m)，再用 (=consequence-same m) 证明之。

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

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

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

1
2
3
4
5

(claim 0≠1 (→ (= Nat zero (add1 zero)) Absurd))
(define 0≠1
  (λ (0=1)
    (use-Nat= zero (add1 zero) 0=1)))