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 with two natural transformations:
I wondered what it would look like to replace the 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 allows one party to encrypt some data, and 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 and ), and a natural transformation:
One party can encrypt some data using , and the other can apply and use 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 and with the following natural transformations:
We write to express this condition. Note that 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 can actually be understood as the same from the monad definition. For any adjunction, is a monad.)
Since we’d like this construct to be useful, we want candidates for and 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 , named after the Haskell programming language.) One such adjunction is
where is the product (or
Tuple) functor, and is the exponential
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
and , which are polymorphic functions that are
But what does any of this have to do with encryption? To answer that question,
we really need to figure out better names for
R. Let’s start with
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
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
supposed to be. The name I settled on (somewhat unsurprisingly) was
this is because the key contained within the tuple can be used to decrypt some
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.
encrypt kon some value of type
ato get an
Encrypted k a.
- Use the
MkDecrypterconstructor, along with a valid value of type
kto make a
Decrypter k (Encrypted k a).
decryptto get the original value out.
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.