Introduction to Programming in ATS:
PrevChapter 10. Datatype RefinementNext

Example: Mergesort on Lists (Redux)

I have previously presented an implementation of mergesort on lists that are formed with the constructors list0_nil and list0_cons. In this section, I give an implementation of mergesort on lists formed with the constructors list_nil and list_cons. This implementation is based on the same algorithm as the previous one but it assigns a type to the implemented sorting function that guarantees the function to be length-preserving, that is, the function always returns a list of the same length as the list it sorts.

The following defined function merge combines two ordered list (according to a given ordering) into a single ordered list: 

//
typedef lte (a:t@ype) = (a, a) -> bool
//
fun{
a:t@ype
} merge
  {m,n:nat} .<m+n>.
(
  xs0: list(a, m), ys0: list(a, n), lte: lte a
) : list(a, m+n) =
  case+ xs0 of
  | list_nil() => ys0
  | list_cons(x, xs1) =>
    (
    case+ ys0 of
    | list_nil() => xs0
    | list_cons(y, ys1) =>
        if x \lte y
          then list_cons(x, merge (xs1, ys0, lte))
          else list_cons(y, merge (xs0, ys1, lte))
        // end of [if]
    ) // end of [list_cons]
// end of [merge]
//

Clearly, the type assigned to merge indicates that the function returns a list whose length equals the sum of the lengths of the two input lists. Note that a termination metric is present for verifying that merge is a terminating function.

The following defined function mergesort mergesorts a list according to a given ordering: 

fun{
a:t@ype
} mergesort{n:nat}
(
  xs: list(a, n), lte: lte a
) : list(a, n) = let
//
  fun msort
    {n:nat} .<n,n>.
  (
    xs: list(a, n), n: int n, lte: lte a
  ) : list(a, n) =
    if n >= 2
      then split(xs, n, lte, half(n), list_nil) else xs
    // end of [if]
  // end of [msort]
  and split
    {n:int | n >= 2}{i:nat | i <= n/2} .<n,i>.
  (
    xs: list(a, n-n/2+i)
  , n: int(n), lte: lte a, i: int(i), xsf: list(a, n/2-i)
  ) : list(a, n) =
    if i > 0 then let
      val+list_cons(x, xs) = xs
    in
      split(xs, n, lte, i-1, list_cons(x, xsf))
    end else let
      val n2 = half(n)
      val xsf = list_reverse<a>(xsf) // make sorting stable!
      val xsf = list_of_list_vt(xsf) // linear list -> nonlinear list
      val xsf = msort(xsf, n2, lte) and xs = msort (xs, n-n2, lte)
    in
      merge(xsf, xs, lte)
    end // end of [if]
  // end of [split]
//
in
  msort(xs, list_length<a>(xs), lte)
end // end of [mergesort]

The type assigned to mergesort indicates that mergesort returns a list of the same length as its input list. The two inner functions msort and split are defined mutually recursively, and the termination metrics for them are pairs of natural numbers that are compared according to the standard lexicographic ordering on integer sequences. The type assigned to msort clearly indicates that its integer argument is required to be the length of its list argument, and a mismatch between the two surely results in a type-error. The type assigned to split is particularly informative, depicting a relation between the arguments and the return value of the function that can be of great help for someone trying to understand the code. The function list_reverse returns a linear list that is the reverse of its input, and the cast function list_of_list_vt turns a linear list into a nonlinear one (while incuring no cost at run-time). I will explain what linear lists are elsewhere.

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

PrevHomeNext
Example: Function Templates on Lists (Redux)UpSequentiality of Pattern Matching