racket - 未知变量 +

Question

在 Little Typer 第 2 章中，第 100 帧给出了以下定义:

(claim pearwise+
  (→ Pear Pear
     Pear))

(define pearwise+
  (λ (anjou bosc)
    (elim-Pear anjou
      (λ (a1 d1)
        (elim-Pear bosc
          (λ (a2 d2)
            (cons
              (+ a1 a2)
              (+ d1 d2))))))))

当我运行它时，我收到以下错误:

Unknown variable +

怎么了？

Answer 1

Pie 没有开箱即用的加法功能，但 Little Typer 的第 3 章第 24、26 和 27 帧对 + 给出了以下定义:

; 3.26
(claim step-+
  (→ Nat
      Nat))

(define step-+
  (λ (+n-1)
    (add1 +n-1)))

; 3.24
(claim +
  (→ Nat Nat
      Nat))

; 3.27
(define +
  (λ (n j)
    (iter-Nat n
      j
      step-+)))

将这些放在 pairwise+ 的定义之前在定义中使用 +。

完整的解决方案如下所示:

#lang pie

; 2.80
(claim Pear U)

(define Pear
  (Pair Nat Nat))

; 2.82
(check-same Pear (cons 3 5) (cons 3 (add1 4)))

; 2.93
(claim Pear-maker U)

(define Pear-maker
  (→ Nat Nat
      Pear))

(claim elim-Pear
  (→ Pear Pear-maker
      Pear))

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

; 2.95
(check-same (Pair Nat Nat)
  (cons 17 3)
  (elim-Pear
    (cons 3 17)
    (λ (a d)
      (cons d a))))

;----------------------
; need to add + define
; taken from chapter 3
;----------------------

; 3.26
(claim step-+
  (→ Nat
      Nat))

(define step-+
  (λ (+n-1)
    (add1 +n-1)))

; 3.24
(claim +
  (→ Nat Nat
      Nat))

; 3.27
(define +
  (λ (n j)
    (iter-Nat n
      j
      step-+)))

; 2.100
(claim pearwise+
  (→ Pear Pear
     Pear))

(define pearwise+
  (λ (anjou bosc)
    (elim-Pear anjou
      (λ (a1 d1)
        (elim-Pear bosc
          (λ (a2 d2)
            (cons
              (+ a1 a2)
              (+ d1 d2))))))))

(check-same Pear
  (cons 3 4)
  (pearwise+
    (cons 1 2)
    (cons 2 2)))