[[project @ 2001-05-21 10:03:36 by simonpj]
simonpj**20010521100336
Documentation for scoped type variables
] {
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2160
+ Pattern type signatures are completely orthogonal to ordinary, separate
+type signatures. The two can be used independently or together.
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2183
+
+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]
+
+
+
+
+
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2233
- 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.
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2257
+
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2315
-
-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.
-
-
-
-
-
-
-
-
-
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2359
-Pattern signatures on other constructs
-
-
+Where a pattern type signature can occur
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2361
+A pattern type signature can occur in any pattern, but there
+are restrictions on pattern bindings:
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2364
-
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2365
+
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2384
-
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2387
-
-
-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.
-
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2400
+
+
+
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2404
-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:
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2412
- case (True,False) of { (x::Bool, y) -> x }
+ \ x :: a -> b -> x
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2418
+
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2422
-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:
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2427
- \ 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]
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2438
+
+
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2443
- Pattern type signatures that bind new type variables
+Pattern type signatures that bind new type variables
hunk ./ghc/docs/users_guide/glasgow_exts.sgml 2497
-
-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]
-
-
-
-
-
-
-
-
-
-
-
}