5 Dec 2012 02:45
confirming order of kinds and rank of types
dude <dude <at> methodeutic.com>
2012-12-05 01:45:20 GMT
2012-12-05 01:45:20 GMT
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)
RSS Feed