Quantification in free theorems (Was: [Haskell-cafe] Exercise in point
free-style)
Janis Voigtlaender
voigt at tcs.inf.tu-dresden.de
Mon Sep 4 04:21:43 EDT 2006
ajb at spamcop.net wrote:
> G'day all.
>
> Quoting Donald Bruce Stewart <dons at cse.unsw.edu.au>:
>
>
>>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 at tcs.inf.tu-dresden.de
More information about the Haskell-Cafe
mailing list