Inexpressible States: The History and Usage of Algebraic Data Types

Every program is ultimately a giant state machine. The problem is that this machine willingly represents in memory even the invalid states that should never exist in the domain. So how should we control this State Space?

A note on sources

It was difficult to find a reliable single reference covering the lineage of early programming language history. One of the surveys consulted described its own conclusions as "A Very Shaky Summary."

Even when papers survive, who influenced whom is mostly a matter of inference.

Background knowledge needed for reading

1. State Space = number of possible cases

Every state a program can occupy is ultimately a matter of possible cases

For example, consider the payment status of an online store.
The so-called old-fashioned approach looks like this
(it is still widely used, of course, but it is a bit removed from the code style that tends to be fashionable these days)

bool is_paid;      // Was it paid?
bool is_refunded;  // Was it refunded?
bool is_failed;    // Did it fail?

The problem with this approach is that impossible states exist mathematically.

• is_paid == true and is_refunded == true — paid and also refunded? (contradiction)

• is_failed == true and is_paid == true — failed and also succeeded? (contradiction)

With three boolean flags, the number of possible cases is 2^3 = 8. However, only 4 states are actually permitted in the domain.

Pending, Paid, Failed, Refunded

A program can fall into not just the 4 permitted states out of 8, but also the remaining 4 invalid combinations, and that is precisely where bugs come from.

2. Sum Type: "It is one of several cases"

The construction McCarthy used in 1961 can be applied directly to express a shopping mall's state mathematically:

PaymentState is one of the following.

PaymentState = Pending + Paid + Failed + Refunded

Here + means "or".
(Mathematically, this is called a "disjoint sum" or "disjoint union.")

This constrains the number of possible cases to exactly 4. A state that is simultaneously Paid and Refunded cannot be expressed in the first place. In languages that support closed Sum Types, the type checker can prevent such values from being constructed. In languages that support both closed sums and Exhaustiveness Checks, the compiler can verify that every case is handled, and any state combination that does not exist in the type simply cannot be created to begin with.

3. Product Type: "Both this and that, together"

Consider the opposite situation: something like user information, where multiple pieces of data must always be present together.

User = Id × Name × Age

Here × means "and."

A user must have an Id, a Name, and an Age, all together.
If even one is missing, it is not a User.

The reason this is called a "product" is that the number of possible combinations is determined by multiplication.

• If Id has 1,000 possible values, Name has 1,000,000, and Age has 100,

• the total number of possible User combinations is 1,000 × 1,000,000 × 100.

4. Combining Sums and Products, Built Up Recursively

The key insight is that these two operations, sum and product, can be combined to build recursive structures.

Take a list as an example.

S = 1 + (A × S)

To put it in plain language:

A list S is either an empty list (1) or the product of one element A and another list S.

In other words, a list is defined as either 'empty' or 'a head and a tail'.

The empty list is = `1` (a single `Nil`)
List<A> = Nil + Cons(A × List<A>)
[1, 2, 3] = Cons(1, Cons(2, Cons(3, Nil)))

This single definition can express lists of any length.

This is the standard way lists are defined in functional languages today, and many data structures follow this same pattern.

5. Why Does This Matter So Much?

Because combining these two (sum and product) with an Empty Type (0), a Unit Type (1), and recursion lets you express a wide range of finitely generated recursive data types.

• Boolean = True + False (sum)

• Tuple = A × B (product)

• Optional = None + Some(A) (sum)

• Tree = Leaf + (Node × Tree × Tree) (recursive sum and product)

The reason this mathematical model matters is that a type checker can verify portions of the state space. In languages that support Closed Sum types and Exhaustiveness Checks, missing cases can be caught at compile time, and state combinations not defined in the type simply cannot be constructed in the first place.

To summarize: when you need to represent mutually exclusive states, rather than stringing together multiple booleans, modeling the state itself as a Sum Type is the first step toward making invalid states literally inexpressible.

1961: Bringing Algebra to the State Space

The essence of what we call a Type ultimately comes down to 'the number of permitted cases'. Long before developers were wrestling with runtime errors born from combinations of dozens of boolean flags, John McCarthy, in his 1961 paper A Basis for a Mathematical Theory of Computation, used the Cartesian product ($A\times B$) and the disjoint union ($A\oplus B$) as operations for constructing new sets. By today's terminology, these map closely to Product Types and Sum Types. McCarthy did not call them types, and he did not group them under the modern name algebraic data type, but most writing on ADT programming traces the starting point back to this work.¹

In any case, a product means this and that exist together, while a sum means one of several possibilities.

Let us take a simple example: a user and a payment state.

User         = Id × Name × Age
PaymentState = Pending + Paid + Failed + Refunded

User = Id × Name × Age means that a user has an Id, a Name, and an Age all at the same time. A single User value is formed by combining these three components. In modern programming-language terminology, this corresponds to product types such as struct, record, or tuple.

In other words, the information represented by a user consists of an ID, a name, and an age.

By contrast, PaymentState = Pending + Paid + Failed + Refunded means that a payment is not in all four states at once, but in exactly one of them. In modern terms, this corresponds to sum types such as enum, variant, or tagged union. A payment may pass through several states over time, but at any given moment it occupies only one of them.

A product therefore combines several pieces of information into a single value, while a sum chooses one value from several possible forms.

McCarthy went further still,

the empty set (0),

the singleton set (1),

the distributive law of sums and products, and even recursively defined data spaces,

for example,

represents either an empty sequence or a sequence consisting of one (A) followed again by (S). From today's perspective, this connects directly to the idea that sums, products, Unit Types, Empty Types, and recursion alone are sufficient to construct most common recursive ADTs.

To mathematicians, this was simply an operation on sets, but to programmers, these formulas meant that every possible State Space a program could inhabit could be calculated and controlled with mathematical rigor. (At least in theory, that is. In practice, we are still fighting NullPointerExceptions in 2026.)

