Thanks for all replies! these gave me many enlightenments.
I have been looking in about free theorem for a while, and I want to
try to describe what I learned, and please collect me where I am wrong
or misunderstood.
Generating random functions for sortBy is meaningless, because, for
testing sortBy, casual comparison function is enough to it. The reason
of this comes from free theorem. By the free theorem, sortBy should
satisfy this theorem (copied from ftshell).
forall t1,t2 in TYPES, f :: t1 -> t2.
forall p :: t1 -> t1 -> Ordering.
forall q :: t2 -> t2 -> Ordering.
(forall x :: t1. p x = q (f x) . f)
==> (map f . sortBy p = sortBy q . map f)
Any linear orderings can be defined by mapping value to Integer. And
above theorem says comparing functions in the theorem must be
homomorphic to each other. Hence comparing function is meaningful only
when it is homomorhpic to Integer's that. (I have not tried to
Generate such function yet, and it may be unnecessary, but) taking
such function is easy.
Furthermore, it should be satisfied by all functions that have same
type signitures to sortBy, because it is implied from only its own
type.
Reference:
- [Theorem for free!](http://citeseerx.ist.psu.edu/viewdoc/summary?
doi=10.1.1.38.9875)
- [ftshell](http://hackage.haskell.org/cgi-bin/hackage-scripts/
package/ftshell-0.3)
Thanks,
Yusaku Hashimoto
On 2009/04/07, at 15:19, Janis Voigtlaender wrote:
Jason Dagit wrote:
On Mon, Apr 6, 2009 at 10:09 PM, Eugene Kirpichov
<[email protected]> 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:[email protected]
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
