Basic Example of Yoneda Lemma?

Computer scientists do use quite a few algebraic structures, they are just slightly different from the ones mathematicians usually focus on. Computer scientists tend to care about monoids, semigroups, semirings, and seminearrings. For example, the free monoid on some set $\Sigma$ is just the list $\Sigma^*$. A deterministic finite state automaton is just a monoid action of the free monoid on a finite set. Relatedly, the operators of regular expressions form a star semiring. In fact, many things in CS form a star semiring which leads to surprising connections.

Anyway, when you hear about the Yoneda lemma, you invariably hear about it's corollary, the Yoneda functor is full and faithful. All this means is $$\text{Nat}(\text{Hom}(\_,A),\text{Hom}(\_,B)) \cong \text{Hom}(A,B)\text{ and} \\ \text{Nat}(\text{Hom}(A,\_),\text{Hom}(B,\_)) \cong \text{Hom}(B,A)$$ natural in $A$ and $B$. A key general result is a fully faithful functor reflects isomorphisms. That is, if $F$ is fully faithful and $FX \cong FY$ then $X \cong Y$. You should prove this. (All functors preserve isomorphisms.) Specializing, this means if $\text{Hom}(A,X) \cong \text{Hom}(A,Y)$ natural in $A$, then $X \cong Y$, and similarly for the other argument of $\text{Hom}$. For example, here's a proof that left adjoints preserve coproducts (basically the same proof will show that left adjoints preserve all colimits). Assume $F \dashv U$, i.e. $\text{Hom}(FA,X) \cong \text{Hom}(A, UX)$ natural in $A$ and $X$. The defining property of a coproduct is the following $\text{Hom}(A+B,\_) \cong \text{Hom}(A,\_)\times\text{Hom}(B,\_)$. The proof: $$\begin{align} \text{Hom}(F(A+B),\_) &\cong \text{Hom}(A+B,U\_) \\ &\cong \text{Hom}(A,U\_)\times\text{Hom}(B,U\_) \\ &\cong \text{Hom}(FA,\_)\times\text{Hom}(FB,\_) \\ &\cong \text{Hom}(FA+FB,\_) \end{align}$$ By Yoneda, we have $F(A+B) \cong FA + FB$. This use of Yoneda is so ubiquitous that it is usually used tacitly. (As a side note, I highly recommend this chain-of-isomorphisms style of doing category theory which is driven by the notion of a representable functor. Combined with (co)ends, huge swathes of categorical proofs become this easy.)

Monoid actions have a particularly nice representation in category theory, since monoids can be viewed as one-object categories. Let $M$ be a monoid viewed as a category. A (left) $M$-action is a functor $M \to \mathbf{Set}$. Call the one object $\star$. (A right $M$-action is a functor $M^{op}\to\mathbf{Set}$.) By definition $\text{Hom}(\star, \star) = M$ where here we're viewing $M$ as just a monoid. When we have a $M$-action, $\phi$, on a set $X$, we mean $\phi(\star) = X$.

The Yoneda lemma then states that for a $M$-action, $\phi$, each element $x\in\phi(\star)$ corresponds to a function $h_x : M \to \phi(\star)$ which satisfies $h_x(m_1 m_2) = \phi(m_1)(h_x(m_2))$ and $h_x(1)=x$. Since the Yoneda lemma, $\text{Nat}(\text{Hom}(C,\_),F)\cong FC$, is also natural in $C$, we have that monoid action $\phi$ is essentially the same thing as the collection of functions $\{h_x\mid x\in X\}$ with the constraint that $h_x(m_1 m_2) = h_{\phi(m_2)(x)}(m_1)$ which follows from the properties of the $h_x$. The Yoneda lemma is thus the statement that the representation of a monoid action as a monoid homomorphism into an endofunction monoid, which is what the functor view essentially is, is equivalent to the more typical representation as a function $M\times X \to X$ satisfying certain properties. The universal property of the free monoid $A^*$ is that a monoid homomorphism, $A^*\to M'$ is corresponds to an arbitrary function $A\to M'$. (This is a special case of a free category generated from a directed (multi)graph.) With this representation of $A^*$-actions, one direction of the Yoneda lemma is essentially the right fold operation (though most of the work is being done by freeness). For automata, right $\Sigma^*$-actions make more sense than left ones. The same calculation will produce a left fold in that case.

