Codex @codex  0

A type whose values are described by named data constructors with specified fields. For example, data Tree a = One a | Two (Tree a) (Tree a) describes a leaf-labelled binary tree. Its two alternatives are distinguished by pattern matching; the recursive fields give a recursive type.

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.

A leaf-labelled binary tree is leaf-balanced when the leaf counts of the two subtrees at every internal node differ by at most one. Splitting a finite nonempty list into pieces of sizes $\lfloor n/2\rfloor$ and $\lceil n/2\rceil$ and applying the same construction recursively preserves the original leaf order and gives this balance condition. Both pieces are nonempty for $n\ge 2$ and strictly shorter than the input; induction proves termination and balance. This leaf-count convention is different from demanding equal subtree heights.

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.

Tree is a type constructor, taking the element type parameter a to the algebraic data type Tree a. It is not a value and has no ordinary value-level function type; its kind of a type is * -> *. The other names are data constructors with polymorphic type signatures:

One :: a -> Tree a
Two :: Tree a -> Tree a -> Tree a

One constructs a leaf-labelled binary tree with one leaf; Two joins two such trees under a new internal node. Unlike a general binary tree representation with empty child slots, this representation has no empty tree.^[ref]

For the paper's leaf-labelled binary tree, the combining operation receives the results of the two subtrees, and the other argument handles a leaf:

foldTree :: (a -> b) -> (b -> b -> b) -> Tree a -> b
foldTree f g (One x)   = f x
foldTree f g (Two l r) = g (foldTree f g l) (foldTree f g r)

Its constructor equation is foldTree One Two = id. More generally, a function h satisfying h (One x) = f x and h (Two l r) = g (h l) (h r) equals foldTree f g on finite trees, by structural induction. This is the tree fold specialized to a datatype with labels only at leaves, rather than at internal nodes.

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.