《The Little Typer》笔记：Tuner's Teaser

在第 14 章之后，第 15 章之前，《The Little Typer》用了一整页描述 Tuner’s Teaser，它的内容就是：定义一个函数，接受任意一个可接受一定数量 Eiher 作为参数的函数 f，判断 f 是否总会返回 left。假设要定义的函数叫 taut，那它必须能接受 (→ Either Either)，(→ Either Either Either)，(→ Either Either Either Either) 乃至任意层多的类型的参数。

以上描述里忽略了 Either 的两个类型参数，Friedman 的代码用的是 (Either Trivial Trivial) 类型，并定义其为 Two 类型。在这篇文章里将采用更熟悉的名称：Bool，这样 Tuner’s Teaser 就是定义一个函数，判断另一个可能接受任意数量 Bool 的函数是否总是返回 true。

1
2
3
4
5
6
7
8

(claim Bool U)
(define Bool (Either Trivial Trivial))

(claim true Bool)
(define true (left sole))

(claim false Bool)
(define false (right sole))

Tuner’s Teaser 的核心是怎么描述“可能接受任意数量 Bool 的函数”的类型。要描述这种类型，要注意到 Pie 的函数是柯里化的， (→ Bool Bool Bool) 其实是 (→ Bool (→ Bool Bool)) 的语法糖，容易看出这种形式与 Nat 同构，于是可以通过解构 Nat 来给出归纳描述：

1
2
3
4
5
6

(claim Bool-Fun (→ Nat U))
(define Bool-Fun
  (λ (n)
    (iter-Nat n
      Bool
      (λ (type) (→ Bool type)))))

这样 (Bool-Fun zero) 就是 Bool，传入非 zero 的 n 时 (Bool-Fun n) 就是接受 n 个 Bool 参数的函数类型。

再定义一个 and 函数，功能和一般的 and 一样：

1
2
3
4
5
6
7

(claim and (→ Bool Bool Bool))
(define and
  (λ (a b)
    (ind-Either a
      (λ (_) Bool)
      (λ (_) b)
      (λ (_) false))))

接下来就可以定义 taut 了：

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

(claim step-taut
  (Π ((n Nat))
    (→ (→ (Bool-Fun n) Bool)
       (→ (Bool-Fun (add1 n)) Bool))))
(define step-taut
  (λ (n taut_n)
    (λ (f) (and (taut_n (f true)) (taut_n (f false))))))

(claim taut (Π ((n Nat)) (→ (Bool-Fun n) Bool)))
(define taut
  (λ (n)
    (ind-Nat n
      (λ (k) (→ (Bool-Fun k) Bool))
      (λ (x) x)
      step-taut)))

关键部分是 step-taut，它把一个判断 (Bool-Fun n) 的函数升级为判断 (Bool-Fun (add1 n)) 的函数，这样在 taut 中即可完成对“所有”n 的定义，升级方法是考虑要检验的函数 f 第一个参数分别为 true 和 false 的情况，而 (f b) 就退化为 (Bool-Fun n)，可以用上一级函数检测了，检测完后用 and 测试是否皆为 true 即可。

使用示例：(taut 2 and)，返回 (the (Either Trivial Trivial) (right sole))，也就是 false。