Sebastian Fischer sebf at informatik.uni-kiel.de
Wed Feb 10 14:35:22 EST 2010

```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.)

```