Recall the definition of folding a list from the right
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f b [] = b
foldr f b (a:as) = f a (foldr f b as)
for example foldr f b [1,2,3] = f 1 (f 2 (f 3 b)).
And folding a list from the left
foldl :: (a -> b -> a) -> a -> [b] -> a
foldl f a [] = a
foldl f a (b:bs) = foldl f (f a b) bs
for example foldl f a [1,2,3] = f (f (f a 1) 2) 3.
According to the uniqueness property of catamorphisms (http://eprints.eemcs.utwente.nl/7281/01/db-utwente-40501F46.pdf),
a function h is a catamorphism foldr f b if and only if h [] = b and h (a:as) = f a (h as).
To apply this rule to derive fold in terms of folder, we temporarily refactor the definition of foldl
to recurse over the list directly such that it fits the pattern for the function h in the theorem:
foldl :: (a -> b -> a) -> a -> [b] -> a
foldl f a bs = h bs a
where
h [] = \a -> a
h (b:bs) = \a -> h bs (f a b)
From the definition of h we can directly read the foldr version of h namely
h = foldr (\b -> \g -> (\a -> g (f a b))) (\a->a).
If we plug this definition back into the refactored foldl we obtain
foldl f a bs = foldr k (\a->a) bs a
where
k = \b -> \g -> (\a -> g (f a b))
Just for fun, since the definition is the witness of of using the uniqueness theorem to prove that h is a catamorphism,
we can unfold our new definition on the example list [1,2,3] as follows:
foldl f a [1,2,3]
=
foldr k (\a->a) [1,2,3] a
=
k 1 (k 2 (k 3 id)) a
=
k 2 (k 3 id) (f a 1)
=
k 3 id (f (f a 1) 2)
=
id (f (f (f a 1) 2) 3)
=
(f (f (f a 1) 2) 3)
=
foldl f a [1,2,3]