Lennart Augustsson wrote:
Keean Schupke wrote:
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.
Yes, the easiest way would be to constrain the output list to be a subset of the input list, and vice-versa... something like: quicksort :: (x::IntList) -> (y::OrderedIntList) {- where x :< y && x :> y -} of course you would have to use the correct definition of subset - you really want to treat the list as a multi-set. Keean.