Product Types

Just like we can do \(+\) and \(\times\) operations on numbers, we can also do them for types. We define the product of two types to be a pair. In Haskell, it’s a pair (a, b), like (Int, Bool). In C++ we have a similar structure std::pair, which is also a product type.

Why a pair is called a product? We can make sense of it by counting possible values. Suppose we have 2 possible values for Bool and 256 for Char, how many possible values we have for (Bool, Char)? The answer is \(2 \times 256 = 512\). Generally, if we have \(n\) possible value for type a, and \(m\) for type b, then (a, b) will have \(n * m\) possible values, that is why we denote (a, b) to be the product of a and b, or a * b. The counting method doesn’t work if a type has infinitely many possible value, like String, but even in this case, we still call pairs product types.

Commutativity and Associativity

The \(\times\) operation for numbers satisfies the commutative law and the associative law, which means \(a \times b = b \times a\) and \((a \times c) \times c = a \times (b \times c)\). Do we also have those laws for product types? Yes! For the commutative law, (a, b) and (b, a) and not strictly the same – they have different memory layouts, but they are isomorphic, which means there is a one-to-one function between them (here it’s just the swap function which exchanges the first and second member of the pairs). In this case, commutative law still holds – up to isomorphism. Similarly, associative law also holds, which means ((a, b), c) and (a, (b, c)) are isomorphic.

Identity Element

The product operation for numbers has an identity element 1 such that \(1 \times a = a\) and \(a \times 1 = a\). Note that product is commutative so it’s sufficient to specify either \(1 \times a = a\) or \(a \times 1 = a\). Do we also have such identity element for types? According to the approach of counting possible values, we want to find a type which has only one value. In fact, such a type is called a unit type. In Haskell the unit type is written as () and contains only one value: (). Similar types are void in C++, NoneType in Python (the corresponding value is None) and Unit in Scala (the value is ()).

Does \(1 \times a = a\) also holds for product types? Yes! It’s easy to argue that ((), a) and a are isomorphic. As a result, we say the set of types is a commutative monoid up to the product operation, since

• the product operation is associative (so it’s a semigroup)
• we have an identity element (the unit type) for the product operation (so it’s a monoid)
• the product operation is commutative (so it’s a commutative monoid)

Comparing with numbers, the set of numbers is also a commutative monoid, but the set of real numbers excluding 0 satisfies an additional property: Every element \(a\) in the set has an unique inverse element \(b\) such that \(a \times b = 1\), and we usually denote the \(b\) as \(a^{-1}\). The existence of the inverse element makes the set of real numbers excluding 0 a commutative group, and enables us to define the inverse operation of product, which is called division and defined as \(a / b = a \times b^{-1}\). We do not have the inverse element for types, so there is no division operation for types.

Sum Types

Similar to product, we define the sum of two types as an Either type.

data Either a b = Left a | Right b

How can we make sense of it? Again, the counting method. Suppose we have \(n\) possible value for type a and \(m\) for type b, how many possible values we have for Either a b? The answer is \(a + b\), so comes the name “sum types”.

The sum of two types is also commutative and associative up to isomorphism, which means

Either a b ~ Either b a
Either (Either a b) c  ~ Either a (Either b c)

(~ means isomorphic)

Identity Element

The identity element of numbers for \(+\) is 0, so what is the identity element for types? It should be a type with 0 possible values, so it’s called the empty type. In Haskell it’s Void and in Scala it’s Nothing. A lot of languages do not have such type, like C++. Note that the type void in C++ is a unit type instead of an empty type. Here is the difference between Haskell Void and C++ void.

In Haskell, we can define functions like this:

absurd :: Void -> a

Those absurd functions take type Void and returns any types. You cannot actually call them. Why? To call them you have to provide a value of type Void, but as we said, there is no such values because Void is empty.

In contrast, a C++ function whose argument is void could be called, just like the func below.

int func(void) {
    return 1;
}

int a = func();

Why? because you actually provide a special value, a value that is the only inhabitant of type void to the func function when calling it!

Similarly, In Haskell you cannot define a function which returns Void – because you cannot provide such a value to return! The Haskell equivalent of C++ functions returning void are functions returning (), the unit type.

In conclusion, C++ void is not an empty type but a unit type, and it’s equivalent to Haskell () instead of Void.

Note that in other languages, we have functions returning the empty type and they can be useful. For example, in Scala a function returning Nothing is used for situations like exceptions (i.e. the function does not return normally). Note that from the mathematical perspective functions should always return, so the Scala way of returning Nothing is kind of a hack. Generally we still think that there is no functions returning an empty type.

Let’s go back to sum type. Void is indeed the identity element for sum operation because Either Void a is isomorphic to a (there is no way to construct the Left version of Either Void a so it’s essentially the same as a). As a result, the set of types is also a commutative monoid up to the sum operation, and the identity element is the empty type Void.

Comparing with numbers, the set of numbers is a commutative group and the inverse element of number \(a\) is \(-a\). As a result, we can define the inverse operation of sum, which is called minus and defined as \(a - b = a + (-b)\). We don’t have a minus operation for types.

