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

Reply via email to