| > 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 _______________________________________________ Cvs-ghc mailing list [email protected] http://www.haskell.org/mailman/listinfo/cvs-ghc
