[Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?

[Lennart Augustsson]

Keean Schupke wrote:
> Other things we can do ... with dependant types we can ask the compiler 
> to prove the correctness of sorting algorithms. If we define an ordered 
> list tgo be one where each element must be larger than the preceding one:
> 
>    data OrderedIntList = Cons (a::Int) (l::OrderedList) | Nil {- where a 
> <= head l -}
>    data IntList = [Int]
> 
> We can now define our sorting function:
> 
>    quicksort :: IntList -> OrderedIntList
> 
> By this we are asking the compiler to prove (by induction) that the 
> function provided can only result in
> correctly ordered lists - irrespective of what arguments it is given (ie 
> proved true for any input)... This would have to be done symbolically 
> but is not beyond what can be achieved using logic programming.

But the output being ordered is not enough.  The output should also
be a permutation of the input.  This can, of course, be expressed
in a similar way.

	-- Lennart