How to understand that the types a and forall r. (a -> r) -> r are isomorphic

Question

In the book Thinking with Types, 6.4 Continuation Monad tells that the types a and forall r. (a -> r) -> r are isomorphic, which can be witnessed by the following functions:

cont :: a -> (forall r. (a -> r) -> r)
cont x = \f -> f x

unCont :: (forall r. (a -> r) -> r) -> a
unCont f = f id

In this book, it tells that any two types that have the same cardinality will always be isomorphic to one another. So I try to figure out the cardinality of the types a and forall r. (a -> r) -> r.

Suppose the cardinality of the type a is |a|. Then for the type forall r. (a -> r) -> r, how to figure out its cardinality equals |a|? The function type a -> b has cardinality |b|^|a|, i.e., |b| to the power of |a|, so forall r. (a -> r) -> r has cardinality of |r|^(|r|^|a|). How can it be equal to |a|?

I'm confused. Thanks for any tips!

Answer 1

Cardinality can not really be defined in the presence of polymorphic types. It is understood nowadays that polymorphic types "are not sets" as one might initially think. A famous pioneering argument by Reynolds was provided in his paper "Polymorphism is not set theoretic", proving that we can't simply interpret types with sets in the "trivial" way and obtain a meaningful notion.

Indeed, in sets 2^K and K are distinct cardinals, the first one being larger. Similarly, 2^(2^K) is larger than K. Yet, F X = 2^(2^X) (resembling F a = (a -> Bool) -> Bool) forms a (covariant) functor, for which we can find a fixed point

newtype T = T ((T -> Bool) -> Bool)

obtaining T being isomorphic to 2^(2^T), which makes no sense in sets, precisely because they can't have the same cardinality.

(The type T above can be obtained even without recursive types, in the presence of polymorphism, through an encoding as forall a. (F a -> a) -> a.)

Anyway, to solve this impasse we need to interpret a -> Bool as something else than the set of functions 2^a. A possible solution is to use Scott-continuous functions, as done by Scott. A related solution is using stable functions (see Girard's "Proofs and types" book), which (if I recall correctly) makes the interpretations of T and T -> Bool to have the same cardinality (unless both are finite).

So, cardinality is not the right tool to use to check type isomorphism in the presence of polymorphic types. We really need to see if it is possible to craft the isomorphism function and its inverse, as the ones you posted in your question.

Answer 2

The cardinality argument doesn't really work with polymorphic types (see @chi's answer).

But isomorphism itself can be intuitively explained like this:

The type forall r. (a -> r) -> r means "if you give me a function that converts a to r, I can give you back an r. Oh, and I can do this for any possible r whatsoever"

The only way to fulfill such promise is by secretly having an a in my hand.

Since I promise to do this for any possible r, it means I can't know anything about r itself, including how to construct a value of it. And the only thing I have available is the function a -> r that you give me. And the only way to call such function is by giving it an a.

This means that if I'm making such promise, I must already secretly have an a behind my back.

---

For a more formal explanation, recall that "isomorphic" in plain terms means "can be unambiguously converted back and forth without losses". This is what the cardinality argument is getting at: if you have the same number of things, you can always arrange a pairing between them.

And in your question you already show the two conversions: cont converts one way, unCont converts the other. And you can trivially show that cont . unCont = unCont . cont = id. Therefore the types are isomorphic.

While showing the existence of the two conversions is more formal, I find it's not always satisfactory for getting an intuition for how the two types are really "kinda the same thing", hence the intuitive explanation I gave above.