Version 16 (modified by ross@…, 9 years ago) (diff) |
---|

# Scoped Type Variables

## Brief Explanation

In Haskell 98, it is sometimes impossible to give a signature for a locally defined variable, e.g. `cmp` in

sortImage :: Ord b => (a -> b) -> [a] -> [a] sortImage f = sortBy cmp where cmp x y = compare (f x) (f y)

The argument type of `cmp` is the type `a` in the signature of `sortImage`, but there is no way to refer to it in a type signature.
Quantification of type variables over expressions is needed.

Haskell already binds type variables in class and instance declarations.
It makes sense for these to also scope over bindings in the `where` part, but currently only GHC implements this.

GHC provides three extensions that bind type variables:

- Explicit
`forall`s in type signature declarations. The bound variables scope over the function body, e.g.sortImage :: forall a b. Ord b => (a -> b) -> [a] -> [a] sortImage f = sortBy cmp where cmp :: a -> a -> Ordering cmp x y = compare (f x) (f y)

This could be a bit awkward with class methods, where the signature can be a long way from the binding.

- Pattern type signatures.
Free variables in the type stand for new types in the scope of the pattern, e.g.
sortImage (f::a->b) = sortBy cmp where cmp :: a -> a -> Ordering cmp x y = compare (f x) (f y)

- Result type signatures, giving the type of both sides of the equation.
Free variables in the type stand for new types in the scope, e.g.
sortImage f :: [a] -> [a] = sortBy cmp where cmp :: a -> a -> Ordering cmp x y = compare (f x) (f y)

In the latter two cases, the variable can stand for any type, not necessarily a type variable as in these examples, i.e. the variable is existentially quantified. In future versions of GHC, type variables will be rigid (universally quantified). Hugs supports only pattern type signatures, with rigid type variables.

## References

Note that although GHC and Hugs use the same syntax, the meaning of type variables is quite different, and there are other differences too.

## Tickets

## Pros

- Allows better documentation (without them, some expressions cannot be annotated with their types).
- Extensions such as RankNTypes and GADTs require such annotations, so even more important in conjunction with them.

## Cons

- Many different forms of scoped type variables in GHC makes them hard to reason about.
For example:
f :: a -> a f = \x -> (x :: a)

is rejected butg = let f :: a -> a = \x -> (x :: a) in f

is allowed.

- With pattern and result signatures, one must examine outer bindings to determine whether an occurrence of a type variable is a binding. This creates a potential trap. A rule like ExplicitQuantification might be needed if these were put into the standard.

## Proposal 1

Both let-bound and lambda-bound type variables are in scope in the body of a function, and can be used in expression signatures. However, just as a let-binding can shadow other values of the same name, let-bound type variables may shadow other type variables. Thus no type variables are ever already in scope in a let-bound signature. Lambda-bound type variables (e.g. in a pattern) do not shadow but rather refer to the same type. ExplicitQuantification is required for all expression type signatures but not let-bound signatures.

This proposal tries to strike a balance between backwards compatibility, avoiding accidental type errors, and simplicity. Let-bound type signatures always create a new scope, lambda-bound ones are always in the same scope, and it is clear from expression type signatures which are the scoped type vars.

(perhaps this text can be cleaned up further? what is a better term for expression type signature?)

## Proposal 2

Restrict the above extensions to:

- for function bindings, optional explicit
`forall`s in type signatures. - for pattern bindings, result type signatures. Explicit universal quantification might be made mandatory.

plus binding of type variables in class and instance heads.