On 2004-12-17 at 17:51GMT "Simon Peyton-Jones" wrote:
This message is about lexically scoped type variables.
I've been trying to work out what I think about this since you sent out the first message in this thread. I'm not sure that I've come to a useful conclusion, so I'll summarise my thoughts and see if that makes anything pop out of someone else's head. First, I've never liked the fact that type variables in signatures aren't declared anywhere -- this was part of the motivation that drove me to use a non-Hindley-Milner type system in Ponder. There, you could put a quantifier on an expression, so instead of
f :: [a] -> [a] f x = <body>
you could write (mangled to make it look more like Haskell) stuff like f = forall a.\(x::[a]) -> <body>::[a] and the scope of a was completely clear. Of course, this doesn't work with the way variables are declared in Haskell. Would it help to stick the quantifier at the beginning of the type declaration?
forall a b . g :: Foo a b => [a] -> [a] g = ...
That reads OK, and one can imagine that whenever you see a "g = ..." bit, you implicitly get the type variables that come at the front of the type declaration in scope as well. Doing this would mean that you keep the old behaviour for cases where there is no quantifier at the beginning of the type declaration, so things wouldn't break.
So there it is. Any one have strong opinions? (This is in addition to the existing mechanism for bringing scoped type variables into scope via pattern type signatures, of course.)
If I have a strong opinion about anything it's that the only thing that should bring type variables into scope is a(n implied) quantifier. Free variables are nasty. I don't hold out much hope of convincing anyone of this last, though. Jón -- Jón Fairbairn Jon.Fairbairn@cl.cam.ac.uk