Version 11 (modified by ross@…, 10 years ago) (diff) |
---|

# Rank-N Types

## Brief Explanation

In Haskell 98, all free variables in a type are implicitly universally quantified, e.g.

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:

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 in the GHC User's Guide.
- Practical type inference for arbitrary-rank types, 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, Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones, ICFP 2006.
- Semantics of Types and Classes in the Haskell 98 Report
- PolymorphicComponents would also be allowed higher-rank types
- Rank2Types are a special case

## Tickets

- #60
- add RankNTypes or Rank2Types

## 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), 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).

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

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

## Cons

- More complex than Rank2Types, 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:

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.