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

[Dan Doel]

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

  http://code.haskell.org/~dolio/

in the pts repository (I'll try to get a little documentation for the REPL 
uploaded). And let me know if you find something that types but shouldn't, or 
some such nonsense.

Cheers,

-- Dan