[Haskell-cafe] What is the rank of a polymorphic type?
Dan Doel
dan.doel at gmail.com
Sun Dec 6 02:48:09 EST 2009
On Sunday 06 December 2009 1:42:34 am Eugene Kirpichov wrote:
> OK, thanks.
> However, isn't the type (forall a . a) -> String impredicative because
> it instantiates a type variable of the type constructor (->) p q with
> p = forall a . a?
There's probably no clear cut answer to this independent of how you think of
(->). For instance, if we explain the Haskell type system by way of a pure
type system, (->) is a special case of a pi type, which looks like:
pi x : k. t
where any xs in t are bound by the pi. We then have:
p -> q = pi _ : p. q
forall a : k. b = pi a : k. b
pi types are given types by sets of rules, which look like triples. If (s,t,u)
is a rule, then:
G |- k : s G, a : k |- b : t
-------------------------------
G |- (pi a : k. b) : u
is the corresponding typing rule. Type systems like Haskell's are commonly
thought of in terms of the lambda cube, which has constant sorts * and [],
with * : []. The rule (*,*,*) gives you ordinary functions. (*,[],[]) gives
you dependent types, so that's out.
([],*,*) is an impredicative rule for polymorphism. This says that, for
instance:
forall a. a -> a = (pi a : *. pi _ : a. a) : *
because (pi _ : a. a) : * if a : *, by the (*,*,*) rule, and then we apply the
impredicative rule for the universal quantification. One could also use the
predicative rule ([],*,[]), which would result in forall a. a -> a having type
[].
However, Haskell also has arbitrarily higher-order types. This is given by the
rule ([],[],[]), which allows expressions like:
(* -> *) -> * = pi _ : (pi _ : *. *). *
This type system is called F_omega, while just the ([],*,?) rule is known as
F_2.
However, the F_omega rule also allows for arbitrary rank polymorphism even
with the predicative universal quantifier rule above (predicative F_2 allows a
little, but it's very limited*). For instance, the higher rank type:
forall a. (forall b. b) -> a
checks thusly:
(forall b. b) : [] via ([],*,[])
((forall b. b) -> a) : [] via ([],*,[])
(forall a. (forall b. b) -> a) : [] via ([],[],[])
Data types, by contrast, have kinds like * -> *, so using say,
Maybe (forall a. a -> a)
genuinely relies on the impredicative rule. GHC's type system isn't exactly
set up in this way, but (->) is similarly special in that it somehow isn't
quite just another type constructor with kind * -> * -> * (or even whatever
special kinds GHC uses to support unboxed values and such).
Hope that wasn't too confusing. :)
-- Dan
* Predicative F_2 will essentially allow one universal quantifier somewhere in
the type. This can be:
forall a. a -> a
or it can be:
(((forall a. a) -> T) -> U) -> V
for T, U and V of kind * (the only kind in F_2), which is a rank-4 type. It
doesn't allow:
forall a b. a -> b
even, because the inner (forall b. a -> b) : [], so adding the forall a
requires the F_omega rule.
Predicative F_2 and F_w also blow up with quantification on the right of an
arrow, because it looks like the rule for dependent types:
T -> (forall a. a)
T : *, (forall a. a) : []
so the rule (*,[],[]) would be invoked.
GHC doesn't have this sort of hierarchy, and so doesn't have these sorts of
weird cases, despite being predicative of a sort. Instead it distinguishes
somehow between monotypes ([Float], String -> Int, a -> b) and polytypes
(forall a. a, ...), although it doesn't really display the difference.
Quantifiers are only supposed to range over kinds that classify monotypes (or
monotype constructors), which keeps the predicativity (although, even this
gets fudged some: If I have forall a. a -> a, I can instantiate a to the
polytype forall a. a -> a with rank-n polymorphism, because it only seems to
worry about the validity of the resulting type, and (->) is special; by
contrast, the same cannot be said for forall a. Maybe a, because Maybe
genuinely only accepts monotypes without -XImpredicativeTypes).
More information about the Haskell-Cafe
mailing list