Primitive Recursive Functions Excercise in Haskell

Question

For a functional programming excercise I am required to apply primitive recursive functions in haskell. However I do not quite understand yet the definition (and application) of this type of functions.

We are presented the data type Nat to be used, its constructor is: data Nat = Zero | Succ Nat

To my understanding this means that the type "Nat" can be either a Zero or a Natural Succesor.

Then we have a recursor:

recNat :: a -> (Nat -> a -> a) -> Nat -> a
recNat a _ Zero = a
recNat a h (Succ n) = h n (recNat a h n)

Which I understand is meant to apply recursion to a function?

And I've also been given an example of an addition function using the recursor:

addR :: Nat -> Nat -> Nat
addR m n = recNat n (\ _ y -> Succ y) m

But I don't get how it works, it uses the recNat function with the given two Nats, and also uses an anonymous function as input for recNat ( that is the part I'm not sure what it does! )

So my main issue is what does this do in the function exactly > \ _ y -> Succ y

I'm suppossed to apply this same recursor (RecNat) to apply other operations to Nat, but I'm stuck still trying to understand the example!

user_3234959 · Answer

Roughly, recNat x f n computes

f (n-1) (f (n-2) (f (n-3) (... (f 0 x))))

So, it applies f to x for n times, each time also passing a "counter" as the first argument of f.

In your case \_ y -> ... ignores the "counter" argument. Hence

addR m n = recNat n (\ _ y -> Succ y) m

can be read as "to compute m+n, apply m times the function Succ to n". This effectively computes ((n+1)+1)+1... where there are m ones in the sum.

You can try to compute the product of two naturals in a similar way. Use \_ y -> ... and express multiplication as repeated addition. You'll need to use the already-defined addR for that.

Additional hint: after multiplication, if you want to compute the predecessor n-1, then the "counter" argument will be very handy, so don't discard that and use \x y -> ... instead. After that, you can derive (truncated) subtraction as repeated predecessor.

user_246886 · Answer

You’re right that data Nat = Zero | Succ Nat means that a Nat may be Zero or the Successor of another Nat; this represents natural numbers as a linked list, i.e.:

zero, one, two, three, four, five :: Nat

zero  = Zero
one   = Succ Zero                              -- or: Succ zero
two   = Succ (Succ Zero)                       --     Succ one
three = Succ (Succ (Succ Zero))                --     Succ two
four  = Succ (Succ (Succ (Succ Zero)))         --     Succ three
five  = Succ (Succ (Succ (Succ (Succ Zero))))  --     Succ four
-- …

The function of recNat is to fold over a Nat: recNat z k takes a Nat and “counts down” by ones to the final Zero, calling k on every intermediate Succ, and replacing the Zero with z:

recNat z k three
recNat z k (Succ (Succ (Succ Zero)))

-- by second equation of ‘recNat’:
k two                (recNat z k two)
k (Succ (Succ Zero)) (recNat z k (Succ (Succ Zero)))

-- by second equation of ‘recNat’:
k two                (k one         (recNat z k one))
k (Succ (Succ Zero)) (k (Succ Zero) (recNat z k (Succ Zero)))

-- by second equation of ‘recNat’:
k two                (k one         (k zero (recNat z k zero)))
k (Succ (Succ Zero)) (k (Succ Zero) (k Zero (recNat z k Zero)))

-- by first equation of ‘recNat’:
k two                (k one         (k zero z))
k (Succ (Succ Zero)) (k (Succ Zero) (k Zero z))

The lambda \ _ y -> Succ y has type a -> Nat -> Nat; it just ignores its first argument and returns the successor of its second argument. Here’s an illustration of how addR works to compute the sum of two Nats:

addR two three
addR (Succ (Succ Zero)) (Succ (Succ (Succ Zero)))

-- by definition of ‘addR’:
recNat three                     (\ _ y -> Succ y) two
recNat (Succ (Succ (Succ Zero))) (\ _ y -> Succ y) (Succ (Succ Zero))

-- by second equation of ‘recNat’:
(\ _ y -> Succ y) one         (recNat three                     (\ _ y -> Succ y) one)
(\ _ y -> Succ y) (Succ Zero) (recNat (Succ (Succ (Succ Zero))) (\ _ y -> Succ y) (Succ Zero))

-- by application of the lambda:
Succ (recNat three                     (\ _ y -> Succ y) one)
Succ (recNat (Succ (Succ (Succ Zero))) (\ _ y -> Succ y) (Succ Zero))

-- by second equation of ‘recNat’:
Succ ((\ _ y -> Succ y) zero (recNat three                     (\ _ y -> Succ y) zero))
Succ ((\ _ y -> Succ y) zero (recNat (Succ (Succ (Succ Zero))) (\ _ y -> Succ y) zero))

-- by application of the lambda:
Succ (Succ (recNat three                     (\ _ y -> Succ y) zero))
Succ (Succ (recNat (Succ (Succ (Succ Zero))) (\ _ y -> Succ y) zero))

-- by first equation of ‘recNat’:
Succ (Succ three)
Succ (Succ (Succ (Succ (Succ Zero))))

-- by definition of ‘five’:
five
Succ (Succ (Succ (Succ (Succ Zero))))

As you can see, what’s happening here is we’re essentially taking off each Succ from one number and putting it on the end of the other, or equivalently, replacing the Zero in one number with the other number, i.e., the steps go like this:

1+1+0 + 1+1+1+0           2 + 3
1+(1+0 + 1+1+1+0)      1+(1 + 3)
1+1+(0 + 1+1+1+0)    1+1+(0 + 3)
1+1+(1+1+1+0)        1+1+(3)
1+1+1+1+1+0          5

The inner lambda always ignores its first argument with _, so it may be simpler to see how this works with a simpler definition of recNat that literally replaces Zero with a value z and Succ with a function s:

recNat' :: a -> (a -> a) -> Nat -> a
recNat' z _ Zero     = z
recNat' z s (Succ n) = s (recNat z s n)

Then addition is slightly simplified:

addR' m n = recNat' n Succ m

This literally says “to compute the sum of m and n, add one m times to n”.

You may find it easier to play around with these numbers if you make a Num instance and Show instance for them:

{-# LANGUAGE InstanceSigs #-}  -- for explicitness

instance Num Nat where

  fromInteger :: Integer -> Nat
  fromInteger n
    | n <= 0    = Zero
    | otherwise = Succ (fromInteger (n - 1))

  (+) :: Nat -> Nat -> Nat
  (+) = addR

  (*) :: Nat -> Nat -> Nat
  (*) = …  -- left as an exercise

  (-) :: Nat -> Nat -> Nat
  (-) = …  -- left as an exercise

  abs :: Nat -> Nat
  abs n = n

  signum :: Nat -> Nat
  signum Zero   = Zero
  signum Succ{} = Succ Zero

  negate :: Nat -> Nat
  negate n = n  -- somewhat hackish

instance Show Nat where
  show n = show (recNat' (+ 1) 0 n :: Int)

Then you can write 2 + 3 :: Nat and have it display as 5.

Primitive Recursive Functions Excercise in Haskell

2 Answers