[Haskell-cafe] What is the rank of a polymorphic type?
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:
This is obvious, because it allows normal functions.
This gives arbitrary order type constructors (that is, it expands the
m-kinds to km ::= *m | km -> km)
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
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
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.
More information about the Haskell-Cafe