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

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

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.