Scoped type variables

[Simon Peyton-Jones]

| | When you say there's a good theoretical foundation (typed lambda
| | calcului) I think you are imagining that when we say
| |=20
| | 	f (x::a) =3D e
| |=20
| | we are saying "There's a /\a as well as a \x::a in this definition".
|=20
| No, that's not what I'm thinking.=20

OK, let me try to give some type rules for what I have in mind.
In these rules, I'm going to have an environment, T, that binds
user type variables to types.  (A "user type variable" is a type
variable that appears in the program text.)

There is still a conventional type environment, G (usually written=20
Greek Gamma), that associates user term variables with their
types.

I'll just deal with type variables in lambda patterns, like

		\ (x::a) -> E

Here's the rule:

	x_i =3D free-term-vars(pat)
	a_i =3D free-type-vars(pat) \ T
	(T, a_i=3Dtaua_i); (G, x_i:taux_i) |- pat : tau_1
	(T, a_i=3Dtaua_i); (G, x_i:taux_i) |-- E : tau_2
	-------------------------------------------------------
	T;G |- \pat -> E : tau_1 -> tau_2

The a_i are the type variables brought into scope by the pattern;
namely the free type variable of the pattern which are not already
in scope (hence the \ T).

The T environment is extended by binding each user type variable
a_i to a type taua_i that is gotten out of thin air (as is  common in
type
rules).  This new T env is used when typechecking the pattern itself and
the body E.


The intereesting bit is how to typecheck patterns, and type inside them:

	T;G |- pat  : tau
	T    |- ty : tau
	-----------------
	T;G |- pat::ty  :  tau

That is, to typecheck the pattern (pat::ty), typecheck pat and typecheck
ty.

The judgement  T |- ty : tau checks that the user type ty is well formed
with
type tau.  The key rule of this judgement looks up a type variable in T:

	-----------------
	T |- a : T(a)




OK, that's it.  The point is simply that the user type variables are
regarded
as the name of a type; the programmer doesn't specify just what that
type
is.  The type rules just 'inline' the type wherever the name is used.

All this translates into completely unmodified System F. =20

| OK, so there are two questions
| a) does that answer the question about the techincal foundation
| b) is it a good design from a software engineering point of view
|=20
| I hope the answer to (a) is yes, but I realise that opinions may=20
| differ about (b).

This message is really just a second attempt at (a)

Simon