Types in RULES
simonpj at microsoft.com
Mon Sep 15 07:16:09 EDT 2008
| > 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?
More information about the Cvs-ghc