dude | 5 Dec 02:45 2012

confirming order of kinds and rank of types

I hope you can help me confirm my understanding of the order of kinds 
and rank of types as reported in [1,2]. I have been validating the 
mapping functions in Section 2 against the GHC 7.4.2 type checker by 
explicitly annotating the universal quantifiers as described in [1].

1. Just to baseline my understanding, given the following data type

data U a = UC (forall a. a)
-- :k U, U :: * -> * -- order of kind = 1
-- :t UC, UC :: (forall a1. a1) -> U a -- rank of type = 2

am I correct that the order of the kind is 1 and the rank of the type 
constructor is 2? See page 3 of [1] for counting the order and also page 
3 of [2] for counting rank.

2. Assuming the answer to #1 above is yes, am I also correct that the 
order of Fix is 2 and the rank of In is also 2 and the annotation to In 
does not affect its rank?

newtype Fix f = In (forall f. f (Fix f))
-- :k Fix, Fix :: (* -> *) -> * -- order of kind = 2
-- :t In, In :: (forall (f1 :: * -> *). f1 (Fix f1)) -> Fix f -- rank of 
type still = 2

3. Are the explicit annotations I added to the following fixpoint 
operator correct? Hinze indicates this is a third order kind and it 
seems that although the annotation on HIn has a higher order, the rank 
of the type hasn't changed, correct?

newtype HFix h a = HIn (forall h. (forall a. h (HFix h) a))
(Continue reading)


Gmane