= Solution
Carry the eventual output tail as an accumulator, thereby avoiding repeated <list concatenation>:
``
abs :: CatList a -> [a]
abs t = flatten t []
where
flatten Nil zs = zs
flatten (One x) zs = x : zs
flatten (Cat l r) zs = flatten l (flatten r zs)
``
The invariant is `flatten t zs = denotation t ++ zs`. It is immediate for `Nil` and `One`; at `Cat`, applying the two induction hypotheses and <associativity> of <list concatenation> proves it. In particular, the empty accumulator gives the required abstraction.
Each <concatenation tree> constructor is processed once, and each `One` emits one result cons. Consequently full production takes \b[$\Theta(m)$ time], where $m$ is the input constructor count, on every tree shape. This is a <difference list> calculation written with an explicit tail, an instance of <linear flattening of a binary tree>. The <call stack> can have depth $m$ for a badly skewed input; a linear time bound does not imply logarithmic stack space.
Back to article page
