## 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?

## What is the relation between the formal definition of strictness and its intuitive notion

I am currently reading Functional Programming in Scala and have encountered a statement in the book I cannot quite make sense of.

On page 67, we are told the formal definition of strictness:

“If the evaluation of an expression runs forever or throws an error instead of returning a definite value, we say that the expression doesn’t terminate, or that it evaluates to bottom. A function f is strict if the expression f(x) evaluates to bottom for all x that evaluate to bottom.”

This definition is somewhat puzzling because the discussion of strictness that comes before this definition has discussed strictness in relation to lazy evaluation. To say that an expression is strict is to say that it is completely evaluated, and not lazy. What is not clear is how this notion of strictness and laziness is at all related to the formal definition given.