= Solution
For every accumulator $a$, <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 \i[every] accumulator, including `s a x`. Consequently every such finite approximation has result $\bot$.
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 $\bot$, hence \b[`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 $\bot$, whereas the <right fold> returns \b[`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.
Back to article page
