rank 2-polymorphism and type checking

Koen Claessen koen@cs.chalmers.se
Wed, 24 Oct 2001 11:12:45 +0200 (MET DST)

Simon Peyton-Jones wrote:

 | So I'm interested to know: if GHC allowed
 | arbitrarily-ranked types, who would use them?

I have certainly come across (very practical) situations
where I would like to use rank-n types (with n > 2). One
example is the following.

When using "runST", I often end up with code that looks

  foo =
    ( do ...

Because I think it is a bad idea to use parentheses like
this, I would like to use "$":

  foo =
    runST $
      do ...

Alas, the compiler complains, because it wants runST to have
more arguments. So, one could define a special dollar

  infixr 0 $+

  ($+) :: ((forall s . m s a) -> a) -> (forall s . m s a) -> a
  run $+ m = run m

However, this has a rank-3 type.

I have made the following observation. Richard Bird once
wrote an article where he argues that allowing nested
datatypes is useless unless one allows polymorphic
recursion. I think the same is true for allowing functions
with rank-2 polymorphism. If higher rank polymorphism is not
allowed, then rank-2 polymorphic functions are just not
first-class enough for all kinds of generalizations.