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 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] | Sent: 25 February 2002 14:30 | To: Simon Peyton-Jones | Cc: glasgow-haskell-users@haskell.org | Subject: RE: Does GHC simplify RULES? | | | 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 | |