haskelltypesisomorphism

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

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!

Solution

  • 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.