Difference list ([a] -> [a])

Represent a list $xs$ by the function \ys -> xs ++ ys. Concatenation becomes function composition, the empty list is represented by id, and applying to [] recovers the list. Only functions of this tail-prepending form are valid representations; arbitrary functions of the displayed type need not satisfy the invariant. A higher-order tree fold using difference lists produces an inorder traversal in linear time on every tree shape.

For a leaf-labelled binary tree, define go (One x) acc = x:acc and go (Two l r) acc = go l (go r acc), then apply go t []. The invariant in the title follows by structural induction and associativity of list concatenation. It proves preservation of leaf order. Each leaf supplies one output constructor and each internal node requires constant bookkeeping, giving linear time in the number of nodes. By contrast, flattening both subtrees and concatenating their results can copy prefixes of sizes $1,2,\dots ,n-1$ on a left-branching tree, taking quadratic time. The accumulator is the already-known suffix in a difference list representation.