= Solution
The necessary domain is a finite, nonempty <list>: the datatype has no representation of an empty leaf sequence, and the supplied size-based balance condition does not specify an infinite-size construction.
``
build :: [a] -> Tree a
build [] = error "build: empty input"
build [x] = One x
build xs = Two (build ys) (build zs)
where
(ys,zs) = split (length xs `div` 2) xs
``
For length $n\ge2$, the two nonempty pieces have $\lfloor n/2\rfloor$ and $\lceil n/2\rceil$ elements. Their sizes differ by at most one, and both are shorter than the input. <Induction> therefore proves termination and the required <leaf-balanced binary tree> property at every node. The same <induction>, using `ys ++ zs = xs`, proves `flatten (build xs) = xs`. This straightforward implementation takes $O(n\log n)$ <running time>; computing the length repeatedly is acceptable here because no faster construction was requested.
Back to article page
