CODEWITHSUNDEEP
rackettyped-racketchurch-encoding
Lyudmila
Lyudmila

Reputation: 1

Typed/Racket: given Natural number defined type need multiply two numbers function to created

Given the following defined structures and type need to write multiply two numbers function. Having trouble to do that. Any advice will be greatly appreciated.

(define-struct Zero ())

(define-struct Succ
  ([n : Nat]))

(define-type Nat (U Zero Succ))

(: one Nat)
(define one (Succ (Zero)))
(: two Nat)
(define two (Succ one))

( : sub-nat : Nat Nat -> Nat)
   (define (sub-nat a y)
     (cond
       [(Zero? a) a]
       [(eq? one y)
          (- a y)]))

( : add-nat ( -> Nat Nat Nat))
(define (add-nat a b)
  (cond
    [(Zero? a) b]
    ((Zero? b) a)
    [else (add-nat (Succ-n a) (Succ b))]))

( : multiply-nat : Number Nat -> Nat)
(define (multiply-nat a b)
 (cond
   [(Zero? a) a]
   [(Zero? b) b]
    [else
     (add-nat b (multiply-nat (sub-nat a one) b))]))

Upvotes: 0

Views: 247

Answers (1)

C. K. Young
C. K. Young

Reputation: 223023

Your sub-nat implementation is incorrect and will not type-check. While you can fix that, semantically it's more correct to just use Succ-n in your multiply-nat (just as you do for add-nat), since Succ-n is the Church numeral equivalent of sub1. Here's a corrected (and tested) version of multiply-nat:

(define (multiply-nat a b)
 (cond
   [(Zero? a) a]
   [(Zero? b) b]
   [else
    (add-nat b (multiply-nat (Succ-n a) b))]))

For testing purposes, I also wrote a nat->number function for converting the Church numerals to actual numerals:

(: nat->number : Nat -> Nonnegative-Integer)
(define (nat->number n)
  (if (Zero? n)
      0
      (add1 (nat->number (Succ-n n)))))

Upvotes: 1

Related Questions