Algabraic Data Types Are Not What you Think They Are

I’ve noticed that some tech content creators have cemented in their heads this idea that Abstract Data Types (ADTs) are just a fancy way of saying sum types, which is an awful shame because ADTs are one of my favorite insights from category theory and can even be an entryway to understanding the big ideas like the Curry–Howard isomorphism (i.e. currying).

The worst part is, from what I’ve seen online most creators don’t even explain how ADTs got their name in the first place? Which is mind boggling to me, but I digress.

ADTs are, as the name suggests, a way to create new types by algebraically manipulating existing types. It can sound a bit alien if you’re not used to abstract algebra (I mean algebra on data types?) but trust me, most of it can fall out using a bit of intuition and a guiding hand.

Product types

The easiest entry point to ADTs isn’t sum types but actually product types, which most people either skip or cover at the very end of their content. You may be surprised to learn that you already know product types, in fact, you’ve certainly written hundreds! If you’re a C++ developer I’m talking about this code:

class Prod {
public:
    int x;
    float y;
    ...
}

or perhaps if you’re a Python developer, in which case this will look familiar:

@dataclass
class Foo:
    x: int
    y: str

or you may have worked in a language where functions can return “multiple arguments”:

def foo(x):
    return x, x + 1

These are all examples of product types, which in code can be thought of as combinations of multiple types together. They’re combined in the sense that every time you initialize (or declare/instantiate for all 4 of you ANSI C stans out there) one of them, you have to instantiate the rest of them too.

If you’ve taken linear algebra before you might remember 2-dimensional vectors being declared like this: $v\in\mathbb{R}\times\mathbb{R}$ This is a good hint as to why they’re called product types and is very analogous to what we’re doing here.

To really hit the point home, Ocaml straight-up defines product types using the astericks symbol:

type Rectangle = float * float

In type theory we call this the cartesain product of types, which is well defined for any valid type. So in type theory we can multiply the string type with the integer type with the vector type and have everything work out fine.

It’s important to recognize that multiplying the TYPES is wholy different from multiplying INSTANCES of said types.

Sum types

The other main category of ADTs, which are usually covered first in my experience, are sum types, which can be a bit trickier to work with but are well worth the effort of getting used to. If you’ve written some Python code you’ve probably seen a function where some code branches return different types than others (this is a super common code smell and usually I try to teach people to avoid doing this because it can lead to very confusing code if not typed). Here’s a simple example:

def intorstr(x, y):
    if x > y:
        return f"my value is {x - y}"
    else:
        return y - x

If you call this function with intorstr(1, 2) you’ll get back the integer 1, but if you called it with intorstr(2, 1) you’ll instead get back the string "my value is 1". In this situation, how would you characterize the return type? The function intorstr is said to have a sum type as its return type.

Sum types, like product types, get their name because they’re created in type theory by adding the types together, which finally begs the question: Can you do both multuplication and addition in the same type expression? What if I wanted to express the signature of a function that could either return a tuple of 2 ints or a tuple of 3 strings? It would look something like this:

which in Python 3.12 can be written like so:

type ReturnType = tuple[int, int] | tuple[str, str, str]

But you didn’t come to this blog post to see simple Python types, did you? No! you came to understand what the heck those crazy rust enums you saw mean. Here’s one of those more interesting examples that:

enum E {
    A,
    B(i32),
    C(u64, u8, u64, u8),
    D(Vec<u32>),
}

So here’s a challenge: how do we express this in type theory? To answer that, notice that it’s perfectly legal in rust to instantiate a variable as the A variant of E:

let a = E::A;  // OK

Further - and this is the key part - even if we add other variants that have no data, everything still works fine and we can differentiate between them. In fact, any time you instantiate variables as one of the variants with no data, they always will evaluate as equivalent:

#[derive(Eq)]
enum F {
    A,
    B(u32),
    C,
    D(u32),
}

fn foo() {
    let a = F::A;
    let b = F::b;
    let c = F::A;

    assert!(a != b); // OK: they're distinct
    assert!(a == c); // OK: they're equivalent
}

So to answer the challenge, the way you would write this is:

where

I’ve noted that the cardinality of the types $A$ and $C$ are 1, meaning that in their set theory representation they would only have 1 element in them. Types that only have 1 element in them have a special property known as being isomorphic to each other. This means that you can translate between them with no loss in information. Because of this, we’ve defined a special type - the unit type - which types $A$ and $C$ are isomorphic to.

the unit type is actually defined in the rust docs too - you can instantiate it using the empty tuple ()

In type theory you can denote the unit type as the literal $1$, so we can rewrite our rust enum in type theory in a more simplified way:

I did the last simplification on purpose to prove a point here: any Rust enum you create that has the same type theory representation will always be equivalent to each other up to isomorphism. For example, all of these enums are equivalent (up to isomorphism):

enum X {
    A,
    B,
    C(u32),
    D(u32),
}

enum Y {
    A(u32),
    B(u32),
    C,
    D,
}

enum Z {
    B(u32),
    C,
    A,
    D(u32),
}

These types are looking an awful lot like numbers…

Type theorists use the same symbols of addition and multiplication as we do for numbers for a good reason. This “feels like addition” and “feels like multiplication” can be made even more concrete with this mapping from one field to the other:

In fact, numbers aren’t the only place where we find these similarities. If you’re familiar with propositional logic you can also make a similar mapping to type theory:

A Final note about implementation details

I wanted to quickly touch on the implementation detail of Rust with its enums. Unlike C, rust doesn’t provide a stable ABI which means they get to map enums to memory in whatever order and method they want. In the above example of the enum E, we can see the compiler makes use of 8-byte alignment to pack the values in a smarter way:

print-type-size type: `E`: 32 bytes, alignment: 8 bytes
print-type-size     discriminant: 1 bytes
print-type-size     variant `D`: 31 bytes
print-type-size         padding: 7 bytes
print-type-size         field `.0`: 24 bytes, alignment: 8 bytes
print-type-size     variant `C`: 23 bytes
print-type-size         field `.1`: 1 bytes
print-type-size         field `.3`: 1 bytes
print-type-size         padding: 5 bytes
print-type-size         field `.0`: 8 bytes, alignment: 8 bytes
print-type-size         field `.2`: 8 bytes
print-type-size     variant `B`: 7 bytes
print-type-size         padding: 3 bytes
print-type-size         field `.0`: 4 bytes, alignment: 4 bytes
print-type-size     variant `A`: 0 bytes

we see that, because a discriminant is being stored (to tell in the runtime which variant the variable’s state is in) there’s no need to store even 1 byte for the empty variant A

This is important to note because usually only variables of the type Void should have a memory size of 0, while variables of type Unit usually have 1 byte stored, because instantiable variables can’t have no memory mapping!

Another thing we see is that variant D has 7 bytes of padding, because the actual size needed is 24 bytes, which wouldn’t have as easy of a cachelining as a memory size of 32 bytes. Since all variants need less than 31 bytes to store their data, we can strategically add padding in all the variants that store data to optimize the cacheline.