On 15/09/2008, at 21:16, 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)?
No, that's easily inferred, since to :: [a] -> t a
Right, it's either f *or* x that need a signature (to bind a) but not
both.
| > 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.
We could look at how the variable is used in the rest of the rule. Or
is that ambiguous?
| 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?
We need to quantify over local term variables to distinguish them from
ones bound on the top level. This problem doesn't arise with type
variables so they might be treated differently here. That is, unless
the rule is local to a let or where (is that even supported?) and
ScopedTypeVariables is on.
Anyway, whatever is easiest to implement is fine with me. I guess it's
'type'.
Roman
_______________________________________________
Cvs-ghc mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/cvs-ghc
