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

[Keean Schupke]

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.