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]