The following questions are in fact exercises 6.3-i, 6.3-ii, 6.3-iii from _Thinking with Types_
What is the rank of
Int -> forall a. a -> a?What is the rank of
(a -> b) -> (forall c. c -> a) -> b?What is the rank of
((forall x. m x -> b (z m x)) -> b (z m a)) -> m a?
I think I know the answer to the first part of the question (what is the rank):
Int -> forall a. a -> ahas implicit paranthesis like inInt -> forall a. (a -> a), so it is a function that returns a polymorphic function, i.e. the caller, when passing anIntto this function, gets back aforall a. (a -> a), that they (the caller) will instantiate withaequal to whatever the context deduces, so I can move theforall a.to the beginning, like inforall a. Int -> (a -> a), henceforall a. Int -> a -> a, or evenInt -> a -> a. So it is rank 1, the caller decidesaand the implementation of the function can't do anything with thataprecisely because it doesn't know what it is (to doa + iit'd need to knowa :: Int, to doa ++ ""it'd need to knowa :: String, and so on);(a -> b) -> (forall c. c -> a) -> bI cannot move theforall c.anywhere because it's not around the return value, but around an argument, something that the caller passes, so the caller must pass aforall c. c -> ai.e. a function that can accept anycat all, because the implementation makes the decision of whatcis, e.g. the implementation could be
(-- (I've actually added another parameter to pattern match on to show that -- g can be called on any type.) bar :: Int -> (a -> b) -> (forall c. c -> a) -> b bar 1 f g = f (g "") -- c == String bar _ f g = f (g 3) -- c == Integerais instead determined by the caller's context);((forall x. m x -> b (z m x)) -> b (z m a)) -> m ais an even weirder beast, and I can't really reason about it; intuitively, I can tell that this function accepts a function (of type(forall x. m x -> b (z m x)) -> b (z m a)) that accepts a function (of typeforall x. m x -> b (z m x)) that is polymorphic, so it must be of rank 3.
But I feel like I'm more getting used to reading this stuff and doing some reasoning in my head I'm not even entirely aware of, then really understanding the matter.
I wondered about this topic in the past, but I've never got to the bottom of it. Currently I'm reading the aforementioned book, Thinking with Types, and at some point it reads like this:
Even higher-yet ranks also work in this fashion. The caller of the function and the implementations seesaw between who is responsible for instantiating the polymorphic types.
I perceive this is an important point, but I haven't quite understood it.