# Exercise 3.8
(a) Define foldL′ in terms of foldL.
We can use the universal property for this. We have:
foldL′ f = foldL g e
if and only if
foldL′ f xs = case xs of
Nil → e
Cons y ys → g y (foldL′ f ys)
which gives us two equations,
foldL′ f Nil = e
foldL′ f (Cons y ys) = g y (foldL′ f ys)
The solution to the first is immediate: e = f Nothing. For the
second, we reason:
foldL′ f (Cons y ys) = g y (foldL′ f ys)
≡ { foldL′.2 }
f (Just (y, foldL′ f ys)) = g y (foldL′ f ys)
≡ { generalizing (foldL′ f ys) ∷ β to z }
f (Just (y, z)) = g y z
Having solved for e and g, we can apply the universal property:
foldL′ f = foldL g (f Nothing)
where
g y z = f (Just (y, z))
(b) Define foldL in terms of foldL′.
We're looking for a definition of the form
foldL f e xs = foldL′ g xs
which holds for all lists xs. To obtain this, we only need a
definition of g ∷ (Maybe (α, β) → β). We reason by synthesis on
the list xs.
Case Nil:
foldL f e Nil = foldL′ g Nil
≡ { foldL.1, foldL′.1 }
e = g Nothing
which gives the first equation for g.
Case (Cons x xs): We use the induction hypothesis
foldL f e xs = foldL′ g xs,
reasoning as follows:
foldL′ g (Cons x xs) = foldL f e xs
≡ { foldL.2, foldL′.1 }
g (Just (x, foldL′ g xs)) = f x (foldL f e xs)
≡ { hypothesis }
g (Just (x, foldL′ g xs)) = f x (foldL′ g xs)
≡ { generalizing (foldL′ g xs) to ys }
g (Just (x, ys)) = f x ys
which gives the second equation for g. We have:
foldL f e = foldL′ g
where
g Nothing = e
g (Just (x, ys)) = f x ys
This completes the synthesis.