Miguel Mitrofanov miguelimo38 at yandex.ru
Wed Feb 10 15:17:29 EST 2010

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