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
