How to manually evaluate my mult function?

Question

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?

Answer 1

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.