It was three years later, in 1964, that this abstract notion of data space was brought down to earth as concrete data types in a programming language.

In 1964, McCarthy proposed in "Definition of new data types in ALGOL x" the inclusion of cartesian and union data types in an actual programming language. ALGOL 68 subsequently provided STRUCT and UNION as construction mechanisms. It is safer to interpret this not as a single linear lineage but as a broader movement in which the mathematical construction of data spaces was migrating into the data models of programming languages.²

Counting the State Space

What makes sums and products interesting is that the analogy does not stop at metaphor. For finite types, arithmetic applies directly to the count of possible cases.

Sum Type, OR: 'It is either A or B.' Enumerations (Enum) and Union types fall into this category. Combining two types grows the number of possible cases by addition.
(Note that Enum is a simple form of a sum without a payload, while Union allows each case to carry different data.)

Product Type, AND: 'A and B exist together.' This is the class or struct we commonly write. Every time you add a field, the total number of possible cases explodes by multiplication.

Function Type: 'Put in A, get out exactly one B.' Each additional value of input A requires choosing one of the possible B values for that input. So the number of possible functions between finite types is $|B|^{|A|}$.

And when this mathematical arithmetic crosses over into programming reality, it immediately becomes a question of data model quality and a breeding ground for bugs. Consider the classic Payment class below.

public sealed class Payment
{
    public bool IsPending { get; set; }
    public bool IsPaid { get; set; }
    public bool IsFailed { get; set; }
    public bool IsRefunded { get; set; }

    public string? TransactionId { get; set; }
    public string? FailureReason { get; set; }
}

With just four boolean fields,

combinations are possible.

On top of that, simply accounting for whether the two nullable fields TransactionId and FailureReason are present or not multiplies the count by another

factor.

So even if you ignore the actual contents of every field and count only which state each field is in, this class can represent

distinct shapes.

Yet the payment states we would actually allow in the real domain are just these four:

• Pending — no TransactionId, no FailureReason

• Paid — TransactionId required, no FailureReason

• Failed — no TransactionId, FailureReason required

• Refunded — TransactionId required, no FailureReason

In other words, out of 64 possible shapes, only four are actually what we want.

The remaining 60 can be represented by the program, but they should never exist in the domain.

If a QA engineer shows up at your desk with a screenshot of a state where a payment has both failed and been fully refunded, there is really no excuse you can offer short of explaining the existence of a mathematical multiverse.

IsPaid       = true
IsFailed     = true
TransactionId = null

IsPending    = true
IsRefunded   = true
FailureReason = "card declined"

From the type system's perspective, both are perfectly valid. The compiler has no idea whether this combination makes sense in a payment system, so every caller ends up having to re-validate the object each time.

So what exactly is the problem? It lies not in the data itself, but in the State Space that has been left wide open for the data to occupy.

We granted programmers the unlimited freedom to create a payment that is simultaneously "pending and refunded." As someone with a physics background, I find such superposition of states familiar enough, but in software it is a state that simply should not exist. As the software industry's long-established wisdom confirms, when you hand programmers an overly large State Space and unlimited freedom, the first thing they do with that freedom is shoot themselves in the foot.

Let's express the same state using a Sum Type. This time, instead of C#, we can write it as a TypeScript Discriminated Union like this.

type Payment =
    | {
        readonly kind: "pending";
    }
    | {
        readonly kind: "paid";
        readonly transactionId: string;
    }
    | {
        readonly kind: "failed";
        readonly failureReason: string;
    }
    | {
        readonly kind: "refunded";
        readonly transactionId: string;
    };

Notice that the structure itself is fundamentally different.

transactionId exists only when the state is paid or refunded, and failureReason exists only when the state is failed. In the pending state, neither field exists.

As a result, TypeScript's Discriminated Union lets the type checker track the relationship between kind and the required payload, rather than requiring you to write separate validation rules each time. That said, because TypeScript uses a structural type system, it is not an exact union that physically prevents additional fields from other variants from appearing on an object. The core guarantee is type-safe narrowing and the payload required by each kind.

Status is `Paid` but `TransactionId` is missing
Status is `Failed` but `FailureReason` is missing
`kind` is simultaneously `"paid"` and `"failed"`

In the boolean model, you first create a wide-open space and then carve out the invalid parts with validation code.

With Sum Types, you create exactly four branches from the start. (This is, by any measure, considerably more efficient.)

Pending
Paid(TransactionId)
Failed(FailureReason)
Refunded(TransactionId)

Of course, switching to ADT does not mean the actual number of values becomes just four.

Even Paid alone can represent a huge number of values depending on which strings TransactionId accepts, and adding fields like payment timestamp or amount multiplies that count further.

What we are reducing here is not the total number of values, but the shape of the states.

Boolean model Valid shapes 4 / Representable shapes 64 = 1/16
Conceptual closed ADT model Valid shapes 4 / Representable shapes 4 = 1

A good data model is one that brings this ratio as close to 1 as possible.

The closer the expressible states are to the states the domain actually permits, the less defensive code you need to write to bridge the gap between the two.

Expressible States = Valid States

Once that holds, there is no longer any reason to write code that repeatedly checks whether a combination of states is valid.

Ultimately, this is the problem this post addresses.

The idea that a state space can be assembled from the simple mathematical constructs of sum and product has been around for a long time. Yet it took decades for this seemingly simple idea to find its way into the everyday syntax of mainstream general-purpose programming languages.

Why did that take so long?

The 1970s: Who Is Responsible for the Tag?

In mathematics, a value of A + B carries information about whether it came from A or from B. This is distinct from a set-theoretic union, which simply pools values from both sets together.

To implement this distinction in a computer, you need, alongside the value itself, information indicating which case is currently active. That information is the tag, or discriminant.

For example, suppose we have the following type.

PaymentState
    = Paid(TransactionId)
    + Failed(ErrorCode)

Conceptually, we can think of it like this.

