Types in RULES

[Simon Peyton-Jones]

[Widening to cvs-ghc; read Roman's message below first.]

Roman

How annoying. You're right, it's impossible, because the 't' isn't mentioned in the type of 'f', or 'x'.

What would we like to write?  Perhaps something like

"myrule" forall (type t :: *->*) (f :: a->a) x.
     from (tmap f (to x :: t a)) = map f (from (to x :: t a))

We need a syntactic clue to distinguish the *type* binders in the forall from the *term* binders.  Saying "the signature mentions "*" seems a bit flaky to me.  My suggestion above is to re-use the keyword 'type'.

What do you think?  Manuel may have an opinion too.

Incidentally, once the rule is parsed and typechecked, the simplifier will have no trouble doing the right thing.

Simon


| -----Original Message-----
| From: Roman Leshchinskiy [mailto:rl at cse.unsw.edu.au]
| Sent: 15 September 2008 10:10
| To: Simon Peyton-Jones
| Subject: Types in RULES
|
| Simon,
|
| here's an example I came across while working on the recycling paper
| and which I subsequently forgot about. Suppose we have:
|
| {-# LANGUAGE Rank2Types #-}
| module T where
|
| class T t where
|    to   :: [a] -> t a
|    from :: t a -> [a]
|    tmap :: (a -> a) -> t a -> t a
|
| Now I'd like to add the following rule:
|
| {-# RULES
|
| "myrule" forall f x.
|      from (tmap f (to x)) = map f (from (to x))
|   #-}
|
| Alas, this fails with:
|
|      Ambiguous type variable `t' in the constraint:
|        `T t' arising from a use of `to' at T.hs:12:40-43
|      Probable fix: add a type signature that fixes these type
| variable(s)
|
| Of course, I'd like the t on the rhs to be the same as on the lhs but
| I don't see how to tell this to GHC. Is it actually possible? The only
| solution I've found was to add a dummy argument to 'to':
|
|      to' :: t a -> [a] -> t a
|
|      to = to' undefined
|
| {-# RULES
|
| "myrule" forall f t x.
|      from (tmap f (to' t x)) = map f (from (to' t x))
|   #-}
|
| That's ugly, of course. Am I missing something or is this just
| impossible to do with the current system?
|
| Roman
|
|