Haskell 数据 Nat

Question

以下摘自 Hutton 的《Programming in Haskell》(第 102 页)。

data Nat = Zero | Succ Nat

natToInt :: Nat -> Int
natToInt Zero = 0
natToInt (Succ n) = 1 + natToInt n

如果我在 ghci 中输入 natToInt Zero，我得到 0。如果我输入 natToInt (Succ Zero)，我得到 1。

但是 natToInt (Succ (Succ Zero)) 返回 2。我从逻辑上理解它，但我不明白它是如何在这个语句中递归工作的。

内部 (Succ Zero) 不返回 1 吗？这意味着，在我看来，outermost 将 1 作为参数这是不正确的，因为 1 不是 Nat 类型。那么就是

natToInt(成功(1 + 0))。

谁能帮我理解一下？

Answer 1

你在替换中有一个小错误 - 你在这里替换了错误的Succ。

让我们一步一步来:

natToInt (Succ (Succ Zero))
{ case 2: (Succ n) = Succ (Succ Zero) so n = Succ Zero}
= 1 + natToInt (Succ Zero)
{ case 2: (Succ n) = Succ Zero so n = Zero}
= 1 + (1 + natToInt Zero)
{ case 1}
= 1 + (1 + 0)
= 1 + 1
= 2

看:你只需要替换/匹配两边的表达式