Натуральные числа как рекурсивный тип данных

Question

Я начал работать с типами данных, но меня смущает следующее:

data Natural = Zero | Succ Natural

add :: Natural -> Natural -> Natural

add m Zero = m

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

Как это дополнение работает? Я понял это Natural 3 представлен Succ(Succ(Succ 0))) хотя мне все еще не ясно на 100%, что это значение само по себе уменьшается или как. Я хочу понять сложение шаг за шагом.

PS: Это было взято из книги Введение в функциональное программирование Ричарда Берда.

Answer 1

В обычной математической записи Zero является 0 а также Succ является 1 +, Так:

add m Zero = m

Говорит m + 0 = m, а также:

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

Говорит m + (1 + n) = 1 + (m + n), Таким образом, при каждом рекурсивном вызове второй аргумент + уменьшается на 1, вплоть до базового случая 0. Например, скажем, мы хотим вычислить 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))))

Или же:

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

Дано:

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

Вы также можете думать о Natural введите как связанный список, не содержащий значений, где длина обозначает число. затем + это просто объединение этих списков.