Rank-2 Types

Brief Explanation

Functions may have polymorphic arguments, subject to three restrictions:

1. Such functions must have explicit type signatures, using forall to bind polymorphic type variables, e.g.

g :: (forall a. a -> a) -> (Bool, Char)

1. In the definition of the function, polymorphic arguments

2. must be matched on the left-hand side, and

3. can only be matched by a variable or wildcard (_) pattern. The variable then has the polymorphic type of the corresponding argument, e.g.

```wiki
g f = (f True, f 'a')
```

1. When such a function is used, it must be applied to at least as many arguments to include the polymorphic ones (so it's a good idea to put those first). Each expression must have a generalized type at least as general as that declared for the corresponding argument, e.g.

g id
g undefined

The more general RankNTypes relax restrictions 2(1) and 3.

References

• PolymorphicComponents do the same thing for data constructors.

Tickets

Pros

• simple type inference
• offered by GHC and Hugs for years
• enables runST and similar devices
• used in cheap deforestation
• useful with non-regular (or nested) types
• useful with PolymorphicComponents

Cons

• functions with rank-2 types are not first class
• can be awkward in comparison with RankNTypes