Swift, Algebraically: Algebraic Structures
Part 3 of 3
In the previous posts we saw that we can perform operations on the sizes of the sets of values represented by programming types. We can add and multiply these sizes, and we can also treat them as exponents. The operations we performed were on the cardinality of the sets of values for the different types. Now we can look for more mathematical properties.
Let's see what happens if we include the unit type, Void, in a structure.
struct Style {
let color: Color
let available: Bool
let unit: Void
}To get the size of a structure we need to multiply the sizes of its properties. For Style it would look like this.
The size doesn't change because we're multiplying by 1. If you read my previous article you might recognize a familiar structure here. This is starting to look like a monoid. A monoid is an algebraic structure with a set of elements, an operation and an identity element. For numbers and multiplication it looks like this.
For product types it might look like this.
Void is the identity element when we multiply the sizes of types. Now let's see what happens if instead we add Never to the structure.
struct Style {
let color: Color
let available: Bool
let never: Never
}If a structure has a Never property, its size is zero. The reason is that it's impossible to populate the Never property in this structure, so it's impossible to create a value for the whole type. Now let's add Never to an enumeration.
enum Color {
case blue
case red
case yellow
case green(Never)
}For an enumeration we have to add 1 for each regular case and add the size of the associated type if a case has one. The original size of color was 3.
When we add a case with an associated Never type, the size doesn't change.
This makes sense because we can still instantiate all the regular cases, but we can't instantiate the case with Never, so it's as if it wasn't there at all. You may have noticed that we have another monoid here.
This isn't at all unusual. Numbers support both addition and multiplication, so they come equipped with two monoids.
In my previous post on algebraic structures I only covered semigroups and monoids so that we could quickly get to the topic of monads. What we're seeing here is a whole new algebraic structure called a commutative semiring.
A semiring has the following requirements.
A monoid with an operation called "addition" and an identity element called "zero"
A monoid with an operation called "multiplication" and an identity element called "one"
An element is absorbed when it is multiplied by the addition identity element.
Addition is commutative.
Multiplication distributes over addition.
A commutative semiring adds one more requirement.
Multiplication is commutative.
Keep in mind that the terms "addition", "multiplication", "zero", and "one" are all abstract. We happen to be dealing with numbers, so the terms have a natural fit, but an algebraic structure may also consist of elements which are not numbers.
We already saw how some of the monoid requirements are fulfilled in the algebra of types. The monoid elements are the sizes, or cardinalities, of the types and we have two operations, addition and multiplication, expressed when we calculate the sizes of enumerations and structures. The identity element for addition is Never and the identity element for multiplication is Void. Now let’s look at some of the other requirements for a semiring.
To make the following discussion easier to understand, imagine every instance of addition as an enumeration and every instance of multiplication as a structure or a tuple.
When an enumeration has no associated types, each of its cases are equal to 1. If any case has an associated type, its size will be equal to the size of that type.
Associativity
We didn’t explicitly mention associativity above, but it is a requirement for a monoid. The rule for associativity looks like this.
This says that when we add or multiply three elements, it doesn’t matter which two elements we add or multiply first. The result will be the same.
When we add the cases in an enumeration we need a way to express the order in which we add them. We can do this by embedding one enumeration in another. Let’s say we have an enumeration with three cases.
enum Three {
case one
case two
case three
}We can put the first two cases in another enumeration and make it an associated type within the first enumeration.
enum OneAndTwo {
case one
case two
}
enum ThreeA {
case first(OneAndTwo)
case three
}Then we can do the same for the two last cases.
enum TwoAndThree {
case two
case three
}
enum ThreeB {
case one
case last(TwoAndThree)
}This allows us to express associativity for sum types.
We can do something similar with structures or tuples. Let’s use tuples to keep things simple. Given a tuple with three values, we can create two equivalent tuples using embedded tuples.
(Color, Bool, Bool)
((Color, Bool), Bool)
(Color, (Bool, Bool))This allows us to express associativity for product types.
Absorption
The idea behind "absorption" of elements is that if we multiply any element by the zero element, the result will be zero. We saw how this requirement is fulfilled when we added the Never type to a structure. Never is the zero element for addition and elements are "absorbed" when we multiply them with Never. Multiplying anything with Never always results in Never.
Commutativity
The rule for commutativity looks like this.
For any two elements, we can switch their order when we perform the operation and the result will be the same. This means that the size of the following two enumerations should be the same.
enum PartyDecoration1 {
case balloon(Color)
case confetti
}
enum PartyDecoration2 {
case confetti
case balloon(Color)
}And the size of the following two structures should also be the same.
struct Style1 {
let color: Color
let available: Bool
}
struct Style2 {
let available: Bool
let color: Color
}Distributivity
The distribution rule looks like this.
We say that multiplication distributes over addition. There are two equations because distribution can happen from the right or from the left.
Let's focus on the first equation, starting with the left side.
We can interpret this as an enumeration inside a structure. An example of this would be our Style structure. It contains the Color enumeration as a property. I'm going to remove one case from the Color enumeration to simplify the equation.
struct Style {
let color: Color
let available: Bool
}
enum Color {
case blue
case red
}Now let’s look at the right hand side of the equation. We can interpret it as an enumeration where each case has an associated type which is a structure.
Notice that in the current example x and y are the sizes of enumeration cases without associated types. Each is equal to one. z is the size of Bool. We can simplify this as follows.
As a type it could look like this.
enum Style {
case blue(Bool)
case red(Bool)
}Now we can compare the original distribution rule to its interpretation with types.
Another way to demonstrate this is to list out all the possible values for the two types. These are all the values for Style defined as a structure.
And these are the values for Style defined as an enumeration.
The structures are different, but they have the exact same set of values.
This isn't a rigorous proof, but it looks like we have a commutative semiring.
Summary
Programming types form an algebraic structure called a commutative semiring. The elements of this structure consist of the cardinalities, or sizes, of the different types. The sizes are the number of values that a type can represent. Structures are product types – the size of the type can be determined by multiplying the sizes of its properties. Enumerations are sum types – the size of the type can be determined by adding the sizes of its cases. Functions are exponential types – the size of the type can be determined by raising the size of the result type to the power of the size of the parameter type. The Never type has size zero and is the identity element for addition. Void has size one and is the identity element for multiplication.
Thanks to my colleagues for their feedback on this essay. Farangis Akhmedova, Eduard Levshteyn, Alex Ozun
Further Reading/Viewing
Chris Taylor. The Algebra of Algebraic Data Types
Bartosz Milewski. Simple Algebraic Data Types
Brandon Williams, Stephen Celis. Algebraic Data Types
Stephen Celis, Brandon Williams. Algebraic Data Types: Exponents
Bartosz Milewski. Why Algebraic Data Types Are Important