Proof that scanl' is fusion-safe

[David Feuer]

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!