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

《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)nMaybe 套娃,每一层要么是 (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) 对应 zeroleft 对应 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),然后递归解构 vecfin,直到 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)))))))