Introduction to Programming in ATS:
Prev	Chapter 15. Dataviewtypes as Linear Datatypes	Next

Example: Insertion Sort on Linear Lists

I present a standard implementation of insertion sort on linear lists in this section. The interface for insertion sort is given as follows:

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

Like mergeSort, insertionSort is implemented in a manner that makes no use of memory allocation or deallocation. Given a linear list, insertionSort essentially shuffles the nodes in the list to form a sorted list.

The following code implements a function insord that inserts a given list-node into a sorted linear list to form another sorted linear list:

fun{
a:t@ype
} insord
  {l0,l1,l2:addr}{n:nat}
(
  pf1: a @ l1
, pf2: list_vt (a, 0)? @ l2
| xs0: &list_vt (a, n) >> list_vt (a, n+1)
, nx0: list_vt_cons_unfold (l0, l1, l2), p1: ptr (l1), p2: ptr (l2)
, cmp: cmp (a)
) : void =
(
  case+ xs0 of
  | @list_vt_cons
      (x0, xs1) => let
      val sgn = compare<a> (x0, !p1, cmp)
    in
      if sgn <= 0 // HX: for stableness: [<=] instead of [<]
        then let
          val () = insord<a> (pf1, pf2 | xs1, nx0, p1, p2, cmp)
          prval () = fold@ (xs0)
        in
          // nothing
        end // end of [then]
        else let
          prval () = fold@ (xs0)
          val () = (!p2 := xs0; xs0 := nx0)
          prval () = fold@ (xs0)
        in
          // nothing
        end // end of [else]
      // end of [if]
    end // end of [list_vt_cons]
  | ~list_vt_nil () =>
    {
      val () = xs0 := nx0
      val () = !p2 := list_vt_nil ()
      prval () = fold@ (xs0)
    }
) (* end of [insord] *)

The implementation of insord is tail-recursive. The type assigned to insord indicates that the argument xs0 of insord is call-by-reference. If xs0 stores a list of length n when insord is called, then it stores a list of length n+1 when insord returns. The arguments nx0, p1 and p2 are call-by-value, and they should be bound to a list-node and the first and second fields in the list-node, respectively, when a call to insord initiates. The proof arguments pf1 and pf2 are needed so that the pointers bound to p1 and p2 can be accessed and updated.

The function template insertionSort can now be readily implemented based insord:

implement{a}
insertionSort
  (xs, cmp) = let
//
fun loop{m,n:nat}
(
  xs: list_vt (a, m)
, ys: &list_vt (a, n) >> list_vt (a, m+n)
, cmp: cmp (a)
) : void =
  case+ xs of
  | @list_vt_cons
      (x, xs1) => let
      val xs1_ = xs1
      val ((*void*)) =
        insord<a> (view@x, view@xs1 | ys, xs, addr@x, addr@xs1, cmp)
      // end of [va]
    in
      loop (xs1_, ys, cmp)
    end // end of [list_vt_cons]
  | ~list_vt_nil ((*void*)) => ()
//
var ys = list_vt_nil{a}()
val () = loop (xs, ys, cmp)
//
in
  ys
end // end of [insertionSort]

Clearly, this implementation of insertionSort is tail-recursive. While insertion sort is of O(n^2)-time complexity, it is often more efficient than merge-sort or quick-sort when sorting very short lists. For instance, we may implement msort (which is called by mergeSort) as follows by taking advantage of the efficiency of insertionSort on short lists:

fun{
a:t@ype
} msort{n:nat} .<n>.
(
  xs: list_vt (a, n)
, n: int n, cmp: cmp(a)
) : list_vt (a, n) = let
//
// cutoff is selected to be 10
//
in
  if n > 10 then let
    val n2 = half(n)
    val n3 = n - n2
    var xs = xs // lvalue for [xs]
    val ys = split<a> (xs, n3)
    val xs = msort<a> (xs, n3, cmp)
    val ys = msort<a> (ys, n2, cmp)
    var res: List_vt (a) // uninitialized
    val () = merge<a> (xs, ys, res(*cbr*), cmp)
  in
    res
  end else insertionSort<a> (xs, cmp)
end // end of [msort]

Note that the stableness of mergeSort is maintained as insertionSort also performs stable sorting.

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

Prev	Home	Next
Example: Merge-Sort on Linear Lists	Up	Example: Quick-Sort on Linear Lists