[Haskell-cafe] lazy'foldl
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.)
>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list