# [Haskell-cafe] Proof that scanl can be written as foldr?

Cristian Ontivero contiver at itba.edu.ar
Sat Jan 3 17:59:15 UTC 2015

```Hello, I'm trying to solve the exercise 4.6.5 of Bird's "Introduction to
Let me quote:

"Prove that scanl f e can be written as a foldr, if f is associative with
unit e. Can scanl f e be written as a foldl without any assumptions on f
and e?"

So far reasoning by myself and googling a bit I reached to the following
scanl definition using foldl (without any assumptions afaik):
scanl f e = foldl (\xs next -> xs ++ [f (last xs) next]) [e]

Furthermore, previously on the same chapter, it says that:
scanl f e = foldr g [e] where g x xs = e : map (f x) xs

Using this definition, I tried proving it by induction, but since I got
stuck, I tried seeing if I could find some way to use the first duality
theorem (with the foldl definition), or fusion, but to no avail.
The induction proof I wrote is the following:

scanl f e = foldr g [e]
where g y ys = e : map (f y) ys
By the principle of extensionality, this is equivalent to:
scanl f e xs = foldr g [e] xs
where g y ys = e : map (f y) ys

We prove this equality by induction on xs.
Case([]). For the left-hand side we reason
scanl f e []
= {scanl.1}
[e]

For the right-hand side
foldr g [e] []
= {foldr.1}
[e]

Case(x:xs). For the left-hand side we reason
scanl f e (x:xs)
= {scanl.2}
e : scanl f (f e x) xs
= {f has unit e}
e : scanl f x xs
= {induction hypothesis}
e : foldr g [x] xs

For the right-hand side
foldr g [e] (x:xs)
= {foldr.2}
g x (foldr g [e] xs)
= {definition of g}
e : map (f x) (foldr g [e] xs)
= {definition of map}
e : foldr ((:) . (f x)) [] (foldr g [e] xs)

I'm not even sure the last step is useful, but I thought maybe I could
combine both foldrs into a single one (that's why I thought about the
fusion law).
Anyway, any help or pointer that can lead me in the right direction is very
much appreciated.