[Sorry, I forgot to reply to the list.] Hi.
I understand these to be Rank 0 terms:
(\(x::Int) . x) (0 :: Int) :: (forall. Int) -- value
(\(x::Int). x) :: (forall. Int -> Int)
Yes.
(\(x::a). x) :: (forall. a -> a)
Although the program prints forall, the absence of a type variable indicates Rank 0, correct?
It's a bit unclear what you mean, and the prototype implementation you seem to be using deviates from Haskell conventions here. The prototype checker sees "a" as a type constant here, so it plays the same role as "Int" before. In particular, "a" isn't a type variable, and there's no quantification.
I understand these to be Rank 1 terms:
(\x. x) :: (forall a. a -> a) -- This is not the same as the third example above, right? This one identifies the type variable a, the one above does not. Also, there's no explicit annotation, it's inferred.
The implementation indeed considers them to be different. Before "a" was a concrete type, and the function was the monomorphic identity function on that type. Now, "a" is a type variable, and the function is the polymorphic identity function. [...]
I understand these to be Rank 2 terms:
(\(x::(forall a. a)). 0) :: (forall. (forall a. a) -> Int)
The explicit forall annotation on the bound and binding variable x causes the program to infer a Rank 2 polytype as indicated by the "-> Int" following the (forall a. a), while noting the absence of a type variable following the left-most forall printed by the program, correct?
Your description here is a bit strange. It's a rank-2 type because there's a rank-1 type occurring to the left of the function arrow.
(\(x::(forall a. a -> a)). x) :: (forall b. (forall a. a -> a) -> b -> b)
Also Rank 2, only one arrow to the right of (forall a. a -> a) counts.
It's rank 2, yes. I'm not sure what you mean here by saying that only one arrow counts.
The universal quantifier on type variable b ranges over the type variable a, correct?
No. The universal quantifier ranges over all (mono)types.
I understand this to be a Rank 3 term:
(\(f::(forall a. a -> a)). \(x::(forall b. b)). f (f x)) :: (forall c. (forall a. a -> a) -> (forall b. b) -> c)
No, this is still rank 2. It uses two rank 1 types as function arguments. For it to be rank 3, it'd have to use a rank 2 type in the argument position of a function type. Note that the function arrow associates to the right: forall c. (forall a. a -> a) -> ((forall b. b) -> c) -- rank 2 (forall c. ((forall a. a -> a) -> (forall b. b)) -> c) -- rank 3
The arrows to the right of the universally quantified a and b expressions qualify this as Rank 3.
No, you seem to be applying a wrong definition of rank. The correct definition is given in Section 3.1 of the paper. Here's how you can derive the type above as a sigma_2: sigma_2 ~> forall c. sigma_2 ~> forall c. sigma_1 -> sigma_2 ~> forall c. sigma_1 -> sigma_1 -> sigma_2 ~> forall c. sigma_1 -> sigma_1 -> sigma_1 ~> forall c. sigma_1 -> sigma_1 -> sigma_0 ~> forall c. sigma_1 -> sigma_1 -> c ~> forall c. (forall a. sigma_1) -> sigma_1 -> c ~> forall c. (forall a. sigma_0) -> sigma_1 -> c ~> forall c. (forall a. tau -> tau) -> sigma_1 -> c ~> forall c. (forall a. a -> a) -> sigma_1 -> c ~> forall c. (forall a. a -> a) -> (forall b. sigma_1) -> c ~> forall c. (forall a. a -> a) -> (forall b. sigma_0) -> c ~> forall c. (forall a. a -> a) -> (forall b. b) -> c
Type variable c ranges over type variables a and b, correct?
No. Each of the type variables ranges over all (mono)types. (Or do you mean what the scope of "c" is? If so, then the scope of c is the complete type signature.) Cheers, Andres -- Andres Löh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com