[Haskell-cafe] Generating arbitrary function in QuickCheck

[Janis Voigtlaender]

Jason Dagit wrote:
> On Mon, Apr 6, 2009 at 10:09 PM, Eugene Kirpichov <ekirpichov at gmail.com> 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 at tcs.inf.tu-dresden.de