# Proof that scanl' is fusion-safe

David Feuer david.feuer at gmail.com
Fri Jul 25 16:07:27 UTC 2014

```This proof is horribly inefficient. I imagine it could be fixed by
appealing to the universal property of foldr or something like that,
but I don't have time to look at that right now, so I'll just show you
what I have right now; I'm hoping someone will be willing to verify
that I haven't made any major errors.

scanl' :: (b -> a -> b) -> b -> [a] -> [b]
scanl' f a bs = build \$ \c n ->
a `seq` a `c`
foldr (\b g x -> let b' = f x b in b' `seq` (b' `c` g b'))
(\b -> b `seq` n)
bs
a

-- Inlining build in scanl' gives

scanl' f a bs =
a `seq`
a : foldr (\b g x -> let b' = f x b in b' `seq` (b` : g b'))
(\b -> b `seq` [])
bs
a

foldr evil wrong (scanl' f a bs)
= foldr evil wrong \$
a `seq`
a : foldr (\b g x -> let b' = f x b in b' `seq` (b` : g b'))
(\b -> b `seq` [])
bs
a -- Call this e1 a bs

=?= (\c n ->
a `seq`
a `c` foldr (\b g x -> let b' = f x b in b' `seq` (b' `c` g b'))
(\b -> b `seq` n)
bs
a) evil wrong  -- Call this e2 a bs

-- Expanding the outer foldr of e1 one step:

e1 a bs = a `seq` evil a
(foldr evil wrong \$
foldr (\b g x -> let b' = f x b in b' `seq` (b' : g b'))
(\b -> b `seq` [])
bs
a)

--Beta reduction of e2 gives

e2 a bs = a `seq` a `evil`
foldr (\b g x -> let b' = f x b in b' `seq` (b' `evil` g b'))
(\b -> b `seq` wrong)
bs
a

-- Now if a = _|_, these are clearly both _|_, so for the rest of all eternity,
-- assume a /= _|_. This eliminates one `seq`:

e1 a bs = evil a \$
foldr evil wrong \$
foldr (\b g x -> let b' = f x b in b' `seq` (b' : g b'))
(\b -> b `seq` [])
bs
a

e2 a bs = evil a \$
foldr (\b g x -> let b' = f x b in b' `seq` (b' `evil` g b'))
(\b -> b `seq` wrong)
bs
a

-- We will work by induction on the structure of bs, assuming that bs =
-- b1:b2:...:[] or b1:b2:...:_|_  I believe that the proof for the
-- partially defined case will somehow magically cover the infinite
-- case too by some general principle, but I don't know how that magic
-- works.

-- The base cases are kind of dull, so I'll start with the
-- inductive case. Assume that e1 bs = e2 bs

e1 a (q:bs) = evil a \$
foldr evil wrong \$
foldr (\b g x -> let b' = f x b in b' `seq` (b' : g b'))
(\b -> b `seq` [])
(q:bs)
a
= evil a \$
foldr evil wrong \$ (\b1 g1 x1 -> let b1' = f x1 b1 in b1'
`seq` (b1' : g1 b1')) q
(foldr (\b g x -> let b' = f x b in b' `seq` (b' : g b'))
(\b -> b `seq` [])
bs)
a
= evil a \$
foldr evil wrong \$ (\g1 x1 -> let b1' = f x1 q in b1'
`seq` (b1' : g1 b1'))
(foldr (\b g x -> let b' = f x b in b' `seq` (b' : g b'))
(\b -> b `seq` [])
bs)
a
= evil a \$
foldr evil wrong \$
(let b1' = f a q in b1' `seq` (b1' :
(foldr (\b g x -> let b' = f x b in b' `seq` (b' : g b'))
(\b -> b `seq` [])
bs) b1'

-- Since foldr is strict in its list argument, we can move the first
`seq` outward:

= evil a \$ let b1' = f a q in b1' `seq`
foldr evil wrong \$ (b1' :
(foldr (\b g x -> let b' = f x b in b' `seq` (b' : g b'))
(\b -> b `seq` [])
bs) b1'
= evil a \$ let b1' = f a q in b1' `seq`
evil b1' (foldr evil wrong \$ (foldr (\b g x -> let b' = f
x b in b' `seq` (b' : g b'))
(\b -> b `seq` [])
bs) b1')
= evil a \$ let b1' = f a q in b1' `seq` e1 b1' bs

e2 a (q:bs) = evil a \$
foldr (\b g x -> let b' = f x b in b' `seq` (b' `evil` g b'))
(\b -> b `seq` wrong)
(q:bs)
a
= evil a \$
(\b1 g1 x1 -> let b1' = f x1 b1 in b1' `seq` (b1' `evil` g1 b1')) q
(foldr (\b g x -> let b' = f x b in b' `seq` (b' `evil` g b'))
(\b -> b `seq` wrong)
bs) a
= evil a \$
let b1' = f a q in b1' `seq` (evil b1'
(foldr (\b g x -> let b' = f x b in b' `seq`
(b' `evil` g b'))
(\b -> b `seq` wrong)
bs)  b1')
= evil a \$
let b1' = f a q in b1' `seq` e2 b1' bs

scanl' f a bs =
a `seq`
a : foldr (\b g x -> (let b' = f x b in b' `seq` (b` : g b')))
(\b -> b `seq` [])
bs
a

-- The first base case is bs = _|_

e1 _|_ = evil a \$
foldr evil wrong \$
foldr (\b g x -> (let b' = f x b in b' `seq` (b' : g b')))
(\b -> b `seq` [])
_|_
a

-- Since foldr is strict in its list argument, this reduces to

e1 _|_ = evil a \$
foldr evil wrong \$ _|_ a
= evil a (_|_ a) = evil a _|_

-- Next we look at e2 _|_

e2 _|_ = evil a \$
foldr (\b g x -> (let b' = f x b in b' `seq` (b' `evil` g b')))
(\b -> b `seq` wrong)
_|_
a
= evil a (_|_ a) = evil a _|_

-- The second base case is bs = [].

e1 [] = evil a \$
foldr evil wrong \$
foldr (\b g x -> (let b' = f x b in b' `seq` (b' : g b')))
(\b -> b `seq` [])
[]
a
= evil a \$
foldr evil wrong \$ (\b -> b `seq` []) a
= evil a \$
foldr evil wrong (a `seq` [])

-- Since we haven't reached the end of all eternity yet, a /= _|_

e1 [] = evil a \$ foldr evil wrong []
= evil a wrong

e2 [] = evil a \$
foldr (\b g x -> (let b' = f x b in b' `seq` (b' `evil` g b')))
(\b -> b `seq` wrong)
[]
a
= evil a \$ (\b -> b `seq` wrong) a
= evil a (a `seq` wrong)
= evil a wrong  -- Eternity passes so slowly!
```