#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

Reply via email to