理解函数式编程中的递归代数类型

Question

嘿,我在理解递归代数类型如何工作以及如何准确使用它们时遇到了一些麻烦.例如,对自然数采用以下RAT定义:

data Nat = Zero | Succ Nat

我们在这里使用RAT是因为这组值必须是无限的,我知道原则是用前一个表示每个新值,但我不明白它是如何形成自然数的.有人会介意清除这个吗？谢谢

Answer 1

这表明:

因此,例如,Succ (Succ Zero)表示2,Succ (Succ (Succ Zero))表示3,Succ (Succ (Succ (Succ Zero)))表示4,依此类推.(这种定义0和后继自然数的系统称为Peano公理.)

实际上,Zero并且Succ只是声明为创建值的特殊类型的函数(构造函数)Nat:

Zero :: Nat
Succ :: Nat -> Nat

与常规函数的区别在于您可以使用模式匹配将它们分开:

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

对于递归代数数据类型,当然只有代数数据类型,这一点并不特别; 但是代数数据类型可以具有与其字段之一相同类型的值的简单事实是在此处创建递归.

@ user1058210不,Succ不是内置的.它只是你给构造函数的名字.你需要一种从"n"到"n + 1"的方法,所以你可以代表任何数字.如果定义只是"数据Nat = Zero",则只能表示零.当然你可以将它扩展到更多数字,例如`data Nat = Zero | 一个| 两个`,但这种方法只给你一个有限数量的数字.使用Succ,您只需将`Succ`应用于'Zero``n`次来表示数字`n`. (3认同)