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

[Dan Doel]

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).