Algebraically interpreting polymorphism

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

Leave a Comment

Hata!: SQLSTATE[HY000] [1045] Access denied for user 'divattrend_liink'@'localhost' (using password: YES)