Types in RULES

[Simon Peyton-Jones]

| > 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)?

No, that's easily inferred, since to :: [a] -> 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'.
|
| Do we really need to distinguish them?

Yes I think so. Different name spaces etc.

| 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))

Well, we are explicitly quantifying over 'f' and 'x', so it'd be odd not to explicitly quantify over 'a', wouldn't it?

S