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
foldr f a bs = foldl (\g b x -> g (f b x)) id bs a. Today I’ll try to derive this definition.
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
1 2 3
1 2 3
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
I first reorganize the arguments order a bit, putting
a at the end:
The base case is once again
and is trivially true:
1 2 3
The recursive case is not surprising either:
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
foldl is nowhere to be seen… which is not surprising considering that
foldl is tail recursive while
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,
foldr_acc is once again easy to define. The base case:
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:
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:
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
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.
foldr_acc defined as above, converting to
foldl is immediate:
If I rename
g, and move
x to the parameter list (uncurrying the
go function), I get the original definition.