Mistake at Exercise 3.3.2 #1
Description
On the solution of Exercise 3.3.2, you wrote:
-- prove that n + m = m + n
-- n + m ==
-- (n +) . foldn Succ Zero m ==
-- by fusion law
-- foldn Succ n m
...
-- let's define + using first argument pattern mathing:
(+) :: Nat -> Nat -> Nat
Zero + n = n
(Succ m) + n = Succ(m + n)
A pre-requisite condition of applying fusion law on the equation is that (n+).Succ = Succ.(n+). However, if (+) is defined in the above-shown way, we can only get (+n).Succ = Succ. (+n). Thus, under this definition, the fusion law is not applicable.
Thanks for writing those solutions, they really helped me a lot in learning functional programming!