Scoped type variables

Fri Dec 17 13:14:56 EST 2004

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 at cl.cam.ac.uk