
Prev	Chapter 7. GHC Language Features	Next

7.14. Scoped Type Variables

A pattern type signature can introduce a scoped type variable. For example

f (xs::[a]) = 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.

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

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

7.14.2. Scope and implicit quantification

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

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.

Prev	Home	Next
Assertions	Up	Pragmas