
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:
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