[Haskell-cafe] sample terms and interpreting program output from Tc Monad

[rickmurphy]

Hi All:

I'm still working through the following paper [1] and I wondered whether
you could help me confirm my understanding of some sample terms and
program output from the Tc Monad. For those interested, the language is
specified in Parser.lhs available in the protoype here [2].

I understand these to be Rank 0 terms:

(\(x::Int) . x) (0 :: Int) :: (forall. Int) -- value

(\(x::Int). x) :: (forall. Int -> Int)

(\(x::a). x) :: (forall. a -> a)

Although the program prints forall, the absence of a type variable
indicates Rank 0, correct?

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.

(\x. \y. x) :: (forall a b. b -> a -> b) -- Still rank 1.

Although there's no explicit annotation, the program infers the type
variables and prints the forall and the appropriate type variables for
the Rank 1 polytypes. 

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?

(\(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.
The universal quantifier on type variable b ranges over the type
variable a, correct?

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)

The arrows to the right of the universally quantified a and b
expressions qualify this as Rank 3. Type variable c ranges over type
variables a and b, correct?

Thanks for your help in better understanding this information. I'm home
schooling myself on Haskell and community support is a big help.

1. Practical Type Inference for Arbitrary-Rank Types.
2.http://research.microsoft.com/en-us/um/people/simonpj/papers/higher-rank/

--
Rick