haskell - 自然数作为递归数据类型

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% 清楚该值是自行减少还是什么。我想了解一步一步的加法。

P.S:这摘自 Richard Bird 的《函数式编程简介》一书。

Answer 1

在通常的数学符号中，0 是 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 类型视为不包含值的链表，其中长度表示数字。那么 + 只是这些列表的串联。