Navid's Awesome Site!

Welcome to My Awesome Site!

Mathematics of Types - A 90s GeoCities Tribute!

Mathematics of Types

22 Jan, 2025

This post is my understanding of a paper by Conor McBride titled "The Derivative of a Regular Type is its Type of One-Hole Contexts." But before we get to calculus, let's start with something simpler, like algebra.

I will use Scala for this post because it's a beautiful and concise language with amazing support for algebraic data types. But many modern languages also have good support ADTs, pick your poison.

Algebra

To talk about how types can even have algebras, let's first understand what an algebra even is. An algebra is something that has:

  • Symbols (Things)

    • In your school algebra you had concrete symbols like 0, 1, 2 or generic symbols (or variables) like x, y etc. In the algebra of types our symbols are types, such as Unit, Int, Boolean, or generics types, as in parametric polymorphism

  • Operators (How to make new things)

    • In your school algebra these were ways to combine the numbers to make new numbers like +, −, ×, ÷. They are not Symbols themselves, but they are symbol constructors. In the algebra of types these are ways to combine types to get new types like List, Option and Either. They are not types themselves but type constructors.

  • Laws (Rules that things follow)

    • We will get into Laws in a bit, but just for reference, these are rules like 0 × x = 0 or 0 + x = x

Symbols

Types can have a 1 to 1 relationship to numbers (an isomorphism), so we can reuse and explore a lot of what we know from school algebra already. How can we assign numbers to types? One way to do it would be to count the number of values inhabited by that type. We are looking at types as bags of values (I am avoiding the word Set on purpose).

For example, how can we represent 0? We need a type that has no members at all, or a so-called Bottom Type. One that you can never actually instantiate. In Scala's type system, it's called Nothing. You could even make your own enum with no members. (Unfortunately, the enum keyword expects at least one variant but you can always make a sealed class with no subclasses.)

sealed abstract class Zero

What about 1? A type that is only occupied by a single value, or a so-called Unit Type In Scala there's Unit. This could also be any type that has exactly one element. Like an empty option.

type One = None
type One = Nil

What about 2? A type that is either something or something else, doesn't really matter what those things are, the important part is that there are 2 of them. An obvious choice is Boolean. How about 3? I can't think of a type in the base language but you can always make your own!

enum Color:
    case Red, Green, Blue

So the idea is that types are bags that contain some countable number of values and you can think of that count as their counterpart in school algebra.

Operations: Addition

Let's explore what operations look like for types. A simple one is the addition operator. For instance, let's explore what 2 + 3 would look like in the land of types. We already established that 2 is Boolean. A bag that holds {true, false}. And 3 is Color. A bag that holds {Red, Green, Blue}. We also know 2 + 3 = 5. How can we combine Boolean and Color to a bag that has 5 variants? Namely {true, false, Red, Green, Blue}. With an enum of course!

enum Five:
    case Two(boolean: Boolean)
    case Three(color: Color)

You can just add arbitrary numbers and you can also just add arbitrary types. This is why enums are also called sum types.

enum +[A, B]:
    case Left(a: A)
    case Right(b: B)
type Five = Boolean + Color

Actually, many languages have a built-in type constructor for addition, like Scala's Either or Rust's Result, commonly used for error handling.

type +[A, B] = Either[A, B]
type Five = Boolean + Color

Operations: Multiplication

The next operator to explore is multiplication, we will now try to represent 2 × 3 = 6 to try to find a way to combine Boolean and Color to create a new type with 6 variants. You can do this by creating pairs of these values. {(true, Red), (true, Green), (true, Blue), (false, Red), (false, Green), (false, Blue)}

How can we represent this in code? With something like a struct or a class.

case class ×[A, B](a: A, b: B)
type Six = Boolean × Color

Again, many languages also support tuples which let you multiply as many types as you want. This is why classes and tuples are called product types.

Operations: Exponentials

An interpretation of exponentials is to represent them as enumerating choices. When writing code, you choose what to return based on an input. So in some sense exponentials are functions. For a signature Color => Bool, let's enumerate all the choices you can make on how to implement it.

type Choice = Color => Bool
val allTrue: Choice = _ => true // 1
val allFalse: Choice = _ => false // 2
val isRed: Choice = _ == Color.Red // 3
val isGreen: Choice = _ == Color.Green // 4
val isBlue: Choice = _ == Color.Blue // 5
val notRed: Choice = _ != Color.Red // 6
val notGreen: Choice = _ != Color.Green // 7
val notBlue: Choice = _ != Color.Blue // 8

There are 8 ways to implement this. For any function A => B you have B different possible return values for each value of A so you can think of it as BA.

type Exp[Base, Exponent] = Exponent => Base

Laws

Armed with what we learned so far we can now try to interpret some basic laws in algebra, with types. We can then observe that Algebraic Laws translate into refactoring transformations that we can apply to our code.

Let's take a simple law and observe how it translates to Scala.

