For every accumulator , pattern matching makes foldl s a undefined the bottom value. Now use structural induction on a finite list prefix ending in the bottom value. The induction step is foldl s a (x:ps) = foldl s (s a x) ps; the induction hypothesis applies to every accumulator, including s a x. Consequently every such finite approximation has result .
An infinite lazy list is the limit of its finite prefixes, each interpreted as a finite approximation of a lazy list. Definable Haskell operations are Scott continuous maps, so the result on the infinite lazy list is the supremum of the results on these approximations. Every result is , hence foldl s a xs = undefined on every infinite input spine, irrespective of whether s would inspect the accumulator.
For a concrete separation, choose s = (&&), a = True, and xs = False : repeat True. The left fold is , whereas the right fold returns False after observing the first element: False && r does not demand r. It is reaching the end of the input spine, rather than strictness of the combining operation, that prevents this left fold from returning.

Articles by others on the same topic (0)

There are currently no matching articles.