Typed Racket: Natural Numbers

Question

I have to solve a problem with a unique definition of the natural numbers:

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

So basically, 0 = 'Zero, 1 = (Succ 'Zero), 2 = (Succ (Succ 'Zero)).... etc.

Using this form, without converting them into integers, I have write recursive functions to add, subtract, and multiply the natural numbers. For the add function I've tried this

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

but I get the error

p: unbound identifier in module in: p.

Does anyone have any advice for writing this type of recursive function.

Jack Jack · Accepted Answer · 2014-10-29T06:53:49

The problem is your use of quoting. When you quote a list, say '(n m), it doesn't mean "a list containing whatever n is and whatever m is - it means a list containing the literal symbols n and m. Quoting things completely ignores whatever bindings they have and only gives you the literal interpretation of whatever you quote. So when you do match '(n m), you are not matching a list containing the values n and m are bound to, you are matching a list containing the symbols n and m. Similar problems exist with your usage of quote everywhere else - in the pattern matching clauses you have to use list instead of quote to get the behavior you expect:

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

Note that the use of quote remains in 'Zero - this is because Zero is not a binding with a value, you're using the literal symbol Zero so it's quoted.

Additionally, you can make this more succinct by using the define/match form:

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

This form lets you match against the arguments directly, instead of having to pack them together into a list first.

Typed Racket: Natural Numbers

1 Answers