Algebraic data types and their algebra

When we think about types we usually think about how they can help us to abstract concepts. In this post we will learn how we can think about types in terms of cardinality and why some types are equivalent to others even though, at first sight, it could seem that they are different. In this post you will learn why functional programmers are so interested in the word algebra when describing their programs.

Cardinality

The cardinality of a type is the number of possible values that the type can have. A simple example is Boolean, it can host only True or False values, so the cardinality is 2.

A type that has a higher cardinality has more possible values, therefore it is more complex to reason about, it is easier to make mistakes and to make invalid representations of it. An example could be to represent a Boolean as a String. If we do so we will have to guard ourselves when the string is not 'true' or 'false' like null, undefined, possible typos, or any other random string. Take into account that cardinality of String is infinite, you can have a really huge amount of possible values for that type so it is always a good idea to avoid it if you can.

The age of a person is usually represented with an Integer, even if a person can't have a negative age. That leads us to do some defensive programming or create a new type Age that throws an exception in the constructor if the age is less than zero. That is usually because programming languages don't have a built-in unsigned Integer or natural number representation. Wouldn't it be nice to restrict that type to be a natural number? If so, we don't have to check whether a type is less than zero. For example, in Haskell there is a representation of natural numbers. In Scala there is an encoding as well if you use shapeless.

But this is only an example, when building our own types we should keep that in mind, limit the cardinality of types and make invalid states unrepresentable.

Algebras

Now that we know about the cardinality of types, we should explain what makes a type an ADT. Maybe you are asking yourself how is a type related to an algebra? To explain this, first, let's define the basic components to form an elementary algebra.

To form an abstract algebra we need numbers, variables and operations; those are the basic components. Now, let's try to encode this in the type system:

Numbers

Previously we defined Boolean as 2 given that it can host 2 values, here you can find some other types and its cardinality:

Notice that they are reduced to its normal form, that is, no further reduction can be done on those types. Those types are examples that form the numbers of our algebra.

Variables

Variables are fairly easy, they are just a symbol to represent an unknown value. Given that those variables have to be encoded in the type system, they have to be parameters of our types. For example, List[A], Option[B]. We don't know the cardinality of A or B because they can be whatever value.

Operations

Having defined our numbers and variables the last step is to define operations. The most basic ones are sums and products so let's encode those:

Sum types

Also called disjoint unions in some languages, are types that can be either one value or another. Let's take Boolean for a moment as an example, Boolean can be True Or False. The cardinality for this type is: 1 (True) + 1 (False). Do you see why it is a sum type? To check the cardinality of a sum type we sum the cardinality of each of its possible values.

Do you remember when we defined list in the previous post? If we fix the parameter to be unit (a single habitant) we can say that a List can be either Empty (Nil) or a Node (::), therefore its structure is another sum type.

There is an alternative encoding which uses Either[A, B], that type can be either A or B so our previous List definition:

List[A] = Nil | List[A] is equivalent to: List[A] = Either[Nil, List[A]]

Although no one in practice uses that last encoding, it is completely equivalent.

Product types

In the same manner that sum types exist, we can express product types. We are used to working with them in many languages. Some possible forms are objects, records and tuples. If we take a tuple like (Boolean, Boolean) the possible values are:

(True, True) - (True, False) - (False, True) - (False, False)

In other words, 2 times 2. Another example of a product type would be a Scala case class:

case class AnElement(propertyA: Boolean, propertyB: Boolean)

or its algebraic equivalent in typescript:

type AnElement = { propertyA: Boolean, propertyB: Boolean }

It is the same, its cardinality is equivalent. Even if they could represent different things for us because the 2nd example has names in the type system they represent the same, a set with 4 possible values.

Creating our own types

Let's define the domain of a poker deck using types. I will use typescript because the syntax is less verbose than Scala and quite similar to Haskell, although I will show you how to do the same in Scala later on.

A poker deck has 4 suites:

type Suite = Hearts | Diamonds | Clubs | Spades

As we can see the cardinality is 4. Let's define now the ranks that you can find in the cards:

type Rank = 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | 10 | J | Q | K

