David Feuer | 25 Jul 18:07 2014
Picon

Proof that scanl' is fusion-safe

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
(Continue reading)


Gmane