Past exam of the year 1 of the computer science course of the University of Oxford / 2018 / Functional programming, design and analysis of algorithms / 3 / e / 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 $\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.