0 + X = X
Either[Nothing, X] ≈ X

To translate this into words, we know at compile-time that this Either can never be occupied by a Left variant. That would imply that you managed to instantiate a value of type Nothing, which we KNOW is empty and has no inhabitants. Either[Nothing, X] is ALWAYS some Right(x). So you could just treat it as an X. It is isomorphic to it. Let's look at another one.

1 × X = X
(Unit, X) ≈ X

Tupling any X with Unit, does not add any information to X. You can always tuple X with Unit and strip that Unit back again. So it is isomorphic X. Let's look at something slightly less trivial and slightly more useful.

(A × B)X = AX × BX
(A, B) => X ≈ (X => A, X => B)

An exponential of a product is equivalent to the product of each component exponentiated. This translates into code that any function returning a tuple can be unzipped into a tuple of two functions.

Lists

We are now going to try to represent a recursive type. Singly linked lists are implemented in many functional languages as cons lists. With a representation similar to the following:

enum List[A]:
    case Nil
    case Cons(head: A, tail: List[A])

Let's try to represent this algebraically.

List[A] = 1 + A × List[A]

This definition is recursive because List[A] is defined in terms of List[A]. We can use this definition to substitute the List[A] on the right-hand side. Doing this once yields:

List[A] = 1 + A × (1 + A × List[A]) = 1 + A + A² × List[A]

We can do this again!

List[A] = 1 + A + A² × (1 + A × List[A]) = 1 + A + A² + A³ × List[A]

Doing this substitution infinitely many times yields:

List[A] = 1 + A + A² + A³ + A⁴ + ...

It turns out singly linked lists are just the geometric series!

List[A] = ∑ k=0 to ∞ Aᵏ

You can justify this to yourself this way, a List[A] is one of:

  • Empty (1)
  • A single element of type A (A)
  • Two elements of type A (A²)
  • Three elements of type A (A³)
  • Four elements of type A (A⁴)
  • ...

Now, I am going to abuse our mathematical notation a bit. Let's go back to our original definition of cons lists.

List[A] = 1 + A × List[A]

We can find the value of List[A] by isolating all the List[A]s on the left-hand side of the equation. Let's ignore for now that we don't even know what subtracting two types means.

List[A] - A × List[A] = 1

We can now factor out List[A] from the left-hand side of this equality.

List[A] × (1 - A) = 1

Now we can isolate List[A] on the left-hand side by dividing both sides by 1 - A. Of course for now we just ignore that we don't know what this operation really means for types.

List[A] = 1 / (1 - A)

You might have already noticed, that this is the closed form of the geometric series (under specific bounds, but we are playing incredibly fast and loose with both mathematics and type theory, for fun and profit).

Here is the fun part. We can actually take the Taylor expansion of this expression to regain our original definition of lists!

First, let's recall that the Taylor expansion around the point a for a function f can be represented as

f(x) ≈ ∑ n=0 to ∞ f⁽ⁿ⁾(0) / n! * xⁿ

Also, notice that

dⁿ / dxⁿ (1 / (1 - x)) = n! / (1 - x)⁽ⁿ⁺¹⁾

Around the point 0 this simplifies to 1 / (1 - x)⁽ⁿ⁾(0) = n!

Plugging this back in, we get

List[A] = 1 / (1 - x) = 1 + 1/1! x + 2/2! x² + 3/3! x³ + ... = 1 + x + x² + x³ + ...

The fact that we can use Taylor expansions will later help us turn seemingly meaningless expressions, into ones that are meaningful in the landscape of types. If you want to read a bit more about negative and fractional types this paper could be a good read.

Trees

Another fundamental recursive type is the binary tree, so let's look at those next. One representation of a binary tree is the following:

enum Tree[A]:
    case Leaf
    case Branch(left: Tree[A], value: A, right: Tree[A])

I hope by now you can see that this can be represented algebraically as:

Tree[A] = 1 + A × Tree²[A]

This is in fact a quadratic equation! And you hopefully remember the formula we can use to solve these kinds of equations:

x = (-b ± √(b² - 4ac)) / 2a

Plugging that in we get:

Tree[A] = (1 - √(1 - 4A)) / 2A

That is absolutely horrifying. But fret not, remember that Taylor expansions can save us. Going through the motions we can actually derive the infinite series form of a binary tree as:

Tree[A] = 1 + 1A + 2A² + 5A³ + 14A⁴ + ...

We have discovered a way to count the number of possible binary trees of any size!

  • The number of empty binary trees is 1
  • The number of binary trees with a single element is also 1
  • There are 2 binary trees of size 2
  • There are 5 different binary trees of size 3
  • There are 14 different binary trees of size 4

By the way, these particular coefficients show up a lot in counting problems, they are called Catalan numbers if you want to read more about them!

Zippers

