如何手动推导计算Haskell自定义Nat类型对应的mult函数的求值过程？

你定义的mult是皮亚诺自然数体系下的标准乘法实现，逻辑本质是a * b等价于把b累加a次，完全不会出现无限循环。核心原因是每次递归的第一个参数都会逐层减少一层Succ构造子，最终一定会触发Zero对应的终止分支。

我们拿你熟悉的自然数计算举例，比如求2 * 1，对应的Nat写法是mult (Succ (Succ Zero)) (Succ Zero)，完整推导步骤如下：

-- 初始调用：对应自然数2 * 1
mult (Succ (Succ Zero)) (Succ Zero)
-- 匹配mult的第二个分支：Succ m = Succ (Succ Zero)，即m = Succ Zero，展开为 add n (mult m n)
→ add (Succ Zero) (mult (Succ Zero) (Succ Zero))
-- 计算内层的mult调用：对应1 * 1，再次匹配第二个分支，此时m = Zero
→ add (Succ Zero) (add (Succ Zero) (mult Zero (Succ Zero)))
-- 匹配mult的第一个终止分支：Zero乘任意值直接返回Zero
→ add (Succ Zero) (add (Succ Zero) Zero)
-- 计算内层add调用：add (Succ Zero) Zero = Succ Zero
→ add (Succ Zero) (Succ Zero)
-- 计算外层add调用，得到最终结果
→ Succ (Succ Zero) -- 对应自然数2，和2*1=2的预期完全一致

你担心的无限循环问题不会发生，因为整个递归的终止条件非常明确：当第一个参数为Zero时直接返回，不需要继续递归。每次调用mult时，第一个参数都会比上一次少一层Succ，递归深度严格等于第一个参数对应的自然数大小，一定会在有限步内终止。
你可以自己尝试推导3 * 2这类更复杂的计算，逻辑完全一致，就是把2累加3次，每一步都严格递减第一个参数，最终走到终止分支。

内容的提问来源于stack exchange，提问作者Djewey