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