tag = Paid
value = TransactionId("A123")

What does this mean? If the language ties the relationship between a tag and its payload into the type, then in a branch discriminated as Paid, the payload can only be treated as a TransactionId. Because no field named ErrorCode exists within the structure of a Paid value, it is physically impossible to accidentally stuff an error value into a successful payment.

Or alternatively,

tag = Failed
value = ErrorCode(500)

When the tag is Failed, the system reads value solely as an error code. Since the payment failed, the Failed variant has no place defined for a TransactionId from the start. The bizarre state we saw earlier with Product Types, where "a payment failed yet a transaction ID remains," cannot even be instantiated in this structure.

Simplified to its memory representation, it looks like this.

If the tag is Paid, the payload is read as a TransactionId; if it is Failed, it is read as an ErrorCode.

This is, however, a conceptual representation. It does not mean an actual compiler always stores a separate tag field in memory. Optimizations that omit the tag by exploiting bit patterns of values or unused representations are also possible. What matters is not how many physical bytes are used, but whether the program and the type system can know which variant is currently valid.

In his 1972 "Notes on Data Structuring," Hoare explained that a discriminated union value carries a tag field indicating which constituent type it came from. ³

The problem should now be clear. Who, exactly, is responsible for managing this tag?

Of course, each approach has its trade-offs. Leave it to the programmer, and you get runtime failures with 100% certainty; leave it to the compiler, and you get compile-time stress with 100% certainty. In the end, we have to decide which kind of pain we are willing to accept.

In that respect, the choices made by various programming languages are quite interesting.

Pascal left it to the programmer

Pascal had the variant record.

For example, you could make a single record hold different fields depending on whether it represented a circle or a rectangle.

type
    ShapeKind = (Circle, Rectangle);

    Shape = record
        case Kind: ShapeKind of
            Circle:
                (Radius: Real);
            Rectangle:
                (Width, Height: Real);
    end;

Here, Kind is the tag.

Kind = Circle
→ Radius is meaningful

Kind = Rectangle
→ Width, Height are meaningful

Pascal, however, also allowed a form of variant record where the tag field itself was omitted, meaning you could have a value where there was no way to tell from inside the value which variant was currently valid. Wirth later noted, in a retrospective on Pascal, that in the 1973 revised edition the tag field of a variant record was optional.

Pascal's original language definition and its variant records can be found in Jensen and Wirth's PASCAL User Manual and Report.⁴

In this design, the program had to correctly track which variant was currently meaningful, and reading a field from the wrong variant did not necessarily cause the program to halt immediately, but this is precisely where the tag stops being mere supplementary information and becomes a question of who bears responsibility for type safety.

Trust the programmer

Pascal and C share a common trait: the same storage space can be shared by values of multiple types, yet the language does not track which of those values is currently valid all the way through.

In his essay "The Development of the C Language," Dennis Ritchie recalled that ALGOL 68's union and cast constructs had an influence on the C language.

Algol 68's concept of unions and casts also had an influence that appeared later.⁵

Under the philosophy of trusting the programmer, union lets multiple types share the same storage space, but gives no indication of which member currently holds a meaningful value.

For example, if you put an integer and a floating-point number into a single union, you cannot tell from memory alone whether the current value is an integer or a float. The program must separately maintain something like an enum to remember which one is active.

Put simply, C just gives you the box.

You can put an integer in it, or you can put a float in it. But what you put in there — that's on you to remember.

It's a bit like drawing a box for the Little Prince and saying, "The sheep is inside."

The difference is that the Little Prince innocently imagined the sheep inside the box, while a C programmer bears sole responsibility, to the very end, for remembering what they put in. The Little Prince may have been happy, but the developer doing maintenance is not.

This is why the enum + union combination so commonly seen in C is essentially a tagged union built by hand.

The problem lies in managing the two values separately. You can write Integer in the tag while putting a float in the actual union. As an analogy, it's like a file that is actually a ZIP archive but has its extension renamed to .jpg.

The compiler cannot catch this disguise, nor does it need to. After all, C has that wonderfully convenient system-wide disclaimer: "Trust the programmer." Any such mistake is neatly offloaded as the fault of some feeble human who could not handle the freedom.

In the end, the problem circles back to square one.

Who, other than a human, can guarantee that the tag and the actual value actually match?

Hoare thought of the two as inseparable

C. A. R. Hoare's 1972 paper Notes on Data Structuring contains a dedicated section titled The Discriminated Union.

The core idea is straightforward: if you store a value that can take one of several forms, you must also carry a discriminant indicating which form it is in.

In other words, a value is not treated as a mere payload alone, but as

which case it is + the value belonging to that case

a combination of which case it is + the value belonging to that case.

If you strip away the tag, you must rely on external information to know how to interpret the memory at that point. And if that external information is wrong, the program goes wrong along with it.⁶

The truly significant shift begins here:

whereas Pascal and C left this relationship largely to programmer discipline, later languages moved in the direction of having the language itself know more about the relationship between the tag and the value.

CLU bound the tag and value together as a single unit.

Barbara Liskov and the CLU research team introduced a feature called oneof.

CLU's oneof represents, true to its name, exactly one of several possible cases. The key point is that the tag and the payload are not kept separate from each other.

When it is an integer, an integer value comes along with it; when it is a real number, a real value comes along. You check which case you are in and simultaneously extract the value that belongs to that case.

CLU handled this with an operation called tagcase.

This is where the contrast with the earlier C approach becomes sharp.

In C, programmers generally had to reason like this:

"I need to check whether kind is Integer first, and if it is, then read the integer member of the union."

In CLU, these two steps are folded into a single type-level operation provided by the language.

With C's union approach, the programmer had to manually check kind first and then read the appropriate member by hand. This was an inherently fragile structure that depended entirely on human discipline: because the check and the extraction were separate steps, the compiler could not stop a mismatch between the tag and the actual member, which could lead to misinterpreted values or logical state inconsistencies.

