Example: Mergesort on Linear Lists

When mergesort is employed to sort an array of elements, it requires additional memory proportionate to the size of the array in order to move the elements around, which is considered a significant weakness of mergesort. However, mergesort does not have this requirement when it operates on a linear list. I present as follows an implementation of mergesort on linear lists that can readily rival its counterpart in C in terms of time-efficiency as well as memory-efficiency. The invariants captured in this implementation and the easiness to capture them should provide strong evidence to ATS being a programming language capable of enforcing great precision in practical programming.

First, let us introduce a type definition and an interface for a function template (for comparing elements in a list to be sorted):

typedef cmp (a:t@ype) = (&a, &a) -> int

extern
fun{a:t@ype} compare (x: &a, y: &a, cmp: cmp (a)): int

The interface for mergesort is given as follows:

extern
fun{a:t@ype}
mergesort {n:nat}
  (xs: list_vt (a, n), cmp: cmp a): list_vt (a, n)
// end of [mergesort]

The first argument of mergesort is a linear list (to be sorted) and the second one a function for comparing the elements in the linear list. Clearly, the interface of mergesort indicates that mergesort consumes its first argument and then returns a linear list that is of same length as its first argument. As is to become clear, the returned linear list is constructed with the nodes of the consumed one. In particular, the implementation of mergesort given here does not involve any memory allocation or deallocation.

The function template for merging two sorted lists into one is given as follows:

fun{a:t@ype}
merge // tail-rec
  {m,n:nat} .<m+n>. (
  xs: list_vt (a, m)
, ys: list_vt (a, n)
, res: &List_vt(a)? >> list_vt (a, m+n)
, cmp: cmp a
) : void =
  case+ xs of
  | list_vt_cons (!p_x, !p_xs1) => (
    case+ ys of
    | list_vt_cons (!p_y, !p_ys1) => let
        val sgn = compare<a> (!p_x, !p_y, cmp)
      in
        if sgn <= 0 then let // stable sorting
          val () = res := xs
          val xs1 = !p_xs1
          val () = fold@ (ys)
          val () = merge (xs1, ys, !p_xs1, cmp)
        in
          fold@ (res)
        end else let
          val () = res := ys
          val ys1 = !p_ys1
          val () = fold@ (xs)
          val () = merge (xs, ys1, !p_ys1, cmp)
        in
          fold@ (res)
        end // end of [if]
      end (* end of [list_vt_cons] *)
    | ~list_vt_nil () => (fold@ (xs); res := xs)
    ) // end of [list_vt_cons]
  | ~list_vt_nil () => (res := ys)
// end of [merge]

Unlike the one given in a previous functional implementation, this implementation of merge is tail-recursive and thus is guaranteed to be translated into a loop in C by the ATS compiler. This means that the concern of merge being unable to handle very long lists (e.g., containg 1 million elements) due to potential stack overflow is completely eliminated.

The next function template is for splitting a given linear lists into two:

fun{a:t@ype}
split {n,k:nat | k <= n} .<n-k>. (
  xs: &list_vt (a, n) >> list_vt (a, n-k), nk: int (n-k)
) : list_vt (a, k) =
  if nk > 0 then let
    val+ list_vt_cons (_, !p_xs1) = xs
    val res = split (!p_xs1, nk-1); val () = fold@ (xs)
  in
    res
  end else let
    val res = xs; val () = xs := list_vt_nil () in res
  end // end of [if]
// end of [split]

Note that the implementation of split is also tail-recursive.

The following function template msort takes a linear list, its length and a comparsion function, and it returns a sorted version of the given linear list:

fun{a:t@ype}
msort {n:nat} .<n>. (
  xs: list_vt (a, n), n: int n, cmp: cmp(a)
) : list_vt (a, n) =
  if n >= 2 then let
    val n2 = n / 2
    val n3 = n - n2
    var xs = xs // a left-value for [xs]
    val ys = split {n,n/2} (xs(*cbr*), n3) // xs: call-by-ref
    val xs = msort (xs, n3, cmp)
    val ys = msort (ys, n2, cmp)
    var res: List_vt (a)
    val () = merge (xs, ys, res(*cbr*), cmp) // xs: call-by-ref
  in
    res
  end else xs
// end of [msort]

The second argument of msort is passed so that the length of the list being sorted does not have to be computed directly by traversing the list when each recursive call to msort is made.

Finally, mergesort can be implemented with a call to msort:

implement{a}
mergesort (xs, cmp) = msort (xs, length (xs), cmp)

Please find the entire code in this section plus some additional code for testing on-line.