rank 2-polymorphism and type checking
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
( do ...
Because I think it is a bad idea to use parentheses like
this, I would like to use "$":
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.