[Documentation for lexically-scoped type variables
simonpj@microsoft.com**20060906164103
GHC's design for lexically scoped type variables has changed.
Here, belatedly, is the documentation.
] {
hunk ./docs/users_guide/glasgow_exts.xml 3204
-Scoped type variables
+<title>Lexically scoped type variables
hunk ./docs/users_guide/glasgow_exts.xml 3208
-A <emphasis>lexically scoped type variable</emphasis> can be bound by:
-<itemizedlist>
-<listitem><para>A declaration type signature (<xref linkend="decl-type-sigs"/>)</para></listitem>
-<listitem><para>A pattern type signature (<xref linkend="pattern-type-sigs"/>)</para></listitem>
-<listitem><para>A result type signature (<xref linkend="result-type-sigs"/>)</para></listitem>
-</itemizedlist>
-For example:
+GHC supports <emphasis>lexically scoped type variables</emphasis>, without
+which some type signatures are simply impossible to write. For example:
hunk ./docs/users_guide/glasgow_exts.xml 3211
-f (xs::[a]) = ys ++ ys
- where
- ys :: [a]
- ys = reverse xs
+f :: forall a. [a] -> [a]
+f xs = ys ++ ys
+ where
+ ys :: [a]
+ ys = reverse xs
hunk ./docs/users_guide/glasgow_exts.xml 3217
-The pattern <literal>(xs::[a])</literal> includes a type signature for <varname>xs</varname>.
-This brings the type variable <literal>a</literal> into scope; it scopes over
-all the patterns and right hand sides for this equation for <function>f</function>.
-In particular, it is in scope at the type signature for <varname>y</varname>.
-</para>
-
-<para>
-At ordinary type signatures, such as that for <varname>ys</varname>, any type variables
-mentioned in the type signature <emphasis>that are not in scope</emphasis> are
-implicitly universally quantified. (If there are no type variables in
-scope, all type variables mentioned in the signature are universally
-quantified, which is just as in Haskell 98.) In this case, since <varname>a</varname>
-is in scope, it is not universally quantified, so the type of <varname>ys</varname> is
-the same as that of <varname>xs</varname>. In Haskell 98 it is not possible to declare
+The type signature for <literal>f</literal> brings the type variable <literal>a</literal> into scope; it scopes over
+the entire definition of <literal>f</literal>.
+In particular, it is in scope at the type signature for <varname>y</varname>.
+In Haskell 98 it is not possible to declare
hunk ./docs/users_guide/glasgow_exts.xml 3224
-
-<para>
-Scoped type variables are implemented in both GHC and Hugs. Where the
-implementations differ from the specification below, those differences
-are noted.
-</para>
-
-<para>
-So much for the basic idea. Here are the details.
+<para>Lexically-scoped type variables are enabled by
+<option>-fglasgow-exts</option>.
hunk ./docs/users_guide/glasgow_exts.xml 3227
+<para>Note: GHC 6.6 contains substantial changes to the way that scoped type
+variables work, compared to earlier releases. Read this section
+carefully!</para>
hunk ./docs/users_guide/glasgow_exts.xml 3232
-<title>What a scoped type variable means
-
-A lexically-scoped type variable is simply
-the name for a type. The restriction it expresses is that all occurrences
-of the same name mean the same type. For example:
-
- f :: [Int] -> Int -> Int
- f (xs::[a]) (y::a) = (head xs + y) :: a
-
-The pattern type signatures on the left hand side of
-f express the fact that xs
-must be a list of things of some type a; and that y
-must have this same type. The type signature on the expression (head xs)
-specifies that this expression must have the same type a.
-There is no requirement that the type named by "a" is
-in fact a type variable. Indeed, in this case, the type named by "a" is
-Int. (This is a slight liberalisation from the original rather complex
-rules, which specified that a pattern-bound type variable should be universally quantified.)
-For example, all of these are legal:
-
-
- t (x::a) (y::a) = x+y*2
-
- f (x::a) (y::b) = [x,y] -- a unifies with b
-
- g (x::a) = x + 1::Int -- a unifies with Int
-
- h x = let k (y::a) = [x,y] -- a is free in the
- in k x -- environment
-
- k (x::a) True = ... -- a unifies with Int
- k (x::Int) False = ...
-
- w :: [b] -> [b]
- w (x::a) = x -- a unifies with [b]
-
-
-
-
-
-Scope and implicit quantification
-
-
+Overview
hunk ./docs/users_guide/glasgow_exts.xml 3234
+The design follows the following principles
hunk ./docs/users_guide/glasgow_exts.xml 3236
-
-
-
-All the type variables mentioned in a pattern,
-that are not already in scope,
-are brought into scope by the pattern. We describe this set as
-the type variables bound by the pattern.
-For example:
-
- f (x::a) = let g (y::(a,b)) = fst y
- in
- g (x,True)
-
-The pattern (x::a) brings the type variable
-a into scope, as well as the term
-variable x. The pattern (y::(a,b))
-contains an occurrence of the already-in-scope type variable a,
-and brings into scope the type variable b.
-
-
-
-
-
-The type variable(s) bound by the pattern have the same scope
-as the term variable(s) bound by the pattern. For example:
-
- let
- f (x::a) = <...rhs of f...>
- (p::b, q::b) = (1,2)
- in <...body of let...>
-
-Here, the type variable a scopes over the right hand side of f,
-just like x does; while the type variable b scopes over the
-body of the let, and all the other definitions in the let,
-just like p and q do.
-Indeed, the newly bound type variables also scope over any ordinary, separate
-type signatures in the let group.
-
-
-
-
-
-
-The type variables bound by the pattern may be
-mentioned in ordinary type signatures or pattern
-type signatures anywhere within their scope.
-
-
-
-
-
-
- In ordinary type signatures, any type variable mentioned in the
-signature that is in scope is not universally quantified.
-
-
-
-
-
-
-
- Ordinary type signatures do not bring any new type variables
-into scope (except in the type signature itself!). So this is illegal:
-
-
- f :: a -> a
- f x = x::a
-
-
-It's illegal because a is not in scope in the body of f,
-so the ordinary signature x::a is equivalent to x::forall a.a;
-and that is an incorrect typing.
-
+A scoped type variable stands for a type variable, and not for
+a type. (This is a change from GHC's earlier
+design.)
+Furthermore, distinct lexical type variables stand for distinct
+type variables. This means that every programmer-written type signature
+(includin one that contains free scoped type variables) denotes a
+rigid type; that is, the type is fully known to the type
+checker, and no inference is involved.
+Lexical type variables may be alpha-renamed freely, without
+changing the program.
+
hunk ./docs/users_guide/glasgow_exts.xml 3248
-
-
-
hunk ./docs/users_guide/glasgow_exts.xml 3249
-The pattern type signature is a monotype:
-
-
+A lexically scoped type variable can be bound by:
hunk ./docs/users_guide/glasgow_exts.xml 3251
-
-A pattern type signature cannot contain any explicit forall quantification.
-
-
-
-The type variables bound by a pattern type signature can only be instantiated to monotypes,
-not to type schemes.
-
-
-
-There is no implicit universal quantification on pattern type signatures (in contrast to
-ordinary type signatures).
-
-
+A declaration type signature ()
+A pattern type signature ()
+Class and instance declarations ()
hunk ./docs/users_guide/glasgow_exts.xml 3255
-
-
-
-
+In addition, GHC supports result type signatures (), although they never bind type variables.
+
hunk ./docs/users_guide/glasgow_exts.xml 3259
-
-The type variables in the head of a class or instance declaration
-scope over the methods defined in the where part. For example:
-
-
+In Haskell, a programmer-written type signature is implicitly quantifed over
+its free type variables (Section
+4.1.2
+of the Haskel Report).
+Lexically scoped type variables affect this implicit quantification rules
+as follows: any type variable that is in scope is not universally
+quantified. For example, if type variable a is in scope,
+then
hunk ./docs/users_guide/glasgow_exts.xml 3269
- class C a where
- op :: [a] -> a
-
- op xs = let ys::[a]
- ys = reverse xs
- in
- head ys
+ (e :: a -> a) means (e :: a -> a)
+ (e :: b -> b) means (e :: forall b. b->b)
+ (e :: a -> b) means (e :: forall b. a->b)
hunk ./docs/users_guide/glasgow_exts.xml 3273
-
-
-(Not implemented in Hugs yet, Dec 98).
hunk ./docs/users_guide/glasgow_exts.xml 3274
-
hunk ./docs/users_guide/glasgow_exts.xml 3275
-
-
-
hunk ./docs/users_guide/glasgow_exts.xml 3278
+
hunk ./docs/users_guide/glasgow_exts.xml 3306
-Where a pattern type signature can occur
-
-
-A pattern type signature can occur in any pattern. For example:
-
-
-
+Pattern type signatures
hunk ./docs/users_guide/glasgow_exts.xml 3308
-A pattern type signature can be on an arbitrary sub-pattern, not
-just on a variable:
-
-
-
- f ((x,y)::(a,b)) = (y,x) :: (b,a)
-
-
-
-
-
-
-
-
- Pattern type signatures, including the result part, can be used
-in lambda abstractions:
-
-
- (\ (x::a, y) :: a -> x)
-
-
-
-
-
-
- Pattern type signatures, including the result part, can be used
-in case expressions:
-
-
- case e of { ((x::a, y) :: (a,b)) -> x }
-
-
-Note that the -> symbol in a case alternative
-leads to difficulties when parsing a type signature in the pattern: in
-the absence of the extra parentheses in the example above, the parser
-would try to interpret the -> as a function
-arrow and give a parse error later.
-
-
-
-
-
-
-
-To avoid ambiguity, the type after the “::” in a result
-pattern signature on a lambda or case must be atomic (i.e. a single
-token or a parenthesised type of some sort). To see why,
-consider how one would parse this:
-
-
+A type signature may occur in any pattern; this is a pattern type
+signature.
+For example:
hunk ./docs/users_guide/glasgow_exts.xml 3312
- \ x :: a -> b -> x
+ -- f and g assume that 'a' is already in scope
+ f = \(x::Int, y) -> x
+ g (x::a) = x
+ h ((x,y) :: (Int,Bool)) = (y,x)
hunk ./docs/users_guide/glasgow_exts.xml 3317
-
-
+In the case where all the type variables in the pattern type sigature are
+already in scope (i.e. bound by the enclosing context), matters are simple: the
+signature simply constrains the type of the pattern in the obvious way.
hunk ./docs/users_guide/glasgow_exts.xml 3321
-
-
-
-
hunk ./docs/users_guide/glasgow_exts.xml 3322
- Pattern type signatures can bind existential type variables.
-For example:
-
-
+There is only one situation in which you can write a pattern type signature that
+mentions a type variable that is not already in scope, namely in pattern match
+of an existential data constructor. For example:
hunk ./docs/users_guide/glasgow_exts.xml 3328
- f :: T -> T
- f (MkT [t::a]) = MkT t3
+ k :: T -> T
+ k (MkT [t::a]) = MkT t3
hunk ./docs/users_guide/glasgow_exts.xml 3333
-
-
+Here, the pattern type signature (t::a) mentions a lexical type
+variable that is not already in scope. Indeed, it cannot already be in scope,
+because it is bound by the pattern match. GHC's rule is that in this situation
+(and only then), a pattern type signature can mention a type variable that is
+not already in scope; the effect is to bring it into scope, standing for the
+existentially-bound type variable.
hunk ./docs/users_guide/glasgow_exts.xml 3340
-
-
-
-
-
hunk ./docs/users_guide/glasgow_exts.xml 3341
-Pattern type signatures
-can be used in pattern bindings:
-
-
- f x = let (y, z::a) = x in ...
- f1 x = let (y, z::Int) = x in ...
- f2 (x::(Int,a)) = let (y, z::a) = x in ...
- f3 :: (b->b) = \x -> x
-
-
-In all such cases, the binding is not generalised over the pattern-bound
-type variables. Thus f3 is monomorphic; f3
-has type b -> b for some type b,
-and not forall b. b -> b.
-In contrast, the binding
-
- f4 :: b->b
- f4 = \x -> x
-
-makes a polymorphic function, but b is not in scope anywhere
-in f4's scope.
-
+If this seems a little odd, we think so too. But we must have
+some way to bring such type variables into scope, else we
+could not name existentially-bound type variables in subequent type signatures.
hunk ./docs/users_guide/glasgow_exts.xml 3345
-
-
+
+This is (now) the only situation in which a pattern type
+signature is allowed to mention a lexical variable that is not already in
+scope.
+For example, both f and g would be
+illegal if a was not already in scope.
hunk ./docs/users_guide/glasgow_exts.xml 3352
-Pattern type signatures are completely orthogonal to ordinary, separate
-type signatures. The two can be used independently or together.
hunk ./docs/users_guide/glasgow_exts.xml 3353
-
hunk ./docs/users_guide/glasgow_exts.xml 3354
+
hunk ./docs/users_guide/glasgow_exts.xml 3359
-The result type of a function can be given a signature, thus:
-
+The result type of a function, lambda, or case expression alternative can be given a signature, thus:
hunk ./docs/users_guide/glasgow_exts.xml 3362
- f (x::a) :: [a] = [x,x,x]
-
-
+ -- f assumes that 'a' is already in scope
+ f x y :: [a] = [x,y,x]
hunk ./docs/users_guide/glasgow_exts.xml 3365
-The final :: [a] after all the patterns gives a signature to the
-result type. Sometimes this is the only way of naming the type variable
-you want:
+ g = \ x :: [Int] -> [3,4]
hunk ./docs/users_guide/glasgow_exts.xml 3367
-
-
- f :: Int -> [a] -> [a]
- f n :: ([a] -> [a]) = let g (x::a, y::a) = (y,x)
- in \xs -> map g (reverse xs `zip` xs)
+ h :: forall a. [a] -> a
+ h xs = case xs of
+ (y:ys) :: a -> y
hunk ./docs/users_guide/glasgow_exts.xml 3371
-
+The final :: [a] after the patterns of f gives the type of
+the result of the function. Similarly, the body of the lambda in the RHS of
+g is [Int], and the RHS of the case
+alternative in h is a.
hunk ./docs/users_guide/glasgow_exts.xml 3376
+ A result type signature never brings new type variables into scope.
hunk ./docs/users_guide/glasgow_exts.xml 3378
-The type variables bound in a result type signature scope over the right hand side
-of the definition. However, consider this corner-case:
+There are a couple of syntactic wrinkles. First, notice that all three
+examples would parse quite differently with parentheses:
hunk ./docs/users_guide/glasgow_exts.xml 3381
- rev1 :: [a] -> [a] = \xs -> reverse xs
+ -- f assumes that 'a' is already in scope
+ f x (y :: [a]) = [x,y,x]
hunk ./docs/users_guide/glasgow_exts.xml 3384
- foo ys = rev (ys::[a])
+ g = \ (x :: [Int]) -> [3,4]
+
+ h :: forall a. [a] -> a
+ h xs = case xs of
+ ((y:ys) :: a) -> y
hunk ./docs/users_guide/glasgow_exts.xml 3390
-The signature on rev1 is considered a pattern type signature, not a result
-type signature, and the type variables it binds have the same scope as rev1
-itself (i.e. the right-hand side of rev1 and the rest of the module too).
-In particular, the expression (ys::[a]) is OK, because the type variable a
-is in scope (otherwise it would mean (ys::forall a.[a]), which would be rejected).
-
-
-As mentioned above, rev1 is made monomorphic by this scoping rule.
-For example, the following program would be rejected, because it claims that rev1
-is polymorphic:
+Now the signature is on the pattern; and
+h would certainly be ill-typed (since the pattern
+(y:ys) cannot have the type a.
+
+Second, to avoid ambiguity, the type after the “::” in a result
+pattern signature on a lambda or case must be atomic (i.e. a single
+token or a parenthesised type of some sort). To see why,
+consider how one would parse this:
hunk ./docs/users_guide/glasgow_exts.xml 3399
- rev1 :: [b] -> [b]
- rev1 :: [a] -> [a] = \xs -> reverse xs
+ \ x :: a -> b -> x
hunk ./docs/users_guide/glasgow_exts.xml 3402
+
hunk ./docs/users_guide/glasgow_exts.xml 3404
+
+Class and instance declarations
hunk ./docs/users_guide/glasgow_exts.xml 3407
-Result type signatures are not yet implemented in Hugs.
-
hunk ./docs/users_guide/glasgow_exts.xml 3408
+The type variables in the head of a class or instance declaration
+scope over the methods defined in the where part. For example:
+
+
+
+ class C a where
+ op :: [a] -> a
+
+ op xs = let ys::[a]
+ ys = reverse xs
+ in
+ head ys
+
+
}