Scoped type variables

Sun Dec 19 17:32:20 EST 2004

At 17:51 +0000 17/12/2004, Simon Peyton-Jones wrote:
>OK, OK, I yield!
>
>This message is about lexically scoped type variables.  I've gradually
>become convinced that if you write
>
>	f :: [a] -> [a]
>	f x = <body>
>
>then the type variable 'a' should be in scope in <body>.   At present in
>GHC you have to write
>	f (x :: [a]) = <body>
>to bring 'a' into scope.
>
>I've fought against this because it seems funny for a 'forall' in a type
>signature to bring a type variable into scope in perhaps-distant
>function body, but it's just so convenient and "natural".  Furthermore,
>as Martin Sulzmann points out, you might have type variables that are
>mentioned only in the context of the type:
>	g :: Foo a b => [a] -> [a]
>	g = ...
>GHC provides no way to bring 'b' into scope at the moment, and that
>seems bad design.

Some design choices are unclear, at least to me. First, the 
separation of body and signature. I am used to locally introduced 
identifiers being visible locally too (i.e. requiring minimal 
scrolling through a file). This would break, meaning that I have to 
know which identifier was used in the signature. Related to this, how 
does this work out for signatures of class members and their 
instances, often separated over different files? A change in a type 
variable in a signature in a class inside a library might then break 
my instance of that class. Or is this mechanism only meant for let 
bound values? If not, and if taken to the other extreme, a type 
variable identifier may well become part of the type itself and its 
'meaning'. That is, given a type signature and a value definition 
complying with the signature always has the type variables available. 
The following then also might be admitted:

	f :: (forall a . a -> a) -> ...
         v = f (\x -> x::a)

Second, for a duplicate introduction of 'a' in:

	f :: [a] -> [a]
	f (x::a) = <body>

Is the 'a' introduced in 'f (x::a)' shadowing the 'a' introduced in 
'f :: [a] -> [a]'? If so, the separation of body and signature is 
slightly less of a problem because the 'a' introduced in the pattern 
will not create a 'duplicate identifier introduction' error message 
or a type mismatch (here between [a] and a).

 From a purist point of view I prefer to avoid spreading local 
information globally because we humans can cater with large programs 
only because we keep things local. From a pragmatic point of view as 
a Haskell user the feature seems to be a convenient one indeed. From 
a pragmatic point of view as a Haskell implementor I obviously still 
have questions.

cheers,
-- 

                 - Atze -

Atze Dijkstra, Institute of Information & Computing Sciences,    /|\
Utrecht University, PO Box 80089, 3508 TB Utrecht, Netherlands  / | \
Tel.: +31-30-2534093/1454 | WWW  : http://www.cs.uu.nl/~atze   /--|  \
Fax : +31-30-2513971      | Email: atze at cs.uu.nl              /   |___\