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