CLU's tagcase, by contrast, unified the control flow of checking which case applies with the data flow of extracting the value of that type into a single construct. CLU prevented the payload from being extracted directly without regard to the tag, and instead required that the corresponding typed value be bound to a local variable only within the branch of tagcase where that tag had been confirmed.

Determining which case applies and obtaining a value of the type for that case are never separated.

Liskov et al.'s 1977 paper also describes oneof as a discriminated union, defining it conceptually as a pair of a tag and a value.⁷

CLU also had cluster. The name can be a bit confusing, but while oneof deals with which cases a value can take on, cluster is best understood as a mechanism that hides the internal implementation of a type from the outside world.

This is why the abbreviation ADT today actually stands for two different things.

Algebraic Data Type concerns the possible shapes a value can take, while Abstract Data Type concerns how much of the internal representation is exposed.

To summarize further: if CLU's oneof illustrates the Sum Type aspect of algebraic data types, it can be said to control "the shapes of values permitted in the State Space."

Abstract Data Type (cluster) can be understood as controlling "the boundary through which those values interact with the outside." It is also possible to hide an algebraic data type inside a module and expose it as an abstract data type.

Ada checks for incorrect tag access.

In Ada, the language manages this relationship more directly.

Ada's variant record has a discriminant, which determines which variant the current record represents.

For example, a Printer device has fields needed for a printer, and a Disk device has fields needed for a disk. If the current discriminant is Printer but you try to read a disk-specific field, Ada does not treat this as a valid access.

When necessary, a discriminant check is performed at runtime, and if it fails, a Constraint_Error is raised.⁸

The important trend to notice here is

that rules the programmer once had to remember in their head began to be taken over as rules enforced by the language itself.

In C, it was up to the programmer to remember "which value did I put in here?"

In Ada, at least part of that relationship is something the language knows about and enforces.

Of course, the more the language checks, the more rules the programmer must follow, but that arguably makes it safer.

The choice is between suffering through incorrect memory reads at runtime or suffering through convincing the compiler and type system at compile time. It ultimately comes down to where you want to feel the pain. What is unfortunate, though, is that most failures in modern systems trace back to trusting humans.

TypeScript splits the responsibility down the middle

The reason I wrote this post is actually TypeScript, and what is interesting is that this problem still has not been fully solved.

"Who records which case we are in, and who proves that the record matches the actual value?"

This question, which has persisted since the 1970s, defines the history of programming languages as a gradual process of transferring responsibility from the developer to the compiler by force.

In TypeScript, developers typically create a field like kind themselves.

For example, if a download state is one of queued, running, completed, or failed, you put kind in each object, defining that running has a progress field and failed has an errorMessage field.

Up to this point, it might look superficially similar to keeping a separate enum in C, but the difference comes next.

The moment you check state.kind === "running", TypeScript tracks the fact that state is in the running state within that branch, and therefore also knows that progress exists.

In other words, TypeScript splits the work in half.

The tag is created by the developer. The relationship between the tag and the payload is tracked by the type checker.

In C, both were essentially a matter of programmer discipline. In TypeScript, creating the discriminant is still the programmer's responsibility, but once it is defined correctly, the compiler follows the relationships from there.

Languages like Rust, Swift, and F# that support Sum Types go one step further, though: they let you express which cases exist and what value each case carries as part of the Sum Type definition itself. (I should note that I am not deeply familiar with those three languages, so I will not go into great detail about them.)

One question repeated itself from the 1970s onward.

Who records which case is active, and who proves that the record matches the actual value?

How much of this responsibility to leave to the programmer, and how much to delegate to the compiler, is a thread woven through the evolutionary history of modern languages. Looking at where things have landed, it seems far safer to push most of it onto the compiler's side.

From 1969 to 1980, exhaustiveness checking is thought to have emerged from the demands of formal proof.

Pattern matching and Exhaustiveness Checking can be described as the obsessive byproduct of efforts to mathematically prove the logical integrity of programs.

In 1969, Rod Burstall, in "Proving properties of programs by structural induction," presented a method for proving properties of programs over recursive data structures using structural induction. The preconditions for this proof to hold logically were clear.

1. The ways to construct a value must be finitely enumerable.

2. Each constructor must be mutually exclusive.

3. The proof must cover every constructor case without omission.

If the first two conditions represent the design philosophy behind today's Tagged Union, the last condition is the mathematical backbone of the Exhaustiveness Check by which the compiler governs control flow.

Robin Milner's "A Theory of Type Polymorphism in Programming," published in 1978, can be said to have laid the framework for the early ML family of languages by explicitly introducing + for sum and × for product.

ML (Meta Language) was originally designed as a meta-language to maintain control over the LCF theorem prover, where the syntax tree of the object language could not be arbitrarily decomposed or assembled but had to be produced only through trusted inference rules. The systemic safety of LCF came precisely from this strict control over construction, and this became the ground in which Algebraic Data Types (ADT) would eventually take root.

Finally, in 1980, with the language HOPE published by Burstall, MacQueen, and Sannella, "constructor-tagged Sum Types," "pattern matching," and "compiler-verified exhaustiveness" were physically unified within a single system. Of course, it would be wrong to say that what we see today in Rust or Swift was complete at that point. Erasing the forty years of engineering struggle involving the combination with records, memory representation optimization, generics, and separate compilation would be a mistake. What is fair to say, however, is that the core architecture, in which the type system and the compiler interact to enforce data integrity, had at last appeared.

Today, we do not need to learn a complex theorem prover just to enjoy the runtime safety that Exhaustiveness Checking provides. That is genuinely fortunate, since I myself gave up trying to learn one.

Using Exhaustiveness Checking as a Change Detector in Practice

What are the benefits of ADTs? Prettier code? Code aesthetics are personal, of course, but the benefits do not stop there. (It would be accurate to say the code gets more complex, too.)

