Functional Programming: A PragPub Anthology

Another Look at Sorting

We started off looking at the type of sort and now know enough to see what we can really do with dependent types.

     A:Type           n:Nat          v:Vec A n
     lteq:Sigma[f: A -> A -> Bool]is_ordering(f)
---------------------------------------------------------
sort A n lteq v : Sigma[w:Vec A n] is_permutation_of(v,w)
                                && is_sorted(w,lteq)

Don’t panic! Let’s take it piece by piece. As before, sorting is polymorphic, so we can use it on vectors of any element type. Input length can be anything, and the result contains a vector of the same length—in other words, length is preserved. We also have an argument, lteq, that supplies the information about comparing A values. And, as you may have guessed, this will be our less-than-or-equal ...