Algebraic Data Types
Algebraic Data Types are the bread and butter of many functional languages. In languages such as
Haskell, there are no classes or inheritance. Haskell does not even have a null
value. The absence
of a value is expressed through ADTs. You could probably even say that Haskell’s type system is
ADTs and you would not be too far off.
In object-oriented languages, such as Kotlin, Swift, TypeScript, etc., we are not forced to design
our code using ADTs. We can still use null
s wherever we want, use runtime condition checking, and
generally write our code in a very imperative C-style way. But using language features such as
sealed classes and exhaustive type checking, we can replicate much of the ADTs’ power even
in non-functional languages.
Before proceeding to explain ADTs any further, let me first explain a related concept that we will use throughout the rest of this article.
Type’s size
Each type has a number of possible values it can represent. Let’s refer to this number as the size of a type. Here is a table of some primitive types and their sizes.
- The size of the
Boolean
type is 2 since it can represent only true or false. - The size of the
Byte
type is 256 since it can represent all integer numbers ranging from 0 to 255. - Etc.
In mathematics, this attribute is generally called cardinality, but I never saw the term used in the programming context, so I opted to using a more reader-friendly term.
Just be aware that “size” of a type in other contexts may refer to a different concept. In C, for
example, the sizeof
operator is used to calculate how many bytes a type occupies in memory. The
cardinality of a type is much more abstract concept and is unrelated from the memory representation.
For the rest of the article, the size will always refer to the type’s cardinality.
String
does have a theoretical limit, but it is so large that for any practical use, we can
pretend it is infinite.
On JVM, a String
may hold up to 231-1 characters, which brings us
to whopping (28)231-1 = 2562147483647 possibilities.
In comparison, there are only 1082 ≈ 25634 atoms in the observable universe.
Algebraic Data Types
ADTs are simply types composed of other types. This might be quite an anticlimactic revelation, but there is a lot to unpack. There are two fundamental ways how we can compose types together. These are represented by Product types and Sum types.
Sum types
Sum types are composed of components where only a single component is required to represent the sum type.
These components have an OR relationship – to instantiate a sum type, we must specify one component OR any other component.
The size of a Direction
type is 4 since it can represent up
or down
or left
or right
values.
The size of a State
is 3 since it can represent 3 values—initial
, loading
or loaded
.
Product types
Product types are composed of components where all components are required to represent the product type.
These components have an AND relationship – to instantiate a product type, we must specify one component AND all other components.
The size of a Format
type is 8 since it can represent any of
the (⊤, ⊤, ⊤), (⊤, ⊤, ⊥), (⊤, ⊥, ⊤), (⊤, ⊥, ⊥), (⊥, ⊤, ⊤), (⊥, ⊤, ⊥), (⊥, ⊥, ⊤), (⊥, ⊥, ⊥)
combinations.
The size of a Color
is 224 since each color component can represent 28 values and all 3
color components are required at the same time.
Abstract types
All the types we’ve shown so far were concrete types and have a fixed, constant size.
Abstract types (i.e. types parametrized by other types) fit into the ADT system as well. Unlike concrete types, the size of an abstract type depends on other types, which may be concrete but also abstract types.
Abstract sum types
Abstract product types
For example, the size of Optional<T>
is T+1 where T simply refers to the size of the type
T. This is similar to variables in mathematical equations.
We know now that the size of a Boolean
is 2 and the size of a Byte
is 256,
thus Optional<Boolean>
has a size of 3, while Optional<Byte>
has a size of 257.
Combination
Finally, we can also combine sum types and product types to represent other complex types.
Although primitive types are typically not regarded as ADTs, if you squint your eyes enough, they can be seen as a form of Sum and Product types as well.
They can be regarded as Sum types, each simply enumerating their values:
Or alternatively as Product types, representing how they are physically stored in memory:
Relation with algebra
Sum types and Product types are called Algebraic Data Types because they exhibit properties similar to Algebraic structures. You might remember some of these from school:
- (ℤ, +) Integers under addition form an abelian group.
- (ℤ, ×) Integers under multiplication form a semigroup.
- (ℝ, +) Real numbers under addition form an abelian group.
- (ℝ∖{0}, ×) Real numbers without zero under multiplication form an abelian group.
- (ℝ, +, ×) Real numbers under addition and multiplication form a ring.
- (ℕ, +, ×) Natural numbers under addition and multiplication form a commutative monoid.
Algebraic structures are not limited only to infinite numbers though:
- The Rubik’s cube as well can be defined as a group, commonly known as the Rubik’s group.
- Quaternions form a cyclic group known as the quaternion group.
- Even a simple clock can be described as a group.
Although we cannot say that ADTs are an algebraic structure, if we bend the rules a little, use sum types to represent the + operation, and use product types to represent the × operation, we can observe that ADTs in many ways behave like an algebraic structure!
Isomorphism
For example, the concept of isomorphism (as applied to graphs or groups, for example) applies to ADTs as well.
Two types (graphs, groups, …) are isomorphic if there is a bijection between the two types (graphs, groups, …). In other words, there has to be a 1:1 mapping between the elements of one and the elements of the other.
What this means in practice is that we can, for example, substitute a Sum type composed of two elements with a Boolean type.
Of course, State and Boolean types are not equal. Passing one into a function that expects the other one would yield a compilation error. But we can create functions that map one type to another without losing any information along the way.
Associativity, commutativity, distributivity, identity
Understanding isomorphism between types allows us to apply other algebraic properties to ADTs as well.
Additive associativity
(a + b) + c = a + (b + c)
Additive commutativity
a + b = b + a
Additive identity
0 + a = a + 0 = a
Multiplicative associativity
(a × b) × c = a × (b × c)
Multiplicative commutativity
a × b = b × a
Multiplicative identity
1 × a = a × 1 = a
Left and right distributivity
a × (b + c) = (a × b) + (a × c)
(b + c) × a = (b × a) + (c × a)
Zero element (?)
a × 0 = 0 × a = 0
For example, the multiplicative associativity rule tells us that the following two types are isomorphic.
Indeed, with a bit of refactoring, one type can be replaced with the other one since both types have the same size and represent the same amount of possibilities.
But what about the additive identity and multiplicative identity rules? How can we represent a type with a size of 1 or even a size of 0?
Any, Unit, and Nothing
Compared to Java, where the Void
type was more of a keyword rather than an actual type,
Kotlin’s Unit
and Nothing
types form a much sounder type system.
Any
can be literally anything and thus has a size of ∞.Unit
is a singleton and has a size of 1.Nothing
cannot be initialized and has a size of 0.
These types fit very nicely into the algebra of ADTs!
- The
Unit
type can be used to represent the multiplicative identity. - The
Nothing
type can be used to represent the additive identity.
The same concept can be found in many other languages as well. These types are commonly referred to as the top, unit and bottom types.
In languages that support subtyping, roughly speaking, the top type is the supertype of all other types and the bottom type is the subtype of all other types (ignoring nullability and primitive types for simplicity).
top | unit | bottom | |
---|---|---|---|
Kotlin | Any | Unit | Nothing |
Scala | Any | Unit | Nothing |
Swift | AnyObject | Void | Never |
TypeScript | unknown | null1 | never |
Rust | Any | () | ! |
Haskell | ❌ | () | Void |
Dart | Object | ❌ | Never |
Java | Object | ❌ | ❌ |
C++ | std::any | ❌ | ❌ |
Nullable types
The use of optional types is so ubiquitous that most modern languages offer a succinct syntax to
represent them, usually by appending an ?
to the type.
Effectively, Optional<T> ≅ T?
.
There is an interesting relationship between nullable types and the Nothing
type.
As we already know, the Nothing
type represents an uninstantiable value and has a size of 0.
There is simply no value we can assign to val result: Nothing
.
But the Nothing?
type has a size of 1+0=1. As it turns out, there is exactly one value we can
assign to val result: Nothing?
—the null
value.
Kotlin’s nullable types and Optional
types are not strictly isomorphic.
While we can declare a type such as Optional<Optional<T>>
with a size of 2 + T, in
Kotlin T??
effectively becomes T?
. There is no way to differentiate between None
and Some(None)
since both map to null
.
More isomorphisms
Now that we learned that the Unit
type has a size of 1 and the Nothing
type has a size of
0, let’s define a few more isomorphisms.
The list of examples here is not exhaustive as there are infinitely many more isomorphisms.
In mathematical terms, ADTs, when expressed as their size, represent a semiring.
ADTs do not qualify as a ring since they are missing the additive inverse and multiplicative inverse properties, but they satisfy other properties not required for a semiring such as additive identity, multiplicative identity, and multiplicative commutativity.
Why do we care?
Although all this theory is without a doubt very interesting, where can we actually put it to use?
It turns out that ADTs are great for modeling the domain layer in a way that makes it impossible to represent illegal states, effectively removing dead code for cases when such an illegal state would be actually reached.
Furthermore, sum types can be narrowed down to one of their possible values. This can be used to express runtime checks at the type level, essentially exalting certain runtime checks to compile time checks.
Making illegal states unrepresentable
Network responses
It is not uncommon to represent a network response with a structure similar to the following.
Every network response will always contain code
and message
meanwhile exception
and data
fields are nullable. For clarity, we can replace the nullable types with an Optional
type since
they are isomorphic.
The problem with this design is that not all possible values of Response
are valid. From the
type-system perspective, it’s possible to instantiate a Response
with both exception
AND data
fields empty (or, in a similar fashion, to have both exception
AND data
fields populated). We
know that this situation should never occur, so why don’t we reflect that information in our type
system?
We need to reflect the exclusivity of data
or exception
in our type, which can be easily
achieved using a sum type. But what about the other two pieces of data—code
and message
? We can
model this either as a sum of product types or a product of sum types.
By applying the distributive property, we can actually convert one into the other. Both types are isomorphic. In the end, which one to use comes down to personal preference and convenience.
We can even prove the isomorphic inequality between the original and new types!
c×m×(d+1)×(e+1) ≟ (c×m×d)+(c×m×e) c×m×(d×e+d+e+1) ≟ c×m×(d+e) d×e+d+e+1 ≟ d+e d×e +1 ≠ 0
From the d×e+1 ≠ 0 inequality we can conclude the two types are not isomorphic. It also gives us a hint about what is the difference between the two types.
- The left side of the equation has two terms left—d×e and 1—which loosely translates
to a state where both
data
andexception
are present or a state where neitherdata
norexception
is present. - The right side of the equation has no terms left, meaning there are no additional states that can not be represented by the original state.
TextFieldState
As a more complex example, imagine that we are implementing a custom TextField
widget.
We got a rough list of requirements what the widget should be able to do, and so we reflected them
in a TextFieldState
type.
Unfortunately, some combinations of these attributes above are not valid.
- The
cursorColor
is not used whenisEditable = false
. - The
isStrikethrough
is not used whenisEditable = true
. - The
isMasked
is not used whenisEditable = true
. - The
isMasked = true
is not valid together withisStrikethrough = true
. - The
mask
is not used whenisMasked = false
(and honestly, it makes little to no sense to mask the text whenisEditable = true
).
Can we do better?
Notice that wherever we previously had a Boolean (isEditable
, isStrikethrough
, isMasked
), now
the same information is expressed on the level of types (Editable
or Static
, Normal
or Strikethrough
or Masked
).
By expressing this information on the type level, we can leverage the type safety guaranteed by the compiler and convert some runtime checks into compile-time checks!
Furthermore, by removing the senseless combinations, we potentially saved ourselves from writing essentially dead code. In the best case, illegal combinations do not require any special treatment, and we do not have to write any additional code. However, more often than not, we have to address these conflicting requirements. In the better case, we throw an exception, delegating the problem closer to its root. In the worse case, we may try to recover from the illegal state ourselves. That, however, often leads to even more inconsistencies soon after and potentially even more unnecessary code.
Type narrowing
To better explain the power of type narrowing, imagine we are implementing a platform where users
review restaurants and give them ratings on a scale from 1 to 5 stars. When viewing details about
a restaurant, we want to display the average rating given by the users. That could be as simple as
collecting all the ratings in a List<Int>
and calculating the average()
on it.
@Composable
fun Restaurant(..., ratings: List<Int>) {
...
Text(ratings.average().toString())
}
While some operations, such as list.sum()
, are safe to execute on an empty collection; other operations, such as list.average()
, are not. If a list is empty, calculating list.average()
will result in a runtime error since we attempt to divide by zero when calculating list.sum() / list.size. We should check whether the collection is empty first.
@Composable
fun Restaurant(..., ratings: List<Int>) {
...
if (ratings.isNotEmpty()) {
Text(ratings.average().toString())
} else {
Icon(Icons.Default.QuestionMark)
}
}
This is a trivial example and in reality, this logic could be split across multiple functions, classes, or even modules. Let’s extract the formatting into a separate function.
fun formatAverageRating(ratings: List<Int>): String =
String.format("%.1f ★", ratings.average())
@Composable
fun Restaurant(..., ratings: List<Int>) {
...
if (ratings.isNotEmpty()) {
Text(formatAverageRating(ratings))
} else {
Icon(Icons.Default.QuestionMark)
}
}
By extracting this logic, we have unfortunately introduced another problem.
Although the Restaurant
function checks the contents of ratings
, we opened the possibility
for other components to call formatAverageRating
with an empty list.
Every consumer of the formatAverageRating
function should check also whether the passed ratings
parameter is not empty.
Alternatively, we can add an isNotEmpty()
check inside of formatAverageRating()
too,
“just to be safe”, but what value should we return then?
This situation gets worse and worse as we make function call stack deeper and deeper and the gap between validation and execution gets further apart.
fun formatAverageRating(ratings: List<Int>): String {
...
scale(..., ratings)
...
}
fun scale(..., ratings: List<Int>): String {
...
rotate(ratings)
...
}
fun rotate(..., ratings: List<Int>): String {
...
translate(..., ratings)
...
}
fun translate(..., ratings: List<Int>): String {
...
ratings.average()
...
}
@Composable
fun Restaurant(..., ratings: List<Int>) {
...
if (ratings.isNotEmpty()) {
Text(formatAverageRating(ratings))
} else {
Icon(Icons.Default.QuestionMark)
}
}
The problem is that the validation (e.g. ratings.isNotEmpty()
) and execution of the validated
data (e.g. ratings.average()
) is separated by layers of other functions and this “unwritten
contract” is soon lost in heaps of code.
In any bigger codebase, this is obviously unsustainable. It also often leads to adding more validations in the intermediate steps “just to be safe” even though there is no good way to resolve the edge case.
Option 1: Just rethrow the exception
One solution would be to simply rethrow the exception, but this is what we wanted to prevent in the
first place. Although Kotlin does not enforce checked exceptions, we still can, at the very least,
add the @Throws
annotation as a hint that the function is “dangerous”.
@Throws
fun formatAverageRating(ratings: List<Int>): String
@Throws
fun scale(ratings: List<Int>): String
@Throws
fun rotate(ratings: List<Int>): String
@Throws
fun translate(ratings: List<Int>): String =
ratings.average()
@Composable
fun Restaurant(..., ratings: List<Int>) {
...
try {
Text(formatAverageRating(ratings))
} catch (ex: IllegalArgumentException) {
Icon(Icons.Default.QuestionMark)
}
}
Option 2: Return a Sum type
Another solution would be to return a widened type representing either a success or a failure.
This can be modeled using a Sum type, such as Either<Failure, String>
or Validated<String>
.
fun formatAverageRating(ratings: List<Int>): Validated<String>
fun scale(ratings: List<Int>): Validated<String>
fun rotate(ratings: List<Int>): Validated<String>
fun translate(ratings: List<Int>): Validated<String> =
if (ratings.isEmpty()) {
Invalid
} else {
Valid(ratings.average())
}
@Composable
fun Restaurant(..., ratings: List<Int>) {
...
when (val rating = formatAverageRating(ratings)) {
is Valid -> Text(rating.value)
is Invalid -> Icon(Icons.Default.QuestionMark)
}
}
This is basically the same as checked exceptions.
This feels very monadic because instead of operating on plain String
values, we are required to
manipulate the Validated
result in intermediate steps using map
, flatMap
, fold
, and similar
operations, which may feel clunky at times.
Whether it is better to represent illegal states using exceptions or monads is an endless topic on its own, so we will not delve into the differences any further.
Option 3: Pass in a narrowed type
Remember that this whole ordeal is caused by the list.average()
operation not being safe when
invoked on an empty list. Even though we check for list.isEmpty()
, the result of this check is
not reflected in the type system and the information cannot be safely propagated throughout other
functions. So why don’t we create a type representing a non-empty list?
We can make use of the fact that any implementation of a List
is isomorphic to a LinkedList
.
LinkedList
is simply a chain of Node
s that each hold a value and reference to the next
Node
or an Empty
object, symbolizing the end of the chain.
In ADT terms, LinkedList
is a Sum type of either Empty
or Node
types. Since there are only two
types to choose from, the Node
type represents a list that is not Empty
—a
non-empty list. That’s exactly what we are after!
Let’s rename the Node
to a NonEmptyList
and represent the Empty
state using an Optional<T>
.
This structure is still isomorphic to a List
but allows us to narrow the type to a NonEmptyList
when we check for list.isEmpty()
.
class NonEmptyList<T>(
val head: T,
val tail: List<T>,
) : List<T> by listOf(head) + tail
fun <T> List<T>.toNonEmptyListOrNull(): NonEmptyList<T>? =
if (isEmpty()) null else NonEmptyList(first(), drop(1))
fun NonEmptyList<Int>.safeAverage(): Int =
sum() / size // Can not divide by zero
fun formatAverageRating(ratings: NonEmptyList<Int>): String
fun scale(ratings: NonEmptyList<Int>): String
fun rotate(ratings: NonEmptyList<Int>): String
fun translate(ratings: NonEmptyList<Int>): String =
ratings.safeAverage()
@Composable
fun Restaurant(..., ratings: List<Int>) {
...
val nonEmptyRatings: NonEmptyList<T>? = ratings.toNonEmptyListOrNull()
if (nonEmptyRatings != null) {
Text(formatAverageRating(nonEmptyRatings))
} else {
Icon(Icons.Default.QuestionMark)
}
}
The crucial part of this example is the isomorphic transformation of the List<T>
type to the
NonEmptyList<T>?
type. Here, the null
value represents an empty list, and we can narrow down the
type to a non-empty list with a simple null check.
The NonEmptyList
type expresses the ratings.isEmpty() == false
check on the level of types. All
functions that transitively depend on the ratings.average()
call now accept a NonEmptyList
instead of a List
. This way, we completely removed the dredged edge case scenario from all the
functions.
Kotlin has an idiomatic way of representing results of potentially problematic operations using nullable types, e.g.:
fun String.toIntOrNull(): Int?
fun List<T>.firstOrNull(): T?
fun List<T>.toNonEmptyListOrNull(): NonEmptyList<T>?
This works exceptionally well with the Kotlin compiler which automatically refines null-checked and type-checked types using smart casting and provides a succinct null coalescing operator (a.k.a. Elvis operator) and safe calls on nullable receivers.
Conclusion
Algebraic data types are a foundation for a strong type system that goes beyond primitive number types and strings. By expressing business constraints on the level of types, we can convert some runtime checks into compile-time checks. They allow us to reason about the program more easily and with more confidence since the compilation of the program can be seen as a form of a unit test.
A strong type system allows us to build applications where not only we guaranteed that the business logic is valid but also guards us against inadvertently breaking type invariants when making changes to the application.
Further reading
Functional types
Functional types, such as (A) -> B
, can also be regarded as Algebraic Data
Types with an exponential cardinality of BA. They fit into the algebra described
above just like one would expect from exponentiation. I intentionally left it out since I could
not find a practical example where the knowledge of this type’s existence could be used to write
better programs.
Also, the article was getting too long.
Howard-Curry Correspondence
Howard-Curry Correspondence is a fascinating observation that there is an isomorphism between computer programs and mathematical proofs. In other words, we can convert programs to mathematical proofs but also express mathematical proofs as programs. This, however, requires the programming language to have a strong type system.
At the heart of Howard-Curry Correspondence
- programs correspond to proofs,
- types correspond to formulae,
- sum types correspond to disjunction,
- product types correspond to conjunction,
- function types correspond to implication,
- the unit (
Unit
) type corresponds to truth and - the bottom (
Nothing
) type corresponds to falsity.
Through more complex structures we can also express negation, universal quantification, and existential quantification. Through Howard-Curry Correspondence, the compilation of a program using a type system to represent formulae we aim to prove serves as a formal proof (or lack thereof) that the formulae indeed hold.
-
TypeScript’s type system is complicated. ↩