Types in RULES
rl at cse.unsw.edu.au
Mon Sep 15 07:10:02 EDT 2008
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
More information about the Cvs-ghc