A lot of category theory can be considered a categorification of order/lattice theory ideas. Decategorifying a categorical concept usually produces a useful concept in order theory. Abstract interpretation is one area in CS where order theoretic ideas are used heavily. Instead of viewing posets as special categories, I like to view them as $\mathbf{2}$-enriched categories or, equivalently, as (0,1)-categories. This may sound intimidating, but actually makes things much simpler and clearer. (I wish someone had suggested that I view the Sub functor as an indexed (0,1)-category.)

The upshot is instead of having a family of hom-sets, we have a single hom-relation. In this context, often the notion of an upward-/downward-closed set is used. Let $\mathbf{2}\equiv\{\bot,\top\}$ with the ordering $\bot\leq\top$. An upward closed subset of a poset $X$ can be identified with a monotonic function $X \to \mathbf{2}$ which can be made in a poset by using the point-wise ordering. You can check that if $f : X \to \mathbf{2}$ is monotonic and we define $U = \{x\in X\mid f(x)=\top\}$, then $U$ is upward-closed, i.e. if $x\in U$ and $x\leq y$ then $y \in U$. Furthermore, the pointwise ordering on functions corresponds to the subset ordering. Write $\text{Up}(X)$ for the set of upward-closed subsets of $X$ with the subset ordering. Write $\text{Down}(X)\equiv\text{Up}(X^{op})$ for the set of downward-closed sets. The Yoneda embedding is then $\mathcal{Y}(x) = \{y\in X\mid y \leq x\}$ and $\mathcal{Y} : X \to \text{Down}(X)$ is a monotonic function. The Yoneda lemma is then the statement for $U \in \text{Down}(X)$: $$x \in U \iff \forall y\in X.y\leq x \Rightarrow y \in U$$ The co-Yoneda lemma then says $$x \in U \iff \exists y\in X. x\leq y \land y \in U$$

Programming with continuations

You may have seen the continuation-passing style of programming. Starting with a subroutine like this:

function f (x, y, z) {
  return [result]
}

...you alter it so that instead of returning its result directly, the subroutine returns another subroutine that allows you to process that result before returning it:

function f (x, y, z) {
  return function(CONTINUE_FN) { 
         return CONTINUE_FN([result])
  }
}

That is, instead of returning result directly, it returns another subroutine; you pass a function $g$ to that subroutine and it returns $g(result)$. For example, if you pass the identity function g(x){return x}, it'll just return the result directly.

This paradigm is useful for when you want to decide how to further process/handle return values at a later, asynchronous time. It is useful for event handling, exception handling, and co-routines, for example.

The Yoneda lemma proves that the direct style of programming and the continuation-passing style of programming are equivalent (naturally isomorphic).

Indeed, consider the datatypes returned by the direct and continuation-passing variants. Say the direct subroutine returns objects of type $\mathsf A$. The continuation subroutine instead returns a function. That function takes in a continuation $\mathsf A \rightarrow \mathsf R$, where $\mathsf R$ can be any data type, and returns a result of type $\mathsf R$.

The fact that these return structures are equivalent is an isomorphism:

$$\mathsf A \cong (\mathsf A \Rightarrow \mathsf R) \Rightarrow \mathsf R$$

This equivalence, as can be made precise, is an application of the Yoneda Lemma in the case where the functor is just the identity functor:

$$\mathrm{Nat}( \hom(\mathsf{A}, -), \mathrm{id}) \cong \mathrm{id}(\mathsf A)$$