Skip to content

Changes

Page history
Fix names of language exnteions pages authored by Ben Gamari's avatar Ben Gamari
Hide whitespace changes
Inline Side-by-side
ScopedTypeVariables.md 0 → 100644
View page @ d5606db0
# 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
```wiki
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.
Proposal (see below for details):
- extend the scope of type variables in `class` and `instance` heads.
- allow bindings of type variables in type annotations, as in GHC 6.6, but with existential types handled by something other than pattern type signatures.
## References
- [ Hugs documentation](http://cvs.haskell.org/Hugs/pages/users_guide/type-annotations.html)
- [ GHC 6.4 documentation](http://www.haskell.org/ghc/docs/6.4-latest/html/users_guide/type-extensions.html#scoped-type-variables)
- [ GHC 6.6 documentation](http://www.haskell.org/ghc/dist/current/docs/users_guide/type-extensions.html#scoped-type-variables)
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
<table><tr><th>[\#67](https://gitlab.haskell.org//haskell/prime/issues/67)</th>
<td>add Scoped Type Variables</td></tr>
<tr><th>[\#81](https://gitlab.haskell.org//haskell/prime/issues/81)</th>
<td>scoping of type variables in class instances</td></tr></table>
## Binding sites for type variables
### Class and instance declarations
Haskell already binds type variables in class and instance declarations.
It is proposed that these also scope over bindings in the `where` part (as currently implemented by GHC, but not Hugs).
This permits signatures that would not otherwise be possible.
An example of a class declaration:
```wiki
class C a where
op :: [a] -> a
op xs = let ys :: [a]
ys = reverse xs
in head ys
```
An example of an instance declaration:
```wiki
class C t where
op :: t -> t
instance C [a] where
op xs = let ys :: [a]
ys = reverse xs
in ys ++ ys
```
### Type annotations
**Hugs** provides only one mechanism for binding type variables:
- Pattern type signatures.
Free variables in the type stand for distinct new type variables in the scope of the pattern, e.g.
```wiki
sortImage (f::a->b) = sortBy cmp
where cmp :: a -> a -> Ordering
cmp x y = compare (f x) (f y)
```
That is, the type variables are rigid (universally quantified).
**GHC 6.4** provides three extensions that bind type variables:
- Explicit `forall`s in type signature declarations.
The bound variables scope over the function body, e.g.
```wiki
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.
```wiki
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.
```wiki
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.
**GHC 6.6** allows binding via:
- Explicit `forall`s in type signature declarations, as above.
- A mechanism to name type variables in [existentially quantified types](existential-quantification), currently by a version of pattern type signature; no other type variables in pattern type signatures produce bindings.
This is sufficient if we assume [MonomorphicPatternBindings](monomorphic-pattern-bindings).
*Notes*:
- [RankNTypes](rank-n-types) allows function types like
```wiki
shallowTerm :: (forall a. Data a => Maybe a) -> (forall b. Data b => b)
```
in which referring to the type variable `b` seems to require a binding in a result type signature.
Nor are binding result type signatures sufficient to name all type variables, e.g. consider naming the type variable `a` in the body of the following function:
```wiki
iter :: Int -> (forall a. (a -> a) -> (a -> R) -> a -> R)
iter n step k init = ...
```
In these cases the `forall` and context can be floated out, but not if they were buried in a type synonym.
- If there were a special syntax for binding type variables in existentials, pattern type signatures would be independent of type variable binding (and thus an othogonal design choice).
- If the language does not include [GADTs](gad-ts), such type variables could be bound with a new pattern syntax mimicking the `data` declaration, e.g.
```wiki
data Accum a = forall s. MkAccum s (a -> s -> s) (s -> a)
f (forall s. MkAccum st a e) = ...
```
(*Mutatis mutandi* for other variants of [ExistentialQuantification](existential-quantification) syntax.)
With [GADTs](gad-ts) one can define existential types without explicit quantification, so the order of multiple type variables wouldn't be clear.
## Pros
- Allows better documentation (without them, some expressions cannot be annotated with their types).
- Extensions such as [RankNTypes](rank-n-types) and [GADTs](gad-ts) require such annotations, so even more important in conjunction with them.
## Cons
These apply to the GHC 6.4 version:
- Many different forms of scoped type variables makes them hard to reason about.
For example:
```wiki
f :: a -> a
f = \x -> (x :: a)
```
is rejected but
```wiki
g = 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](explicit-quantification) might be needed if these were put into the standard.
## Alternative proposal
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](explicit-quantification) 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?)