RULES map (\x -> x) = id

[Simon Peyton-Jones]

|  So I wonder: Why is rule "map id2" not enough here?

Compile with -ddump-rules.  What you see is below.

* The rule "map id" actually has an LHS like this:
      myMap a (id a)
  where the (id a) is a type application.  It'll ONLY match a term that looks like
      myMap <ty> (id <ty>)
  where <ty> is some type.  It won't match  (myMap (\x.x))

* The rule "map id2" has an LHS like
     myMap a (\x.x)
   If we try to match that against the term (myMap a (id a)), will it match?
   Sadly, GHC *does* expand 'id', to the term is equivalent to
          myMap a ((/\b.\x:b.x) a)
   To make this match (\x:a.x) you'd have to do beta-reduction on the fly during
   matching, at least for type applications.

Conclusion.  Matching functions is bound to be hard.  You could try improving the matcher, which is in Rules.lhs, function 'match'.  Doing some kind of on the fly beta reduction might be worth a try.  

I hope this is helpful. I would be happy if someone felt like augmenting the Commentary to cover some of this information.  (I could review.)

Simon

"map id" [ALWAYS]
    forall (@ a{tv agb} [tv]).
      main:Rules.myMap{v r0} @ a{tv agb} [tv]
                             @ a{tv agb} [tv]
                             (base:GHC.Base.id{v r2s} [gid] @ a{tv agb} [tv])
      = base:GHC.Base.id{v r2s} [gid] @ [a{tv agb} [tv]]
"map id2" [ALWAYS]
    forall (@ a{tv ag3} [tv]).
      main:Rules.myMap{v r0} @ a{tv ag3} [tv]
                             @ a{tv ag3} [tv]
                             (\ (x{v aeP} [lid] :: a{tv ag3} [tv]) -> x{v aeP} [lid])
      = base:GHC.Base.id{v r2s} [gid] @ [a{tv ag3} [tv]]

|  -----Original Message-----
|  From: glasgow-haskell-users-bounces at haskell.org [mailto:glasgow-haskell-users-
|  bounces at haskell.org] On Behalf Of Joachim Breitner
|  Sent: 17 January 2013 10:24
|  To: glasgow-haskell-users at haskell.org
|  Subject: RULES map (\x -> x) = id
|  
|  Hi,
|  
|  I am experimenting with rewrite rules, but found that they do not fire as often as I
|  wanted them. Here is a small example:
|  
|          module MapId where
|  
|          myMap f [] = []
|          myMap f (x:xs) = f x : myMap f xs
|  
|          {-# RULES "map id" myMap id = id #-}
|          {-# RULES "map id2" myMap (\x -> x) = id #-}
|  
|          mapId = myMap id
|          mapIdApp x = myMap id x
|  
|          mapLamId = myMap (\x -> x)
|          mapLamIdApp x = myMap (\x -> x) x
|  
|  This works as expected, i.e. the latter four functions become some kind of identity.
|  But I am a bit surprised that I do need two rules to catch all cases, as I thought
|  that the simplifier „looks through“ definitions like "id". But when I remove the
|  "map id" rule, the functions "mapId"
|  and "mapIdApp" are not optimized.
|  
|  So I wonder: Why is rule "map id2" not enough here?
|  
|  Thanks,
|  Joachim
|  
|  
|  --
|  Joachim "nomeata" Breitner
|    mail at joachim-breitner.de  |  nomeata at debian.org  |  GPG: 0x4743206C
|    xmpp: nomeata at joachim-breitner.de | http://www.joachim-breitner.de/