Version 10 (modified by diatchki, 11 years ago) (diff)

# Rank-2 Types

## Brief Explanation

Functions may have polymorphic arguments, subject to three restrictions:

• Such functions must have explicit type signatures, using `forall` to bind polymorphic type variables, e.g.
```g :: (forall a. a -> a) -> (Bool, Char)
```
• In the definition of the function, polymorphic arguments must be matched on the left-hand side, and can only be matched by a variable or wildcard (`_`) pattern. The variable then has the polymorphic type of the corresponding argument, e.g.
```g f = (f True, f 'a')
```
• 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 remove the last two restrictions.

Questions from Iavor:

• The restriction that polymorphic arguments have to be matched by variable or wildcard (`_`) patterns does not appear to be specific to rank-2 types—-it seems like an orthogonal decision.
• While the rank-N proposal removes restriction (3), in many cases the results may be unexpected. For example, consider the classic example of using `runST`:
```x = runST (return a)     -- OK
y = runST \$ return 'a'
```
The rank-2 design rejects `y` because `runST` needs an extra argument. The rank-N design accepts this use but later fails because the inferred type for '`runST`' is 'less polymorphic than expected'.

## Tickets

#60
add RankNTypes or Rank2Types

## 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