Exercise in point free-style

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
20 messages Options
Reply | Threaded
Open this post in threaded view
|

Exercise in point free-style

Julien Oster
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
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

Neil Mitchell
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

Neil Mitchell
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

Bugzilla from robdockins@fastmail.fm
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

John Hughes-4
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

Udo Stenzel
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

Bulat Ziganshin-2
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

Julien Oster
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

Lennart Augustsson
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

Thomas Davie
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

Julien Oster
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

Donald Bruce Stewart
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

Donald Bruce Stewart
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

ajb@spamcop.net
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)

Janis Voigtlaender
[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)

Lennart Augustsson
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)

ajb@spamcop.net
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

Janis Voigtlaender
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

ajb@spamcop.net
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