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!
More information about the Libraries
mailing list