[Haskell] Lexically scoped type variables

[Simon Peyton-Jones]

This message is about scoped type variables.  I'm sending it to the Haskell mailing list, because I think that the question of scoped type variables is of general interest to Haskellers, but I suggest that you all send *replies* to Haskell Café, where this thread originated.

	Simon

The thread was provoked by Nicholas's message about scoped type variables
	http://www.haskell.org/pipermail/haskell-cafe/2006-October/018947.html

I've thought a lot about this scoped-type-variable issue, and failed to come up with a truly satisfactory solution.  As several of you have noticed, GHC 6.6 changes design wrt GHC 6.4.   Perhaps it'd help if I explained what the problem is, and then some of you may be able to figure out a better solution.

For reference
GHC 6.6: http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#scoped-type-variables
GHC 6.4: http://www.haskell.org/ghc/docs/6.4.2/html/users_guide/type-extensions.html#scoped-type-variables

| I'd like to not have to introduce the forall, because with that comes
| introducing the entire context of the type. Thus I have to maintain
| any changes to the context, which I would prefer to leave to inference
| for modularity's sake.
| 
| In 6.4 I was able to fix this without having to introduce the forall;
| I could introduce scoped type-variables in patterns to get the job
| done.

Well, there is something to be said for the forall approach [plan (B)] -- it is fully explicit, and you can see exactly what the program means. One way forward would be to allow you to abbreviate the context of the type signature (since that is often the awkward bit) to "...", and approach you mention as "partial type signatures".

The only other reasonable alternative that I know of is plan (A), the one taken by earlier versions of GHC, and OCaml.  As Oleg puts it:

| Which of the two occurrences of the type variable |'a| a binding one? Who
| cares... It just works: within the same expression, the same type
| variable stands for the same type.

(I think it does matter which the binding occurrence is, because Oleg's comment begs the question "when are two type variables in the same expression?".  In earlier versions of GHC, it was precisely specified which was the binding occurrence.  However, that's a detail.)  A big difference between the two approaches is that with (B) a type variable stands for a *type variable*, whereas in (A) it stands for a *type*.  


So why did we switch from (A) to (B)?  Because of type inference for GADTs.  If you read our paper "unification based type inference for GADTs" (on my home page) you'll see that 

	a programmer-written type signatures always describes a rigid type

("rigid" means completely known from birth -- no nonsense about unification etc.)   It's very important for GADTs to know when a type is rigid (see the paper).

That invariant in turn motivates the rigidity of type variables, and hence plan (B). 


Now, one could combine (A) and (B).  It'd be possible to have rigid type variables (bound by foralls) standing for type variables, and wobbly ones (bound by patterns) standing for types.  That would do what you want, but it'd be yet more complicated, and I hesitate before making GHC's type system more complicated.

Other alternatives would be: do something about partial type signatures; or make GADT type inference more sophisticated (and thereby perhaps less predicatable).


So there you have it.  For myself I'm not yet convinced that plan (B) is so bad.  Maybe we should do something about partial type signatures, which might be useful regardless of scoped type variables.   But I'd welcome better designs.  It's an annoying issue because it *must* be solved (not having scoped type variables is unacceptable); but no solution seems satisfying.  However, Haskell Prime must incorporate scoped type variables in some form!