Haskell数据Nat

Question

以下是Hutton的Haskell编程(p.102).

data Nat = Zero | Succ Nat

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

如果我输入natToInt Zeroghci,我得到0.如果我输入natToInt (Succ Zero),我得到1.

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

内在的(Succ Zero)回归1？这意味着,在我看来,最外层采用1作为参数,这是不正确的,因为1不是Nat类型.那就是

natToInt (Succ ( 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

请参阅:您只需要替换/匹配双方的表达式