How to manually evaluate my mult function?-CodePudding

This is my first Stack Overflow question so if I forgot any crucial information please just let me know and I will add it!

So I am new to Haskell and just learning about types and classes. Now I've got 1 type and 2 functions declared:

data Nat   = Zero   | Succ Nat  

add :: Nat -> Nat -> Nat 
add Zero n = n 
add (Succ m) n = Succ (add m n)

mult :: Nat -> Nat -> Nat 
mult Zero _ = Zero 
mult (Succ m) n = add n (mult m n);

When calling the first function I can fully evaluate it and understand how Haskell processes it. Like this:

> 2   1 = 3 
>
> add (Succ (Succ Zero)) (Succ Zero)
> 
> Succ (add (Succ zero)) (Succ Zero)) 
>
> Succ (Succ (add Zero (Succ Zero))
>
> Succ (Succ (Succ Zero))

But I can't understand how this would be for the mult function. For me it looks like that will be an infinite loop of adding. Anyone who can explain me how the mult function would be evaluated?

CodePudding user response：

For mult you can evaluate very much the same way you do for add - by substituting definitions for names repeatedly. It will just take longer.

> 2 * 2 = 4

mult (Succ (Succ Zero)) (Succ (Succ Zero))

-- Substituting second case of mult. m = Succ Zero, n = Succ (Succ Zero)
add (Succ (Succ Zero)) (mult (Succ Zero) (Succ (Succ Zero))

-- Substituting second case of mult. m = Zero, n = Succ (Succ Zero)
add (Succ (Succ Zero)) (add (Succ (Succ Zero)) (mult Zero (Succ (Succ Zero))))

-- Substituting FIRST case of mult, because the first parameter is now Zero. 
add (Succ (Succ Zero)) (add (Succ (Succ Zero)) Zero)

-- And now we have nothing but addition left.

-- Substituting the inner add:
add (Succ (Succ Zero)) (Succ (add (Succ Zero) Zero))
add (Succ (Succ Zero)) (Succ (Succ (add Zero Zero)))
add (Succ (Succ Zero)) (Succ (Succ Zero))

-- Substituting the outer add:
Succ (add (Succ Zero) (Succ (Succ Zero)))
Succ (Succ (add Zero (Succ (Succ Zero))))
Succ (Succ (Succ (Succ Zero)))

Q.E.D

The key point for proving that the mult recursion will eventually end is that every recursive call is "smaller" than the previous one - by virtue of "removing" one layer of Succ.

CodePudding user response：

The pattern is almost exactly the same as for add, but with add n instead of Succ as the thing that gets slowly accumulated on the front. Here they are side-by-side; I've replaced your first Succ Zero by n in the add reduction to make the parallels more obvious:

add (Succ (Succ Zero)) n    mult (Succ (Succ Zero)) n
Succ (add (Succ zero) n)    add n (mult (Succ Zero) n)
Succ (Succ (add Zero n))    add n (add n (mult Zero n))
Succ (Succ n)               add n (add n Zero)