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 nulls 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.

1 bitBoolean{ true, false }28 bitsByte{ 0, 1, 2, 3 ... 255 }25632 bitsInt{ 0, 1, 2, 3 ... 4294967295 }4294967296∞ bitsString{ <empty>, a, b, ..., aa, ab, ... ba, bb, ..., aaa, aab, ... }

  • 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 108225634 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.

Algebraic Data Types
Algebraic Data Types
Product Types

(AND)
Product Types...
Sum Types

(OR)
Sum Types...
Text is not SVG - cannot display

Sum types

DirectionORupdownleftright
+ + + 1 = 4
1 + 1 + 1 + 1 = 4
StateORinitialloadingloaded
+ + 1 = 3
1 + 1 + 1 = 3
Text is not SVG - cannot display

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

FormatANDbolditalicunderlined
2 × 2 × 2 = 8
2 × 2 × 2 = 8
ColorANDredgreenblue
28 × 28 × 28 = 224
28 × 28 × 28 = 224
Text is not SVG - cannot display

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


Either<A, B>
Either<A, B>
OR
OR
Left<A>Right<B>
+ B
A + B

Optional<T>
Optional<T>
OR
OR
Some<T>None
+ 1
T + 1

T?
T?
OR
OR
Tnull
+ 1
T + 1
Text is not SVG - cannot display

Abstract product types


Entry<K, V>
Entry<K, V>
ANDkeyvalue
× B
A × B

Triple<A, B, C>
Triple<A, B, C>
ANDabc
× B × C
A × B × C

Array<T>
Array<T>
ANDget(0)get(1)get(2)...
× T × T × ...
T × T × T × ...
Text is not SVG - cannot display

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.

NotificationIndividualstatusGlobalkeyStylechanneltimelinenews
+ K × (1 + 1 + 1)
S + K × (1 + 1 +...
Text is not SVG - cannot display

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:

1 bit
1 bit
Boolean
true OR false
true OR false
2
8 bits
8 bits
Byte
OR 1 OR 2 OR 3 OR ...
0 OR 1 OR 2 OR 3 OR ...
+ 1 + 1 + 1 + ... = 256
1 + 1 + 1 + 1 + ... = 256
32 bits
32 bits
Int
OR 1 OR 2 OR 3 OR ...
0 OR 1 OR 2 OR 3 OR ...
+ 1 + 1 + 1 + ... = 4294967296
1 + 1 + 1 + 1 + ... = 4294967296
∞ bits
∞ bits
String
<empty> OR a OR b OR ab OR ...
<empty> OR a OR b OR ab OR ...
+ 1 + 1 + 1 + ... = 
1 + 1 + 1 + 1 + ... = ∞
Text is not SVG - cannot display

Or alternatively as Product types, representing how they are physically stored in memory:

1 bit
1 bit
Boolean
true OR false
true OR false
2
8 bits
8 bits
Byte
Boolean AND Boolean AND ...
Boolean AND Boolean AND ...
× 2 × ... = 256
2 × 2 × ... = 256
32 bits
32 bits
Int
Boolean AND Boolean AND ...
Boolean AND Boolean AND ...
× 2 × ... = 4294967296
2 × 2 × ... = 4294967296
∞ bits
∞ bits
String
<emptyOR Byte OR (Byte AND Byte) OR ...
<empty> OR Byte OR (Byte AND Byte) OR .....
B0 + B1+ B2 + ... = ∞
B0 + B1+ B2 + ... = ∞
Text is not SVG - cannot display

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:

Algebraic structures are not limited only to infinite numbers though:

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.

0123456789ABCDEFGHIJ

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.

StatedeadaliveBooleanfalsetrue

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.

Pair<Pair<A, B>, C>
Pair<Pair<A, B>, C>
Pair<A, B>
Pair<A, B>
abc

Pair<A, Pair<B, C>>
Pair<A, Pair<B, C>>
a
Pair<B, C>
Pair<B, C>
bc
Text is not SVG - cannot display

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.


Pair<A, B>
Pair<A, B>
× B
A × B

Pair<Boolean, Unit>
Pair<Boolean, Unit>
(true, Unit)(false, Unit)
× 1 = 2
2 × 1 = 2

Pair<Boolean, Nothing>
Pair<Boolean, Nothing>
(true, Nothing)(false, Nothing)
× 0 = 0
2 × 0 = 0

Either<A, B>
Either<A, B>
+ B
A + B

Either<Boolean, Unit>
Either<Boolean, Unit>
Left(true)Left(false)Right(Unit)
+ 1 = 3
2 + 1 = 3

Either<Boolean, Nothing>
Either<Boolean, Nothing>
Left(true)Left(false)Right(Nothing)
+ 0 = 2
2 + 0 = 2

Optional<T>
Optional<T>
+ T
1 + T

Optional<Unit>
Optional<Unit>
NoneSome(Unit)
+ 1 = 2
1 + 1 = 2

Optional<Nothing>
Optional<Nothing>
NoneSome(Nothing)
+ 0 = 1
1 + 0 = 1
Text is not SVG - cannot display

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.

Pair<Unit, Unit>
Pair<Unit, Unit>
(Unit, Unit)UnitUnit
Optional<Nothing>
Optional<Nothing>
None
Either<Unit, Unit>
Either<Unit, Unit>
Left(Unit)Right(Unit)Booleanfalsetrue
Optional<Unit>
Optional<Unit>
NoneSome(Unit)
Either<T, Nothing>
Either<T, Nothing>
Left(T)TT
Pair<T, Unit>
Pair<T, Unit>
(T, Unit)
Either<T, Unit>
Either<T, Unit>
Left(T)Right(Unit)T?Tnull
Optional<T>
Optional<T>
Some(T)None
Text is not SVG - cannot display

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.

Response
Response
codemessage
exception?
exception?
data?
data?
ResponsecodemessageOptionalNoneexceptionOptionalNonedata
Text is not SVG - cannot display

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.

ResponseSuccesscodemessagedataErrorcodemessageexceptionResponsecodemessageEitherdataexception

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 and exception are present or a state where neither data nor exception 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.

TextFieldStatetextisEditablecursorColorisStrikethroughisMaskedmask

Unfortunately, some combinations of these attributes above are not valid.

  • The cursorColor is not used when isEditable = false.
  • The isStrikethrough is not used when isEditable = true.
  • The isMasked is not used when isEditable = true.
  • The isMasked = true is not valid together with isStrikethrough = true.
  • The mask is not used when isMasked = false (and honestly, it makes little to no sense to mask the text when isEditable = true).

Can we do better?

TextFieldStateEditabletextcursorColorStatictextModeNormalStrikethroughMaskedmask

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 Nodes that each hold a value and reference to the next Node or an Empty object, symbolizing the end of the chain.


List<T>
List<T>
elements

LinkedList<T>
LinkedList<T>
Empty
Node<T>
Node<T>
valuenext
Text is not SVG - cannot display

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>.


LinkedList<T>
LinkedList<T>
Empty
Node<T>
Node<T>
valuenext

Optional<NonEmptyList<T>>
Optional<NonEmptyList<T>>
None
NonEmptyList<T>
NonEmptyList<T>
headtail
Text is not SVG - cannot display

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.

  1. TypeScript’s type system is complicated