[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:[EMAIL PROTECTED]
| 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
|
|
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc
