类型化球拍：自然数

Question

我必须解决的一个问题自然数的一个独特的定义：

(define-type Nat (U 'Zero Succ)) 
(define-struct Succ ([prev : Nat]) #:transparent) 

所以基本上，0 = 'Zero, 1 = (Succ 'Zero), 2 = (Succ (Succ 'Zero))....等

使用这种形式，而不将其转换为整数，我写了递归函数来添加，减去和乘以自然数。对于附加功能，我已经试过这

(: nat+ : Nat Nat -> Nat) 
(define (nat+ n m) 
    (match '(n m) 
    ['('Zero 'Zero) 'Zero] 
    ['((Succ p) 'Zero) 
    n] 
    ['('Zero (Succ p)) 
    m] 
    ['((Succ p) (Succ t)) 
    (nat+ p (Succ m))])) 

，但我得到的错误

号码：未绑定的标识在模块中：P。

有没有人有写这种类型的递归函数的任何建议。

Answer 1

问题是您使用引用。当你引用一个清单，说'(n m)，这并不意味着“包含任何n是和任何m是一个列表 - 它是指含有文字符号n和m名单完全引用的东西忽略他们拥有的任何绑定，只有让你无论你引述的字面解释。所以，当你做match '(n m)，你不匹配包含值n和m列表绑定到，你匹配一个包含符号n和m列表。类似的问题与其他地方的引用一起存在 - 在模式匹配子句中，您必须使用list，而不是报价，让你期望的行为：

(: nat+ : Nat Nat -> Nat) 
(define (nat+ n m) 
    (match (list n m) 
    [(list 'Zero 'Zero) 'Zero] 
    [(list (Succ p) 'Zero) n] 
    [(list 'Zero (Succ p)) m] 
    [(list (Succ p) (Succ t)) (nat+ p (Succ m))])) 

注意的是，使用报价保持在'Zero - 这是因为Zero不是，您使用的文字符号Zero所以这是一个值绑定引。

---

此外，您可以通过使用define/match形式这个更简洁：

(: nat+ : Nat Nat -> Nat) 
(define/match (nat+ n m) 
    [('Zero 'Zero) 'Zero] 
    [((Succ p) 'Zero) n] 
    [('Zero (Succ p)) m] 
    [((Succ p) (Succ t)) (nat+ p (Succ m))]) 

这种形式可以让您直接对阵的论据，而不必首先把它们捆绑在一起成一个列表。