#2110: Rules to eliminate casted id's
---------------------------------+------------------------------------------
Reporter: igloo | Owner:
Type: feature request | Status: new
Priority: lowest | Milestone: 7.6.2
Component: Compiler | Version: 6.8.2
Keywords: | Os: Unknown/Multiple
Architecture: Unknown/Multiple | Failure: None/Unknown
Difficulty: Unknown | Testcase:
Blockedby: | Blocking:
Related: |
---------------------------------+------------------------------------------
Comment(by nomeata):
I wish I could edit my comments, at least for 10 minutes or so...
Anyways, I just noticed that I did not understand the ```right``` value
correctly. Shoudln’t that be something of type "(α ~ β) -> ([α] ~ [β])"?
Unless I am reading it wrongly, the typing rule Right in the TLDI'07 paper
goes the other way around. I guess I am expecting something like
{{{
{-# RULES "map/cast" forall f co. map (f `cast` co) = map f `cast` [] co
"map/id" map id = id
#-}
}}}
where ```[] :: (α ~ β) -> ([α] ~ [β])```. Not sure if that already exists,
though, and again Syntax problems pop up.
Or what if we free the programmer from worrying about coercions at all:
{-# RULES "map/cast" forall f co. map (casted f) = casted (map f)
"map/id" map id = id
#-}
On the LHS, ```casted x``` matches any ```x `cast` co```. On the right
hand side, ```casted y``` introduces a new coercion axiom and uses it.
This may be less safe, but then, rewrite rules are already very unsafe.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/2110#comment:22>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
