What is the rank of these 3 functions? And, most imporantely, why?
10:22 12 Dec 2025

The following questions are in fact exercises 6.3-i, 6.3-ii, 6.3-iii from _Thinking with Types_

  1. What is the rank of Int -> forall a. a -> a?

  2. What is the rank of (a -> b) -> (forall c. c -> a) -> b?

  3. 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):

  1. Int -> forall a. a -> a has implicit paranthesis like in Int -> forall a. (a -> a), so it is a function that returns a polymorphic function, i.e. the caller, when passing an Int to this function, gets back a forall a. (a -> a), that they (the caller) will instantiate with a equal to whatever the context deduces, so I can move the forall a. to the beginning, like in forall a. Int -> (a -> a), hence forall a. Int -> a -> a, or even Int -> a -> a. So it is rank 1, the caller decides a and the implementation of the function can't do anything with that a precisely because it doesn't know what it is (to do a + i it'd need to know a :: Int, to do a ++ "" it'd need to know a :: String, and so on);
  2. (a -> b) -> (forall c. c -> a) -> b I cannot move the forall c. anywhere because it's not around the return value, but around an argument, something that the caller passes, so the caller must pass a forall c. c -> a i.e. a function that can accept any c at all, because the implementation makes the decision of what c is, 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 == Integer
    
    (a is instead determined by the caller's context);
  3. ((forall x. m x -> b (z m x)) -> b (z m a)) -> m a is 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 type forall 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.

haskell existential-type type-theory higher-rank-types