# [Haskell-cafe] What is the rank of a polymorphic type?

Dan Doel dan.doel at gmail.com
Sun Dec 6 08:39:05 EST 2009

```Apologies for the double-reply...

Your mail prompted me to finally get around to adding a mono/polytype system
to an interpreter I've been working on for pure type systems, to see what a
GHC-alike type system would look like. Here's what I came up with.

Constants are: *m, []m, *p and []p

Axioms are: *m : []m, *p : []p

Rules go as follows:

(*m,*m,*m)
This is obvious, because it allows normal functions.

([]m,[]m,[]m)
This gives arbitrary order type constructors (that is, it expands the
m-kinds to km ::= *m | km -> km)

([]m,*m,*p)
([]m,*p,*p)
These allows quantification over types. Note that if you erase the mono/poly
distinctions, you get the single rule ([],*,*), which is the impredicative
rule for the lambda cube. However, this system tracks a distinction, so it
remains predicative (universal quantifiers don't range over types that
contain universal quantifiers).

With just these rules, I think we accept just the types valid in ordinary
Haskell. We have higher order types, but we can only have polytypes in prenex
normal form, because quantification sticks a type into *p, and the only thing
we can do with a *p is add more quantifiers (over []m) to the beginning.r

To get rank-n types back, we need to be able to write functions that accept
and return polytypes as arguments. This corresponds to the rules:

(*m,*p,*p) (*p,*m,*p) (*p,*p,*p)

Note that []p never appears in our rules; it exists only to give *p a type
(which may not strictly be necessary, even, but it doesn't hurt). Data types
would have kinds like:

Maybe : *m -> *m

and so types like Maybe (forall a. a -> a) would be invalid, because it's
trying to use the type constructor with a *p. This type system is a bit
stricter than the one GHC uses for rank-n types, as if you have:

id : forall a : *m. a -> a

You cannot instantiate a to forall a. a -> a, because it has kind *p. GHC
allows that sort of impredicative instantiation with just rank-n types turned
on.

As alluded to earlier, one can recover an ordinary impredicative F_w by
erasing the mono/poly distinctions. The rules collapse to:

(*,*,*) ([],*,*) ([],[],[])

If anyone's interested in playing with the checker, it can be found at