自然数作为递归数据类型

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:这是摘自Richard Bird的"功能编程简介"一书.

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类型视为不包含值的链接列表,其中length表示数字.然后+就是这些列表的连接.