# Wakatta!

## Like Eureka!, only cooler

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`:

Then `foldl`:

## 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:

The base case is once again `id`:

and is trivially true:

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`

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`.

`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 `acc`.

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:

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

QED.