wiki:Rank2Types

Version 10 (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

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