From c949e1a9af96cd5241d8cfc74fe3c622258edd7e Mon Sep 17 00:00:00 2001 From: "simonpj@microsoft.com" Date: Wed, 6 Sep 2006 16:41:03 +0000 Subject: [PATCH] Documentation for lexically-scoped type variables GHC's design for lexically scoped type variables has changed. Here, belatedly, is the documentation. --- docs/users_guide/glasgow_exts.xml | 459 +++++++++++-------------------------- 1 file changed, 129 insertions(+), 330 deletions(-) diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml index 19e1416..5339c43 100644 --- a/docs/users_guide/glasgow_exts.xml +++ b/docs/users_guide/glasgow_exts.xml @@ -3201,225 +3201,81 @@ for rank-2 types. -Scoped type variables +<title>Lexically scoped type variables -A lexically scoped type variable can be bound by: - -A declaration type signature () -A pattern type signature () -A result type signature () - -For example: +GHC supports lexically scoped type variables, without +which some type signatures are simply impossible to write. For example: -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 -The pattern (xs::[a]) includes a type signature for xs. -This brings the type variable a into scope; it scopes over -all the patterns and right hand sides for this equation for f. -In particular, it is in scope at the type signature for y. - - - -At ordinary type signatures, such as that for ys, any type variables -mentioned in the type signature that are not in scope 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 a -is in scope, it is not universally quantified, so the type of ys is -the same as that of xs. In Haskell 98 it is not possible to declare +The type signature for f brings the type variable a into scope; it scopes over +the entire definition of f. +In particular, it is in scope at the type signature for y. +In Haskell 98 it is not possible to declare a type for ys; a major benefit of scoped type variables is that it becomes possible to do so. - - -Scoped type variables are implemented in both GHC and Hugs. Where the -implementations differ from the specification below, those differences -are noted. - - - -So much for the basic idea. Here are the details. +Lexically-scoped type variables are enabled by +. +Note: GHC 6.6 contains substantial changes to the way that scoped type +variables work, compared to earlier releases. Read this section +carefully! -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 +The design follows the following principles - - - -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. + - - - -The pattern type signature is a monotype: - - +A lexically scoped type variable can be bound by: - -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 () - - - - +In addition, GHC supports result type signatures (), although they never bind type variables. + - -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 - 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) - - -(Not implemented in Hugs yet, Dec 98). - - - - + Declaration type signatures A declaration type signature that has explicit @@ -3447,179 +3303,122 @@ quantification rules. -Where a pattern type signature can occur - - -A pattern type signature can occur in any pattern. For example: - - - - -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 - 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: - \ 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) - - +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. - - - - - 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: data T = forall a. MkT [a] - f :: T -> T - f (MkT [t::a]) = MkT t3 + k :: T -> T + k (MkT [t::a]) = MkT t3 where t3::[a] = [t,t,t] - - +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. - - - - - -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. - - + +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. -Pattern type signatures are completely orthogonal to ordinary, separate -type signatures. The two can be used independently or together. - + Result type signatures -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: - f (x::a) :: [a] = [x,x,x] - + -- f assumes that 'a' is already in scope + f x y :: [a] = [x,y,x] + g = \ x :: [Int] -> [3,4] -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: - - - - 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 - +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. + A result type signature never brings new type variables into scope. -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: - rev1 :: [a] -> [a] = \xs -> reverse xs + -- f assumes that 'a' is already in scope + f x (y :: [a]) = [x,y,x] + + g = \ (x :: [Int]) -> [3,4] - foo ys = rev (ys::[a]) + h :: forall a. [a] -> a + h xs = case xs of + ((y:ys) :: a) -> y -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: - rev1 :: [b] -> [b] - rev1 :: [a] -> [a] = \xs -> reverse xs + \ x :: a -> b -> x + + +Class and instance declarations -Result type signatures are not yet implemented in Hugs. - +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 + + -- 1.7.10.4