Exercise G in Chapter 6 of Richard Bird’s Thinking Functionally with Haskell asks the reader to prove
foldl f e . concat = foldl (foldl f) e given the rule
foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys There’s no mention whether the given rule applies to infinite lists, nor does the answer in the book mention infinite lists. If my reasoning is correct, they are indeed both valid for infinite lists, provided f is strict.
The undefined case for the given rule requires this additional proof:
-- f is strict ⟹ foldl f is strict (i.e., foldl f undefined = undefined) foldl f undefined xs = undefined xs -- case undefined foldl f undefined undefined undefined undefined -- = {foldl.0} = {?} undefined undefined -- case [] foldl f undefined [] undefined [] -- = {foldl.1} = {?} undefined undefined -- case (x:xs) foldl f undefined (x:xs) undefined (x:xs) -- = {foldl.2} = {?} foldl f (f undefined x) xs undefined -- = {f is strict} foldl f (undefined x) xs -- = {?} foldl f undefined xs -- = {induction} undefined xs -- = {?} undefined As an aside, my proof for the dual of the above rule for foldr:
-- f x is strict ⟹ foldr f is strict (i.e., foldr f undefined = undefined) foldr f undefined xs = undefined xs -- case undefined foldr f undefined undefined undefined undefined -- = {foldr.0} = {?} undefined undefined -- case [] foldr f undefined [] undefined [] -- = {foldr.1} = {?} undefined undefined -- case (x:xs) foldr f undefined (x:xs) undefined (x:xs) -- = {foldr.2} = {?} f x (foldr f undefined xs) undefined -- = {induction} f x (undefined xs) -- = {?} f x undefined -- = {f x is strict} undefined The given rule:
-- f is strict ⟹ foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys -- case undefined foldl f e (undefined ++ ys) foldl f (foldl f e undefined) ys -- = {++.0} = {foldl.0} foldl f e undefined foldl f undefined ys -- = {foldl.0} = {f is strict ⟹ foldl f is strict} undefined undefined ys -- = {?} undefined -- case [] foldl f e ([] ++ ys) foldl f (foldl f e []) ys -- = {++.1} = {foldl.1} foldl f e ys foldl f e ys -- case (x:xs) foldl f e ((x:xs) ++ ys) foldl f (foldl f e (x:xs)) ys -- = {++.2} = {foldl.2} foldl f e (x : (xs ++ ys)) foldl f (foldl f (f e x) xs) ys -- = {foldl.2} = {induction} foldl f (f e x) (xs ++ ys) foldl f (f e x) (xs ++ ys) My solution to the exercise:
-- f is strict ⟹ foldl f e . concat = foldl (foldl f) e foldl f e (concat xs) = foldl (foldl f) e xs -- case undefined foldl f e (concat undefined) foldl (foldl f) e undefined -- = {concat.0} = {foldl.0} foldl f e undefined undefined -- = {foldl.0} undefined -- case [] foldl f e (concat []) foldl (foldl f) e [] -- = {concat.1} = {foldl.1} foldl f e [] e -- = {foldl.1} e -- case (x:xs) foldl f e (concat (x:xs)) foldl (foldl f) e (x:xs) -- = {concat.2} = {foldl.2} foldl f e (x ++ concat xs) foldl (foldl f) (foldl f e x) xs -- = {f is strict ⟹ foldl f e (xs ++ ys) = foldl f (foldl f e xs) ys} foldl f (foldl f e x) (concat xs) -- = {induction} foldl (foldl f) (foldl f e x) xs Does this work? If so, is it often the case that rules restricted to finite lists can be made to work for all lists given additional strictness requirements like this?
There are several lines above with {?} given as my reasoning. They could be replaced by {undefined x = undefined}, but I am just guessing there. If that is true, how could it be justified?
