Version 9 (modified by diatchki, 7 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'.

## References

- PolymorphicComponents do the same thing for data constructors.

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

- can be awkward in comparison with RankNTypes