Summary of Product and Sum Types

Below is a table summerizing product and sum types.

Considering that the set of types:

• is a commutative monoid up to the sum and product operations
• satisfies the distributive law
• the identity element of sum is also the annihilating element of product

We call such structure a semiring, and the set of types is a semiring.

Interesting data types

Here are some interesting correspondence between algebraic expression and data types

In the table above, True, False and Nothing are all unit types because they contain only one value. If we are to define Bool and Maybe using Either, The definition will be

data Bool = Either () ()
data Maybe a = Either () a

List

A more interesting example is List, since it’s a recursive type

List a = Nil | Cons a (List a)

Such recursive types are equivalent to equations. For example, below is the corresponding equation of List. We just replace List a with \(x\).

$$ x = 1 + ax $$ The solution of this equation is \(x = \frac{1}{1-a}\). How to make sense of it? We did not define subtraction or division for types, so we should convert it to another form. Notice that \(\frac{1}{1-a}\) is the result of geometric series. As a result, we get

$$ \begin{aligned} x &= \frac{1}{1-a} \\ &= 1 + a + aa + aaa + \cdots \end{aligned} $$ The same equation could be obtained using Taylor series by expanding \(f(a) = \frac{1}{1-a}\) at point \(a_0 = 0\). Remember the Taylor series for \(f(x)\) at point \(x_0 = 0\) is

$$ f(x) = f(0) + \frac{f’(0)}{1!}x + \frac{f’’(0)}{2!}x^2 + \frac{f’’’(0)}{3!}x^3 + \cdots $$ If it does not make sense to you, you can also expand manually which gives the same result.

$$ \begin{aligned} x &= 1 + ax \\ &= 1 + a(1 + a \times x) = 1 + a + aax \\ &= 1 + a + aa(1 + ax) = 1 + a + aa + aaax \\ &= 1 + a + aa + aaa + \cdots \end{aligned} $$ What does it mean? It means a list is either empty (1), or a single element ($a$), or two elements ($aa$), or three elements ($aaa$), etc.

Or, in Haskell, someything like the following

List a = Nil 
        | Cons a Nil 
        | Cons a (Cons a Nil) 
        | Cons a (Cons a (Cons a Nil)) 
        | ... 

Binary Tree

Another example is the definition of binary trees

data BinaryTree a = Leaf a | Branch (BinaryTree a) (BinaryTree a)

The equivalent expression for numbers is

$$ x = a + x^2 $$ which expands to (either by Taylor series or manually) $$ x = a + a^2 + 2a^3 + 5a^4 + \cdots $$

It means, a tree is either

• a single leaf ($a$)
• a tree with 2 leaves ($a^2$)
• one of the two trees with 3 leaves ($2a^3$)
• etc.

Algebratic Data Types for other languages

In C++, besides representing a product type with std::pair, we can also use a struct or class. For example, the following is the product of int and bool and it’s isomorphic to a pair<int, bool>.

class Foo {
    int a;
    bool b;
}

As for sum types, there are a lot of different ways to represent them in C++, for example:

• Special values like negative values or null pointer could be used to represent Maybe
• Enum types are another example of sum types, where every enum value is equivalent to a unit type
• std::variant is used to simulate Either
• As an object oriented language, C++ also use subclasses to represent sum types. For example, say we have a base class Shape and two subclasses Circle and Square, it’s equivalent to data Shape = Circle | Square

In Scala, we mainly use case classes to represent product types and inheritance to represent sum types. For example, below is the definition of List in Scala where List is the sum of Nil and Cons, while Cons is the product of type A and a list.

sealed trait List[+A]

case object Nil extends List[Nothing]
case class Cons[+A](head: A, tail: List[A]) extends List[A]

While being a functional language, Scala defines algebratic data types using a different form than Haskell. It’s more similar to C++ such that product types are represented as classes and sum types are represented as subclass relations. That is because in addition of being functional, Scala is also an object oriented langauge.

Function Types and Exponentials

We already know that functions also have types. A function taking type a and returning b can be denoted as a -> b. Note that here we only consider pure functions with only one argument. Functions with multiple arguments could be obtained by currying. So how does function types fit into algebratic data types?

The answer might be surprising: function types are exponentials! In fact, the function type a -> b could be represented as \(b^a\).

Why? Here comes our old friend – counting possible values. Say we have type Bool which has 2 possible values, and type Char which has 256. How many possible functions are there from Char to Bool? The answer is \(\underbrace{2 \times 2 \times 2 \cdots \times 2}_{256}\), or \(2^{256}\). Generally, there are \(m^n\) possible functions from a type a with \(n\) values to a type b with \(m\) values, so the function type a -> b are denoted as \(b^a\). Even if there might be infinitely many inhabitants we still denote it as an exponential.

Below are the interesting laws about function types.

Conclusion

There is magical similarities between type algebra and number algebra. The similaries come from that we could define types algebraically, using constructs like sum, product and exponential.

Further Readings

I recommend the book (in the form of a series of blog posts) Category Theory for Programmers and the lecture videos (by the same author) if you want to learn more.