The usual reason to use an Exhaustiveness Checker is that the compiler produces a list of every place that needs to be updated whenever a new state is added.

const assertNever = (value: never): never => {
    throw new Error(`Unexpected value: ${JSON.stringify(value)}`);
};

const getDisplayText = (state: DownloadState): string => {
    switch (state.kind) {
        case "queued": {
            return "Waiting";
        }
        case "running": {
            return `Downloading: ${state.progress}%`;
        }
        case "completed": {
            return `Saved to ${state.filePath}`;
        }
        case "failed": {
            return `Failed: ${state.errorMessage}`;
        }
        default: {
            return assertNever(state);
        }
    }
};

If you add "paused" to DownloadState, the state in the default branch is no longer never, and the assertNever call becomes a compile error. If there are ten such functions, all ten show up in the list.

There is a prerequisite here: TypeScript does not automatically emit an error when a switch case is missing. You need either the assertNever idiom, an explicit return type combined with noImplicitReturns enabled, or a Record<Kind, Handler> mapping in place of the switch. Without at least one of these, adding a new variant still compiles cleanly, so you must deliberately leave one of these mechanisms in the code if you want to use Exhaustiveness Checking as a change detector.

In C#, Discriminated Unions are not yet in a stable release, so you approximate them with a record hierarchy.

using System;
using System.Diagnostics;

public abstract record PaymentState
{
    private PaymentState()
    {
    }

    public sealed record Pending(DateTimeOffset CreatedAt) : PaymentState;

    public sealed record Paid(string TransactionId, DateTimeOffset PaidAt) : PaymentState;

    public sealed record Failed(string Code, string Message) : PaymentState;

    public sealed record Refunded(string TransactionId, DateTimeOffset RefundedAt) : PaymentState;
}

public static class PaymentFormatter
{
    public static string Describe(PaymentState state)
    {
        return state switch
        {
            PaymentState.Pending pending => $"Pending since {pending.CreatedAt:O}",
            PaymentState.Paid paid => $"Paid: {paid.TransactionId}",
            PaymentState.Failed failed => $"Failed: {failed.Code} - {failed.Message}",
            PaymentState.Refunded refunded => $"Refunded: {refunded.TransactionId}",
            _ => throw new UnreachableException(),
        };
    }
}

Making the base constructor private and defining variants as nested types prevents external code from adding new subtypes. This works because nested types can access the outer type's private members. The limitation is the final branch: since the compiler cannot prove the hierarchy is closed, omitting the last branch produces a CS8509 warning, while including it leaves an unreachable exception in the code.

Python combines the match statement from 3.10 with typing.assert_never from 3.11, but nothing is caught statically unless you integrate mypy or Pyright into your CI pipeline. If execution actually reaches typing.assert_never(), an exception is raised at runtime.

Python did not introduce ADTs itself. Instead, it made the clever decision to introduce syntax for consuming ADTs while leaving the production of them to the user.

default: throw blocks missing cases at runtime but gives up static change detection for new variants, deferring to the compiler what it should have caught until an actual call site receives that value. TypeScript's assertNever(state) is a mechanism that keeps the default branch while still making a new variant a compile error, so the two should not be treated as the same thing.

1985: The Year It Was Named

Turner's 1985 Miranda paper contains a section titled "Algebraic data types" and explicitly discusses free algebras. It is one of the earliest confirmed explicit uses of the term. HOPE simply called them data types.

We call it a free algebra, because there are no associated laws, such as a law equating a tree with its mirror image.

In a free algebra, constructors are mutually distinct and each constructor is injective. As a result, the decomposition of a value into its constructor is unique. Because no commutativity law is given to make Add(x, y) equal to Add(y, x), the two values are distinct whenever x and y differ. The commutativity of addition is not a property of the constructor Add; it is a law that belongs to the functions that interpret it.

Because decomposition is unique, structural pattern matching works straightforwardly. Adding equational laws to constructors allows different expressions to denote the same value, which can make naive syntactic matching incompatible with those equations. This does not make it impossible: you can handle it through normalization, view patterns, or quotient-aware elimination. Miranda actually experimented with types carrying laws and later removed the feature because it made type inference significantly more complex.

The algebraic laws of sums and products, together with cardinality arithmetic, are also a legitimate context for explaining the name. There is no basis for asserting that either is the sole etymological origin. What the author verified through research is simply that Turner's usage explicitly pointed to the free algebra side.

In recursive ADTs, the structure becomes the grammar

List<T> = Nil + Cons(T × List<T>)

The initial algebra of the functor F(X) = 1 + T × X is the finite, well-founded list. The equations alone do not fix the semantics. Taking the initial algebra yields finite inductive lists, while taking the terminal coalgebra admits infinite structures as well; Miranda itself is a non-strict language and therefore handles potentially infinite lists. What initiality guarantees is that, once you specify how to handle each constructor, the function over the entire structure is uniquely determined, and fold follows directly from this.

type Expression =
    | {
        readonly kind: "number";
        readonly value: number;
    }
    | {
        readonly kind: "add";
        readonly left: Expression;
        readonly right: Expression;
    }
    | {
        readonly kind: "multiply";
        readonly left: Expression;
        readonly right: Expression;
    };

const evaluate = (expression: Expression): number => {
    switch (expression.kind) {
        case "number": {
            return expression.value;
        }
        case "add": {
            return evaluate(expression.left) + evaluate(expression.right);
        }
        case "multiply": {
            return evaluate(expression.left) * evaluate(expression.right);
        }
        default: {
            return assertNever(expression);
        }
    }
};

An evaluation function naturally follows the shape of the type definition. That is why parsers, compilers, rule engines, and UI state trees fit ADTs so well. Stack consumption during recursive traversal is, however, a separate concern. A deep tree will grow the stack proportionally to the input depth, so when parsing untrusted input you should either bound the depth or switch to an explicit stack. Type checking does not solve this problem.

