Eugene Kirpichov wrote:
Hello.
Consider the type: (forall a . a) -> String.
On one hand, it is rank-2 polymorphic, because it abstracts over a rank-1 polymorphic type. On the other hand, it is monomorphic because it isn't actually quantified itself: in my intuitive view, a parametrically polymorphic type has infinitely many instantiations (for example, Int -> Int is an instantiation of forall a . a -> a, and String -> String also is), and this type doesn't have any instantiations at all.
Which is correct? Is there really a contradiction? What is the definition of rank of a polymorphic type?
There's a nice paper about this: Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich and Mark Shields "Practical type inference for arbitrary-rank types" http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/put... Section 3.1 of that paper defines what rank types have: "The rank of a type describes the depth at which universal quantifiers appear contravariantly" Looking at the examples that are then given I'd say your example has rank 2 (but I'm no expert). It only mentions the depth of the forall, not whether it has any instantiations. HTH, Martijn.