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