There is a branch of Mathematics called “Type Theory” that studies the “type” of things. For example, the type of the real number $\pi$ can be said to be the real numbers $\mathbb{R}$. Usually, we would write this as $\pi : \mathbb{R}$ because $\pi$ is of type $\mathbb{R}$. Here are more examples:

• $2 : \mathbb{Z}$
• $\frac{8}{9} : \mathbb{Q}$
• $0.110100100010000 \dots : \mathbb{R}$
• $\{1, 2, 3\} : \mathbf{Set}$¹
• $\mathbb{R} : \mathbf{Set}$
• $(4, 2) : \mathbb{Z} \times \mathbb{Z}$

These are all pretty normal, where it gets interesting is when giving a function a type. For example, consider this map $x \mapsto x + 1$ which simply adds $1$ to its argument. We can say that it takes an integer and produces an integer. This is denoted as $\mathbb{Z} \to \mathbb{Z}$. Before moving on, there is some more intuition here. Because $x \mapsto x + 1$ has type $\mathbb{Z} \to \mathbb{Z}$, we know that $x : \mathbb{Z}$. Furthermore, we know that $1 : \mathbb{Z}$. We are adding two integers, $x : \mathbb{Z}$ and $1 : \mathbb{Z}$, so we know this will result in an integer as well $x + 1 : \mathbb{Z}$.

Interestingly, we can also make functions that return functions. A function that returns a function could be: $x \mapsto y \mapsto x + y$. If I add parentheses this becomes clearer $x \mapsto (y \mapsto x + y)$. The thing that the first function returns is $y \mapsto x + y$ which is itself a function as well. So a type for the first function could be $x \mapsto y \mapsto x + y : \mathbb{Z} \to (\mathbb{Z} \to \mathbb{Z})$. Usually, we don’t write the parentheses in a function type like that, in the same sense that we don’t write the parentheses in $x \mapsto y \mapsto x + y$ so we get:

$$ x \mapsto y \mapsto x + y : \mathbb{Z} \to \mathbb{Z} \to \mathbb{Z}. $$

As you can see, we are able to create types out of functions. As it turns out, one can go the other way as well. Creating a function from a type, which is not as easy as deriving the type from a function. This is called the Curry-Howard-Lambek isomorphism. We have two directions here: creating types from functions and creating functions from types. I’ll call the former the “forward” direction and the latter the “backward” direction. This essay will focus on the “forward” direction since it’s what is most useful to programmers. The “backward” direction is useful for Mathematicians since this is the basis for proof languages like Lean, Idris and Coq among others.

I’d like to make explicit two kinds of types that we’ve seen already:

• the function type $A \to B$
• the tuple type $A \times B$

Usually these are called the “exponential” type and the “product” type. The place they come from will inform a third very necessary type. The intuition to see why these are named that way comes from observing the structure in the category of sets $\mathbf{Set}$. In the category of sets, types² are sets as well. In other words, the type of functions from $A \to B$ in $\mathbf{Set}$ is just another set. As we saw in my previous essay about equality, the structure in $\mathbf{Set}$ is highly intertwined with the cardinality of sets. In the second essay I wrote: functional equality, we saw that the set of functions from $A$ to $B$ has cardinality $|B|^{|A|}$. This is why the type $A \to B$ is called an exponential type. So much so, that it’s even usual to see category theorists denote this simply as $B^A$.

Something interesting happens when we consider the set corresponding to the type $A \to B \to C$. Let’s put the parentheses back: $A \to (B \to C)$ and now denote it like a category theorist: $(B \to C)^A$. But, we can do this again, yielding $\left(C^B\right)^A$. If these were cardinalities, we can use the property that $\left(|C|^{|B|}\right)^{|A|} = |C|^{|B| \times |A|}$ to simply say that $\left(C^B\right)^A$ is the same type as $C^{B \times A}$. The cardinalities are respected so these sets are, for all intents and purposes³, the same set. Now, if we go back and try extracting the function type from this exponential we get that $C^{B \times A}$ is the same type as $B \times A \to C$. Since products of cardinalities are commutative this is the same type as $A \times B \to C$. So, we can finally say that $A \to B \to C$ is the same type as $A \times B \to C$. This is called Currying.

