= Solution
An unfold expands a seed into either no node or a bucket and two new seeds:
``
unfoldTree :: (s -> Maybe (s,[a],s)) -> s -> Tree a
unfoldTree split seed =
case split seed of
Nothing -> Empty
Just (left,equal,right) ->
Node (unfoldTree split left) equal (unfoldTree split right)
toTreeUnfold :: Ord a => [a] -> Tree a
toTreeUnfold = unfoldTree split
where
split [] = Nothing
split (pivot:xs) =
let (lo,eq,hi) = partition3 pivot xs
in Just (lo,pivot:eq,hi)
``
The seed is the remaining <list>. Expanding a nonempty seed partitions it exactly as `toTree` does, and both child seeds are shorter. <Induction> establishes \b[`toTreeUnfold = toTree`] and <algorithm termination> on finite inputs. The unfold separates the local decomposition rule from the recursive construction of the tree.
Back to article page
