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

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.

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:

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

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:

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@tcs.inf.tu-dresden.de

G'day all. Quoting Janis Voigtlaender :

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

G'day all. Quoting Janis Voigtlaender :

Maybe it is just an accidental swapping of the arguments to (.) in your implementation.

That was it, yes. Thanks for debugging my code for me. :-) (For those keeping score, it was actually the incorrect unzipping of a zipper data structure. If only I could scrap my boilerplate...)

Regarding Lennart's suggestion: I am pretty sure that it would be easy to adapt Sascha's system to omit top level quantifiers. All that should be needed would be an extra pass prior to prettyprinting, to strip off any outermost quantifiers from the data type representing free theorems.

In my case, the approach taken was to pass a Bool around the pretty printer which says whether or not to include quantifiers. (It's okay to strip quantifiers off the right-hand side of an implication if it's okay to strip quantifiers off the implication itself.)

The latter approach has advantages when it comes to producing free theorems that are faithful to the presence of _|_ and general recursion in Haskell, which is not supported by Andrew's system, as far as I can see.

That's correct. Once again, different design criteria apply. IRC has anti-flooding rules which encourage brevity rather than full-featuredness. Cheers, Andrew Bromage