wiki:RankNTypes

Version 8 (modified by ross@…, 8 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 ->.

foralls 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

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.

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

Pros

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.

Tickets

#60
add RankNTypes or Rank2Types