wiki:RankNTypes

Version 5 (modified by ross@…, 8 years ago) (diff)

--

Rank-N Types

See ExtensionDescriptionHowto for information on how to write these extension descriptions. Please add any new extensions to the list of HaskellExtensions.

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.