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] //

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]

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