Solution (source code)

= Solution

A <three-way quicksort> can use a common partition helper so that the tree factorisation below makes the same key comparisons. The `compare` operation is assumed to be a terminating lawful total ordering on the supplied keys.
``
partition3 :: Ord a => a -> [a] -> ([a],[a],[a])
partition3 pivot = foldr step ([],[],[])
  where
    step x rest =
      let (lo,eq,hi) = rest
      in case compare x pivot of
           LT -> (x:lo,eq,hi)
           EQ -> (lo,x:eq,hi)
           GT -> (lo,eq,x:hi)

sort :: Ord a => [a] -> [a]
sort [] = []
sort (pivot:xs) =
  let (lo,eq,hi) = partition3 pivot xs
  in sort lo ++ (pivot:eq) ++ sort hi
``
Every non-pivot entry appears in exactly one partition, and the equal bucket contains the original pivot exactly once. The recursive sublists have length at most one less than the current finite input, so <recursion> terminates. <Induction> gives sorted recursive results with the original multiplicities; placing the equal bucket between them gives a sorted <permutation> of the input. There is no <recursive call> on the equal bucket, which avoids needless descent on repeated keys.