Natural numbers as a recursive datatype

Question

I have started working with datatypes but I am getting confused with the following:

data Natural = Zero | Succ Natural

add :: Natural -> Natural -> Natural

add m Zero = m

add m (Succ n) = Succ (add m n)

How is this the addition working. I understood that Natural 3 is represented by Succ(Succ(Succ 0))) though this is still not 100% clear to me that is the value decreasing on its own or what. I want to understand addition of step by step.

P.S: This was taken from the book Introduction to Functional Programming by Richard Bird.

Answer 1

In usual math notation, Zero is 0 and Succ is 1 +. So:

add m Zero = m

Is saying m + 0 = m, and:

add m (Succ n) = Succ (add m n)

Is saying m + (1 + n) = 1 + (m + n). So at every recursive call, the second argument to + decreases by 1, down to the base case of 0. For example, say we want to compute 2 + 3:

                  add (Succ (Succ Zero)) (Succ (Succ (Succ Zero)))
Succ             (add (Succ (Succ Zero))       (Succ (Succ Zero)))
Succ (Succ       (add (Succ (Succ Zero))             (Succ Zero)))
Succ (Succ (Succ (add (Succ (Succ Zero))                   Zero)))
Succ (Succ (Succ      (Succ (Succ Zero))))

Or:

                  add two three
Succ             (add two two)
Succ (Succ       (add two one))
Succ (Succ (Succ (add two Zero)))
Succ (Succ (Succ      two))
five

Given:

one = Succ Zero
two = Succ one
three = Succ two
four = Succ three
five = Succ four

You can also think of the Natural type as a linked list containing no values, where the length denotes a number. Then + is just concatenation of those lists.