|
|
|
|
|
|
|
|
|
|
|
# Rank-N Types
|
|
|
|
|
|
|
|
|
## Brief Explanation
|
|
|
|
|
|
|
|
|
|
|
|
In Haskell 98, all free variables in a type are implicitly universally quantified, e.g.
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
const :: a -> b -> a
|
|
|
```
|
|
|
|
|
|
|
|
|
Thus Haskell 98 permits only rank-1 types.
|
|
|
The proposal is to allow explicit universal quantification within types using a `forall` keyword, so types can have the forms
|
|
|
|
|
|
|
|
|
- *type* `->` *type*
|
|
|
- `forall` *vars*. \[*context* `=>`\] *type*
|
|
|
- *monotype*
|
|
|
|
|
|
|
|
|
where *monotype* is a Haskell 98 type.
|
|
|
Note that `forall`'s are not allowed inside type constructors other than `->`.
|
|
|
|
|
|
|
|
|
|
|
|
`forall`s and contexts in the second argument of `->` may be floated out, e.g. the following types are equivalent:
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
succ :: (forall a. a -> a) -> (forall b. b -> b)
|
|
|
succ :: forall b. (forall a. a -> a) -> b -> b
|
|
|
```
|
|
|
|
|
|
|
|
|
It is not possible to infer higher-rank types in general; type annotations must be supplied by the programmer in many cases.
|
|
|
|
|
|
|
|
|
## References
|
|
|
|
|
|
|
|
|
- [ Arbitrary-rank polymorphism](http://www.haskell.org/ghc/docs/latest/html/users_guide/type-extensions.html#universal-quantification) in the GHC User's Guide.
|
|
|
- [ Practical type inference for arbitrary-rank types](http://research.microsoft.com/Users/simonpj/papers/higher-rank/), Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich and Mark Shields, July 2005. To appear in *Journal of Functional Programming*.
|
|
|
- [ Boxy types: type inference for higher-rank types and impredicativity](http://research.microsoft.com/Users/simonpj/papers/boxy/), Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones, ICFP 2006.
|
|
|
- [ Semantics of Types and Classes](http://www.haskell.org/onlinereport/decls.html#type-semantics) in the Haskell 98 Report
|
|
|
- [PolymorphicComponents](polymorphic-components) would also be allowed higher-rank types
|
|
|
- [Rank2Types](rank2-types) are a special case
|
|
|
|
|
|
## Tickets
|
|
|
|
|
|
|
|
|
|
|
|
<table><tr><th>[\#60](https://gitlab.haskell.org//haskell/prime/issues/60)</th>
|
|
|
<td>add RankNTypes or Rank2Types</td></tr></table>
|
|
|
|
|
|
|
|
|
|
|
|
## Details
|
|
|
|
|
|
|
|
|
|
|
|
Hindley-Milner type systems (e.g. in Haskell 98) may be specified by rules deriving the type of an expression from those of its constituents, providing a simple way to reason about the types of expressions.
|
|
|
The rules may also be used as a bottom-up procedure for inferring principal types, with inferred types matched against any signatures supplied, but many other traversals yield the same answer.
|
|
|
A mixture of bottom-up inference and top-down checking often produces more informative error messages.
|
|
|
|
|
|
|
|
|
### Bidirectional type inference
|
|
|
|
|
|
|
|
|
|
|
|
For arbitrary-rank types, a particular bidirectional traversal is specified by the type rules (see Fig. 8 on p25 of [ the arbitrary-rank paper](http://research.microsoft.com/Users/simonpj/papers/higher-rank/)), to make use of programmer-supplied annotations.
|
|
|
In particular,
|
|
|
|
|
|
|
|
|
- functions and expressions with type signatures are checked top-down.
|
|
|
- parameter variables without explicit signatures are assigned monotypes in upwards inference, but may inherit arbitrary-rank types in downwards checking.
|
|
|
- in an application (whether inferred or checked), the type of the function is inferred bottom-up, and the argument checked top-down against the inferred argument type.
|
|
|
|
|
|
|
|
|
The generalization preorder must be recursively defined, with contravariance for `->` types (see Fig. 7 on p22 of
|
|
|
[ the arbitrary-rank paper](http://research.microsoft.com/Users/simonpj/papers/higher-rank/)).
|
|
|
|
|
|
|
|
|
|
|
|
The system has the following properties:
|
|
|
|
|
|
|
|
|
- Programs containing no `forall`s are typeable if and only if they are typeable in Haskell 98.
|
|
|
- Inference produces principal types, though checking may accept more types.
|
|
|
- Both checking and inference are monotonic with respect to the generalization preorder.
|
|
|
|
|
|
|
|
|
However it does not permit
|
|
|
|
|
|
|
|
|
```wiki
|
|
|
runST $ do { ... }
|
|
|
```
|
|
|
|
|
|
|
|
|
as that requires impredicative types.
|
|
|
|
|
|
|
|
|
### Boxy types
|
|
|
|
|
|
|
|
|
|
|
|
Boxy types generalize bidirectional inference, and also allow impredicative types (type variables may be instantiated to polytypes, and polytypes may occurs as arguments of type constructors).
|
|
|
|
|
|
|
|
|
## Pros
|
|
|
|
|
|
|
|
|
- More convenient than encodings using [PolymorphicComponents](polymorphic-components)
|
|
|
|
|
|
## Cons
|
|
|
|
|
|
|
|
|
- More complex than [Rank2Types](rank2-types), which cover the most common cases (and can encode the rest, though clumsily).
|
|
|
- No clear programmer-level description of the restrictions that apply.
|
|
|
To quote the [ boxy-types paper](http://research.microsoft.com/Users/simonpj/papers/boxy/):
|
|
|
|
|
|
>
|
|
|
> >
|
|
|
> >
|
|
|
> > The type system is arguably too complicated for Joe Programmer to understand, but that is true of many type systems, and perhaps it does not matter too much: in practice, Joe Programmer usually works by running the compiler repeatedly, treating the compiler as the specification of the type system. Indeed, a good deal of the complexity of the type system (especially Section 6) is there to accommodate programs that "ought" to work, according to our understanding of Joe's intuitions.
|
|
|
> >
|
|
|
> >
|
|
|
>
|
|
|
|