Does GHC simplify RULES?

[Josef Svenningsson]

On Mon, 25 Feb 2002, Simon Peyton-Jones wrote:

>
> | Suppose I have the following RULES pragma:
> |
> | {-# RULES
> |   "foo" forall a . foo a = (\x -> bar x) a
> | #-}
> |
> | Ok, it's stupid but I have examples where this is motivated, trust me.
> |
> | Now, it seems that GHC simplifies the rule because what I get
> | when compiling it with -ddump-rules is the following rule:
> |
> | "foo" __forall {@ t_a2UD a :: t_a2UD}
> | 	Test.foo @ t_a2UD a
> | 	= 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
> after
> the rule fires is that the beta reduction will be done.  So why not
> do it first?  (The desugarer can leave quite a lot of crud around,
> so a gentle simplification is indeed run.)
>
> You'll need to explain your motivation a bit more.  Perhaps give
> the rules you'd like along with a sample simplification sequence.
>
Alright. Some more motivation is probarbly justified here. This message is
a bit lengthy. If you're not very interested in this I suggest you stop
reading now.

What I am really trying to do is trying to express the foldr/build rule
without build. Intuitively this should be possible since build just sits a
a tag on a function saying that it has the right type.

Expressing the foldr/build-build (read: foldr build minus build) rule is
easy:

{-# RULES
  "foldr fuse" forall c n (g :: forall b . (a -> b -> b) -> b -> b).
   foldr c n (g (:) []) = g c n
#-}

Now, the problem is writing list producing functions so that they get the
right type. Let's look at an example, our favourite function map. Suppose
we have the following code snippet:

foldr p z (map f xs)

How do we write map so that the intermediate list is not built? We can
define map in the following way:

map f xs = mapFB f xs (:) []

mapFB is a function where all the conses and nils are abstracted out. Now,
we can arrange so that map gets inlined in the above example. So for the
rule "foldr fuse" to apply mapFB must have the right type. Note that mapFB
takes four arguments and g in the rule takes two. BUT, g takes a type
argument before these two arguments because it is polymorphic. Therefore
mapFB must also take a type argument in that position in order for the
rule to apply. With this in mind we might try to give mapFB the following
type:

mapaux :: (a -> b) -> [a] -> (forall c. (b -> c -> c) -> c -> c)

But GHC completely ignores our explicit forall quantifier and moves the
quantification to the top level. Bummer!

OK, so we want to force GHC to put a type lambda where we want to. My idea
was then to have a rule that generates a piece of polymorphic code and
insert some redundancy so that GHC would not understand that it could
remove the type lambda. Here's what I tried:

{-# RULES
  "map" forall (f :: a -> b) xs .
    map f xs =
    ((\c n -> mapaux f xs c n) :: forall c . (a -> c -> c) -> c -> c) (:) []
#-}

The idea is to fool GHC to insert a lambda before my explicit lambdas in
the rhs of the rule. Then the "foldr fuse" rule whould fire on the
example above. Or will it? It depends on how GHC does things and I'm not
100% sure. If GHC start simplifying something which just came out of an
application of a rule then I guess this trick is really wasted. What I
hoped for was this:

foldr p z (map f xs) ={ Rule "map" }=>
foldr p z ((\c n -> mapaux f xs c n) (:) []) ={ Rule "foldr fuse" }=>
(\c n -> mapaux f xs c n) p z ={ \beta reduction }=>
mapaux f xs p z

In actual GHC the \beta reduction will probarbly happen before the second
rule application. But I suppose I would have found that out if the rule
was not simplified, now there was no way to tell.

Ok, so maybe you guys have already though about removing build and decided
against it. It might not be the most important problem in the world. But
intuitively build is completely redundant and that really bugs me. That's
why I've been playing around with this.

Cheers,

	/Josef