From 417aae6f638fb8a8e8b12fa330a9070f3cc62ee5 Mon Sep 17 00:00:00 2001 From: simonpj Date: Mon, 21 May 2001 10:03:36 +0000 Subject: [PATCH] [project @ 2001-05-21 10:03:36 by simonpj] Documentation for scoped type variables --- ghc/docs/users_guide/glasgow_exts.sgml | 249 ++++++++++---------------------- 1 file changed, 73 insertions(+), 176 deletions(-) diff --git a/ghc/docs/users_guide/glasgow_exts.sgml b/ghc/docs/users_guide/glasgow_exts.sgml index 57dbc00..44fcad0 100644 --- a/ghc/docs/users_guide/glasgow_exts.sgml +++ b/ghc/docs/users_guide/glasgow_exts.sgml @@ -2157,6 +2157,8 @@ In particular, it is in scope at the type signature for y. + Pattern type signatures are completely orthogonal to ordinary, separate +type signatures. The two can be used independently or together. 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 @@ -2179,6 +2181,47 @@ So much for the basic idea. Here are the details. +What a pattern type signature means + +A type variable brought into scope by a pattern type signature is simply +the name for a type. The restriction they express 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 @@ -2187,10 +2230,10 @@ So much for the basic idea. Here are the details. - All the type variables mentioned in the patterns for a single -function definition equation, that are not already in scope, -are brought into scope by the patterns. We describe this set as -the type variables bound by the equation. + 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. @@ -2211,6 +2254,7 @@ signature that is in scope is not universally quantified. + @@ -2269,103 +2313,6 @@ scope over the methods defined in the where part. For exampl -Polymorphism - - - - - - - - Pattern type signatures are completely orthogonal to ordinary, separate -type signatures. The two can be used independently or together. There is -no scoping associated with the names of the type variables in a separate type signature. - - - - f :: [a] -> [a] - f (xs::[b]) = reverse xs - - - - - - - - - The function must be polymorphic in the type variables -bound by all its equations. Operationally, the type variables bound -by one equation must not: - - - - - - - Be unified with a type (such as Int, or [a]). - - - - - - Be unified with a type variable free in the environment. - - - - - - Be unified with each other. (They may unify with the type variables -bound by another equation for the same function, of course.) - - - - - - -For example, the following all fail to type check: - - - - 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] - - - - - - - - - The pattern-bound type variable may, however, be constrained -by the context of the principal type, thus: - - - - f (x::a) (y::a) = x+y*2 - - - -gets the inferred type: forall a. Num a => a -> a -> a. - - - - - - - - - - Result type signatures @@ -2409,13 +2356,13 @@ Result type signatures are not yet implemented in Hugs. -Pattern signatures on other constructs - - +Where a pattern type signature can occur +A pattern type signature can occur in any pattern, but there +are restrictions on pattern bindings: - + A pattern type signature can be on an arbitrary sub-pattern, not just on a variable: @@ -2434,28 +2381,9 @@ just on a variable: Pattern type signatures, including the result part, can be used in lambda abstractions: - (\ (x::a, y) :: a -> x) - - -Type variables bound by these patterns must be polymorphic in -the sense defined above. -For example: - - - - f1 (x::c) = f1 x -- ok - f2 = \(x::c) -> f2 x -- not ok - - - -Here, f1 is OK, but f2 is not, because c gets unified -with a type variable free in the environment, in this -case, the type of f2, which is in the environment when -the lambda abstraction is checked. - @@ -2469,50 +2397,50 @@ in case expressions: case e of { (x::a, y) :: a -> x } + + + -The pattern-bound type variables must, as usual, -be polymorphic in the following sense: each case alternative, -considered as a lambda abstraction, must be polymorphic. -Thus this is OK: - - - - case (True,False) of { (x::a, y) -> x } - - - -Even though the context is that of a pair of booleans, -the alternative itself is polymorphic. Of course, it is -also OK to say: + +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: - case (True,False) of { (x::Bool, y) -> x } + \ x :: a -> b -> x + -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: + Pattern type signatures can bind existential type variables. +For example: - \ x :: a -> b -> x + data T = forall a. MkT [a] + + f :: T -> T + f (MkT [t::a]) = MkT t3 + where + t3::[a] = [t,t,t] + + - Pattern type signatures that bind new type variables +Pattern type signatures that bind new type variables may not be used in pattern bindings at all. So this is illegal: @@ -2566,37 +2494,6 @@ would get a monomorphic type. - -Existentials - - - - - - - - Pattern type signatures can bind existential type variables. -For example: - - - - data T = forall a. MkT [a] - - f :: T -> T - f (MkT [t::a]) = MkT t3 - where - t3::[a] = [t,t,t] - - - - - - - - - - - -- 1.7.10.4