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 on a left-branching tree, taking quadratic time. The accumulator is the already-known suffix in a difference list representation.
List concatenation 2026-10-24
Append the second list after the first. For a finite left list of length , consuming the concatenation costs to copy its spine and can share the second argument. Repeatedly appending large left lists can cause quadratic time complexity; difference lists make concatenation into function composition.
Let be the number of leaves; the total number of nodes is . List concatenation copies its left operand. For a tree whose left subtree contains leaves at each successive internal node, these copied lengths are . Their sum is , so the worst-case running time is .
A difference list representation avoids copying prefixes:
flattenFast :: Tree a -> [a]
flattenFast t = go t []
  where
    go (One x)   acc = x:acc
    go (Two l r) acc = go l (go r acc)
The recursion invariant is go t acc = flatten t ++ acc. The leaf case is immediate; the internal-node case uses associativity of list concatenation. Each node is visited once and each leaf contributes one output constructor, giving running time when the result is fully consumed. This is linear flattening of a binary tree and does not assume balance.
The direct tree fold for an inorder traversal is
flattenFold :: Tree a -> [a]
flattenFold = foldTree (\ls x rs -> ls ++ (x:rs)) []
By structural induction, the child lists are ascending; the binary search tree property places every left value below the root and every right value above it. The displayed list concatenation therefore gives an ascending list containing every stored value exactly once.
For a version with linear time complexity on every tree shape, use an accumulator:
flatten :: Tree a -> [a]
flatten t = onto t []
  where
    onto Empty zs = zs
    onto (Tree l x r) zs = onto l (x : onto r zs)
This also has a higher-order tree fold expression using difference lists:
flattenLinear :: Tree a -> [a]
flattenLinear t =
  foldTree (\l x r -> l . (x:) . r) id t []
Its folded value is a function that prepends the inorder traversal to a supplied tail. The accumulator invariant is onto t zs = flattenFold t ++ zs. Each node contributes one constructor, giving time to consume the output. By contrast, the direct list-valued fold can take on a left-skewed tree because ++ repeatedly copies left traversals.
Tree fold 2026-10-24
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.