Does GHC simplify RULES?

[Simon Peyton-Jones]

Josef,

Ah, I see.  I think you are trying to do something quite hard,
akin to higher-order matching, which is the kind of thing Oege's
MAG system does.  I'm copying him so he can confirm or deny.

In general, it is true that

	(\x. ...x...) E

might match (f E), for some expression E, where

	(...E...)

does not match.  But since the two are beta-convertible, it's hard
to ensure that the expression has the "right" form. Higher-order
matching is simply matching modulo beta, which means that it
wouldn't matter which form it's in.

GHC does not do HO matching; it is tricky and expensive, and
I think not suitable for a compiler.  You are trying to help GHC with
cunning crafting of your program, but as you observe it's all terribly
fragile. That's not GHC's fault --- it's just that hand-driving HO
matching
is a fragile process.

I have to say that I'm not very optimistic.  I doubt that moving=20
in the direction of switching off beta here and there would be a robust
solution.

Simon

| -----Original Message-----
| From: Josef Svenningsson [mailto:josefs@cs.chalmers.se]=20
| Sent: 25 February 2002 14:30
| To: Simon Peyton-Jones
| Cc: glasgow-haskell-users@haskell.org
| Subject: RE: Does GHC simplify RULES?
|=20
|=20
| On Mon, 25 Feb 2002, Simon Peyton-Jones wrote:
|=20
| >
| > | Suppose I have the following RULES pragma:
| > |
| > | {-# RULES
| > |   "foo" forall a . foo a =3D (\x -> bar x) a
| > | #-}
| > |
| > | Ok, it's stupid but I have examples where this is=20
| motivated, trust=20
| > | me.
| > |
| > | Now, it seems that GHC simplifies the rule because what I=20
| get when=20
| > | compiling it with -ddump-rules is the following rule:
| > |
| > | "foo" __forall {@ t_a2UD a :: t_a2UD}
| > | 	Test.foo @ t_a2UD a
| > | 	=3D Test.bar @ t_a2UD a ;
| > |
| > | It's \beta-reduced! Argh! Why is that?
| >
| > Because if it's left unsimplified, the first thing that will happen=20
| > after the rule fires is that the beta reduction will be=20
| done.  So why=20
| > not do it first?  (The desugarer can leave quite a lot of=20
| crud around,
| > so a gentle simplification is indeed run.)
| >
| > You'll need to explain your motivation a bit more.  Perhaps=20
| give the=20
| > rules you'd like along with a sample simplification sequence.
| >
| Alright. Some more motivation is probarbly justified here.=20
| This message is a bit lengthy. If you're not very interested=20
| in this I suggest you stop reading now.
|=20
| What I am really trying to do is trying to express the=20
| foldr/build rule without build. Intuitively this should be=20
| possible since build just sits a a tag on a function saying=20
| that it has the right type.
|=20
| Expressing the foldr/build-build (read: foldr build minus=20
| build) rule is
| easy:
|=20
| {-# RULES
|   "foldr fuse" forall c n (g :: forall b . (a -> b -> b) -> b -> b).
|    foldr c n (g (:) []) =3D g c n
| #-}
|=20
| Now, the problem is writing list producing functions so that=20
| they get the right type. Let's look at an example, our=20
| favourite function map. Suppose we have the following code snippet:
|=20
| foldr p z (map f xs)
|=20
| How do we write map so that the intermediate list is not=20
| built? We can define map in the following way:
|=20
| map f xs =3D mapFB f xs (:) []
|=20
| mapFB is a function where all the conses and nils are=20
| abstracted out. Now, we can arrange so that map gets inlined=20
| in the above example. So for the rule "foldr fuse" to apply=20
| mapFB must have the right type. Note that mapFB takes four=20
| arguments and g in the rule takes two. BUT, g takes a type=20
| argument before these two arguments because it is=20
| polymorphic. Therefore mapFB must also take a type argument=20
| in that position in order for the rule to apply. With this in=20
| mind we might try to give mapFB the following
| type:
|=20
| mapaux :: (a -> b) -> [a] -> (forall c. (b -> c -> c) -> c -> c)
|=20
| But GHC completely ignores our explicit forall quantifier and=20
| moves the quantification to the top level. Bummer!
|=20
| OK, so we want to force GHC to put a type lambda where we=20
| want to. My idea was then to have a rule that generates a=20
| piece of polymorphic code and insert some redundancy so that=20
| GHC would not understand that it could remove the type=20
| lambda. Here's what I tried:
|=20
| {-# RULES
|   "map" forall (f :: a -> b) xs .
|     map f xs =3D
|     ((\c n -> mapaux f xs c n) :: forall c . (a -> c -> c) ->=20
| c -> c) (:) [] #-}
|=20
| The idea is to fool GHC to insert a lambda before my explicit=20
| lambdas in the rhs of the rule. Then the "foldr fuse" rule=20
| whould fire on the example above. Or will it? It depends on=20
| how GHC does things and I'm not 100% sure. If GHC start=20
| simplifying something which just came out of an application=20
| of a rule then I guess this trick is really wasted. What I=20
| hoped for was this:
|=20
| foldr p z (map f xs) =3D{ Rule "map" }=3D>
| foldr p z ((\c n -> mapaux f xs c n) (:) []) =3D{ Rule "foldr=20
| fuse" }=3D> (\c n -> mapaux f xs c n) p z =3D{ \beta reduction=20
| }=3D> mapaux f xs p z
|=20
| In actual GHC the \beta reduction will probarbly happen=20
| before the second rule application. But I suppose I would=20
| have found that out if the rule was not simplified, now there=20
| was no way to tell.
|=20
| Ok, so maybe you guys have already though about removing=20
| build and decided against it. It might not be the most=20
| important problem in the world. But intuitively build is=20
| completely redundant and that really bugs me. That's why I've=20
| been playing around with this.
|=20
| Cheers,
|=20
| 	/Josef
|=20
|=20