Haskell中Nat类型乘法定义错误排查与修正

I recently ran into a bug when implementing a multiplication function mult for a custom natural number type Nat in Haskell. Let me walk through the issue and how I fixed it.

The Broken Implementation #

First, here's the incorrect code I wrote:

mult :: Nat -> Nat -> Nat
mult Z m = Z
mult m Z = Z
mult (S m)(S n) = S (mult m n)
two = S (S Z)
three = S (S (S Z))

When testing this, the results were way off from what I expected:

> mult Z three
Z
> mult two three
S (S Z)
> mult three three
S (S (S Z))

What Went Wrong #

The core mistake was in the recursive case mult (S m)(S n) = S (mult m n). If you translate this to mathematical terms, it's claiming (1 + m) * (1 + n) = 1 + (m * n)—which is totally not how multiplication works! This recursive step didn't follow the actual logic of natural number multiplication.

The Corrected Implementation #

I rewrote the function using the correct recursive rule for multiplication: for any natural number m, (n+1)*m = m + (n*m), plus the base case that 0 multiplied by anything is 0. Here's the fixed code:

mult :: Nat -> Nat -> Nat
mult Z m = Z -------- 0*m = 0
mult (S n) m = plus m (mult n m) -------- (n+1)*m = m + n*m

(Note: This assumes you already have a correctly implemented plus function for adding two Nat values.)

Correct Results #

After fixing the code, testing it gives the expected outputs:

> mult Z three
Z
> mult two three
S (S (S (S (S (S Z)))))
> mult three three
S (S (S (S (S (S (S (S (S Z))))))))

The problem is now fully resolved!

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