7.14. Scoped Type Variables

7.14.1. Scope and implicit quantification

• 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.

• The type variables thus brought into scope 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.

• There is no implicit universal quantification on pattern type signatures, nor may one write an explicit forall type in a pattern type signature. The pattern type signature is a monotype.

• 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

  (Not implemented in Hugs yet, Dec 98).

7.14.2. 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.

7.14.3. Result type signatures

• The result type of a function can be given a signature, thus:

  f (x::a) :: [a] = [x,x,x]

  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)

Result type signatures are not yet implemented in Hugs.

7.14.4. Pattern signatures on other constructs

• 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)

  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.

• Pattern type signatures, including the result part, can be used 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:

  case (True,False) of { (x::Bool, y) -> 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:

  \ x :: a -> b -> x

• Pattern type signatures that bind new type variables may not be used in pattern bindings at all. So this is illegal:

  f x = let (y, z::a) = x in ...

  But these are OK, because they do not bind fresh type variables:

  f1 x = let (y, z::Int) = x in ... f2 (x::(Int,a)) = let (y, z::a) = x in ...

  However a single variable is considered a degenerate function binding, rather than a degerate pattern binding, so this is permitted, even though it binds a type variable:

  f :: (b->b) = \(x::b) -> x

Such degnerate function bindings do not fall under the monomorphism restriction. Thus:

g :: a -> a -> Bool = \x y. x==y

Here g has type forall a. Eq a => a -> a -> Bool, just as if g had a separate type signature. Lacking a type signature, g would get a monomorphic type.

7.14.5. 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]