3 added 269 characters in body

If you program in a pure functional programming language like Haskell then the Yoneda lemma tells you that for any functor $F$, the types $F a$ and $\forall b . (a \rightarrow b) \rightarrow F b$ are isomorphic. (Restricting attention to computable total functions.) This really is a non-trivial statement and quite surprising when you first see it. Unfortunately it's tricky to explain without some CS backround.

Nonetheless I'll risk failure and try to explain a specific example when $F$ is the 'list' functor, assuming a little computing knowledge:

Fix a type $a$. Suppose you have a (polymorphic) Haskell function $f$ that for any type $b$ maps functions $g\colon a\rightarrow b$ into a list of elements of type $b$. Then $f$ is equal to a function that applies $g$ elementwise to some fixed list of elements of $a$. It's a powerful result. Just knowing the type of the function $f$ is enough to deduce significant detail about what it does. It can reduce the amount of work required to prove the correctness of programs.

The crucial thing that makes this work is that Haskell uses "parametric polymorphism". If you write a function that is polymorphic it's impossible to use specific knowledge about the type, you have to write your function generically to work with all possible types.

If you program in a pure functional programming language like Haskell then the Yoneda lemma tells you that for any functor $F$, the types $F a$ and $\forall b . (a \rightarrow b) \rightarrow F b$ are isomorphic. (Restricting attention to computable total functions.) This really is a non-trivial statement and quite surprising when you first see it. Unfortunately it's tricky to explain without some CS backround.

Nonetheless I'll risk failure and try to explain a specific example when $F$ is the 'list' functor, assuming a little computing knowledge:

Fix a type $a$. Suppose you have a (polymorphic) Haskell function $f$ that for any type $b$ maps functions $g\colon a\rightarrow b$ into a list of elements of type $b$. Then $f$ is equal to a function that applies $g$ elementwise to some fixed list of elements of $a$. It's a powerful result. Just knowing the type of the function $f$ is enough to deduce significant detail about what it does. It can reduce the amount of work required to prove the correctness of programs.

1

If you program in a pure functional programming language like Haskell then the Yoneda lemma tells you that the types $F a$ and $\forall b . (a \rightarrow b) \rightarrow F b$ are isomorphic. (Restricting attention to computable total functions.) This really is a non-trivial statement and quite surprising when you first see it. Unfortunately it's tricky to explain without some CS backround.

Nonetheless I'll risk failure and try to explain a specific example when $F$ is the 'list' functor, assuming a little computing knowledge:

Fix a type $a$. Suppose you have a (polymorphic) Haskell function $f$ that for any type $b$ maps functions $g\colon a\rightarrow b$ into a list of elements of type $b$. Then $f$ is equal to a function that applies $g$ elementwise to some fixed list of elements of $a$. It's a powerful result. Just knowing the type of the function $f$ is enough to deduce significant detail about what it does. It can reduce the amount of work required to prove the correctness of programs.