[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
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
More information about the Haskell-Cafe
mailing list