Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2021/functional-programming-design-and-analysis-of-algorithms-resit/4/g/solution

Merge by comparing the present heads and consuming just the chosen one. The implementation uses only the functional representation:
merge' :: Ord a => List a -> List a -> List a
merge' left right
  | null' left  = right
  | null' right = left
  | head' left <= head' right =
      cons' (head' left) (merge' (tail' left) right)
  | otherwise =
      cons' (head' right) (merge' left (tail' right))

mergeSort' :: Ord a => List a -> List a
mergeSort' input =
  let n = length' input
      middle = n `div` 2
  in if n <= 1 then input
     else merge' (mergeSort' (take' middle input))
                 (mergeSort' (drop' middle input))
The two recursive inputs are the disjoint initial and final portions of the represented sequence; they preserve every occurrence and have smaller lengths when . In merge', the smaller current head can precede every remaining value in both sorted inputs. Selecting the left head on equality preserves stability. Each merge step reduces the total number of remaining elements, and induction proves a sorted permutation of the original sequence.
This establishes algorithm termination and correctness on total finite representations, not an unconditional implementation bound. Nested index functions can make queries costly, and repeatedly finding lengths or heads may revisit them. The familiar merge-sort bound assumes suitable constant-time access or consumption primitives; the source's function-only representation supplies no such cost guarantee.

New to topics? Read the docs here!