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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
