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

Keean Schupke k.schupke at imperial.ac.uk
Tue Aug 16 17:23:28 EDT 2005

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.


More information about the Haskell-Cafe mailing list