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.
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.
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:
Previously we defined Boolean as 2 given that it can host 2 values, here you can find some other types and its cardinality:
|Void||0||There is no way to construct a Void type, therefore its cardinality is 0|
|Unit||1||Unit has the cardinality of one because it has only one value. Its usual representation is ()|
|Boolean||2||Boolean has 2 possible values, True and False|
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 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, [crayon-5beb2ce9d8421046165155-i/], [crayon-5beb2ce9d842d452898490-i/]. We don’t know the cardinality of A or B because they can be whatever value.
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:
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 [crayon-5beb2ce9d8434526169533-i/] or a [crayon-5beb2ce9d843a618495895-i/], therefore its structure is another sum type.
There is an alternative encoding which uses [crayon-5beb2ce9d843f961663718-i/], that type can be either A or B so our previous [crayon-5beb2ce9d8444862731448-i/] definition:
[crayon-5beb2ce9d844a536789804-i/] is equivalent to: [crayon-5beb2ce9d844f761220521-i/]
Although no one in practice uses that last encoding, it is completely equivalent.
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:
In other words, 2 times 2. Another example of a product type would be a Scala case class:
or its algebraic equivalent in typescript:
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:
As we can see the cardinality is 4. Let’s define now the ranks that you can find in the cards:
We can sum again the habitants to get its cardinality: 13. Last type for our example, let’s define a Card:
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:
And I’m not going to define the other two because it is the same.
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:
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:
And that property holds for our product types:
[crayon-5beb2ce9d8480761924253-i/] is equivalent to: [crayon-5beb2ce9d8486377940929-i/]
And for sum types: [crayon-5beb2ce9d848b380728668-i/] is equivalent to: [crayon-5beb2ce9d8490252557244-i/]
We could use the other encoding just to make it even more explicit:
is equivalent to:
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:
As we proved before, it holds for product types:
is equivalent to:
And for sum types:
is equivalent to:
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:
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:
is equivalent to:
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.
This is fun, show me more algebraic equivalence!
[crayon-5beb2ce9d84cc238574117-i/] is equivalent to: [crayon-5beb2ce9d84d2244234836-i/] which is equivalent to Void because we can’t construct any Void therefore it can’t be constructed
[crayon-5beb2ce9d84d7367537150-i/] is equivalent to: [crayon-5beb2ce9d84dc919370786-i/] which is equivalent to just a
Option can be [crayon-5beb2ce9d84e2016813918-i/] or [crayon-5beb2ce9d84e7931856127-i/], given that there is only one value of type [crayon-5beb2ce9d84ec222551712-i/], the following is equivalent to:
The cardinality of a function that goes from [crayon-5beb2ce9d84f7767295948-i/] is defined as [crayon-5beb2ce9d84fc575933616-i/]. For example, using our previous defined types, a function like: [crayon-5beb2ce9d8502614825406-i/] has a cardinality of [crayon-5beb2ce9d8507549507883-i/].
[crayon-5beb2ce9d850c509190517-i/] is equivalent to: [crayon-5beb2ce9d8511409596882-i/]
We discussed currying before [crayon-5beb2ce9d8517688242074-i/] is the same as [crayon-5beb2ce9d851c707895505-i/]. We can formulate that in an algebraic way: