《The Little Typer》笔记：Fin 类型

看《The Little Typer》的时候，由于已经看过了 PLFA 第一分册，因此很多东西是 trivial 的，是剥离了 Agda 语法糖以后的再认识，其中也有很多新知识，有必要记下来。

第 14 章 “There’s Safty in Numbers” 讨论在编译期证明程序合法性的问题。索引 (List E) 的 list-ref 函数的返回类型是 (Maybe E)，而 vec-ref 则应做得更好——Vec 的类型签名本身就带有长度信息，应当直接检查传入的参数是否合法，不合法则通不过编译。

Pie 的函数都是完全函数，参数类型是 Nat，则必须允许传入全部自然数值。想要限制这个参数的范围，可以使用 dependent type，加一个 (Less n l) 参数，意义为 n < l 的证据，而 Friedman 则选择使用 Fin 类型。

Fin 应当代表 “finite”，它的定义是：

1
2
3

(claim Fin (→ Nat U))
(define Fin
  (λ (n) (iter-Nat n Absurd Maybe)))

于是 (Fin 0) 是 Absurd，(Fin 1) 是 (Maybe Absurd)，(Fin 2) 是 (Maybe (Maybe Absurd))……(Fin (add1 n)) 是 (Maybe (Fin n))，根据一点类型代数知识我们可以知道 (Fin n) 就是恰好有 n 个不同值的类型。于是，(Fin n) 可以和集合 0, 1, ... , n - 1 } 里的元素一一对应，用来索引 Vec E n 里的元素。

让我们再来看看 (Fin n) 类型的值的结构。Pie 其实没有内置 Maybe，而是由用户自定义为 (λ (E) (Either E Trivial))，其中 Trivial 是只有一个元素 sole 的类型。为了方便我们只展开到 Maybe 一级。由上文可知 (Fin n) 是 n 层 Maybe 套娃，每一层要么是 (right sole)，这时就到头了，要么是 (left ...)，开始下一层套娃。所以：

• (Fin 1) 有一个元素：(right sole)；
• (Fin 2) 有两个元素：(right sole)，(left (right sole))；
• (Fin 3) 有三个元素：(right sole)，(left (right sole))，(left (left (right sole)))；
• (Fin 4) 有四个元素：(right sole)，(left (right sole))，(left (left (right sole)))，(left (left (left (right sole))))； ……

容易发现，(Fin n) 的值的结构和 Nat 很像，(right sole) 对应 zero，left 对应 add1，那么我们可以用类似构造 Nat 的方式构造出 (Fin n)：

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

(claim nothing (Π ((E U)) (Maybe E)))
(define nothing (λ (E) (right sole)))

(claim just (Π ((E U)) (→ E (Maybe E))))
(define just (λ (E e) (left e)))

(claim fzero (Π ((n Nat)) (Fin (add1 n))))
(define fzero
  (λ (n) (nothing (Fin n))))

(claim fadd1 (Π ((n Nat)) (→ (Fin n) (Fin (add1 n)))))
(define fadd1 (λ (n) (λ (i-1) (just (Fin n) i-1))))

例如 (Fin 7) 里的 “2”（指和 (the Nat 2) 对应的元素）就可以用 (fadd1 6 (fadd1 5 (fzero 4))) 构造，如果假装 Pie 有隐式参数，写成 (fadd1 (fadd1 (fzero))) 就更像一个 2 了。

那么 vec-ref 也就清晰了：接受一个 fin : (Fin n) 和一个 vec : (Vec E n)，然后递归解构 vec 和 fin，直到 fin 解构成 (right sole)，返回此时的 vec 中元素。代码如下：

1
2
3
4
5
6
7
8
9
10
11

(claim vec-ref (Π ((E U)(l Nat)) (→ (Fin l) (Vec E l) E)))
(define vec-ref
  (λ (E l)
    (ind-Nat l
      (λ (k) (→ (Fin k) (Vec E k) E))
      (λ (fin_0 es) (ind-Absurd fin_0 E))
      (λ (l-1 vec-ref_l-1 fin_l-1 es_l-1)
        (ind-Either fin_l-1
          (λ (_) E)
          (λ (i-1) (vec-ref_l-1 i-1 (tail es_l-1)))
          (λ (_) (head es_l-1)))))))