# Encryption and Adjunctions

This post goes pretty deep into Category Theory, fairly quickly. For explanations of some of the concepts used in this post, I highly recommend this blog. The post on adjunctions is especially relevant.

In Category Theory, a monad is (loosely) defined as a functor \(T\) with two natural transformations:

\[\begin{aligned} \eta &: Id \to T \\ \mu &: T \circ T \to T \end{aligned}\]I wondered what it would look like to replace the \(\mu\) with a slightly different natural transformation:

\[\mu' : T \circ T \to Id\]My intuition was that this might be useful for some kind of security application. If the functor represented some kind of encryption, then \(\eta\) allows one party to encrypt some data, and \(\mu'\) allows the data to be used after being properly decrypted.

In practice, however, this didn’t quite make sense. The biggest problem was that encryption and decryption are inverses, but they aren’t symmetric. It seemed that if this was going to work, I’d need two functors (call them \(L\) and \(R\)), and a natural transformation:

\[\epsilon : L \circ R \to Id\]One party can encrypt some data using \(R\), and the other can apply \(L\) and use \(\epsilon\) to retrieve the data.

If you know some Category Theory, you might know where this is going: adjunctions! An adjunction is a pair of functors \(L\) and \(R\) with the following natural transformations:

\[\begin{aligned} \eta &: Id \to R \circ L \\ \epsilon &: L \circ R \to Id \end{aligned}\]We write \(L \dashv R\) to express this condition. Note that \(\epsilon\) is
exactly what we wrote before! If we want to represent encryption as a pair of
functors, it would be smart to choose two *adjoined* functors. (If you’re
curious, the \(\eta\) can actually be understood as the same \(\eta\) from the
monad definition. For any adjunction, \(R \circ L\) is a monad.)

Since we’d like this construct to be useful, we want candidates for \(L\) and
\(R\) that are endofunctors (functors from a category to itself) in the category
where objects are **types**, and morphisms are **pure functions**. (This
category is often called \(Hask\), named after the Haskell programming
language.) One such adjunction is

where \(L\) is the product (or `Tuple`

) functor, and \(R\) is the exponential
(or `Reader`

) functor. Using actual code (I’m
using Idris here), the functors are just data
types, and are written as follows:

We can convince ourselves that these functors are adjoined by implementing
\(\eta\) and \(\epsilon\), which are polymorphic functions that are
conventionally called `unit`

and `counit`

respectively:

But what does any of this have to do with encryption? To answer that question,
we really need to figure out better names for `L`

and `R`

. Let’s start with `R`

.
The key insight here is that `R`

sort of *hides* data behind a function call. It
takes a value of type `a`

, and requires that we have a value of type `k`

if we
want our value back. Let’s rename `R`

to `Encrypted`

, and write a function
`encrypt`

as follows:

This function is the reason that I opted to use a dependently typed language
like Idris over a more standard language. In order to get any use out of this
function, we need to be able to specify what type `k`

actually is; that requires
passing a type to encrypt as if it were data.

Now that we have the `Encrypted`

functor, we can make a guess at what `L`

is
supposed to be. The name I settled on (somewhat unsurprisingly) was `Decrypter`

;
this is because the key contained within the tuple can be used to decrypt some
encrypted value.

If we rewrite `counit`

from before, we can finally get:

With all of this machinery, we can:

- Pick a type
`k`

; in a dependently typed language, this type can be a proof of some sort. - Call
`encrypt k`

on some value of type`a`

to get an`Encrypted k a`

. - Use the
`MkDecrypter`

constructor, along with a valid value of type`k`

to make a`Decrypter k (Encrypted k a)`

. - Call
`decrypt`

to get the original value out.

## Conclusion

My main purpose with this exploration was to gain a deeper understanding of how
Category Theory interacts with real-world programming problems. While the end
result is not particularly useful, it does give some interesting insight into
what a *proof-relevant* encryption system would look like.

In addition, I found it extremely interesting how two inverse concepts like encryption and decryption map nicely onto adjoined functors. While it is easy to see that adjoined functors are inverses conceptually, it is exciting to see how they model those behaviors in practice.