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