Понимание рекурсивных алгебраических типов в функциональном программировании

Question

Эй, у меня возникли проблемы с пониманием того, как работают рекурсивные алгебраические типы и как их использовать. Возьмем, например, определение ниже RAT для натуральных чисел:

data Nat = Zero | Succ Nat 

Мы используем RAT здесь, потому что набор значений должен быть бесконечным, и я знаю, что принцип заключается в том, чтобы выразить каждое новое значение с точки зрения предыдущий, но я не понимаю, как это образует натуральные числа. Кто-то умнул бы это очистить? Благодаря

Answer 1

Это утверждает, что:

• Nat тип.

• Zero имеет тип Nat. Это представляет собой натуральное число 0.

• Если n имеет тип Nat, то Succ n имеет тип Nat. Это представляет собой натуральное число n +1.

Так, например, Succ (Succ Zero) представляет собой 2, 3 представляет Succ (Succ (Succ Zero)), Succ (Succ (Succ (Succ Zero))) представляет 4, и так далее. (Эта система определения натуральных чисел от 0 и преемников называют Peano axioms.)

В самом деле, Zero и Succ просто специальные виды функций (конструкторы), объявленные для создания Nat значения:

Zero :: Nat 
Succ :: Nat -> Nat 

Отличия от обычных функций является то, что вы можете взять их друг от друга с сопоставлением с образцом:

predecessor :: Nat -> Nat 
predecessor Zero = Zero 
predecessor (Succ n) = n 

Ничто об этом не относится к рекурсивным алгебраическим типам данных, конечно, только к алгебраическим типам данных; но простой факт, что тип алгебраических данных может иметь значение того же типа, что и одно из его полей, является тем, что создает здесь рекурсию.