FW: Scoped type variables

[Simon Peyton-Jones]

This is the message that Marcin referred to, proposing a change in
the semantics of scoped type variables.  I may just go ahead and
implement it in GHC.   (The implementation is easy: delete a couple
of lines; and I guess the same is so for Hugs.  The question is whether
it's a desirable change.)

Simon


-----Original Message-----
From: Simon Peyton-Jones=20
Sent: 08 February 2001 02:32
Cc: Simon Peyton-Jones; qrczak@knm.org.pl
Subject: Scoped type variables


Dear Huggy people

| But for pattern and result type signatures changing the rules makes=20
| sense.
|     f (x::a) =3D ...
| does not mean that x has type "forall a. a" anyway. It should actually

| only give the type a name, no matter what it is.
|=20
| Similarly,
|     f (x :: (a,b)) =3D ...
| should unify the appropriate type variable with (,), and give names to

| monomorphic arguments of (,) used in the call we are in.

I must say that I agree with Marcin's point.  When we write

	f x =3D e

we mean that x is a name for whatever argument f is given.   Marcin
argues
that the same should apply for=20

	f (x :: (a,b)) =3D e

Namely, that x is a name for the argument, a is a name for the type of
the fst of x, and slly b.

Arguments in favour:
	- It's more like term-variable pattern matching

	- In the present system, saying (x::a) doesn't mean x's type is
	  really universally quantified -- it may have a type
constraint.
	  And there's really a continuum between saying=20
		forall a. C a =3D> t[a]
	  and
		t[Int]
	  because the Int amounts to a rather strong constraint on a.
Indeed,
	  when we have functional dependencies,
	      forall a. C Int a =3D> t[a]
	  may indeed be the same as
	      C Int Int =3D> t[Int]

	- It's simpler; less to explain to the programmer (quite a bit
of the
	  GHC documentation on this stuff is to explain what about the
universal
	  quantification)

Arguments against
	- It's not what GHC and Hugs do now.


It would be an easy change to make, but I'd prefer it if GHC and Hugs
stayed in sync over this (modulo release schedules), so I'd be
interested in your views.

Simon

Someone (Jeff?) wrote:

|     Could you clarify what you are proposing?  Is it
| something like "let me name that type `a' even tho I know=20
| it's really something more specific"?  (i.e. similar to the=20
| current hugs extension, but without the "can't be more=20
| specific than inferred" restriction)

Exactly so.  For example

	f (x::a) =3D let y::a =3D x+1
		     in h x y

would be legal even if=20

	h :: Int -> Int -> Int

The point is that 'a' simply names the type of x, even if
that type isn't a type variable.