RE: Does GHC simplify RULES?
| 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.
Simon
___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
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
___
Glasgow-haskell-users mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
RE: Does GHC simplify RULES?
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:[EMAIL PROTECTED]]
| Sent: 25 February 2002 14:30
| To: Simon Peyton-Jones
| Cc: [EMAIL PROTECTED]
| 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
