Scoped type variables
atze at cs.uu.nl
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
- 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 / |___\
More information about the Glasgow-haskell-users