We can use this idea to unlock the third, equally as important, kind of type. Consider the type $(A \to B) \times (C \to B)$. Very strange and convoluted, but you’ll see where it comes from once we arrange it as an exponential. This type would look like this: $B^A \times B^C$. Changing this to cardinalities we get that $|B|^{|A|} \times |B|^{|C|} = |B|^{|A| + |C|}$. But, what set has cardinality $|A| + |C|$? The disjoint union of $A$ and $C$! This is denoted as $A \sqcup C$, you can think of this set as a bunch of items that are either $A$ or $C$, but never both. Practically, this is done by defining this set as $A \times \{0\} \cup C \times \{1\}$ giving you elements of the form $(a, 0)$ or $(c, 1)$. Usually category theorists denote this set as $A + C$ and call it a “coproduct”, that is what I’ll do as well. So, going back to types, this would be the type $A + C \to B$. Intuitively, an object of type $(A \to B) \times (C \to B)$ basically contains 2 functions that, when evaluated on $A$ or $C$, give you a $B$; and object of type $A + C \to B$ when evaluated on $A$ or $C$ give you a $B$.

Utility

As programmers what does this do for us? Well, observing constructions that occur naturally from the structure of $\mathbf{Set}$ let us program in a way that doesn’t go against the grain of what the structure expects from us. Many times, I have had the displeasure of interacting with programming languages that did not support products or coproducts or function objects as first-class objects. This did not mean that those kinds of types were completely impossible to encode in the language. What it means is that one would have to go through hoops, making complicated and most times non-idiomatic code just to be able to encode these basic types.

One would think that a programming language targeted primarily towards data scientist like R would support products as a first-class object. The closest one can get to a “product” is a data.frame which really just encodes an ordered list of products, not just a single product. In order to encode a single product, one would have to use a “vector”, which is not a tuple since tuples are fixed in size and can be of different types at each entry. This leads many R developers to use complicated external libraries to the language to get around this limitation.

Going more low-level, C completely lacks coproducts, having to use unions and enums in order to encode a coproduct, leading to the prolific term “tagged union”. I’ll give C credit where credit is due though, a pointer of the form *A works exactly how a coproduct of the form $A + \{0\}$ works. This coproduct is exactly what Rust’s Option, Haskell’s Maybe and C++’s std::optional encode, built-in to the language. The utility of having this built-in to the language is so known that the list data structure is still one of the first taught data structures, which relies on pointers to be implemented and has the the type (for a given type $A$)

$$\text{List}(A) = (A \times \text{List}(A)) + \{0\}.$$

More recently created languages like Zig and Hare have a notion of “error types”. Some functions can error, and instead of crashing the program, they instead return an error to the caller. This then lets the caller treat that error and decide what to do with it. This idea that functions can return their original types or an “error” is exactly what’s encoded by coproducts. I see the usefulness of telling the compiler to treat those coproducts in a special manner since you really want to be sure that you handled the error cases correctly, and the compiler can just scream at you in case you didn’t do that correctly. But, making this distinction between error types and normal types perpetuates the idea that coproducts aren’t actually supposed to be used by other parts of the program.

Fini

Astute readers might ask, why these three kinds of types? Well, this is directly what the Curry-Howard-Lambek isomorphism produced. Without the Curry-Howard-Lambek isomorphism, we wouldn’t be talking about any of this in the first place. I did not pull these three kinds of types out of thin air, they are inextricably linked to the structure of programs. In mathematics, we make them explicit and first-class. Products are $\land$ (logical AND), coproducts are $\lor$ (logical OR) and exponentials are $\implies$ (implication). When programming languages special-case any of these or simply not support them out of the box, we the programmers have to go out of our way to encode them ourselves. Languages can then decide whether they care enough about them to implement them, but, regardless of being implemented badly or not, I know that one thing will remain true:

we will still have a need to use them, and use them we will.