Proving a sorting operation in type system

I want to know how far a type system in a programming language can be beneficial. For example, I know that in a dependently typed programming language, we can create a Vector class incorporating size of the vector in the type signature. It is like a de-facto example. We can also write a function append using those signatures so that compiler proves resulting list's size will be the sum of the input lists.

Is there a way to encode, for example, in a sorting algorithm's type signature so that compiler guarantees resulting list to be a permutation of the input list? How this can be done, if it is possible?

Yes, it is possible to express a precise type for a sorting routine, such that any function having that type must indeed sort the input list.

While there might be a more advanced and elegant solution, I'll sketch an elementary one, only.

We will use a Coq-like notation. We start by defining a predicate requiring that f: nat -> nat acts as a permutation on $0..n-1$:

Definition permutation (n: nat) (f: nat -> nat): Prop :=
(* once restricted, its codomain is 0..n-1 *)
(forall m, m < n -> f m < n) /\
(* it is injective, hence surjective *)
(forall m1 m2, m1 < n -> m2 < n -> f m1 = f m2 -> m1 = m2) .

A simple lemma can easily be proved.

Lemma lem1: forall n f, permutation n f -> m < n -> f m < n.
... (* from the def *)

We define what is the $m$th element of a list having length $n$. This function requires a proof h stating that $m<n$ indeed holds.

Definition nth {A} {n} (l: list A n) m (h : m < n): A :=
... (* recursion over n *)

Given an ordering on A, we can express that a list is sorted:

Definition ordering (A: Type) :=
{ leq: A->A->bool |
(* axioms for ordering *)
(forall a, leq a a = true) /\
(forall a b c, leq a b = true -> leq b c = true -> leq a c = true) /\
(forall a b, leq a b = true -> leq b a = true -> a = b)
} .

Definition sorted {A} {n} (o: ordering A) (l: list A n): Prop :=
...

Finally here's the type for a sorting algorithm:

Definition mysort (A: Type) (o: ordering A) (n: nat) (l: list A n):
{s: list A n | sorted o s /\
exists f (p: permutation n f),
forall (m: nat) (h: m < n),
nth l m h = nth s (f m) (lem1 n f p h) } :=
... (* the sorting algorithm, and a certificate for its output *)

The output type states that the result list s is $n$ elements long, it is sorted, and that there's a permutation of $0..n-1$ that maps the elements in the input list l to the ones in the output list s. Note that we have to invoke the lemma above to prove $f(m) < n$, which is required by nth.

Note however that it is the user, i.e. the programmer, which has to prove their sorting algorithm correct. The compiler will not simply verify that the sorting is correct: all it does is checking a provided proof. Indeed, the compiler can not do much more than that: semantic properties such as "this program is a sorting algorithm" are undecidable (by Rice theorem), so we can not hope to make the proving step fully automatic.

In the far, far future, we can still hope that automatic theorem provers get so smart that "most" practically used algorithms can be automatically proved correct. The Rice theorem only states that this can not be done in all cases. All we can hope for is a correct, widely applicable, but inherently incomplete system.

As a final note, it is sometimes forgotten that even simple type systems are incomplete! E.g. even in Java

int f(int x) {
if (x+2 != 2+x)
return "Houston, we have a problem!";
return 42;
}

is semantically type safe (it always returns an integer), but the type checker will complain about the unreachable return.

Twan van Laarhoven has a nice fully worked out example in Agda of the "Correctness and runtime of mergesort, insertion sort and selection sort".

The comments are also interesting: in them, Bob Atkey's solution involving a deep embedding of Linear Logic is for instance mentioned.