Scoped type variables

[Simon Peyton-Jones]

Hi Mark,=20

Thanks for your reply.

| | Arguments in favour:
| | 	- It's more like term-variable pattern matching
|=20
| Term variables in a pattern are binding occurrences, but type=20
| variables are not.  Making the latter look more like the=20
| former would appear to be a recipe for unnecessary confusion=20
| given that that they are actually different.

Why do you say "type variables are not"?.  When I say

	f x =3D e

I mean "inside e, use x as the name for whatever value is=20
passed as argument to f".

Under what Marcin proposes=20

	f (x::a) =3D e

would mean "inside (type signatures in) e, use a as the name for
whatever type is the type of the argument passed to f".



When you say there's a good theoretical foundation (typed lambda
calcului) I think you are imagining that when we say

	f (x::a) =3D e

we are saying "There's a /\a as well as a \x::a in this definition".  In
which
case it would certainly be wrong to allow
	f :: Int -> Int
	f (x::a) =3D e

But I'm suggesting something different

* Place the big lambdas wherever they would be now (i.e. not influenced
   by the position of (x::a) type signatures.

* Explain the pattern type signatures as let-bindings for types.  Thus
  we might translate f to system-F like this:

	f =3D \x::T -> let-type a =3D T in e

I've use let-type here, but one could equally well say (/\a -> e) T.

This (admittedly informal) translation works fine if T happens to be
Int,
for exampe; i.e. x's type is not universally quantified. =20

In short, the pattern type signature is used solely to bind names to
types,
and not for universal quantification.  I want to have a slightly more
elaborate
let-type, thus:

	g :: (Int,Bool) -> Int
	g (x::(a,b)) =3D e

translates to

	g =3D \x::(Int,Bool) -> let-type (a,b) =3D (Int,Bool) in e

But notice that the RHS of a pattern-matching let-type is statically
guaranteed to have the right shape.  So I don't allow

	let-type (a,b) =3D c in ...

(where c is  a type variable).  So it's just syntactic sugar, like
let-type itself,
and I could equally well write

	g =3D \x::(Int,Bool) -> let-type a =3D Int; b =3D Bool in e



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

I hope the answer to (a) is yes, but I realise that opinions may differ
about (b).

I thought this might be of general enough interest to be worth
continuing to cc the
Haskell list.

Simon