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
Re: [Haskell-cafe] Exercise in point free-style
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/ 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
Re[2]: [Haskell-cafe] Exercise in point free-style
Hello Udo, Friday, September 1, 2006, 10:14:44 PM, you wrote: The general process is called lambda elimination and can be done mechanically. Ask Goole for Unlambda, the not-quite-serious programming language; since it's missing the lambda, afaik, FP proposed by Backus was serious lambda-missing programming language :) -- Best regards, Bulatmailto:[EMAIL PROTECTED] ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Exercise in point free-style
Hello, I was just doing Exercise 7.1 of Hal Daumé's very good Yet Another Haskell Tutorial. It consists of 5 short functions which are to be converted into point-free style (if possible). It's insightful and after some thinking I've been able to come up with solutions that make me understand things better. But I'm having problems with one of the functions: func3 f l = l ++ map f l Looks pretty clear and simple. However, I can't come up with a solution. Is it even possible to remove one of the variables, f or l? If so, how? Thanks, Julien ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exercise in point free-style
Julien Oster wrote: But I'm having problems with one of the functions: func3 f l = l ++ map f l While we're at it: The best thing I could come up for func2 f g l = filter f (map g l) is func2p f g = (filter f) . (map g) Which isn't exactly point-_free_. Is it possible to reduce that further? Thanks, Julien ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exercise in point free-style
Hi Julien, func3 f l = l ++ map f l func3 f = ap (++) (map f) func3 = ap (++) . map Looks pretty clear and simple. However, I can't come up with a solution. Is it even possible to remove one of the variables, f or l? If so, how? I have no idea how to do this - the solution is to log into #haskell irc and fire off @pl - which automatically converts things to point free form. I'm not sure if its possible to do without the auxiliary ap (which is defined in Monad). Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exercise in point free-style
Hi func2 f g l = filter f (map g l) is func2p f g = (filter f) . (map g) func2 = (. map) . (.) . filter Again, how anyone can come up with a solution like this, is entirely beyond me... Thanks Neil ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exercise in point free-style
On Friday 01 September 2006 11:44, Neil Mitchell wrote: Hi func2 f g l = filter f (map g l) is func2p f g = (filter f) . (map g) func2 = (. map) . (.) . filter Again, how anyone can come up with a solution like this, is entirely beyond me... To answer part of the OP's question, it's always possible to rewrite a lambda term using point-free style (using a surprisingly small set of basic combinators). The price you pay is that the new term is often quite a bit larger than the old term. Rewriting complicated lambda terms as point-free terms is often of, em, dubious value. OTOH, it can be interesting for understanding arrows, which are a lot like monads in points-free style (from what little experience I have with them). BTW, the process of rewriting can be entirely automated. I assume the lambdabot is using one of the well-known algorithms, probably tweaked a bit. Goolge combinatory logic or Turner's combinators if you're curious. Thanks Neil -- Rob Dockins Talk softly and drive a Sherman tank. Laugh hard, it's a long way to the bank. -- TMBG ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exercise in point free-style
Julien Oster wrote: While we're at it: The best thing I could come up for func2 f g l = filter f (map g l) is func2p f g = (filter f) . (map g) Which isn't exactly point-_free_. Is it possible to reduce that further? Sure it is: func2 f g l = filter f (map g l) func2 f g = (filter f) . (map g)-- definition of (.) func2 f g = ((.) (filter f)) (map g)-- desugaring func2 f = ((.) (filter f)) . map-- definition of (.) func2 f = flip (.) map ((.) (filter f)) -- desugaring, def. of flip func2 = flip (.) map . (.) . filter -- def. of (.), twice func2 = (. map) . (.) . filter -- add back some sugar The general process is called lambda elimination and can be done mechanically. Ask Goole for Unlambda, the not-quite-serious programming language; since it's missing the lambda, its manual explains lambda elimination in some detail. I think, all that's needed is flip, (.) and liftM2. Udo. -- I'm not prejudiced, I hate everyone equally. signature.asc Description: Digital signature ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exercise in point free-style
Udo Stenzel wrote: Thank you all a lot for helping me, it's amazing how quickly I received these detailed answers! func2 f g l = filter f (map g l) func2 f g = (filter f) . (map g) -- definition of (.) func2 f g = ((.) (filter f)) (map g) -- desugaring func2 f = ((.) (filter f)) . map -- definition of (.) func2 f = flip (.) map ((.) (filter f)) -- desugaring, def. of flip func2 = flip (.) map . (.) . filter -- def. of (.), twice func2 = (. map) . (.) . filter-- add back some sugar Aaaah. After learning from Neil's answer and from @pl that (.) is just another infix function, too (well, what else should it be, but it wasn't clear to me) I still wasn't able to come up with that solution without hurting my brain. The desugaring was the bit that was missing. Thanks, I will keep that in mind for other infix functions as well. I tried to work it out on paper again, without looking at your posting while doing it. I did almost the same thing, however, I did not use flip. Instead the last few steps read: = ((.) (filter f)) . map g l = (.)((.) . filter f)(map) g l -- desugaring = (.map)((.) . filter f) g l -- sweeten up = (.map) . (.) . filter g l -- definition of (.) I guess that's possible as well? The general process is called lambda elimination and can be done mechanically. Ask Goole for Unlambda, the not-quite-serious programming language; since it's missing the lambda, its manual explains lambda elimination in some detail. I think, all that's needed is flip, (.) and liftM2. Will do, thank you! Cheers, Julien ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exercise in point free-style
Julien Oster wrote: = ((.) (filter f)) . map g l = (.)((.) . filter f)(map) g l -- desugaring = (.map)((.) . filter f) g l -- sweeten up = (.map) . (.) . filter g l-- definition of (.) By the way, I think from now on, when doing point-free-ifying, my philosophy will be: If it involves composing a composition, don't do it. I just think that this really messes up readability. Cheers, Julien ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exercise in point free-style
haskell: Hello, I was just doing Exercise 7.1 of Hal Daum?'s very good Yet Another Haskell Tutorial. It consists of 5 short functions which are to be converted into point-free style (if possible). It's insightful and after some thinking I've been able to come up with solutions that make me understand things better. But I'm having problems with one of the functions: func3 f l = l ++ map f l Looks pretty clear and simple. However, I can't come up with a solution. Is it even possible to remove one of the variables, f or l? If so, how? The solution is to install lambdabot ;) Point free refactoring: lambdabot pl func3 f l = l ++ map f l func3 = ap (++) . map Find the type: lambdabot type ap (++) . map forall b. (b - b) - [b] - [b] Get some free theorems: lambdabot free f :: (b - b) - [b] - [b] f . g = h . f = map f . f g = f h . map f :) -- Don ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Exercise in point free-style
haskell: Julien Oster wrote: But I'm having problems with one of the functions: func3 f l = l ++ map f l While we're at it: The best thing I could come up for func2 f g l = filter f (map g l) is func2p f g = (filter f) . (map g) Which isn't exactly point-_free_. Is it possible to reduce that further? Similarly: lambdabot pl func2 f g l = filter f (map g l) func2 = (. map) . (.) . filter :) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
