Hello, I have implemented the following function: lazy'foldl :: (a -> b -> Maybe a) -> Maybe a -> [b] -> Maybe a lazy'foldl _ Nothing _ = Nothing lazy'foldl _ m [] = m lazy'foldl f (Just y) (x:xs) = lazy'foldl f (f y x) xs After hoogling its type, I found that Control.Monad.foldM :: (a -> b -> Maybe a) -> a -> [b] -> Maybe a seems like a perfect replacement because lazy'foldl f (Just x) xs == foldM f x xs holds for all finite lists xs. Here is an inductive proof: lazy'foldl f (Just x) [] == Just x == foldM f x [] lazy'foldl f (Just x) (y:ys) == lazy'foldl f (f x y) ys (if f x y == Nothing) == lazy'foldl f Nothing ys == Nothing == Nothing >>= \z -> foldM f z ys == f x y >>= \z -> foldM f z ys == foldM f x (y:ys) lazy'foldl f (Just x) (y:ys) == lazy'foldl f (f x y) ys (if f x y == Just z) == lazy'foldl f (Just z) ys (induction) == foldM f z ys == Just z >>= \z -> foldM f z ys == f x y >>= \z -> foldM f z ys == foldM f x (y:ys) I think the above equation holds even for infinite lists xs. Both functions terminate on infinite lists, if the accumulator is eventually Nothing. Do you see any differences in terms of strictness, i.e., a counter example to the above equation that involves bottom? I don't. Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.)