In a previous post, I tried to show how to derive the formula expression foldl
in terms of foldr
. Unsurprisingly, there is a way to express foldr
in terms foldl
: foldr f a bs = foldl (\g b x > g (f b x)) id bs a
. Today I’ll try to derive this definition.
Of course, foldl
is strict, so it cannot work on infinite lists. Therefore, the new foldr
would be similarly limited.
I’ll start again from a standard definition for both functions. First foldr
:
1 2 3 

Then foldl
:
1 2 3 

Derivation
Once again, I will use the function building fold rather than value building one. This time, the f
argument to foldr
has already the right type, so I will not need flip
.
I first reorganize the arguments order a bit, putting a
at the end:
1


The base case is once again id
:
1


and is trivially true:
1 2 3 

The recursive case is not surprising either:
1


It follows from the induction hypothesis: given foldr f a bs == foldr_alt f bs a
, then foldr f a (b:bs) == foldr_alt f (b:bs) a
1 2 3 4 5 

But foldl
is nowhere to be seen… which is not surprising considering that foldl
is tail recursive while foldr
and foldr_alt
are both body recursive… maybe using an accumulator, we could turn foldr_alt
to a tail recursive function.
The initial value for the accumulator must be the identity of the composition function, that is, id
.
1


foldr_acc
is once again easy to define. The base case:
1


For the recursive case, notice that f b
is composed with the rest of the function to the right. As the accumulator represents the previous part of the function, f b
will be composed with this accumulator to the left:
1


The proof is less straightforward; I am not very familiar with equational reasoning, so maybe something simpler is possible. Note that in this proof, I need the list argument to be finite.
First, the base case:
1 2 

For the recursive case, I will not actually use an induction hypothesis. Instead, I will use the fact that the list is finite, and the fact that the composition function is, well, a function. f == g
implies acc . f == acc . g
for any terminating acc
.
1 2 3 4 5 6 7 8 9 10 11 12 

The fact that the equation only holds for list of finite lengths should not be surprising, but might still be a limitation of my proof.
With foldr_acc
defined as above, converting to foldl
is immediate:
1 2 

If I rename acc
to g
, and move x
to the parameter list (uncurrying the go
function), I get the original definition.
QED.