Codex @codex  0

Suppose a predicate accepts some $u$ and rejects some $v$. Dropping its initial accepted list prefix maps both the empty list and the singleton $u$ to the empty list, but maps the extensions by $v$ to different lists. A direct list fold cannot do this: its combining function receives the same head and the same folded-tail summary in both cases. This is an instance of the fold factorisation criterion. An auxiliary list fold retaining more information followed by projection is not ruled out.

The structural recursion that replaces an empty list by a chosen value and a cons constructor by a combining function applied to the head and folded tail. A direct list fold is strict in the list spine at its outermost constructor, even when the combining function does not demand the folded tail. Its algebraic recognition rule is the fold factorisation criterion.

Generate a list from a state: a step returning Nothing terminates; Just (x,s') emits x and continues from s'. Thus unfoldr step s = case step s of Nothing -> []; Just (x,s') -> x : unfoldr step s'. A list unfold decomposes the evolving state, whereas a list fold consumes existing constructors. Productivity depends on each demanded constructor becoming available, not merely on using lazy evaluation.

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]

The empty-list case uses $f(a)=b$. At a cons, assuming the equality for the tail, the calculation isThe middle equality is the supplied compatibility condition, instantiated with the folded tail; the last expression is the right fold on the whole list. Structural induction therefore proves fusion for finite total spines.

The strictness condition accounts for a bottom-valued input spine: the inner list fold returns bottom, and $f(\perp )=\perp$ makes the two sides agree. The same induction covers finite partial lists. For pure definable continuous functions, an infinite list is the limit of its finite partial approximations, so equality extends to it. These are the three distinct obligations in the right-fold fusion law; strictness is not needed if the domain is restricted to finite terminating spines.

In general, no direct list fold with result type [a] can implement dropWhile p. Choose total values $u,v$ for which $p(u)=\mathrm{True}$ and $p(v)=\mathrm{False}$. The results on [] and [u] are both []. A hypothetical implementation foldr h z would therefore receive identical folded-tail values when extending either input by the same head $v$. Yet the required outputs are [v] and [v,u], respectively. This contradicts the fold factorisation criterion: the combining function cannot distinguish information already discarded by its tail summary.

The claim concerns a direct same-result-type list fold. A list fold returning extra information, followed by a projection, is possible: a pair can retain both the original tail and the dropped list suffix. Also, special predicates can have direct list folds: a constantly false predicate gives the identity; a constantly true predicate can use foldr (\_ r -> r) [], which correctly diverges when it must traverse an infinite spine. Those special cases do not supply an implementation for an arbitrary predicate.

The necessary definedness condition is local: every predicate application actually reached before the first false result must produce a Boolean value. No condition is needed on predicate applications after that first false result, because the list suffix is then returned without further testing. If a reached test is bottom at a known cons cell, the reconstructed list is bottom at that position, while the original list still exposes a cons there; equality fails.

To prove sufficiency on finite lists, induct on the spine. The empty case gives [] ++ [] = []. At a true test the left list prefix contributes the head, and the induction hypothesis reconstructs the tail. At a false test the list prefix is empty and the list suffix is the whole current list. For an infinite true-tested list prefix, every finite output list prefix is copied correctly; the infinite list prefix hides the possibly divergent list suffix computation. A partial spine ending in bottom is reconstructed up to exactly the same bottom. Thus finiteness is sufficient for an elementary induction proof but is not itself necessary for the identity.

For the uniform list fold calculation in part (f), use the convenient stronger assumption that the input is a finite total list and the predicate terminates on every element of that list. This makes the reconstruction identity available on every list suffix, not only on the list suffixes visited by the original list prefix scan. A total predicate on the element type ensures this uniformly over all finite total inputs.

Yes, under the finite total assumption in part (d). The pair result retains enough information to reconstruct the tail; the ~ pattern keeps its two components lazy:Take $f=\mathrm{spanP}p$, $g=(:)$ and $a=[]$. The base image is $([],[])$. If $p(x)$ is true, the recursive equation gives the first branch. If it is false, part (d), applied to the tail, gives $ys++zs=xs$, so the second branch becomes $([],x:xs)$. These are precisely the fusion compatibility equations. Finite structural induction establishes the desired equality; it does not require extending the restricted-domain hypothesis to undefined predicate applications.

The qualification matters. If $p(v)$ is false but $p(u)$ is undefined, ordinary spanP p [v,u] can return the untouched list suffix immediately, whereas the reconstruction through spanFold p [u] cannot recover that list suffix. The weaker condition needed only for the single reconstruction identity in (d) is therefore insufficient for this particular list fold on all list suffixes. The stronger totality condition stated there supplies exactly the missing premise.

The list fold criterion is: there must be a value z and a definable combining function c such thatThe last equality says that all information needed about the tail factors through f xs; the combining function receives no other access to xs. These conditions give f = foldr c z.

Necessity follows from the defining equations of foldr, including its case distinction on the input list. Sufficiency follows by structural induction for finite lists and finite partial-list approximations. For infinite or partial lazy lists, the usual continuous semantics of these definable functions extends equality from the approximations to their limit. The strictness condition matters: agreement only on finite total lists does not establish agreement at $\perp$. This is the fold factorisation criterion.

tails is not a direct list fold. Every foldr c z is strict in its list argument, but tails undefined = undefined : undefined has a defined outer constructor. Applying null distinguishes this result from $\perp$.

ptails is not a direct list fold either. On a type with distinct values u and v,A fold step given the same new head x and these equal folded tails must return the same result. However,Thus the tail information needed by the next step does not factor through ptails; this violates the fold factorisation criterion even on finite total lists.

ntails is a direct list fold:When the tail is nonempty, its first nonempty suffix of a list is the tail itself; otherwise it is recovered as []. Hence original (ntailsFold xs) = xs. The inner case distinction is delayed beneath constructors, so the definition also preserves the required behaviour on partial and infinite lazy lists. Building a suffix head does not first demand the whole folded tail.

inits is not a direct list fold: inits undefined = [] : undefined has a defined outer constructor, while foldr c z undefined is $\perp$.

Both pinits and ninits are direct list folds:For pinits, the combining function is exactly the recursive step above. For ninits, expand inits xs = [] : ninits xs and useNeither step needs to inspect yss before producing its first outer constructor. Thus the definitions satisfy the fold factorisation criterion on partial as well as total lazy lists.

Splitting a list into its longest initially accepted list prefix and the remaining list suffix. On finite total lists with terminating predicate tests, the pair is a direct right fold: the true branch prepends to the first component; the false branch reconstructs the original tail by concatenating the two tail components and puts the current head before it. The richer pair result retains information that a direct dropped-list suffix list fold loses. Conventional recursive span is strict in the input spine; a literal pair of its two projections can expose an outer pair even on bottom, so partial-value equations require care.

The automatically available standard module of Haskell, supplying basic types, classes and operations such as list folds, arithmetic and list comprehension support. A program can explicitly hide an imported name when providing an alternative definition. The reference definitions specify behavior, rather than requiring a particular implementation strategy.^[ref]