Re: Quantification in free theorems (Was: [Haskell-cafe] Exercise in point free-style)

I'd like to see a mix of the two systems. Top level quantifiers should be optional; they often don't improve readability. -- Lennart On Sep 4, 2006, at 04:21 , Janis Voigtlaender wrote:

ajb@spamcop.net wrote:

...

G'day all. Quoting Donald Bruce Stewart :

...

Get some free theorems: lambdabot> free f :: (b -> b) -> [b] -> [b] f . g = h . f => map f . f g = f h . map f I finally got around to fixing the name clash bug. It now reports: g . h = k . g => map g . f h = f k . map g Get your free theorems from: http://andrew.bromage.org/darcs/freetheorems/

I find the omission of quantifications in the produced theorems problematic. It certainly makes the output more readable in some cases, as in the example above. But consider the following type:

filter :: (a -> Bool) -> [a] -> [a]

For this, you produce the following theorem:

g x = h (f x) => $map f . filter g = filter h . $map f

Lacking any information about the scope of free variables, the only reasonable assumption is that they are all implicitly forall- quantified at the outermost level (as for types in Haskell). But then the above theorem is wrong. Consider:

g = const False x = 0 h = even f = (+1)

Clearly, for these choices the precondition g x = h (f x) is fulfilled, since (const False) 0 = False = even ((+1) 0). But the conclusion is not fulfilled, because with Haskell's standard filter-function we have, for example:

map f (filter g [1]) = [] /= [2] = filter h (map f [1])

The correct free theorem, as produced by the online tool at

http://haskell.as9x.info/ft.html

(and after renaming variables to agree with your output) is as follows:

forall T1,T2 in TYPES. forall f :: T1 -> T2. forall g :: T1 -> Bool. forall h :: T2 -> Bool. (forall x :: T1. g x = h (f x)) ==> forall xs :: [T1]. map f (filter g xs) = filter h (map f xs)

The essential difference is, of course, that the x is (and must be) locally quantified here, not globally. That is not reflected in the other version above.

Ciao, Janis.

-- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/ mailto:voigt@tcs.inf.tu-dresden.de _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe