[Haskell-cafe] Generating arbitrary function in QuickCheck
Janis Voigtlaender
voigt at tcs.inf.tu-dresden.de
Tue Apr 7 02:19:23 EDT 2009
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
More information about the Haskell-Cafe
mailing list