(*
 * This example shows that sorting a list using
 * quickSort yields a list of the same length
 *)

(* 2 type annotations, whcih occupy 3 lines *)

fun('a)
    quickSort cmp [] = []
  | quickSort cmp (x::xs) = par cmp (x, [], [], xs)
where quickSort <| {n:nat} ('a * 'a -> bool) -> 'a list(n) -> 'a list(n)

and('a)
    par cmp (x, left, right, xs) =
    case xs of
	[] => (quickSort cmp left) @ (x :: (quickSort cmp right))
      | y::ys =>
	    if cmp(y, x) then par cmp (x, y::left, right, ys)
	    else par cmp (x, left, y::right, ys)
where par <|
 {p:nat,q:nat,r:nat}
 ('a * 'a -> bool) -> 'a * 'a list(p) * 'a list(q) * 'a list(r) -> 'a list(p+q+r+1)