[Haskell-cafe] Re: [Haskell] pros and cons of static typing and
side effects ?
Lennart Augustsson
lennart at augustsson.net
Tue Aug 16 16:26:03 EDT 2005
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
More information about the Haskell-Cafe
mailing list