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!