類型化球拍：自然數

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

這種形式可以讓您直接對陣的論據，而不必首先把它們捆綁在一起成一個列表。