Example: Quick-Sort on Linear Lists

In this section, I give an implementation of quick-sort on linear lists. While list-based quick-sort may not be a preferred sorting method in practice, its implementation is nonetheless interesting. The interface for quick-sort is given as follows:

// fun{a:t@ype} quickSort{n:nat} (xs: list_vt (a, n), cmp: cmp a): list_vt (a, n) //

Like the implementation of mergeSort and insertionSort, the implementation of quickSort given as follows makes no use of memory allocation and deallocation.

The following code implements a function takeout_node_at that takes out a node from a linear list at a given position:

fun{a:t@ype} takeout_node_at {n:int}{k:nat | k < n} ( xs: &list_vt (a, n) >> list_vt (a, n-1), k: int(k) ) : list_vt_cons_pstruct (a, ptr?) = ( // if k > 0 then let val+@list_vt_cons (x, xs1) = xs val res = takeout_node_at<a> (xs1, k-1) prval () = fold@ (xs) in res end else let val+@list_vt_cons (x, xs1) = xs val nx = xs val () = xs := xs1 in $UNSAFE.castvwtp0 ((view@x, view@xs1 | nx)) // HX: this is a safe cast end // end of [if] // ) (* end of [takeout_node_at] *)

Assume that a data constructor named foo is associated with a dataviewtype. Then there is a corresponding viewtype construtor of the name foo_pstruct that takes n types to form a viewtype, where n is the arity of foo. For instance, there is a viewtype constructor list_vt_cons_pstruct that takes 2 types T1 and T2 to form a viewtype list_vt_cons_pstruct(T1, T2). This viewtype is for a list-node created by a call to list_vt_cons such that the two arguments of list_vt_cons are of types T1 and T2. Essentially, list_vt_cons_pstruct(T1, T2) stands for list_vt_cons_unfold(L0, L1, L2) for some addresses L0, L1 and L2 plus two views T1@L1 and T2@L2.

A key step in quick-sort lies in partitioning a linear list based on a given pivot. This step is fulfilled by the following code that implements a function template named partition:

fun{ a:t@ype } partition{n,r1,r2:nat} ( xs: list_vt (a, n), pvt: &a , r1: int(r1), res1: list_vt (a, r1), res2: list_vt (a, r2) , cmp: cmp (a) ) : [n1,n2:nat | n1+n2==n+r1+r2] (int(n1), list_vt (a, n1), list_vt (a, n2)) = ( case+ xs of | @list_vt_cons (x, xs_tail) => let val xs_tail_ = xs_tail val sgn = compare<a> (x, pvt, cmp) in if sgn <= 0 then let val r1 = r1 + 1 val () = xs_tail := res1 prval () = fold@ (xs) in partition<a> (xs_tail_, pvt, r1, xs, res2, cmp) end else let val () = xs_tail := res2 prval () = fold@ (xs) in partition<a> (xs_tail_, pvt, r1, res1, xs, cmp) end // end of [if] end (* end of [list_vt_cons] *) | ~list_vt_nil ((*void*)) => (r1, res1, res2) ) (* end of [partition] *)

The implementation of partition is tail-recursive. Given a linear list and a pivot, partition returns a tuple (r1, res1, res2) such that res1 contains every element in the list that is less than or equal to the pivot, res2 contains the rest, and r1 is the length of res1. The way in which the nodes of the given linear list are moved into res1 and res2 is quite an interesting aspect of this implementation.

By making use of takeout_node_at and partition, we can readily implement quickSort as follows:

implement {a}(*tmp*) quickSort (xs, cmp) = let // fun sort{n:nat} ( xs: list_vt (a, n), n: int n ) : list_vt (a, n) = ( if n > 10 then let val n2 = half (n) var xs = xs val nx = takeout_node_at<a> (xs, n2) val+list_vt_cons (pvt, nx_next) = nx val (n1, xs1, xs2) = partition<a> (xs, pvt, 0, list_vt_nil, list_vt_nil, cmp) val xs1 = sort (xs1, n1) val xs2 = sort (xs2, n - 1 - n1) val () = nx_next := xs2 prval () = fold@ (nx) in list_vt_append (xs1, nx) end else insertionSort<a> (xs, cmp) ) (* end of [sort] *) // in sort (xs, list_vt_length (xs)) end // end of [quickSort]

Note that the pivot for each round is taken from the middle of the list being sorted, which can be time-consuming as taking out a node from the middle of a list is O(n)-time. This issue can be addressed by always choosing the first element to be the pivot. However, doing so can often lead to degenerated O(n^2)-time performance of quick-sort in practice.

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