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?

How may I simplifies foldl where some element might be erroneous in Haskell?

I have a function that will calculate the sum of a list of integer, however if any of the number is negative, it will should an error instead (not throwing exception).

The following is a working Haskell code (Glasgow Haskell Compiler, Version 7.10.3):

addAll :: [Int] -> Either String Int                                                                                                                           addAll xs = foldl safeAdd (Right 0) xs                                                                                                                            where                                                                                                                                                           safeAdd :: Either String Int -> Int -> Either String Int                                                                                                    safeAdd = (\acc next -> case acc of                                                                                                                                         Left s  -> Left s                                                                                                                                           Right n -> if next < 0                                                                                                                                                  then Left (show next ++ " is not positive")                                                                                                                 else Right (n + next)) 

Examples output of the function:

addAll [1,2,3]  -- Right 6 addAll [-1,2,3] -- Left "-1 is not positive" 

Although the code works, but I’m not entirely satisfied with it, because the recursion keeps going until the last element even though errors are encountered early. Not only that, it feels a little more complicated than it should be.

After reading some SO posts such as this one, I think that the code above can be further simplified using functions like foldM or even applicative <$ >.

But, I’m just not sure how to use those functions, so please do show me a way to simplify the code above.