#2110: Rules to eliminate casted id's
------------------------------+---------------------------------------------
Reporter: igloo | Owner:
Type: feature request | Status: new
Priority: normal | Milestone: 6.12 branch
Component: Compiler | Version: 6.8.2
Resolution: | Keywords:
Difficulty: Unknown | Os: Unknown/Multiple
Testcase: | Architecture: Unknown/Multiple
Failure: None/Unknown |
------------------------------+---------------------------------------------
Changes (by simonpj):
* cc: rl, dimit...@microsoft.com (added)
* failure: => None/Unknown
Comment:
The issue here is how to write the rule in source syntax. The internal
form is fine. Here's what it should look like in internal form, I think:
{{{
RULE "map/cast" forall (a::*) (b::*) (c::*)
(co :: (a->b ~ a->c))
(f::a->b)
map a c (f |> co) = map a b f |> [right co]
RULE "map/id" forall (a::*) map a a id = id
}}}
I've split the rule into two. One lifts out the cast, and one spots map-
of-identity. I think (but I have not tested) that these rules will work,
if only we could ''write'' them in the source program. We can write the
second but not the first.
This question is related to #2600, where we want to bind type variables in
rules. Here we want to bind equality constraints too, and we might want
to bind dictionaries too. How about this?
{{{
RULE "map/cast" forall type a b c. (a~b) =>
forall (f :: a->b).
map (f :: a->c) = map f :: [b]
}}}
Two things going on here:
* I've used two `forall`s. The first has just the same syntax as a type-
level `forall`, apart from the "`type`" keyword. It and binds type
variables and constraints. The second is the one we have right now in
RULES. Maybe we could omit the "`type`", but that might be hard to parse.
* I've used type signatures to force the casts to appear in the "right"
place. But this is a bit indirect.
Better suggestions on syntax welcome.
Simon
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2110#comment:5>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
Glasgow-haskell-bugs@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs