# Is my understanding of strictness correct in this proof of a `foldl` rule? 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? Posted on Categories proxies