[Haskell-cafe] lazy'foldl

[Sebastian Fischer]

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