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

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

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%, что значение уменьшается само по себе или что. Я хочу понять добавление шаг за шагом.

P.S. Это взято из книги Ричарда Берда «Введение в функциональное программирование».


person 0908    schedule 22.11.2015    source источник
comment
Значение есть значение; он не увеличивается и не уменьшается.   -  person Daniel Wagner    schedule 22.11.2015
comment
Второй аргумент add уменьшается при каждом рекурсивном вызове: с Succ n до n.   -  person chi    schedule 22.11.2015


Ответы (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))))

Or:

                  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 как о связанном списке, не содержащем значений, где длина обозначает число. Тогда + — это просто объединение этих списков.

person Jon Purdy    schedule 22.11.2015