The Little Typer

'atom

'ratatouille

'---

---

'

'ratatouille是一个Atom

'cœurs-d-artichauts是一个Atom

____是一个____.

'ratatouille

'ratatouille

Atom

'ratatouille

'courgette

Atom

____和____是相同的____.

'pomme和'orange是相同的Atom

(cons 'ratatouille 'baguette)

(Pair Atom Atom)

(Pair Atom Atom)

(cons 'ratatouille 'baguette)

(cons 'ratatouille 'baguette)

(Pair Atom Atom)

(cons 'ratatouille 'baguette)

(cons 'baguette 'ratatouille)

(Pair Atom Atom)

(cdr
 (cons 'ratatouille 'baguette))

(Pair Atom Atom)是一个类型吗?

____是一个类型.

'courgette是一个类型.

____和____是相同的类型.

Atom和(Pair Atom Atom)是相同的类型.

(Pair Atom Atom)

(Pair Atom Atom)

'pêche和'pêche是相同的'fruit吗?

'fruit是一个类型

某些形式的判断只有在早前的判断的基础之上才具备意义.

(car
 (cons 'ratatouille 'baguette))

'ratatouille

Atom

(cdr
 (cons 'ratatouille 'baguette))

'baguette

Atom

(car
 (cons
  (cons 'aubergine 'courgette)
  'tomato))

(car
 (cdr
  (cons
   'ratatouille
   (cons 'baguette 'olive-oil))))

'baguette

Atom

相同总是相对于某个类型而言的, 因此规范形式也由类型决定.

(cons 'ratatouille 'baguette)

(Pair Atom Atom)

然而, 给定一个类型, 每个由该类型描述的表达式的确都有一个由该类型确定的规范形式.

(car
 (cons
  (cons 'aubergine 'courgette)
  'tomato))

之前我们对于什么是一个

(Pair Atom Atom)

(car
 (cons
  (cons 'aubergine 'courgette)
  'tomato))

(cons 'aubergine 'courgette)

(Pair Atom Atom)

(cons 'aubergine 'courgette)

(cons 'aubergine 'courgette)

第1章第23框描述了何谓一个表达式和另一个表达式是相同的

(Pair Atom Atom)

(Pair
 (cdr
  (cons Atom 'olive))
 (car
  (cons 'oil Atom)))

(Pair
 (cdr
  (cons Atom 'olive))
 (car
  (cons 'oil Atom)))

只有在其参数均为类型 (例如Atom) 时, 它才是一个表达式.

(Pair
 (car
  (cons Atom 'olive))
 (cdr
  (cons 'oil Atom)))

(cons 'ratatouille 'baguette)

(Pair
 (car
  (cons Atom 'olive))
 (cdr
  (cons 'oil Atom)))

(Pair
 (car
  (cons Atom 'olive))
 (cdr
  (cons 'oil Atom)))

(Pair Atom Atom)

(Pair Atom Atom)

(Pair
 (car
  (cons Atom 'olive))
 (cdr
  (cons 'oil Atom)))

(cons '17 'pepper)

(Pair Atom Atom)

0和26是相同的Nat吗?

(+ 0 26)和26是相同的Nat吗?

one和1是相同的Nat吗?

通过定义使得one为(add1 zero)的确是可行的.

(define one
  (add1 zero))

(claim one Nat)
(define one
  (add1 zero))

(claim four Nat)
(define four
  (add1
   (add1
    (add1
     (add1 zero)))))

(add1
 (+ (add1 zero)
    (add1
     (add1 zero))))

即便

(add1
 (+ (add1 zero)
    (add1
     (add1 zero))))

(+ (add1
    (add1 zero))
   (add1 zero))

对于新类型的解释的一部分是要说明其构造子为何. 构造子表达式是构造具有该类型的表达式的直接方式.

所有的值都是规范的吗?

(add1           )

(add1 'aubergine)

当填充这样的方框时, 我们的期望是作为结果的表达式由某个类型刻画.

(add1
 (+ (add1 zero)
    (add1
     (add1 zero))))

但是, 实际上它们是相同的Nat.

如果两个都是zero, 那么它们就是相同的Nat.

为什么

(add1 zero)

(add1 zero)

Nat

(add1 (+ 0 1))

(add1 (+ 1 0))

Nat

实际上, 其他表达式都不能分辨出four的两种定义之间的不同, 因为这两个定义了four为相同的Nat.

关于这参数的值, 我们能说什么呢?

(car
 (cons (+ 3 5) 'baguette))

(car
 (cons $a$ $d$))

如何找出一个cdr表达式的值呢?

两个表达式为相同的(Pair Atom Nat)是什么意思?

这是不是意味着每个原子都是值?

在表达式zero中, 顶层构造子是什么?

Pair是一个构造子吗?

(cons zero 'onion)

(Pair Atom Atom)

(cons 'zero 'onion)

(Pair Atom Atom)

(cons 'basil
 (cons 'thyme 'oregano))

然而, car既不是构造子也不是类型构造子.

另一个消去子是什么呢?

可以定义一个函数(function), 其表达力相当于car和cdr的联合.

这种值的消去子是什么呢?

(λ (flavor)
  (cons flavor 'lentils))

((λ (flavor)
   (cons flavor 'lentils))
 'garlic)

(+ 1 2)

((λ (root)
   (cons root
         (λ (root) root)))
 'carrot)

成为一个

(→ Atom (Pair Atom Atom))

(Pair Atom Atom)

(→ Atom (Pair Atom Atom))

(Pair Atom Atom)

(car (cons Atom 'pepper))

(cdr (cons 'salt Atom))

(→ Nat Atom)

(→ Nat Atom)

(→ Nat (Pair Nat Nat))

(Pair Nat Nat)

(λ (a d) (cons d a))

(car (cons x x))

(cons y 'rutabaga)

如果x是一个(Pair Nat Atom), 那么

(cdr x)

(λ (x) (car (cons x x)))

(λ (x) x)

(→ Nat Nat)

(λ (x) (car x))

(λ (y) (car y))

(→ (Pair Nat Nat) Nat)

(λ (x) (car x))

(λ (x) (car x))

(→ (Pair Nat Nat) Nat)

(λ (a d) (cons a d))

(→ Atom Atom (Pair Atom Atom))

(claim vegetables
  (Pair Atom Atom))
(define vegetables
  (cons 'celery 'carrot))

(cons 'celery 'carrot)

(Pair Atom Atom)

(Pair Atom (Pair Atom Atom))

vegetables

(cons (car vegetables)
      (cdr vegetables))

(Pair Atom Atom)

(cons (car $p$) (cdr $p$))

(Pair Atom Atom)

(claim five Nat)
(define five (+ 7 2))

(+ five 5)

已经被使用了的名字, 不论是用于构造子, 消去子, 还是之前的定义, 都不适合再与claim或者define一起使用了.

(which-Nat $\mathit{target}$
  $\mathit{base}$
  $\mathit{step}$)

(which-Nat zero
  'naught
  (λ (n)
    'more))

(which-Nat 4
  'naught
  (λ (n)
    'more))

(which-Nat 5
  0
  (λ (n)
    (+ 6 n)))

gauss的类型应该是什么?

(gauss 5)

(gauss 4)和(gauss 5)差不多, 前者是10, 后者是15.

白框框住的是未知的代码, 而白纸黑字的部分则是其中的已知部分. 在这被框住的内容之中, 我们该如何从

(gauss 4)

(gauss 5)

        (gauss 4)    

如果$n$是一个Nat, 那么该如何从

(gauss $n$)

(gauss (add1 $n$))

        (gauss $n$)    

请记得5是书写(add1 4)的另一种方式.

请记得白色的框和白纸黑字的部分.

(claim forever (→ Nat Atom))
(define forever
  (λ (and-ever)
    (forever and-ever)))

诸如Atom, Nat, (Pair Atom Nat)这样的表达式是类型, 而每一个这样的类型都是一个$\mathcal{U}$.

一个为类型的表达式是一个值, 当其以某个类型构造子为顶时. 到目前为止, 我们见过的类型构造子有Nat, Atom, →, 和$\mathcal{U}$.

(car (cons Atom 'prune))

(car (cons Atom 'prune))

Atom

(car (cons Atom 'prune))

作出一个表达式是一个类型的判断需要知道其构造子. 但是, $\mathcal{U}$的意义并不由知道所有的类型构造子给出, 因为可以引入新的类型.

(cons Atom Atom)

(Pair $\mathcal{U}$ $\mathcal{U}$)

定义Pear, 其意指Nat的序对的类型.

Pear有消去子吗?

Pear的消去子必然要使得具有类型Pear的值中的信息能够被使用.

(λ (a d) a)

(→ Nat Nat $X$)

当a和d都为Nat时,

(λ (a d)
  (cons d a))

(claim Pear-maker $\mathcal{U}$)
(define Pear-maker
  (→ Nat Nat Pear))

(claim elim-Pear
  (→ Pear Pear-maker Pear))
(define elim-Pear
  (λ (pear maker)
    (maker (car pear)
           (cdr pear))))

(elim-Pear
 (cons 3 17)
 (λ (a d)
   (cons d a)))

这种pearwise加法的类型是什么?

请定义pearwise+, 以使得

(pearwise+
 (cons 3 8)
 (cons 7 6))

(cons 10 14)

尝试输入

'spinach

在Pie里, 一个表达式要么是一个类型, 要么由一个类型描述. Pie可以自己找出诸多表达式的类型, 包括原子.

此时, 使用the表达式来告诉Pie意图的类型.

(the (Pair Atom Atom)
  (cons 'spinach 'cauliflower))

(the (Pair Atom
       (Pair Atom Atom))
  (cons 'spinach
    (cons 'kale 'cauliflower)))

(Pair Atom Atom)

(cons 'kale 'cauliflower)

(the $X$ $e$)

现在试试这个:

U

当一个表达式是一个类型但不具备类型时, Pie只回以其规范形式.

(Pair $\mathcal{U}$ $\mathcal{U}$)

(Pair Atom $\mathcal{U}$)

(→ $\mathcal{U}$ $\mathcal{U}$)

(define gauss
  (λ (n)
    (which-Nat n
      0
      (λ (n-1)
        (+ (add1 n-1) (gauss n-1))))))

但是, 某些递归定义总是能产生一个值.

(gauss 0)的规范形式是什么?

(add1 (gauss zero))

(gauss 1)的规范形式是什么?

+和gauss都是完全的.

消去子是什么?

(iter-Nat $\mathit{target}$
  $\mathit{base}$
  $\mathit{step}$)

($\mathit{step}$
 (iter-Nat $n$
   $\mathit{base}$
   $\mathit{step}$))

(iter-Nat 5
  3
  (λ (smaller)
    (add1 smaller)))

$\mathit{step}$的类型如何?

以下的iter-Nat表达式里, target, base, step分别是什么?

(iter-Nat 5
  3
  (λ (k)
    (add1 k)))

+的类型应该是什么?

若是递归可以成为一个选项, 那么以下将会是一个正确的定义.

(define +
  (λ (n j)
    (which-Nat n
      j
      (λ (n-1)
        (add1 (+ n-1 j))))))

将白纸黑字的部分 (其包含有递归) 替换以献给step的几乎是答案的参数, 记得保留白框里其他内容.

(+ (add1 zero) 7)是什么?

此即所谓rec-Nat模式.

(define gauss
  (λ (n)
    (which-Nat n
      0
      (λ (n-1)
        (+ (add1 n-1) (gauss n-1))))))

(define gauss
  (λ (n)
    (rec-Nat n
      0
      (λ (n-1 gaussn-1)
        (+ (add1 n-1) gaussn-1)))))

rec-Nat的参数和iter-Nat有着同样的特殊名字: 其总被称为$\mathit{target}$, $\mathit{base}$, $\mathit{step}$.

iter-Nat应用其step于一个新的iter-Nat表达式, 其和原本的表达式带有相同的base和step, 但是以藏在add1下的这更小的Nat为新的target.

这两者该如何结合起来呢?

(rec-Nat (add1 zero)
  0
  (λ (n-1 almost)
    (add1
      (add1 almost))))

那么值是什么呢?

如果base是一个$X$, 那么step必然是一个

(→ Nat $X$ $X$)

(claim step-zerop
  (→ Nat Atom Atom))
(define step-zerop
  (λ (n-1 zeropn-1)
    'nil))
(claim zerop
  (→ Nat Atom))
(define zerop
  (λ (n)
    (rec-Nat n
      't
      step-zerop)))

为什么step-zerop中的λ变量被称为n-1和zeropn-1呢?

step-zerop的两个参数皆未被使用, 故其为黯淡的. 因此, 这个定义只是看上去像递归的, 实则并非如此.

(zerop 37)的值是什么?

(rec-Nat 36
  't
  step-zerop)

(claim step-gauss
  (→ Nat Nat
    Nat))
(define step-gauss
  (λ (n-1 gaussn-1)
    (+ (add1 n-1) gaussn-1)))

定义step的另一个好处在于我们需要显式地写下其类型, 而不是任其由其于rec-Nat中的使用方式被推断出来.

(define gauss
  (λ (n)
    (rec-Nat n
      0
      step-gauss)))

(rec-Nat zero
  0
  step-gauss)

以下是我们找出(gauss (add1 zero))的值的开始.

1. | (gauss (add1 zero))
2. |

   (step-gauss zero
     (rec-Nat zero
       0
       step-gauss))

3. |

   (+ (add1 zero)
     (rec-Nat zero
       0
       step-gauss))

换言之, 如果n和j是Nat, 那么

(* n j)

(claim make-step-*
  (→ Nat
    (→ Nat Nat
      Nat)))
(define make-step-*
  (λ (j)
    (λ (n-1 *n-1)
      (+ j *n-1))))

现在定义*.

(claim step-*
  (→ Nat Nat Nat
    Nat))
(define step-*
  (λ (j n-1 *n-1)
    (+ j *n-1)))

(λ (x y z)
  (+ x (+ y z)))

(λ (x)
  (λ (y)
    (λ (z)
      (+ x (+ y z)))))

(→ Nat
  (→ Nat
    (→ Nat
      Nat)))

(→ Nat Nat Nat
  Nat)

($f$ $x$ $y$ $z$)

(($f$ $x$ $y$) $z$)

((($f$ $x$) $y$) $z$)

定义多参数函数为嵌套的单参数函数的过程被称为Currying.

1. | (* 2 29)
2. |

   ((λ (n j)
      (rec-Nat n
        0
        (step-* j)))
     2 29)

3. |

   (rec-Nat (add1
              (add1 zero))
     0
     (step-* 29))

4. |

   ((step-* 29)
    (add1 zero)
    (rec-Nat (add1 zero)
      0
      (step-* 29)))

5. |

   ((λ (n-1 *n-1)
      (+ 29 *n-1))
    (add1 zero)
    (rec-Nat (add1 zero)
      0
      (step-* 29)))

(claim step-    
  (→ Nat Nat
    Nat))
(define step-    
  (λ (n-1 almost)
    (* (add1 n-1) almost)))
(claim     
  (→ Nat
    Nat))
(define     
  (λ (n)
    (rec-Nat n
      0
      step-    )))

像Nat这样的类型的一个缺陷在于其不能说明哪个(which) Nat是我们所意图的. 之后, 我们将遇到更为强大的类型, 其允许我们讨论特定的Nat.

类型并不能阻止将five定义成是9的愚蠢行径. 但是, 我们可以将我们的一些想法写成类型.

(claim Pear $\mathcal{U}$)
(define Pear
  (Pair Nat Nat))

(Pair Nat Nat)

(Pair Nat Atom)

实际上, 还有更好的方式. 我们可以提供一个(Pair $A$ $D$)的消去子, 不论$A$和$D$为何.

根据第1章第54框, 除非$A$和$D$是类型. 也就是说, $A$必须是一个类型且$D$必须是一个类型.

(claim kar
  (→ (Pair Nat Nat)
    Nat))

(define kar
  (λ (p)
    (elim-Pair
      Nat Nat
      Nat
      p
      (λ (a d)
        a))))

现在请定义一个类似的函数kdr, 其找出一个Nat序对的cdr.

请编写一个叫做swap的函数, 其交换一个(Pair Nat Atom)的car和cdr.

(elim-Pair
  $A$ $D$
  $X$
  $p$
  $f$)

elim-Pair的类型是什么?

然而, 这种思维过程的确言之成理. 回忆一下, 成为一个

(→ $Y$ $X$)

(claim flip
  (Π ((A $\mathcal{U}$)
      (D $\mathcal{U}$))
    (→ (Pair A D)
      (Pair D A))))
(define flip
  (λ (A D)
    (λ (p)
      (cons (cdr p) (car p)))))

的确可以.

(flip Nat Atom)

((flip Nat Atom)
 (cons 17 'apple))

(flip Nat Atom)

(→ (Pair Nat Atom)
  (Pair Atom Nat))

(Π ((A $\mathcal{U}$)
    (D $\mathcal{U}$))
  (→ (Pair A D)
    (Pair D A)))

(Π ((A $\mathcal{U}$)
    (D $\mathcal{U}$))
  (→ (Pair A D)
    (Pair D A)))

(→ (Pair A D)
  (Pair D A))

(→ (Pair $A$ $D$)
  (Pair $D$ $A$))

但为什么会是如此呢?

(Π ((A $\mathcal{U}$)
    (D $\mathcal{U}$))
  (→ (Pair A D)
    (Pair D A)))

(Π ((Lemon $\mathcal{U}$)
    (Meringue $\mathcal{U}$))
  (→ (Pair Lemon Meringue)
    (Pair Meringue Lemon)))

(Π ((A $\mathcal{U}$)
    (D $\mathcal{U}$))
  (→ (Pair A D)
    (Pair D A)))

(Π ((A $\mathcal{U}$)
    (D $\mathcal{U}$))
  (→ (Pair
       (car
         (cons A D))
       (cdr
         (cons A D)))
    (Pair D A)))

(claim flip
  (Π ((A $\mathcal{U}$)
      (D $\mathcal{U}$))
    (→ (Pair A D)
      (Pair D A))))
(define flip
  (λ (C A)
    (λ (p)
      (cons (cdr p) (car p)))))

elim-Pair的定义是什么?

(define kar
  (λ (p)
    (elim-Pair
      Nat Nat
      Nat
      p
      (λ (a d)
        a))))

成为一个

(Π (($Y$ $\mathcal{U}$)) $X$)

基于单参数的Π表达式

(Π (($Y$ $\mathcal{U}$) ($Z$ $\mathcal{U}$)) $X$)

什么表达式具有类型

(Π ((A $\mathcal{U}$))
  (→ A (Pair A A)))

(claim twin-Nat
  (→ Nat
    (Pair Nat Nat)))
(define twin-Nat
  (λ (x)
    (cons x x)))

(twin-Nat 5)

(claim twin-Atom
  (→ Atom
    (Pair Atom Atom)))
(define twin-Atom
  (λ (x)
    (cons x x)))

(twin-Atom 'cherry-pie)

(λ (a)
  (cons a a))

(claim twin-Atom
  (→ Atom
    (Pair Atom Atom)))

(twin-Atom 'cherry-pie)

((twin Atom) 'cherry-pie)

(Pair Atom Atom)

• 烹饪普罗旺斯杂烩,
• 吃完两个樱桃派,
• 尝试使用带图画的餐巾清理一下,
• 理解rec-Nat, 以及
• 休息安睡好

(claim expectations
  (List Atom))
(define expectations
  (:: 'cooked
    (:: 'eaten
      (:: 'tried-cleaning
        (:: 'understood
          (:: 'slept nil))))))

nil是一个(List Nat)吗?

nil是一个(List (List Atom))吗?

之所以(List 'potato)不是一个类型, 是因为'potato是一个Atom, 而不是一个类型.

猜猜(List $E$)还有什么其他的构造子.

构造子::构建一个List...

何时(:: $e$ $\mathit{es}$)是一个(List $E$)?

之所以$e$必须要是一个$E$, 是因为为了能够使用(List $E$)的一个消去子, 我们需要保证这样的列表的每个元素都是一个$E$.

请将rugbrød定义为丹麦黑麦面包的成分.

• 全黑麦面粉,
• 黑麦籽粒, 浸泡直至变软,
• 纯净水,
• 活跃的酵种, 以及
• 盐.

rugbrød和5有什么不同之处?

nil是不是和zero有什么关系?

(rec-Nat $\mathit{target}$
  $\mathit{base}$
  $\mathit{step}$)

(rec-List $\mathit{target}$
  $\mathit{base}$
  $\mathit{step}$)

• $\mathit{target}$是一个(List $E$),
• $\mathit{base}$是一个$X$, 且
• $\mathit{step}$是一个(→ $E$ (List $E$) $X$ $X$)

这和rec-Nat有什么不同之处?

在这两种情况下, step都接受相应构造子的每个参数, 并且也接受对于更小的值的递归性消去.

(claim step-     
  (→ Atom (List Atom) Nat
    Nat))
(define step-     
  (λ (e es n)
    (add1 n)))

(rec-List nil
  0
  step-     )

一个kartoffelmad是带有toppings和condiments的rugbrød.

(claim toppings
  (List Atom))
(define toppings
  (:: 'potato
    (:: 'butter nil)))
(claim condiments
  (List Atom))
(define condiments
  (:: 'chives
    (:: 'mayonnaise nil)))

(rec-List condiments
  0
  step-     )

方框里填什么名字好呢?

(claim length
  (→ (List Atom)
    Nat))
(define length
  (λ (es)
    (rec-List es
      0
      step-length)))

(claim step-length
  (→ Nat (List Nat) Nat
    Nat))
(define step-length
  (λ (e es lengthes)
    (add1 lengthes)))

什么可以用来作成一个对于所有类型成立的step-length版本呢?

(claim step-length
  (Π ((E $\mathcal{U}$))
    (→ E (List E) Nat
      Nat)))

现在定义length.

现在是时候将一片面包, toppings以及condiments组装为一个美味的kartoffelmad.

请定义一个函数, 其合并两个列表.

这是否暗示了append定义中的类型呢?

剩下来的参数应该是什么呢?

(claim append
  (Π ((E $\mathcal{U}$))
    (→ (List E) (List E)
      (List E))))

(append Atom
  nil
  (:: 'salt
    (:: 'pepper nil)))

(append Atom
  (:: 'cucumber
    (:: 'tomato nil))
  (:: 'rye-bread nil))

(define step-append
  (λ (E)
    (λ (e es appendes)
                     )))
(define append
  (λ (E)
    (λ (start end)
      (rec-List start
        end
        (step-append E)))))

所以正确的定义是什么?

例如,

(snoc Atom toppings 'rye-bread)

(:: 'potato
  (:: 'butter
    (:: 'rye-bread nil)))

snoc的类型是什么?

现在请定义concat, 其行为与append类似, 但是在其step中使用了snoc.

(claim concat
  (Π ((E $\mathcal{U}$))
    (→ (List E) (List E)
      (List E))))

reverse的类型应该是什么?

(claim kartoffelmad
  (List Atom))
(define kartoffelmad
  (append Atom
    (concat Atom
      condiments toppings)
    (reverse Atom
      (:: 'plate
        (:: 'rye-bread nil)))))

让我们定义一个函数first, 其找出任意List的第一个元素.

当$E$是一个类型而$k$是一个Nat时, 表达式(Vec $E$ $k$)是一个类型. 这个Nat给出了列表的长度.

(Vec Atom 3)是一个类型吗?

(Vec
  (cdr
    (cons 'pie
      (List (cdr (cons Atom Nat)))))
  (+ 2 1))

vec::是

(Vec $E$ (add1 $k$))

当$e$是一个$E$而$\mathit{es}$是一个(Vec $E$ $k$)时, (vec:: $e$ $\mathit{es}$)是一个(Vec $E$ (add1 $k$)).