[Haskell-cafe] lazy'foldl
Sebastian Fischer
sebf at informatik.uni-kiel.de
Wed Feb 10 14:35:22 EST 2010
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.)
More information about the Haskell-Cafe
mailing list