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 functional programming language with parametric polymorphism and lazy evaluation. The code examples here use the Haskell 2010 Language Report specification.

A list reduction carrying an accumulator from left to right: foldl s z [] = z and foldl s z (x:xs) = foldl s (s z x) xs. In a lazy language this does not by itself force each intermediate accumulator; its association and evaluation strictness are separate issues. An infinite input spine prevents this operation from returning a result.^[ref]

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]

Include nonpositive counts and exhausted input explicitly:

take :: Int -> [a] -> [a]
take n _      | n <= 0 = []
take _ []             = []
take n (x:xs)         = x : take (n-1) xs

drop :: Int -> [a] -> [a]
drop n xs     | n <= 0 = xs
drop _ []             = []
drop n (_:xs)         = drop (n-1) xs

The tests on the count precede inspection of the input list. Thus take 0 undefined = [], while drop 0 undefined = undefined, exactly as these list prefix and list suffix operations require. No element value is inspected merely to traverse the spine.^[ref]

No universally correct sequential Haskell implementation has that guarantee for partial lists. Compare undefined paired with [v], and [v] paired with undefined, where the element type is arbitrary. A generic program cannot fabricate v; it must eventually inspect an input spine to obtain it. Whichever input it first demands can be chosen to be the undefined one, blocking access to the available element in the other input.

In particular, the implementation in part b can emit a defined prefix and then block when alternation reaches an undefined tail. Lazy evaluation postpones demands; it cannot recognize that a demanded computation will never finish. The result is the partial-list interleaving obstruction, not an objection to fairness under the proper-input hypothesis. Additional concurrent primitives would change the computational model.^[ref]

For the finite total inputs just specified, a recursive implementation isAt a true test, the head belongs to the list prefix and splitting continues on the tail; at a false test, the complete remaining list is the list suffix. Induction proves that the first projection is the longest accepted list prefix and the second projection is the remaining list suffix.

There is a small partial-value distinction behind the paper's displayed pair identity. The conventional recursive span is strict in an entirely undefined list, whereas the literal expression (takeWhile p undefined, dropWhile p undefined) exposes an outer pair with two undefined components. The equality as a pair therefore needs the stated defined-input convention, or an interpretation that compares the two projections. This does not affect the finite total answers here.^[ref]

The ordering operations used to decide the partitions require an Ord a constraint. A function with parametric polymorphism and type [a] -> [a] cannot inspect arbitrary element values to decide which one is smaller; for example, functions themselves need not admit the comparison operations required by this sorting algorithm. A Haskell Ord class instance supplies the comparison method, with its ordering laws a separate semantic assumption.^[ref]

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]

A call can instead produce an entire run and recurse on the unused input:Here span returns the longest matching prefix of a list and the remaining suffix of a list. Thus x:ys is the first maximal run, while zs begins the next run or is empty. Each recursive call produces one outer output element. The lazy pair binding permits output of the first constructor before the run's endpoint is known. Every finite input position is scanned a bounded number of times, so the time complexity is $\Theta (n)$ for unit-cost equality, including output construction.^[ref]

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.

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]

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]