# Exercise in point free-style

 Classic List Threaded
20 messages
Reply | Threaded
Open this post in threaded view
|

## 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Exercise in point free-style

 In reply to this post by Julien Oster 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Exercise in point free-style

 In reply to this post by Julien Oster 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Exercise in point free-style

 In reply to this post by Julien Oster > From: Julien Oster <[hidden email]> > Subject: [Haskell-cafe] Exercise in point free-style > > 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 Oh, YES!! Two ways to remove l: func3a f = uncurry ((.map f).(++)) . pair func3b f = uncurry (flip (++).map f) . pair And just to make sure they're right: propab new f l =   func3 f l == new f l   where types = f :: Int->Int quickCheck (propab func3a) quickCheck (propab func3b) If you don't mind swapping the arguments, then propc f l =   func3 f l == func3c l f   where types = f :: Int->Int func3c l = (l++) . (`map` l) With the arguments swapped, you can even remove both! propd f l =   func3 f l == func3d l f   where types = f :: Int -> Int func3d = uncurry ((.(flip map)) . (.) . (++)) . pair MUCH clearer! The trick is to observe that l is duplicated, so you need to use a combinator that duplicates something. The only one available here is pair, which you then have to combine with uncurry. It would be nicer to have (f &&& g) x = (f x,g x) available. (&&& is one of the arrow combinators). Then you could remove l by func3e f = uncurry (++) . (id &&& map f) which is sort of readable, and remove both by func3f = (uncurry (++).) . (id &&&) . map John _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Exercise in point free-style

 In reply to this post by Julien Oster 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. _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe signature.asc (196 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

## Re[2]: 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,  Bulat                            mailto:[hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Exercise in point free-style

 In reply to this post by Udo Stenzel 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Re: Exercise in point free-style

 In reply to this post by John Hughes-4 An easy way to solve this is to ask lambdabot.  Log on to the Haskell   IRC channel: lennart: @pl  \ f l -> l ++ map f l lambdabot: ap (++) . map Notice how it's much shorter than the Hughes' solution. :)         -- Lennart On Sep 1, 2006, at 13:11 , John Hughes wrote: >> From: Julien Oster <[hidden email]> >> Subject: [Haskell-cafe] Exercise in point free-style >> >> 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 > > Oh, YES!! > > Two ways to remove l: > > func3a f = uncurry ((.map f).(++)) . pair > func3b f = uncurry (flip (++).map f) . pair > > And just to make sure they're right: > > propab new f l = >  func3 f l == new f l >  where types = f :: Int->Int > > quickCheck (propab func3a) > quickCheck (propab func3b) > > If you don't mind swapping the arguments, then > > propc f l = >  func3 f l == func3c l f >  where types = f :: Int->Int > > func3c l = (l++) . (`map` l) > > With the arguments swapped, you can even remove both! > > propd f l = >  func3 f l == func3d l f >  where types = f :: Int -> Int > > func3d = uncurry ((.(flip map)) . (.) . (++)) . pair > > MUCH clearer! > > The trick is to observe that l is duplicated, so you need to use a   > combinator that duplicates something. The only one available here   > is pair, which you then have to combine with uncurry. > > It would be nicer to have > > (f &&& g) x = (f x,g x) > > available. (&&& is one of the arrow combinators). Then you could   > remove l by > > func3e f = uncurry (++) . (id &&& map f) > > which is sort of readable, and remove both by > > func3f = (uncurry (++).) . (id &&&) . map > > John > > > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Re: Exercise in point free-style

 Shorter, although perhaps less insightful. Bob On 2 Sep 2006, at 01:36, Lennart Augustsson wrote: > An easy way to solve this is to ask lambdabot.  Log on to the   > Haskell IRC channel: > lennart: @pl  \ f l -> l ++ map f l > lambdabot: ap (++) . map > > Notice how it's much shorter than the Hughes' solution. :) > > -- Lennart > > On Sep 1, 2006, at 13:11 , John Hughes wrote: > >>> From: Julien Oster <[hidden email]> >>> Subject: [Haskell-cafe] Exercise in point free-style >>> >>> 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 >> >> Oh, YES!! >> >> Two ways to remove l: >> >> func3a f = uncurry ((.map f).(++)) . pair >> func3b f = uncurry (flip (++).map f) . pair >> >> And just to make sure they're right: >> >> propab new f l = >>  func3 f l == new f l >>  where types = f :: Int->Int >> >> quickCheck (propab func3a) >> quickCheck (propab func3b) >> >> If you don't mind swapping the arguments, then >> >> propc f l = >>  func3 f l == func3c l f >>  where types = f :: Int->Int >> >> func3c l = (l++) . (`map` l) >> >> With the arguments swapped, you can even remove both! >> >> propd f l = >>  func3 f l == func3d l f >>  where types = f :: Int -> Int >> >> func3d = uncurry ((.(flip map)) . (.) . (++)) . pair >> >> MUCH clearer! >> >> The trick is to observe that l is duplicated, so you need to use a   >> combinator that duplicates something. The only one available here   >> is pair, which you then have to combine with uncurry. >> >> It would be nicer to have >> >> (f &&& g) x = (f x,g x) >> >> available. (&&& is one of the arrow combinators). Then you could   >> remove l by >> >> func3e f = uncurry (++) . (id &&& map f) >> >> which is sort of readable, and remove both by >> >> func3f = (uncurry (++).) . (id &&&) . map >> >> John >> >> >> _______________________________________________ >> Haskell-Cafe mailing list >> [hidden email] >> http://www.haskell.org/mailman/listinfo/haskell-cafe> > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Exercise in point free-style

 In reply to this post by Julien Oster 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Exercise in point free-style

 In reply to this post by Julien Oster 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Exercise in point free-style

 In reply to this post by Julien Oster 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Exercise in point free-style

 In reply to this post by Donald Bruce Stewart G'day all. Quoting Donald Bruce Stewart <[hidden email]>: > 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Quantification in free theorems (Was: Exercise in point free-style)

 [hidden email] wrote: > G'day all. > > Quoting Donald Bruce Stewart <[hidden email]>: > > >>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:[hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Quantification in free theorems (Was: 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: > [hidden email] wrote: >> G'day all. >> Quoting Donald Bruce Stewart <[hidden email]>: >>> 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:[hidden email] > _______________________________________________ > Haskell-Cafe mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-cafe_______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Quantification in free theorems (Was: Exercise in point free-style)

 In reply to this post by Janis Voigtlaender G'day all. Quoting Janis Voigtlaender <[hidden email]>: > 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Quantification in free theorems

 Hello all, [hidden email] wrote: >>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 ... which is also wrong. Consider the following:    f = const False    g = id Then, with the standard filter function:      filter (f . g) (map f [True])    = []   /= [False]    = map f (filter g [True]) Maybe it is just an accidental swapping of the arguments to (.) in your implementation. For if one would swap all such arguments above, one would get:    \$map f . filter (g . f) = filter g . \$map f which would be correct. 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. That wouldn't really be a mix of the two systems, however, because they follow different strategies for output. This can be seen, for example, for the following type:    zip :: [a] -> [b] -> [(a, b)] Here, Andrew's system now produces:    (forall x y. ( f (\$fst x) = \$fst y                   &&                   g (\$snd x) = \$snd y                 )                =>                 h x = y)    =>    \$map h (zip xs ys) = zip (\$map f xs) (\$map g ys) Whereas Sascha's system produces (minus top level quantifiers):    (zip x1 x2, zip (map h1 x1) (map h2 x2)) in    lift_{[]}(lift_{(2)}(h1, h2))    lift_{[]}(lift_{(2)}(h1, h2))    = {([], [])}    u {(x : xs, y : ys) | ((x, y) in lift_{(2)}(h1, h2))                          /\ ((xs, ys) in lift_{[]}(lift_{(2)}(h1, h2)))}    lift_{(2)}(h1, h2)    = {((x1, x2), (y1, y2)) | (h1 x1 = y1) /\ (h2 x2 = y2)} 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. Also, some of Andrew's tricks for making the output look more pointfree would not work when producing the more general "relational" free theorem (prior to the specialization to functions), which is also supported in Sascha's system. Ciao, Janis. -- Dr. Janis Voigtlaender http://wwwtcs.inf.tu-dresden.de/~voigt/mailto:[hidden email] _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

## Re: Quantification in free theorems

 G'day all. Quoting Janis Voigtlaender <[hidden email]>: > 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 _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe