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:

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] *)

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] *)

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]

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