The Algebra of Algebraic Data Types
You may have heard of Algebraic Data Types or ADTs, but where does the term algebra come from in describing ADTs? How does algebra relate to data types? In this article, we explore this question, and develop an intuition for thinking and reasoning about data types algebraically.
Sums and Products
Most programming languages have product types. What do we mean by product types? Colloquially, when we have one piece of data and some other piece of data, we have the product of those two pieces of data. For example, this data type, expressed using the Java programming language, has an int and a String to make up its structure.
class Person {
int age;
String name;
}It can be said that the Person data type is the product of int and String. But why is it called a product type? Product means multiplication, but where is the multiplication?
Let's look at a more trivial example. This data type ThreeSwitches, is made up of a boolean and a boolean and a boolean.
class ThreeSwitches {
boolean sw1;
boolean sw2;
boolean sw3;
}If you'll trust for now that boolean corresponds algebraically to the value 2 (we'll see why later), then we have:
ThreeSwitches = 2 and 2 and 2
Or stated using multiplication, ThreeSwitches is the product of 2, 2 and 2, which is 8. We can conclude from this that there are 8 possible values of ThreeSwitches and indeed, if you count them, there are 8. This is where the multiplication comes from in our product type. We can multiply its parts.
OK, so if we can multiply, can we add? Yes, we can, using sum types. In the same way when we express the term "and", we are describing a product type, when we use the term "or", we are talking about sum types. However, the Java programming language falls a bit short here, in expressing a sum type. For example, what is the data type that is "an int or a String"? It is important in writing our data type that it can never be neither and never be both; it is an int or it is a String and it is never anything else.
Fortunately, Java has a little trick that takes advantage of access to private fields, methods, and constructors1:
class IntOrString {
private IntOrString() {}
class IsInt extends IntOrString {
int i;
IsInt(int i) { this.i = i; }
}
class IsString extends IntOrString {
String s;
IsString(String s) { this.s = s; }
}
}Given a value of the type IntOrString, it is either an int or it is a String and never any other possibility. We have expressed the sum of int and String. Rather than exploit this trick with Java, let's use the Scala programming language, which has native support for sum types:
sealed trait IntOrString
case class IsInt(i: Int) extends IntOrString
case class IsString(s: String) extends IntOrStringSimilar to earlier, we can use a trivial example to make the calculation easier. Take the sum of three boolean values:
sealed trait BoolOrBoolOrBool
case class Bool1(n: Boolean) extends BoolOrBoolOrBool
case class Bool2(n: Boolean) extends BoolOrBoolOrBool
case class Bool3(n: Boolean) extends BoolOrBoolOrBoolIn this case, we have added 2, 2 and 2, which is 6. We can conclude that there are 6 possible values of the type BoolOrBoolOrBool and indeed if you count them, there are.
Identities
It is likely quite obvious that if we take any value and multiply it by 1, we end up with the same value. In short, the value 1 is the identity for multiplication. OK, so let's write the data type for 1:
sealed trait One
case object TheOnlyOne extends OneWe can express this identity using a generic type. We can multiply a value A by the value 1 and we should have the same algebraic structure as just A alone:
case class Multiply1[A](a: A, x: One)We can easily see, even if intuitively, that the number of values of the type Multiply1[A] is the same as the number of values of the type A. This holds for all A and indeed, that is what a generic type parameter in this position means algebraically: "for all", or universal quantification. The One data type is more typically known as Unit, and is included in the Scala standard library as Unit.
The generic form of multiplication is a tuple, or Scala's Product2. This data type multiplies any two values, A and B:
case class Tuple2[A, B](a: A, b: B)We can experiment algebraically with this; for example: Tuple2[Boolean, Boolean] = 2 * 2 = 4. There are 4 values of the type Tuple2[Boolean, Boolean]. We can continue this algebraic reasoning with multiplication and this is why these are named product types.
The identity for addition is 0. Let's write the data type for 0:
sealed trait ZeroThis data type is quite trivial, but the important observation is that there are no values of its type, hence 0. The generic form of Scala's addition is called Either. Given a value of the type Either[A, B], we can derive the equation, A + B. Here is the implementation of Either:
sealed trait Either[A, B]
case class Left[A, B](a: A) extends Either[A, B]
case class Right[A, B](b: B) extends Either[A, B]Knowing that the identity for addition is 0, we can add to it; we'll use a type-alias this time, since we are reasoning algebraically!
type Add0[A] = Either[A, Zero]It should be somewhat intuitive that there are as many values of the type Add0[A] as there are values of the type A, and this is true for all A.
Let's do one more example of reasoning algebraically. Consider this data type:
sealed trait OptionPair[A, B]
case class Empty[A, B]() extends OptionPair[A, B]
case class Both[A, B](a: A, b: B) extends OptionPair[A, B]We can describe this data type as:
"empty or (A and B)"Where a data type constructor carries no data (e.g. Empty), this is equivalent to that constructor carrying the value Unit or 1. Hence, algebraically, this data type corresponds to:
1 + (A * B)Sums, Products and …
… Exponentiation!
We can also express exponentiation using data types. To summarise our correspondence so far:
Either[A, B] // A + B
Tuple2[A, B] // A * BNote that both addition and multiplication are commutative, so we can swap the order of the values and arrive at the same result. Exponentiation, however, is not commutative, so we must be careful about the order. Exponentiation in Scala corresponds to Function1. Specifically, the codomain raised to the power of the domain.
Function1[A, B] // B^ALet's have a look at an example. If we have a look at the built-in Scala data type called Option[A], we find that corresponds algebraically to 1 + A, and we have seen that Boolean corresponds to 2, so Option[Boolean] corresponds to 1 + 2 or 3. If we then look at the following function's type, we can calculate the number of values with this type:
def algebraRoolz(b: Boolean): Option[Boolean] =
...We raise the codomain 3 to the power of the domain 2, which gives us 9 and indeed, there are exactly 9 possible values with this type. Here they are:
def algebraRoolz(b: Boolean): Option[Boolean] =
None // 1
Some(true) // 2
Some(false) // 3
Some(b) // 4
Some(!b) // 5
if(b) None else Some(b) // 6
if(b) Some(b) else None // 7
if(b) None else Some(!b) // 8
if(b) Some(!b) else None // 9
We can keep applying this reasoning to algebraic data types!
Either[Boolean, (B, C)] // 2 + (B * C)
Function1[Boolean, Either[A, Option[B]]] // (A + 1 + B)^2
Tuple2[X, Function1[Y, Z]] // X * Z^YRecursion
What about recursive algebraic data types? How do we reason about those algebraically?
Consider the good ol' cons list:
sealed trait List[A]
case class Nil[A]() extends List[A]
case class Cons[A](h: A, t: List[A]) extends List[A]We can see the Nil constructor carries no data (i.e. Unit) and the Cons constructor corresponds to the product of A and List[A]. Ok, so?
List[A] = 1 + (A * List[A])Well yes, but this gives us a recursive answer!
List[A] = 1 + (A * (1 + (A * (1 + (A * (1 + (A * ...)))))))In fact, if you refactor this equation, you will arrive at:
List[A] = 1 + A^2 + A^3 + A^4 + A^5 + ...This makes sense intuitively:
"List[A] is zero A, or one A, or two A, or three A, or four A, or five A, or ..."In fact, we can take this further:
let List[A] = 1 + (A * List[A])
// subtract (A * List[A]) from both sides
List[A] - (A * List[A]) = 1
// multiply List[A] by 1
(1 * List[A]) - (A * List[A]) = 1
// apply distributive law of multiplication
List[A] = 1 / (1 - A)We arrive at List[A] = 1 / (1 - A) which has both a quotient and a subtraction. How does this correspond algebraically? This would require a different type system to the one we have in Scala. Therefore, we will stick with sums, products and exponents.
Algebraic Rules
We can apply algebraic rules to our data types. Consider, for example, this data type taken from the ChatRoulette production code:
sealed trait Event
case class SocketOpened(
sId: SocketId,
created: Timestamp
) extends Event
case class PartnerFound(
sId: SocketId,
cId: CorrelationId,
token: MatchToken,
created: Timestamp
) extends Event
case class ConnectionTimeout(
cId: CorrelationId,
created: Timestamp
) extends EventWe can see that each constructor for Event carries a Timestamp field called created. Algebraically, we can describe this data type:
Event =
(SocketId * Timestamp) +
(SocketId * CorrelationId * MatchToken * Timestamp) +
(CorrelationId * Timestamp)Notice that each constructor multiplies by Timestamp in this definition. Do you recall the distributive rule of multiplication over addition?
A(B + C) = AB + ACWe can apply this algebraic rule by removing the Timestamp from each constructor and add it as a field. We'd arrive an equal (isomorphic) data type:
sealed trait EventNoTimestamp
case class SocketOpened(
sId: SocketId,
) extends EventNoTimestamp
case class PartnerFound(
sId: SocketId,
cId: CorrelationId,
token: MatchToken,
) extends EventNoTimestamp
case class ConnectionTimeout(
cId: CorrelationId,
) extends EventNoTimestamp
case class Event(e: EventNoTimestamp, created: Timestamp)We can apply other algebraic rules. Consider, the power rule:
(A ^ B) ^ C = A ^ (B * C)
(A ^ B) ^ C = A ^ (C * B)We know that exponentiation corresponds to functions and that multiplication corresponds to tupling. Since we can establish an isomorphism by the power rule, we should be able to implement an isomorphism between the two:
def f[A, B, C](x: C => B => A): (C, B) => A = ...
def g[A, B, C](x: (C, B) => A): C => B => A = ...In fact, this specific isomorphism is so ubiquitous, it even has a name. It is called the curry/uncurry isomorphism and it corresponds algebraically to the power rule. You may have heard of "currying" or "uncurrying" functions — when we do this, we are just applying an algebraic rule!
Let's do one more.
Recall the product rule:
(A ^ X) * (A ^ Y) = A ^ (X + Y)If we implement the correspondence to this rule in code:
def f[A, X, Y](i: X => A, j: Y => A): Either[X, Y] => A = ...
def g[A, X, Y](k: Either[X, Y] => A): (X => A, Y => A) = ...This pair of functions corresponds to fold and unfold for the Either[A, B] data type. Thinking algebraically!
Further thoughts
Some of these algebraic equations are interesting, in that we can apply regular algebraic exercises on them to arrive at an interesting result. Consider, for example, taking the partial derivative of an equation.
Recall, we learned that List[A] = 1 / (1 - A).
What is the result of ∂/∂A 1 / (1 - A)?
∂/∂A 1 / (1 - A)
let U = 1 - a
// apply the chain rule
= (∂/∂U 1 / U) * (∂/∂A 1 - A)
// differentiate 1 / U
∂/∂U 1 / U = -1 / U<sup>2</sup>
// differentiate 1 - A
∂/∂A 1 - A = -1
∴
∂/∂A 1 / (1 - A)
=
(-1 / U<sup>2</sup>) * -1
// substitute U = 1 - A
= (-1 / (1 - A)<sup>2</sup>) * -1
// multiply by -1
= 1 / (1 - A)<sup>2</sup>
// apply exponent rule
= (1 / (1 - A))<sup>2</sup>
// back to code
= (List[A], List[A])The partial derivative of List[A] with respect to A is a pair of List[A]! How interesting.
Since the original Scalaz IO data type was implemented, many other variants of this concept have emerged. What is the algebraic representation of these data types? Typically, and by necessity, the implementation hides this detail and so a semantic description of behaviour cannot be derived. This is unfortunate, but often a requirement of the practical purpose of these data types.
This leads to a common error in reasoning. It is often said that IO is "not functional", is for "impure" code or is for "doing side-effects." All of these descriptions of IO are incorrect. The IO data type is just as "functional" and just as "pure" as other data types such as List or Option in that it preserves all the same properties of functional programming and purity. A correct explanation that differentiates IO from these other data types is that "IO does not have an algebraic semantic description." Be cautious of this error in reasoning about data types.
Algebra roolz!
Footnotes
-
The Java Language Specification Java SE 8 Edition (6.6-5) Access to private Fields, Methods, and Constructors ↩