Let us take a small detour from Algebras to talk about a very useful family of data structures called Zippers. To motivate them, let's assume that you are building a text editor. And of course, you are doing it in a purely functional way! A document is usually built up of many lines. Each line is a sequence of characters and you have decided to represent each line as a singly linked list List[Char]. Your cursor can go anywhere in that line and you want to be able to quickly jump between characters with your cursor and edit the text. By quickly I mean you want to do it in O(1) time complexity. Zippers are exactly the data structure you need. Let's assume that your line has the following text:

the quick brown fox ju[m]ps over the lazy dog.

Your cursor (the focus element) is on the letter m in the word jumps. The requirements are that you need O(1) access to the letters immediately neighboring the focus element. In this case, you need to quickly switch the focus to u on the left side (j[u]mps) or p on the right side (jum[p]s). What kind of data structure would give you this desired time complexity?

Let's separate the line into 3 different segments. The left segment, the focus element, and the right segment.

[the quick brown fox ju], 𝐦, [ps over the lazy dog.]

Consider for now only the right segment. If the right segment is a singly linked list of all the characters to the right of the focus element, then we can, in O(1) time, decompose the right segment into a head and a tail.

[the quick brown fox ju], 𝐦, 𝐩::[s over the lazy dog.]

The head (p) is now the new focus element, and the tail (s over the lazy dog.) is the new right segment. So far so good. However, we now need to append the old focus element to the end of the old left segment. This is bad in the current setup because appending to the end of a singly linked list takes O(n) time.

But all is not lost, what if we kept the left segment in reverse order instead?

[uj xof nworb kciuq eht], 𝐦, [ps over the lazy dog.]

Now after peeling off p we can prepend them to the beginning of the left segment in O(1) time to get:

[muj xof nworb kciuq eht], 𝐩, [s over the lazy dog.]

Conversely, if you wanted to move the cursor to the left, you can decompose the left segment into a head (u) and a tail (j xof nworb kciuq eht). Now the head is the new focus element, and the tail is the new left segment. The old focus element m can now be prepended to the right segment in O(1) time to give you:

[j xof nworb kciuq eht], 𝐮, [mps over the lazy dog.]

They are called Zippers because you can imagine the focus element as the zipper-pull on your jacket's zipper. It can zip up and down and focus on the right "tooth".

the quick brown fox ju←m―ps over the lazy dog.→

In your cool new text editor, you can have two zippers, one for the cursor in the current line and another for the current line in the document!

Don't forget that this is only the zipper for a singly linked list, any immutable data structure can have its own zipper, and that zipper will let you focus on an element and edit that immutable data structure efficiently. So far then, we know, that a zipper for a List[A], is an A, alongside two List[A]s for the left and right segment.

Zipper[List[A]] = (List[A], A, List[A])

One-Hole Context

A one-hole context is the same thing as a zipper, except that there's a hole in place of the focus element!

Zipper: the quick brown fox ju←m―ps over the lazy dog.→

One Hole Context: the quick brown fox ju←◯ps over the lazy dog.→

So the one-hole context of a List[A] is two List[A]s (the left segment and the right segment), forgetting the current focus.

Zipper[List[A]] = (List[A], A, List[A])
OneHoleContext[List[A]] = (List[A], List[A])

Now, as an exercise let's examine the one-hole context of tuples of increasingly bigger sizes. We will do this by selecting a focus element and looking at the "leftovers".

First a Tuple1 or a single element. In this case, you can only focus on that single element. What is left around it is Unit (If this doesn't make sense, remember you can always Tuple anything with Unit because X × 1 = X).

OneHoleContext[(A)] = 1

Let's go one size up, what about a tuple with 2 elements like (A, A) or A²? You can either focus on the left A then your leftover is the right A, or you can focus on the right A and your leftover is the left A. So it is A + A = 2A.

OneHoleContext[(A, A)] = (◯, A) + (A, ◯) = 2A

Now let's try a tuple of 3 As like (A, A, A) or A³. Similarly, you can select any of the 3 As to be the hole and you are left with 2 other As. So the one-hole context is 3A².

OneHoleContext[(A, A, A)] = (◯, A, A) + (A, ◯, A) + (A, A, ◯) = 3A²

Do you notice something funky? The one-hole context seems to be the derivative of the type! The one and the same derivative you learned in high school. As a side note, I find it hilarious that in the paper Conor writes this absolutely unhinged sentence:

"As I wrote down the rules corresponding to the empty type, the unit type, sums, and products, I was astonished to find that Leibniz had beaten me to them by several centuries: they were exactly the rules of differentiation I had learned as a child (???)."

Anyway, let's confirm this by checking a List[A].

OneHoleContext[F[x]] = d/dx F[x]

Recall from previous sections that List[A] = 1 / (1 - A). Taking a derivative of both sides yields:

OneHoleContext[List[A]] = d/dA (1 / (1 - A)) = 1 / (1 - A)²

The derivative of List[A] is List²[A] or two lists. Just as we discovered earlier

Under Construction New! Generate your own 90s page here! Under Construction