An algebra of types

Types can have an algebra. Apparently the idea is important in functional languages.

Algebraic expressions can also be compositions of other expressions, so for example we might see:

x*x

And similarly for data types:

int*int

To explain: the product of two types denotes the type of pairs of those types. In some languages, this might instead be written as pair but as we’ll soon see, it’s useful to think of this as a product.

Of course, the algebraic expression above could be simplified to x**2 (“x squared”) and so you could also write int**2.

Now, in an algebraic expression you might also see:

x+x

And the same concept exists for data types:

int+int

The sum of two types denotes the type of variants which can have values either of the left type or the right (but not both). The sum in the above type might seem superfluous, because whether a value of the above sum type has the left or the right type, it’ll be an int. However, there’s some additional useful information in knowing whether the left or right was chosen.

Consider, for example, a data type representing the balance of a bank account:

type balance = int + int

We might interpret values on the left as positive balances, and values on the right as negative balances. So if we wrote a function to describe a balance for screen-reading, it might look like:

string describe(balance b) {
if (b.is_left()) {
return “The bank owes you $” + b.left();
} else {
return “You owe the bank $” + b.right();
}
}

For many people, sum types are less obvious than product types. It may help to consider that, just as pair corresponds to product types, boost::variant corresponds to sum types. C-style unions also serve a similar function.

Now, we can use these type-composition functions to make arbitrarily complex expressions:

(int*int*string)+(date*(string+int))

Just as we could use them to make arbitrarily complex algebraic expressions:

(x*x*y)+(z*(y+x))

But there is perhaps a simpler algebraic concept to consider:

1

What does the natural number “one” mean at the level of types? This is called the “unit type” and it has only one value, written (). It doesn’t do much good to have a value of the unit type — you already know what it must be. However, it can become useful in composition, for example if you consider the simple identity:

1+1=2

Now “two” becomes the type of bits (or boolean values) — because a value of this type could either be the (trivial) unit value on the left, or the one on the right. This view may help to understand variant types better, consider:

int+int = 2*int

In other words, the sum type of two ints is the same thing as the product type of a boolean value and a single int (the boolean value tells you whether the int is the one on the left or the right of the sum).