Algebraically interpreting polymorphism

Question

So I understand the basic algebraic interpretation of types:

Either a b ~ a + b (a, b) ~ a * b a -> b ~ b^a ()   ~ 1 Void ~ 0 -- from Data.Void 

... and that these relations are true for concrete types, like Bool, as opposed to polymorphic types like a. I also know how to translate type signatures with polymorphic types into their concrete type representations by just translating the Church encoding according to the following isomorphism:

(forall r . (a -> r) -> r) ~ a 

So if I have:

id :: forall a . a -> a 

I know that it does not mean id ~ a^a, but it actually means:

id :: forall a . (() -> a) -> a id ~ ()    ~ 1 

Similarly:

pair :: forall r . (a -> b -> r) -> r pair ~ ((a, b) -> r) - > r      ~ (a, b)      ~ a * b 

Which brings me to my question. What is the "algebraic" interpretation of this rule:

(forall r . (a -> r) -> r) ~ a 

For every concrete type isomorphism I can point to an equivalent algebraic rule, such as:

(a, (b, c)) ~ ((a, b), c) a * (b * c) = (a * b) * c  a -> (b -> c) ~ (a, b) -> c (c^b)^a = c^(b * a) 

But I don't understand the algebraic equality that is analogous to:

(forall r . (a -> r) -> r) ~ a 

Answer 1

This is the famous Yoneda lemma for the identity functor.

Check this post for a readable introduction, and any category theory textbook for more.

Briefly, given f :: forall r. (a -> r) -> r you can apply f id to get an a, and conversely, given x :: a you can take ($x) to get forall r. (a -> r) -> r.

These operations are mutually inverse. Proof:

Obviously ($x) id == x. I will show that

($(f id)) == f,

since functions are equal when they are equal on all arguments, let's take x :: a -> r and show that

($(f id)) x == f x i.e.

x (f id) == f x.

Since f is polymorphic, it works as a natural transformation; this is the naturality diagram for f:

               f_A      Hom(A, A)  →  A (x.)      ↓        ↓ x      Hom(A, R)  →  R                f_R 

So x . f == f . (x.).

Plugging identity, (x . f) id == f x. QED