= Solution
For integer <linked lists>, compare their heads and copy the smaller head, retaining the other list for the next step:
``
fun merge ([], ys) = ys
| merge (xs, []) = xs
| merge (xs as x :: xt, ys as y :: yt) =
if x <= y then x :: merge (xt, ys)
else y :: merge (xs, yt);
``
This <merge algorithm> preserves duplicates and chooses the left list on a tie, making it stable when elements have an ordering key. Each recursive step decreases the combined length. For correctness, the chosen head is no greater than either remaining head and therefore no greater than any remaining element; <structural induction> then proves that the result is ordered and contains exactly the elements of both inputs. For other element types, replace the integer comparison by a supplied ordering function. \b[Merge repeatedly emits the smaller head and reuses the remaining list when the other becomes empty.]
Back to article page
