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:

I wondered what it would look like to replace the \(\mu\) with a slightly different natural transformation:

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:

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:

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:

data L k a = MkL k a
data R k a = MkR (k -> a)

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:

unit : a -> R k (L k a)
unit x = MkR (\y => MkL y x)

counit : L k (R k a) -> a
counit (MkL y (MkR f)) = f y

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:

data Encrypted k a = MkEncrypted (k -> a)

encrypt : (k : Type) -> a -> Encrypted k a
encrypt _ x = MkEncrypted $ \_ => x

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.

data Decrypter k a = MkDecrypter k a

If we rewrite counit from before, we can finally get:

decrypt : Decrypter k (Encrypted k a) -> a
decrypt (MkDecrypter x (MkEncrypted f)) = f x

With all of this machinery, we can:

1. Pick a type k; in a dependently typed language, this type can be a proof of some sort.
2. Call encrypt k on some value of type a to get an Encrypted k a.
3. Use the MkDecrypter constructor, along with a valid value of type k to make a Decrypter k (Encrypted k a).
4. 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.