O'Reilly logo

Functional Programming: A PragPub Anthology by Michael Swaine

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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 ...

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required