# reperiendi

## Yoneda embedding as contrapositive and call-cc as double negation

Posted in Category theory, Math, Programming by Mike Stay on 2008 January 26

Consider the problem of how to represent negation of a proposition $P$ when we only have implication and falsehood: $P \to {\rm F}.$

Since ${\rm F} \to {\rm F}$ is true and ${\rm T} \to {\rm F}$ is false, this does what we want.

The contrapositive says $\neg Q \to \neg P$ has the same truth value as $P \to Q.$ Using only implication, the contrapositive of $P \to Q$ is $(Q \to {\rm F}) \to (P \to {\rm F}).$

What if we don’t even have falsehood? Well, we can pick any proposition $X$ to represent falsehood and form $(Q \to X) \to (P \to X).$

The Yoneda embedding takes a category $C^{\rm op}$ and produces a category $\mbox{HOM}(C, \mbox{Set})$: $\begin{array}{ccccccc}\mbox{Yoneda}_X: & C^{\rm op} & \to & \mbox{HOM}(C, \mbox{Set}) \\ & P & \mapsto & \mbox{hom}(P, X) \\ & f:P \to Q & \mapsto & \mbox{Yoneda}_X(f): & \mbox{hom}(Q, X) & \to & \mbox{hom}(P, X) \\ & & & & k & \mapsto & k \circ f \end{array}$

This embedding is better known among computer scientists as the continuation passing style transformation.

In a symmetric monoidal closed category, like lambda calculus, we can move everything “inside:” every morphism $f:P \to Q$ has an internal version $f:I\to P \multimap Q.$ The internal Yoneda embedding of $f$ is $\mbox{Yoneda}_X(f):I \to (Q \multimap X) \multimap (P \multimap X).$

Here $I$ is the “unit” type; notice how the target type is isomorphic under the Curry-Howard isomorphism to the contrapositive. This is a term that maps a continuation $k:Q\multimap X$ and a value $p:P$ to $k(f(p)).$

To get double negation, first do the Yoneda embedding on the identity to get $\mbox{Yoneda}_X(1_P):hom(P,X) \to hom(P,X),$

then uncurry, braid, and recurry to get $\mbox{Yoneda}_X(1_P):P \to hom(hom(P,X),X),$

or, internally, $\mbox{Yoneda}_X(1_P):I\to P \multimap ((P\multimap X)\multimap X).$

This takes a value $p$ to a function value $k\mapsto k(p).$

Call-with-current-continuation expects a term that has been converted to CPS style as above, and then hands it the remainder of the computation in $k.$

Advertisements

### 2 Responses

Subscribe to comments with RSS.

1. haroldtherebel said, on 2008 January 30 at 11:35 pm

I believe you have a typo on the third line. While “F -> T” is certainly true, it would make more sense to mention that “F -> F” is true.

2. reperiendi said, on 2008 January 31 at 8:55 am

Good catch, thanks! Fixed.