Huet introduced the zipper in 1997, and McBride showed in 2001 that the formal derivative of a regular type computes the one-hole context. d/dT (T × T × T) = 3 × T × T. This means there are three ways to leave one slot empty in a triple. The fact that types can be differentiated has almost no practical application in day-to-day work.

1965 and 2009, null

In 1965, Tony Hoare introduced the null reference into ALGOL W, and at QCon in 2009 he publicly apologized, calling it his "billion-dollar mistake." The billion-dollar figure is admittedly a 2009 estimate, but it is remarkably rare in this industry for an inventor to formally declare their own design a failure and apologize for it. (Personally, I will admit I have some sympathy for the convenience null offers when modeling reality.)

The essence of this "billion-dollar mistake" is that null substituted, far too cheaply, for the place where an Algebraic Data Type (ADT), specifically a Sum Type, should have stood.

This may not be immediately obvious to everyone, but the most representative implementation of a Sum Type is precisely the Option (or Maybe) type. Option explicitly defines the State Space of a value as exactly two variants: the case where a value exists (Some) and the case where it does not (None).

If null is a phantom that parasitizes every reference type in secret, Option elevates the very absence of a value to a legitimate state that the language can recognize and control.

It is common to hear the analogy that "null is an Option type without a Tag," but this holds only as a metaphor; as a technical statement it is inaccurate.

The real difference does not lie in the presence or absence of a physical tag.

For instance, Rust exploits the null bit pattern as a niche in certain types such as Option<NonNull<T>>, representing absence without any additional physical memory tag.

The most fundamental structural difference is whether the absence of a value is made explicit in the Type Contract and whether the compiler forces you to unwrap it before use.

• Unchecked / Legacy Null Reference: The possibility of absent data is not properly reflected in the type contract. A caller can access a value while overlooking the possibility of null, creating a situation where the API surface appears to always carry a value even though the value may actually be absent.

• Option: The absence of a value is itself made explicit as a contract in the type system. To obtain the value, you must pass through a control flow that unwraps the Variant.

The Need for Option

The biggest problem with null is that you cannot tell directly from the data itself that a value is absent.

Consider a single function.

FindUser(id) → User

Looking at this declaration alone, the caller assumes that a User will always be returned.

But suppose the actual implementation returns null when it cannot find the user.

Then the function's true contract is actually this.

FindUser(id) → User or nothing

The problem is that the type only says User.

null exists in practice, but it does not exist in the contract.

What Option<T> does is bring this hidden case out into the open, making it part of the type itself.

Option<User>
    = Some(User)
    + None

The meaning is simple.

A user may or may not exist.

What matters here is not that Option stores a value more safely, but that it makes it impossible for the caller to ignore the possibility that the value may be absent.

You cannot obtain a User directly; you must first check whether it is Some or None.

Some(User)
Value present

None
Value absent

So it is more accurate to think of Option not as a way to eliminate null checks at runtime, but as a way to elevate that check into the function's contract.

In other words,

is closer to the truth.

The reason this structure is necessary is simple.

The absence of a value in a program is not always an error.

A user might not have entered a nickname, the cache might not yet have a value, or a search might return zero results. These are not failures.

The absence of a value is simply part of a normal State Space.

Option carries no reason

But Option is intentionally low on information.

Consider the following three cases.

The first two cases may be adequately expressed as None.

But if the third case is also turned into None, problems arise.

The caller now has no way to tell.

Is the user missing? Is the DB down? Is the network disconnected?

Because Option has no room to carry a reason.

Option<T>
    = Some(T)
    + None

None simply means absent.

It says nothing about why.

So if the reason for absence changes the program's behavior, you need to step down from Option.

That's when Result is what you need.

Result<T, E>
    = Ok(T)
    + Error(E)

For example, a user lookup can be made even more explicit.

LookupOutcome<T>
    = Found(T)
    + NotFound
    + QueryFailed(DbError)

Here, the three cases are no longer hidden behind a single null or None.

• Found

• Not found

• The lookup process itself failed

Each is a distinct state.

This is why Sum Types are used for error handling.

Result pulls failure into the return type

When you handle a predictable failure as an exception, control flow escapes outside the function's return type.

User LoadUser(id)

even if the signature says:

User
or
DbException
or
TimeoutException
or
...

it could actually be:

By contrast, modeling with Result brings failure back inside the type.

LoadUser(id)
→ Result<User, LoadUserError>

The caller can now tell, just by looking at the function's declaration, that this function can fail.

And from this a natural pattern emerges: on success, continue with the next computation; on failure, skip the remaining computations and propagate the error as-is.

type Result<TValue, TError> =
    | {
        readonly kind: "ok";
        readonly value: TValue;
    }
    | {
        readonly kind: "error";
        readonly error: TError;
    };

const bindResult = <TValue, TNext, TError>(
    result: Result<TValue, TError>,
    transform: (value: TValue) => Result<TNext, TError>,
): Result<TNext, TError> => {
    if (result.kind === "error") {
        return result;
    }

    return transform(result.value);
};

This is ultimately the essence of monadic chaining. Since the 2010s, object-oriented languages have been transfusing functional paradigms to prevent runtime exceptions (try/catch) from spiraling out of control, and this pattern has grown beyond a mere "technique" to become the most fundamental control-flow standard for designing predictable systems.

On success, proceed to the next computation. On failure, stop advancing and propagate the failure.

Seen this way, Result, which seemed so grand at first, turns out to be nothing more than a Sum Type that reifies control flow as data.

Exceptions and Result are not the same kind of failure

In practice, when people first learn Result they often develop an obsession with converting every exception into a Result, but there is no need to unconditionally make every failure a Result.

Consider these examples.

• A user does not exist

• A payment authorization is declined

• A file format is invalid

• Permission is denied

These are all things a program can reasonably anticipate.

Failures like these are part of the domain.

On the other hand,

• OutOfMemory

• Runtime internal invariant violation

