Past exam of the year 1 of the computer science course of the University of Oxford / 2019 / Functional programming, design and analysis of algorithms / 1

The right fold replaces the two list constructors by its two arguments; the left fold instead updates an accumulator while traversing the list.

foldr :: (a -> b -> b) -> b -> [a] -> b
foldr c z []     = z
foldr c z (x:xs) = c x (foldr c z xs)

foldl :: (b -> a -> b) -> b -> [a] -> b
foldl s a []     = a
foldl s a (x:xs) = foldl s (s a x) xs

Thus foldr is the natural list fold: it preserves the constructor arrangement while replacing [] by z and (:) by c. In particular, foldr (:) [] = id. More generally, the fold factorisation criterion says that the defining equations characterize the corresponding structural recursion. Association and lazy evaluation are separate: the accumulator in this definition of left fold is not automatically evaluated at each step.^[ref]

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 every accumulator, including s a x. Consequently every such finite approximation has result $\perp$.

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 $\perp$, 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 $\perp$, 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.

Over integers, choose s = c = (+) and a = b = 0. The left fold and right fold both compute the sum of a finite list.

Over integers, choose s = (-), c = flip (-), and a = b = 0. The left fold and right fold both compute the negative of the sum of a finite list. The combining functions differ: s 1 2 = -1, whereas c 1 2 = 1.

Let $F=\mathrm{foldl}(\ominus )0$, using the specified operation $u\ominus v=v-u$. Direct evaluation gives $F([])=0$, $F([0])=0$, $F([1])=1$, and $F([1,0])=-1$.

Suppose $F=\mathrm{foldr}cb$ with the same integer result type. The empty list forces $b=0$. The two singleton calculations force $c00=0$ and $c10=1$. But thencontrary to $F([1,0])=-1$. No such c,b exist. This is the information restriction in the fold factorisation criterion: equal folded tails must remain indistinguishable after the same head is attached. A larger, function-valued result type can retain the missing information, as the continuation representation of a left fold does below.

Assign $y:u$ and $x:v$. The application s y x forces $s:u\to v\to w$ for a fresh type $w$; applying f to that result forces $f:w\to r$. No further equations identify these four type variables. The principal type is therefore

k :: (u -> v -> w) -> v -> (w -> r) -> u -> r
k s x f y = f (s y x)

Every compatible typing is an instance of this one, because type inference imposed precisely the two application constraints and no class constraints.

Fix s and put $R(xs,a)=\mathrm{foldr}(ks)\mathrm{id}xsa$. The right fold equations giveThese are exactly the left fold equations. Structural induction, with the induction hypothesis quantified over all accumulators, proves equality on finite terminating lists.

To include the other input spines, first observe that both applied expressions give $\perp$ on an undefined spine. The same induction proves equality on every finite prefix ending in $\perp$: the step k s x f a demands the continuation f when its result is demanded. Finally use that the two applied operations are Scott continuous maps, taking the limit over prefixes interpreted as a finite approximation of a lazy list. This covers infinite spines, on which both applied expressions are $\perp$, and proves the identity for all lists under the stated Haskell semantics. The intermediate right fold builds an accumulator-transforming function; it does not provide a terminating left fold of an infinite list.