Haskell 数据 Nat答案

【问题标题】：Haskell data NatHaskell 数据 Nat
【发布时间】：2016-05-06 04:12:10
【问题描述】：

以下内容来自 Hutton 的《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 (Succ ( 1 + 0)).

谁能帮我理解一下？

【问题讨论】：

将Succs 视为从外到内展开。
不，natToInt (Succ Zero) 返回 1。Succ Zero 本身返回一个 Nat 类型的值。

标签： haskell functional-programming

【解决方案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

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

【讨论】：

那么是先执行外层Succ吗？
@MaxKim：是的。你总是只看壳。如果你想了解内脏，你必须明确地这样做。