Types in RULES

[Roman Leshchinskiy]

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