• Programmer uses an incorrect index

• Internal library defect

making every such case a Result variant is rarely meaningful.

So in general, most practitioners recommend drawing the boundary around two broad categories.

• Predictable failures

-> Result

• Programming errors / fatal system errors

-> Exception / fail-fast

Programming is hard precisely because this boundary is rarely as clean as a knife's cut. "Murder is wrong" is a simple proposition, but deciding whether it is ethical for a shipwreck survivor on the brink of starvation to eat a corpse in order to survive requires genuine philosophical judgment. In the same way, programming means confronting a narrow gray zone between seemingly unpredictable defects and domain failures every single day.

There are languages that embody this ambiguous dilemma, and C# is a prime example.

The .NET BCL has historically made heavy use of exceptions. The moment your code touches an external system, whether for file I/O, networking, databases, or serialization, countless APIs throw exceptions.

That said, you should not let those exceptions flow unchecked into your business logic.

If the outside world throws an exception, catch it at the boundary and convert it into a failure that the domain can understand.

.NET / External API
        ↓
Exception
        ↓
Boundary
        ↓
Result<Success, Failure>
        ↓
Domain / Application

For example, suppose a database driver throws a TimeoutException.

There is no reason for the domain logic to need to know about this exception type.

At the boundary:

TimeoutException
→ QueryFailed.Timeout

is all you need to do.

This way, exceptions remain the error-delivery mechanism of external systems, while Result becomes the failure contract inside our program.

Mixing the two indiscriminately creates a dual error channel, but keeping a clear boundary makes each role clear as well.

can be summarized as follows.

The point is not that you should avoid using Result in an exception-centric ecosystem like C#, but that you need to decide where exceptions end and where Result begins.

The fact that F# actively uses Result and Option even on the same .NET runtime and BCL is a good example that this separation is entirely achievable.

Domain State Modeling: Option vs Result vs Custom ADT

There is no need to be bound to the generic names Result or Option. The real purpose of introducing Algebraic Data Types (ADT) into control flow is not to follow a particular naming convention, but to perfectly close (Close) every predictable case a system may encounter within the boundaries of the type system.

Are None and Some(null) the same?

This is actually one of the more confusing points, and there is one peculiar type involved.

Option<T?>

At first glance, it seems strange and hard to understand.

None means there is no value, and null also means there is no value, so why would you layer one on top of the other?

In most cases, it's not actually needed.

None
Some(null)

If these two mean exactly the same thing, the State Space is simply increased by one, needlessly.

But if the two states carry different meanings, that changes things.

The PATCH API is a prime example.

Let's say we are updating a user's name.

A request may need to carry one of three distinct meanings.

None
Do not modify this field

Some(null)
Explicitly delete the existing value

Some("Alice")
Change the value to Alice

Here, all three states have different meanings.

Therefore, Option<T?> is also valid.

The problem arises when this form is carried as-is into the internals of the system.

The None / Some(null) / Some(value) of a PATCH DTO is a boundary representation for interpreting the meaning of an external request.

Once the meaning has been decided, it is better to normalize it internally with a more explicit command.

PATCH DTO
    ↓
None
Some(null)
Some(value)
    ↓
Boundary parsing
    ↓
NoChange
ClearValue
SetValue(value)
    ↓
Domain

In other words, what we actually needed was not null, but a third state.

FieldUpdate<T>
    = NoChange
    + Clear
    + Set(T)

With this change, null disappears again from inside the domain.

Accepting ambiguous external representations at the boundary is an entirely different problem from allowing that ambiguity into the internal model.

The external JSON is something we cannot control.

But the internal State Space is something we can control.

Epictetus opens the first line of the Enchiridion with this: "Some things are in our control, and others are not (Dichotomy of Control)." Programming often begins from exactly this same dichotomy.

The JSON payloads pouring in from outside, user inputs, and third-party API responses are the "chaos of the external world" that we cannot control. We have no way to fundamentally prevent a frontend from ignoring the agreed-upon schema and sending null, or a payment gateway from returning an error code not found in any documentation. But the Internal State Space that accepts that chaos and drives the runtime is entirely within our control.

Stoic philosophers defended their own "Inner Citadel" by filtering external events (Impressions) through reason (Assent), preventing them from disturbing the inner world. The boundary of a robust system performs exactly the same philosophical filtering process. Dragging uncontrolled external raw data (Raw JSON) directly into the business domain is the equivalent of opening the gates of your inner citadel and wheeling in the Trojan horse yourself.

And so, at the boundary, we make a Stoic decision: we accept the ambiguous external values, but we validate them rigorously, forcibly assign meaning appropriate to our domain, and pare down the representable possibilities to the extreme, transforming them into a narrower, harder Narrowed Type.

Ultimately, the ambiguous string or nullable blobs thrown by an external API must, the moment they pass through the rational filter of the system boundary, be normalized into a Result or a closed Sum Type (ADT) that the domain can control completely. Substituting the uncontrollable, infinite possibilities of the outside world with the controllable, closed states of the inside: this is the engineering Stoicism that preserves a system's logical integrity even amid the uncertainty of the external world.

From 1990 to 2005, why did it take so long to gain adoption?

The role of Sum Types had long been occupied by subtype polymorphism. Handling one of several cases was solved with abstract classes and subclasses, and when different branching logic was needed for each case, the Visitor Pattern was used.

The Visitor Pattern is essentially "a manual routing technique that forcibly implements pattern matching, which the language does not natively support, through runtime polymorphism."

Because the compiler cannot safely branch on types the way a match statement does, developers had to manually wire together a double dispatch structure: opening an Accept method inside the data object to receive a visitor, then passing itself back to the visitor's Visit method. The reason the Visitor Pattern is so cumbersome is ultimately that people were hand-patching with interfaces and callbacks what the compiler should have been doing.