We can sum again the habitants to get its cardinality: 13. Last type for our example, let's define a Card:

type Card = { rank: Rank, suite: Suite }

A Card is the combination of a Rank and its suite, the cardinality is: 13 (Rank) ⋅ 4 (Suite) = 52, which is the number of cards that you will find in a common poker deck (excluding jokers, of course). Magic? No, just maths.

The syntax to define a sum type in Scala is a little bit more verbose but equivalent:

sealed trait Suite
case object Hearts
case object Diamonds
case object Clubs
case object Spades

And I'm not going to define the other two because it is the same.

Properties

Now that we have defined all of the needed components to define an algebra, let's prove some of the basic properties in algebra to demonstrate that our elementary algebra still holds for our types:

Commutativity

In maths, an operation of two arguments is commutative if after changing its order, the result is the same. Products and sums are commutative because as we all know:

(a ⋅ b) ≅ (b ⋅ a)
(3 ⋅ 1) ≅ (1 ⋅ 3)

(a + b) ≅ (b + a)
(3 + 1) ≅ (1 + 3)

And that property holds for our product types:

type Card = { rank: Rank, suite: Suite } is equivalent to: Card = { suite: Suite, rank: Rank }

And for sum types: type Boolean = True | False is equivalent to: type Boolean = False | True

We could use the other encoding just to make it even more explicit:

type Boolean = Either[True, False]

is equivalent to:

type Boolean = Either[False, True]

Associativity

In maths an operation is associative if the order of the parenthesis can be changed without modifying the result. That holds for products and sums:

(a ⋅ b) ⋅ c ≅ a ⋅ (b ⋅ c)
(3 ⋅ 1) ⋅ 2 ≅ 3 ⋅ (1 ⋅ 2)

(a + b) + c ≅ a + (b + c)
(3 + 1) + 2 ≅ 3 + (1 + 2)

As we proved before, it holds for product types: type Card = { rank: Rank, suite: Suite, exposed: Boolean }

is equivalent to:

type Card = { rank: Rank, suite: Suite }

type ExposedCard = { card: Card, exposed: Boolean }

And for sum types:

type Suite = Either[Spades, Either[Clubs, Either[Diamonds, Hearts]]]]

is equivalent to:

type Suite = Either[Hearts, Either[Diamonds, Either[Clubs, Spades]]]]

Distributive property

The distributive property is a property of sum and products from basic algebra. If you don't remember that, is fine, let me show you an example with numbers first:

a (b + c) = (a ⋅ b) + (a ⋅ c)
1 (2 + 3) = (1 ⋅ 2) + (1 ⋅ 3)

It is basically saying that you can distribute that product into the components that are inside the parentheses. And that property applies to our types as well, for example:

type Logged = In | Out
type PremiumUser = True | False

type UserState = { logged: Logged, subscription: PremiumUser }

is equivalent to:

type UserState = (In, True) | (In, False) | (Out, True), (Out, False)

The cardinality is still the same, 4. This is a refactor using a mathematical property, we probably will choose the first representation for our systems because it is less verbose but in case that you find any program written with the latter you can safely refactor it.

Bonus algebras

This is fun, show me more algebraic equivalence!

a ⋅ 0 = 0 is equivalent to: (a, Void) which is equivalent to Void because we can't construct any Void therefore it can't be constructed a ⋅ 1 = a is equivalent to: (a, ()) which is equivalent to just a

Option

Option can be None or Some(A), given that there is only one value of type None, the following is equivalent to: Option[A] = Either[(), A]

Functions

The cardinality of a function that goes from A -> B is defined as B ^ A. For example, using our previous defined types, a function like: Card -> Boolean has a cardinality of 2 ^ 4.

1 ^ a = 1 is equivalent to: A => ()

Currying

We discussed currying before (A, B) => C is the same as A => B => C. We can formulate that in an algebraic way:

(A, B) -> C ≅ A -> B -> C
C ^ (A, B) ≅ C ^ B ^ A
C ^ (A ⋅ B) ≅ C ^ (B ⋅ A)

This post was cross-posted to Christian's personal blog.