# Exercise 3.1 (fusion law)
NTS: For strict h,
h ∘ foldL f e = foldL f′ e′
holds if
(h (f a b) = f′ a (h b)) ∧ (h e = e′)
Proof: Using the universal property of foldL, it holds that
h ∘ foldL f e = foldL f′ e′ if we can show the following:
(h ∘ foldL f e) Nil = e′
(h ∘ foldL f e) (Cons y ys) = f′ y ((h ∘ foldL f e) ys)
So we have two cases to deal with.
We assume that
h (f a b) = f′ a (h b) (A)
h e = e′ (B)
Case Nil:
(h ∘ foldL f e) Nil
≡
h (foldL f e Nil)
= { foldL.1 }
h e
= { B }
e′
which establishes the case.
Case (Cons y ys):
h (foldL f e (Cons y ys))
= { foldL.2 }
h (f y (foldL f e ys))
= { A }
f′ y (h (foldL f e ys))
≡
f′ y ((h ∘ foldL f e) ys)
which establishes the case. ∎
Why doesn’t the law hold for non-strict h?