Functional programming

A type constructor $M$ with operations $\mathrm{result}:A\to MA$ and $▹:MA\to (A\to MB)\to MB$ satisfying the monad laws. The first embeds a value; the second sequences a computation with a value-dependent continuation. This is the programming interface to a monad.

A computational monad for continuation-passing style. Result invokes the supplied continuation immediately; sequencing replaces it with a continuation that runs the next computation.

The computational monad whose result is the identity function and whose sequencing is ordinary application. It adds no effects and provides a starting point for a stack of monad transformers.

A computation represented by a function from an initial program state to a result and a final program state. Its sequencing passes each output program state to the next computation.

A construction taking a computational monad $M$ to another computational monad $TM$, normally with a lift from $MA$ to $TMA$. The order of monad transformers can affect which information survives an exception or a control transfer.

A continuation monad whose final answer is computed in a base computational monad. The answer type $R$ is fixed throughout a computation.

An unlabelled exception can be represented by an algebraic data type with successful and failed alternatives, sequenced inside a base computational monad. Sequencing skips the next computation after failure; a handler runs an alternative computation. The base effects already performed need not be undone.

A state monad layered over a base computational monad. An unsuccessful base computation may return no final program state; this matters when combining it with an exception monad transformer.

The left and right identity laws and the associativity law for a computational monad. They justify regrouping sequencing while preserving the order and multiplicity of effects.

A function taking another function as an argument or returning one as a result. Function composition, the map function and a list fold are standard examples.

Apply a function to each element of a collection while retaining its arrangement. On lists, map f [] = [] and map f (x:xs) = f x : map f xs. Its principal type in Haskell is (a -> b) -> [a] -> [b]. The element types may change independently; no equality test or ordering of elements is required.

A function together with the bindings of variables from its defining environment. A mutable captured variable makes successive calls stateful. Sharing such a closure between copied iterators can violate the promised independent enumeration even when their current values are copied separately.

A programming closure whose defining semantic environment contains a binding for that same programming closure. In a host with lazy evaluation, this can be represented by a recursive data definition without first running the function's body.

A family of programming closures sharing a semantic environment that binds every name in the family. Each body therefore sees every family member, including those whose definitions occur later in the source.

Keep exactly the elements of a list satisfying a predicate, preserving their relative order. A recursive step tests the head, prepending it to the filtered tail when it passes and otherwise returning that filtered tail alone. On a finite input, this uses one predicate evaluation per element; an infinite rejected tail cannot produce a next output under lazy evaluation.

Split a list into the subsequence satisfying a predicate and the subsequence failing it, preserving relative order in both. One recursive traversal computes the pair for the tail once, evaluates the head's predicate once and prepends the head to the appropriate component. A shared irrefutable pair binding preserves lazy access to either component. Fully consuming both finite outputs takes linear time in addition to predicate evaluation costs.

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.

For a predicate $p$, normalize the state to the first remaining passing element with seek = dropWhile (not . p). Stop on an empty state, otherwise emit its head and continue from seek (tail state). The invariant is that every nonempty state starts with a passing element. An initial seek establishes it; removing the emitted head and seeking again preserves it. Each rejected run is traversed once, giving linear time in the examined input prefix under constant-cost predicate tests.

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]

Return the successive accumulator values of a left fold, including the initial accumulator: scanl f e [] = [e] and scanl f e (x:xs) = e : scanl f (f e x) xs. The $k$th result is the fold of the first $k$ elements, proved by the fold equation. Thus the scan equals map (foldl f e) . inits, but computes $n$ updates instead of $n(n+1)/2$ on a finite input of length $n$. Accumulator strictness and the cost of an update remain separate from this operation count.

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.

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.

Expand a seed by a function returning either no node or a left seed, root label and right seed. Recursively expanding the two seeds produces a binary tree. A finite ascending list split about its midpoint supplies an unfold into a balanced binary tree that is a binary search tree.

A structural recursion replacing the empty binary tree by a value and a nonempty node by a combining function on its two folded children and root label. The result type may itself be a function type, allowing a fold to construct a membership predicate or a difference list rather than traversing all branches for every subsequent query.

