On 15/09/2008, at 20:05, Simon Peyton-Jones wrote:
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))
Regardless of the syntax, I suspect x will have to be given a type as
well here, as in
(x :: 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'.
Do we really need to distinguish them? If so, reusing 'type' sounds
good. Could it perhaps be possible to treat explicit signatures on
the lhs of a rule as pattern signatures which can introduce new type
variables? This would allow the much simpler
forall f x. from (tmap f (to x :: t a)) = map f (from (to x :: t a))
In any case, I don't think the actual syntax is particularly important
as long as it's backwards compatible. It's not a very frequent problem
anyway.
Roman
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc