Types in RULES
Manuel M T Chakravarty
chak at cse.unsw.edu.au
Mon Sep 15 20:42:11 EDT 2008
> [Widening to cvs-ghc; read Roman's message below first.]
> How annoying. You're right, it's impossible, because the 't' isn't
> mentioned in the type of 'f', or 'x'.
> 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))
> 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'.
> What do you think? Manuel may have an opinion too.
I agree. That seems to be the best option.
More information about the Cvs-ghc