Merge sort

module Main

%default total

%hide merge
%hide sort

merge : Ord a => List a -> List a -> List a
merge Nil b = b
merge a Nil = a
merge (a :: as) (b :: bs) =
  if a < b then a :: merge as (b :: bs)
           else b :: merge (a :: as) bs

sort : Ord a => List a -> List a
sort Nil = Nil
sort [x] = [x]
sort xs = assert_total $
  let n = length xs `div` 2 in
  sort (take n xs) `merge` sort (drop n xs)

main : IO ()
main = do
  printLn $ sort (the (List Nat) [])
  printLn $ sort [1]
  printLn $ sort [1, 2, 3, 4]
  printLn $ sort [5, 2, 8, 6]
  printLn $ sort [8, 2, 5, 6, 6, 5, 4]