[Haskell-cafe] lazy'foldl

[Miguel Mitrofanov]

For the reference: foldM is defined as
foldM :: Monad m => (a -> b -> m a) -> a -> [b] -> ma
foldM _ a [] = return a
foldM f a (x:xs) = f a x >>= \fax -> foldM f fax xs

Let's define

foldM' f x xs = lazy'foldl f (Just x) xs

We can check that foldM' satisfies the same equations as foldM:

foldM' f a [] = lazy'foldl f (Just a) [] = Just a = return a
f a x >>= \fax -> foldM' f fax xs = case f a x of {Nothing -> Nothing;  
Just fax -> foldM' f fax xs} =
   case f a x of {Nothing -> Nothing; Just fax -> lazy'foldl f (Just  
fax) xs} =
   case f a x of {Nothing -> lazy'foldl f Nothing xs; Just fax ->  
lazy'foldl f (Just fax) xs} = (*)
   lazy'foldl f (f a x) xs = lazy'foldl f (Just a) (x:xs) = foldM' f a  
(x:xs)

(*) this holds, because lazy'foldl actually does pattern match on it's  
second argument

This means, that foldM' as at least as defined as foldM (meaning,  
roughly, that if foldM gives a meaningful, non-undefined value, foldM'  
produces the same value; if foldM gives (_|_), foldM' is free to  
produce anything). Therefore, lazy'foldl f (Just x) xs is at least as  
defined as foldM f x xs.

On the other hand, let's define

lazyf f mx xs = case mx of {Nothing -> Nothing, Just x -> foldM f x xs}

lazyf satisfies the same equations as lazy'foldl:

lazyf f Nothing xs = Nothing
lazyf f (Just y) (x:xs) = foldM f y (x:xs) = f y x >>= \fyx -> foldM f  
fyx xs =
   f y x >>= \fyx -> lazyf f (Just fyx) xs =
   case f y x of {Nothing -> Nothing; Just fyx -> lazyf f (Just fyx)  
xs} =
   case f y x of {Nothing -> lazyf f Nothing xs; Just fyx -> lazyf f  
(Just fyx) xs} = (*)
   lazyf f (f y x) xs

(*) again, lazyf does pattern-match on it's second argument, so this  
is valid

lazyf f mx [] = case mx of {Nothing -> Nothing, Just x -> foldM f x  
[]} =
   case mx of {Nothing -> Nothing, Just x -> return x} =
   case mx of {Nothing -> Nothing, Just x -> Just x} = mx

The last equality holds because there are only three kinds of values  
mx can have: Nothing, Just x, or (_|_); in all three cases pattern- 
matching produces the same value.

That means, that lazyf is at least as defined as lasy'foldl, so foldM  
f x xs = lazyf f (Just x) xs is at least as defined as lazyfoldl' f  
(Just x) xs.

All this means that lazy'foldl f (Just x) xs coincides with foldM f x  
xs exactly, for all possible f, x, and xs.


On 10 Feb 2010, at 22:35, Sebastian Fischer wrote:

> 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.)
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe