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

Lennart Augustsson lennart at augustsson.net
Mon Sep 4 10:06:31 EDT 2006


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 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
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe



More information about the Haskell-Cafe mailing list