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))
-- :k HFix, HFix :: ((* -> *) -> * -> *) -> * -> * -- per hinze order of
kind = 3
-- :t HIn, HIn :: (forall (h1 :: (* -> *) -> * -> *) a1. h1 (HFix h1)
a1) -> HFix h a -- still rank of type = 2 because there's one quantifier
to the left of the function arrow.
If all that all checks out, I have a few follow up questions:
4. Hinze reports that mapHFix is Rank3, but the following type checks
with the Rank2Type pragma and if I remove the explicit universal
quantifiers in HIn. Put the quantifiers back in an it does not type check.
mapHFix maph mapa (HIn v) = HIn (maph (mapHFix maph) mapa v)
5. Also, the inferred signature for mapHFix differs from the one stated
by Hinze. It's this ...
mapHFix :: ((t2 -> HFix t t1 -> HFix h a) -> t2 -> t (HFix t) t1 -> h
(HFix h) a) -> t2 -> HFix t t1 -> HFix h a
What is the rank of this type signature? The type variables are not in
the same order as Hinze's and I was able to just wrap a (forall t2 t t1
h a.) around the whole thing and it type checked. Why are they different?
6. What is the correct type signature for mapHFix? The correct type
signature should support changing the pragma from Rank2Types to
RankNTypes, then today's 7.4.2 type checker will succeed where it could
not in 1999 when the paper was written, correct?
Thanks so much for helping me confirm my understanding of these issues!
--
dude
1. Polytypic Values Posess Polykinded Types. (Hinze, 1999)
2. A Direct Algorithm for Type Inference in the Rank 2 Fragment of the
Second Order Lambda Calculus. (Kfoury, 1993)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