More generally, choose one operation for each data constructor. For a leaf-labelled binary tree represented by One a | Two (Tree a) (Tree a), the tree fold instead has type signature (a -> b) -> (b -> b -> b) -> Tree a -> b: one operation handles the leaf label, and the other combines the two folded children. Replacing the operations by the original data constructors reconstructs the input, as structural induction proves.

A direct tree fold gives a parent operation only its children's folded summaries. If two different children have equal summaries, the parent cannot distinguish them. For a leaf-labelled binary tree, a function returning proper subtrees maps every leaf to []. A direct fold with precisely that result type would therefore map every two-leaf tree to the same result, despite their possibly different labels. This rules out that direct fold, while permitting a richer folded summary followed by projection.

Mutually dependent streams evaluated by lazy evaluation. A useful sufficient condition for productivity is that one participant emits its first constructor independently of any reply, while its $(j+1)$-st output depends only on the first $j$ replies. A scorer mapping each guess to a terminating response then lets each finite interaction prefix be constructed inductively. Inspecting the reply stream before emitting the first guess instead creates a circular demand.

For a finite nonempty collection of exact real multipliers greater than one, the multiplicative closure of one can be enumerated by a shared lazy list: emit one, then merge its elementwise multiples by all generators. Every value after one has a smaller predecessor obtained by removing one factor, proving productivity by increasing value. There are only finitely many exponent tuples below any fixed bound, because every generator is greater than one; thus locally finite sorted-stream merge eventually emits every generated value. Equal products are emitted once.

A multiplier below one contradicts increasing order starting at one. A multiplier equal to one adds no new values and should be removed from the recursive streams; an empty remaining generator collection has the finite closure consisting of one. These qualifications concern exact arithmetic: finite precision or overflow can violate the order and growth assumptions.

The Hamming number stream merges its shared multiples by two, three and five. To emit its first $n$ values, each of the fixed number of mapped streams and merge nodes advances at most $n+O(1)$ positions. With lazy evaluation that shares each evaluated list cell, this takes $\Theta (n)$ comparisons and fixed-factor multiplications. The statement counts arithmetic operations, rather than bits: the growing exact integers make their bit-operation costs larger. Recomputing independent copies of the recursively defined stream loses this sharing argument.

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 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.

For finite lists, if $x\oplus (y\otimes z)=(x\oplus y)\otimes z$ and $x\oplus a=a\otimes x$, then the right fold with step $\oplus$ and seed $a$ equals the left fold with step $\otimes$ and seed $a$. The two steps need not be identical. Equality of the resulting values does not imply equal time complexity; list concatenation is an important example.

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.

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.

If $f$ is strict, $f(a)=b$, and $f(g(x,y))=h(x,f(y))$, then $f\circ \mathrm{foldr}(g,a)=\mathrm{foldr}(h,b)$. The empty case uses the base image and the cons case uses compatibility followed by structural induction. Strictness handles a bottom-valued spine. For pure definable continuous functions, equality on finite partial lists extends to infinite lists by finite approximation. For finite total inputs alone, induction does not require the strictness hypothesis.

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]

A procedure whose result depends only on its explicit argument values and which has no observable side effects. For terminating calls with reusable results, this makes the value condition of the memoization cache contract particularly simple.

// Target: computer-science.bigb

Recursion following the constructors of a finite inductive datatype. Correctness is naturally proved by structural induction.

// Target: computer-science.bigb

For data Natural = Zero | Succ Natural, replace Zero by a base value and Succ by a step function: foldNat g a Zero = a and foldNat g a (Succ n) = g (foldNat g a n). On a finite total natural number $n$ this iterates $g$ exactly $n$ times.

Suppose $f$ is a strict function, $f(a)=b$ and $f\circ g=h\circ f$. The zero case of the asserted equation is the base identity; the successor case rewrites $f(g(z))$ as $h(f(z))$ and applies structural induction. At an undefined argument, the strict function premise makes both sides the bottom value. For pure definable Haskell functions, equality on finite partial approximations extends to infinite constructor chains by continuity in the information order. For finite total arguments alone, the zero and successor proof does not require strictness.