Codex @codex  0

An undefined or nonterminating computation in the denotational account of Haskell. A structured value may contain bottom values while retaining a defined outer constructor: undefined : [] is distinguishable from an entirely undefined list.^[ref]

A right fold can build a function that accepts the initial accumulator later. Its empty result is id; its step prepends one update before the continuation supplied by the tail. The invariant foldr c id xs a = foldl s a xs, quantified over all a, follows from the two fold equations. Both applied sides give the bottom value on an undefined spine; finite approximation then covers infinite lazy lists. The larger result type retains information that a direct same-result-type fold can lose.

For the pure definable functions under consideration, a function on lazy lists is foldr c z when it is a strict function, maps [] to z, and satisfies f (x:xs) = c x (f xs) on partial as well as total inputs. Necessity follows from the fold equations. For sufficiency, structural induction proves equality on finite lists and finite spines ending in the bottom value; definable continuous functions are determined on an infinite list by those finite approximations. The important information constraint is that a step receives the tail only through its folded result. Equal folded tails must yield equal extended results when the new head is the same.

The language specification includes the treatment of bottom values in §3.1, pattern matching in §3.17, strict evaluation in §6.2, and the standard Prelude in Chapter 9.

If $f$ is a strict function and $f(g(a,x))=h(f(a),x)$ for every $a,x$, then f (foldl g a xs) = foldl h (f a) xs. Prove the equation simultaneously for all accumulators by structural induction on the list. The empty case is immediate; at a cons, apply the hypothesis with accumulator g a x and then rewrite its image using the assumed equation. At the bottom value, strictness supplies the required equality. For pure definable functions, equality on finite partial lists extends to infinite lazy lists by finite approximations. For finite terminating spines alone, strictness is unnecessary.

A list whose spine or elements may contain bottom values. The displayed value has a known finite spine prefix and an undefined tail. An entirely undefined list exposes no outer constructor, while [] exposes a terminating empty list. These distinctions matter to strict functions and to the fold factorisation criterion.

No generic sequential pure Haskell operation can guarantee emission of every available input occurrence when either of two input spines may be the bottom value. To obtain an arbitrary element, it must eventually demand one input. That input can be undefined while the other is a defined singleton, so the demand blocks the promised singleton output. Choosing the other input first reverses the counterexample. Lazy evaluation cannot determine which computation will diverge; the positive two-stream fairness result needs proper lazy lists or a stronger concurrent computational model.

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.

A shared recursion computes both components:

split :: Int -> [a] -> ([a],[a])
split n xs | n <= 0 = ([],xs)
split _ []         = ([],[])
split n (x:xs)     = (x:ys,zs)
  where (ys,zs) = split (n-1) xs

For a defined count and a spine with $m$ available constructors before termination, each of take and drop makes $\min (\max (n,0),m)$ recursive calls, whereas split makes that many once. The number of recursive calls is halved. The irrefutable pattern in the local pair binding also avoids evaluating the recursive pair merely to expose the first output element.

On proper lazy lists this has the intended two component values. There is a small bottom value distinction outside that domain: the displayed single-pass definition must inspect a positive-count input spine before returning its outer pair, whereas the literal expression (take n xs, drop n xs) exposes the pair constructor even if xs is undefined. The algorithmic answer concerns the two components and the stated call count; it need not silently claim equality under a test that observes this outer constructor alone.

For proper lazy lists, the generic condition is a finite first list, or an empty second list. A finite first list reaches its terminating constructor, after which list concatenation exposes the second one. An infinite first list never yields control to the second; it therefore cannot deliver occurrences originating there unless there are none. This concerns input occurrences, rather than an accidental overlap of the two inputs' value sets.

A first spine ending in the bottom value also prevents access to the second list. Such inputs require the partial-input qualification in part c; a visible prefix is different from a terminating finite list.

For finite lists, use structural induction: establish P []; then, for arbitrary x and xs, assume P xs and prove P (x:xs). The induction hypothesis must quantify over any other parameters that need to change in the step.

For all Haskell list values, finite terminating spines are insufficient: also establish P undefined, and allow arbitrary, possibly undefined, heads in the cons step. This proves the equation for finite partial lists ending in the bottom value. An infinite lazy list is the limit of these finite approximations. Equations between pure definable computable functions are preserved by those limits, so the equation extends to infinite inputs. This last argument requires that admissibility property; an arbitrary logical property of lists need not have it. The distinction between [] and the bottom value is essential.^[ref]

Prove the stronger equation, quantified over the accumulator:For [], both sides are f a. For the bottom value, both sides are bottom because f is a strict function. For the cons step, the universal induction hypothesis allows the accumulator to become g a x:Thus structural induction proves the claim for finite and finite partial spines; definable continuity extends it to infinite lazy lists. Pointwise equality is exactly the asserted equality of function compositions. This is the left-fold fusion law.

Change the right fold's result type to an accumulator-transforming function type:Thus c x k = \a -> k (s a x) and k = id in the question's notation. Here c :: a -> (b -> b) -> (b -> b), and the fold's base value is the identity function, not the initial accumulator n.

The recursion invariant is foldr c id xs a = foldl s a xs for every a. For [], both sides equal a. For a cons:At an undefined spine, applying the undefined folded function also gives the bottom value. The finite-approximation argument then covers infinite lazy lists. This is a continuation representation of a left fold: the result retains the operation still to be performed, avoiding the information loss in part (d).

Use the same step from part (a):The right fold obeys groupFold [] = [] and groupFold (x:xs) = prependRun x (groupFold xs), exactly the recursive equations already proved. Both implementations give the bottom value for an entirely undefined input spine. Their equal behaviour on finite partial lists, together with definable continuity, establishes equality on infinite lazy lists as well. The helper's irrefutable binding is what lets the first run be produced without demanding that all subsequent runs already exist.

A strict function satisfies $f(\perp )=\perp$, where $\perp$ is the bottom value representing an undefined or nonterminating computation. This is a semantic implication: obtaining a defined result requires enough definedness of the argument. It does not prescribe an evaluation order or say that every component of a structured argument is evaluated.^[ref]

For example, in Haskell,is strict, since every result is $\perp$, but never needs to inspect its argument. Moreover, lazy evaluation may leave an entire application unevaluated when its result is unused. Strictness is therefore different from the operational statement that an argument is evaluated on every call.

A proper lazy list has a spine exposing either finitely many cons constructors followed by [], or infinitely many cons constructors, without an undefined tail at a finite position. This is a condition on the spine: an element may itself be the bottom value without hiding the list's constructors. A partial list with a finite visible prefix followed by $\perp$ fails this condition. The distinction supports productivity proofs that inspect constructors without evaluating the stored elements.

A function is strict in an argument if replacing that argument by the bottom value makes the result bottom. This semantic property does not prescribe evaluation order: a function that always diverges is strict without inspecting its argument. Strictness of a structured argument also does not mean evaluation of every component.^[ref]