Put this way, it might sound like a bad pattern, but it was an inevitable socioeconomic product of a generation that grew up in languages without Sum Types. In 1994, the Gang of Four (GoF) called it a great "design pattern"; today, we simply call it the match keyword. Of course, somewhere out there, the Visitor Pattern is still being churned out to this day.

Framing this as the Expression Problem makes the tension along the axis of extensibility clear.

• New implementations (types) keep getting added: Object-oriented programming wins here. (In the Visitor Pattern, adding a new type means ripping apart every Visitor class, which is a nightmare.)

• New operations keep getting added: ADTs win here. (You can write new pattern-matching functions without touching the existing data structures.)

My interpretation is that the axis of extensibility in 1990s industry was on the implementation side: GUI widgets, device drivers, file format handlers, plugins. Today, more domains have the opposite axis: protocol messages, UI state, compiler IR, event sourcing. The set of variants is fixed, while the operations performed on top of them keep growing.

Where ADTs don't fit

The Expression Problem may be uncertain as a historical interpretation, but as a practical decision criterion it is largely settled into recognizable patterns.

Cases where it is better not to use a Sum Type also arise here. Values that can be held simultaneously, such as canRead, canWrite, and canDelete, are not mutually exclusive states, so a Product Type is the right fit. If external modules need to keep registering new implementations, an interface is the right choice. If dozens of variants pile up in a single union, the type itself becomes a God Object, so don't mix bounded contexts.

Create a new type only when it protects a real invariant or a meaningful semantic distinction. Wrapping every string as UserName leaves nothing but overhead, but if you need to distinguish a validated email from an arbitrary string at the type level, creating EmailAddress is justified.

From 2004 to 2026: The Road Back

It took roughly 24 years from the mathematical foundations appearing in 1961 to the name "algebraic data types" being confirmed in 1985. The combination of constructors, pattern matching, and exhaustiveness checking was already present in HOPE by 1980, yet it took another roughly 30 years to spread into major general-purpose languages.

I believe this 30-year delay was not the result of technical limitations but of inertia surrounding control.

The object-oriented ecosystem that dominated the industry from the 1990s onward wielded subtype polymorphism as its weapon and was captivated by the seemingly infinite extensibility of dynamic runtime expansion. Programmers enjoyed the freedom to throw absent states or predictable failures at null and exceptions whenever they pleased, and they largely looked away from the fact that this freedom was planting uncontrollable time bombs in the runtime. ADT and Exhaustiveness Checking, by contrast, reclaimed the developer's fragmented freedom and confined it under the compiler's strict proof. It was therefore inevitable that the mainstream ecosystem needed both community resistance and a generational turnover before it could embrace them.

Java has incrementally introduced records, sealed classes, and switch pattern matching, while C# has expanded nullable reference types, records, and pattern matching. As of 2026, the C# 15 preview adds union types and closed hierarchies, making it ever clearer that the language is moving toward expressing closed State Spaces directly.

As the industry has matured and programs have grown increasingly complex, the cognitive load placed on programmers has grown with it, and modeling techniques for frequently recurring business patterns and control flows have matured in tandem. In other words, the field has arrived at a pragmatic programming evolution: delegate patternable State Spaces to ADTs and the type system to mechanically reduce cognitive burden, while reserving polymorphism exclusively for dynamic, open requirements that are genuinely difficult to model upfront.

There are, of course, early adopters such as Jane Street that have actively used ADTs and Exhaustiveness Checking for a long time.

And now, as LLM-generated code becomes increasingly common, these closed types may gain new importance as a mechanism that constrains the State Space not only for human developers but also for generated code.

We have entered an era where LLMs, which do nothing more than predict the next token probabilistically, pour out a system's internal logic at a frightening pace. Ultimately, the central axis of software engineering will shift entirely from "how do we implement logic" to "how do we constrain state." When that time comes, the author believes ADT programming will serve as a powerful pillar.

Primary Sources

• John McCarthy, A Basis for a Mathematical Theory of Computation (1961)

• John McCarthy, Definition of new data types in ALGOL x (1964)

• R. M. Burstall, Proving properties of programs by structural induction, The Computer Journal 12(1) (1969)

• C. A. R. Hoare, Notes on Data Structuring, in Dahl, Dijkstra, Hoare, Structured Programming (1972)

• Robin Milner, A Theory of Type Polymorphism in Programming, Journal of Computer and System Sciences 17(3), 348-375 (1978, manuscript 1977)

• R. M. Burstall, D. B. MacQueen, D. T. Sannella, HOPE: An experimental applicative language, ACM LISP Conference (1980)

• David Turner, Miranda: a non-strict functional language with polymorphic types (1985). Experiments with and elimination of lawful types

• Dennis Ritchie, The Development of the C Language (1993)

• Gérard Huet, The Zipper, Journal of Functional Programming 7(5) (1997)

• Conor McBride, The derivative of a regular type is its type of one-hole contexts (2001)

• Tony Hoare, Null References: The Billion Dollar Mistake, QCon London (2009)

• Record of Yaron Minsky's maxim as cited in January 2009

• Alexis King, Parse, don't validate (2019)

Language Documentation

• Ada 83 Rationale, 4.7 Discriminants

• TypeScript 1.4 Release Notes (union type)

• TypeScript 2.0 Release Notes (tagged union, strictNullChecks)

• JEP 409 Sealed Classes

• JEP 440 Record Patterns

• JEP 441 Pattern Matching for switch

• Java 26 MatchException

• Effective Go, Multiple return values and errors

• Python typing.assertnever

• Rust std::ptr::NonNull (niche optimization)

• OCaml Polymorphic variants

• Microsoft Learn, Union types, C# reference

• Microsoft Learn, What's new in C# 15

• Microsoft, Explore new features available in C# 15 preview, .NET Blog (2026-08-24)

• Unity Entities, Archetypes concepts

• Unity Entities, Tag components

• Hillel Wayne, A Very Early History of Algebraic Data Types

• Lysxia, Where does the name "algebraic data type" come from?