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))

(claim Pear U)
(define Pear
  (Pair Nat Nat))

(Pair Nat Nat)

(Pair Nat Atom)