
Jason Dagit wrote:
On Mon, Apr 6, 2009 at 10:09 PM, Eugene Kirpichov
wrote: Since the argument to sortBy must impose a linear ordering on its arguments, and any linear ordering may as well be generated by assigning an integer to each element of type 'a', and your sorting function is polymorphic, from the free theorem for the sorting function we may deduce that it suffices to test your function on integer lists with a casual comparison function (Data.Ord.compare), and there is no need to generate a random comparison function.
Interesting. How is this free theorem stated for the sorting function? Intuitively I understand that if the type is polymorphic, then it seems reasonable to just pick one type and go with it.
You can try free theorems here: http://linux.tcs.inf.tu-dresden.de/~voigt/ft/ For example, for sort :: Ord a => [a] -> [a] it generates the following: forall t1,t2 in TYPES(Ord), f :: t1 -> t2, f respects Ord. forall x :: [t1]. map f (sort x) = sort (map f x) where: f respects Ord if f respects Eq and forall x :: t1. forall y :: t1. compare x y = compare (f x) (f y) forall x :: t1. forall y :: t1. (<) x y = (<) (f x) (f y) forall x :: t1. forall y :: t1. (<=) x y = (<=) (f x) (f y) forall x :: t1. forall y :: t1. (>) x y = (>) (f x) (f y) forall x :: t1. forall y :: t1. (>=) x y = (>=) (f x) (f y) f respects Eq if forall x :: t1. forall y :: t1. (==) x y = (==) (f x) (f y) forall x :: t1. forall y :: t1. (/=) x y = (/=) (f x) (f y) Assuming that all the comparison functions relate to each other in the mathematically sensible way, the latter can be reduced to: f respects Ord if forall x :: t1. forall y :: t1. (x <= y) = (f x <= f y) For sortBy you would get a similar free theorem. To see how the free theorem allows you to switch from an arbitrary type to just integers, set t2=Int and simply use f to build a order-preserving bijection between elements in the list x and a prefix of [1,2,3,4,...] Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de