Re: Quantification in free theorems (Was: [Haskell-cafe] Exercise in point free-style)
G'day all. Quoting Janis Voigtlaender [EMAIL PROTECTED]: I find the omission of quantifications in the produced theorems problematic. I agree. Indeed, if you look at the source code, the quantifications _are_ generated, they're just not printed. The reason is that the output was (re-)designed for use on IRC where space is at a premium. However, you're correct that sometimes they're semantically important. Fixed. For this, you produce the following theorem: g x = h (f x) = $map f . filter g = filter h . $map f It now produces: filter (f . g) . $map f = $map f . filter g Cheers, Andrew Bromage ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Quantification in free theorems (Was: [Haskell-cafe] Exercise in point free-style)
[EMAIL PROTECTED] wrote: G'day all. Quoting Donald Bruce Stewart [EMAIL PROTECTED]: 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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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: [EMAIL PROTECTED] wrote: G'day all. Quoting Donald Bruce Stewart [EMAIL PROTECTED]: 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:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
