Jadon.

Introduction to Algebraic Data Types

plt

Continuing from last time on our quest to learn everything about Type Theory, today’s post will be an introduction to Algebraic Data Types. ADTs are a fundamental part of many type systems because they allow the user to express structures eloquently.

There are only two ADTs that are used throughout many programming languages, so they will be the only ones we will look at today.

Product Types

Product Types are akin to structs in C or classes in Java. They’re usually called records in functional languages. They hold multiple fields of different types. The identifying factor here is that all instances of a product type hold the same types of values. Here’s an example:

struct Container {
    int x;
    double y;
};

When you construct a Container, both x and y are required to have a value that is of their defined type. You can’t construct a Container with a char and a long, for example. Every instance of a Container has an x that is an int and a y that is a double.

Most languages have structures analgous to product types, and because of that most people understand them quite well. The same can’t be said for Sum Types.

Sum Types

Sum Types are akin to enums in Rust or sealed classes in Kotlin. They consist of a list of possible variants of a type. An instance of a sum type can only occupy one variant.

enum Expr {
    Num(i32),
    Add(Expr, Expr),
    Subtract(Expr, Expr),
}

Here you can see I have defined an enum that represents an expression containing numbers, addition, and subtraction. When I create an instance of this type, I have to choose a variant to create. My instance can’t be a Num and an Add at the same time.

When I choose a variant to create, I have to create values for all of the types in that variant. I cant create a Num without an i32, and I can’t create an Add without two Exprs.

It’s also important to note that ADTs can be recursive. Expr here refers to itself, so you could construct an infinite tree of expressions (or at least as big as your hard drive could hold). Some languages like Rust hold constraints on recursiveness such as requiring the type to have a known size, which would require indirection through a pointer.

False Examples

It’s important to be aware that not all languages share the same vocabulary, and while an enum in Rust is a Sum Type, enum in Java, C, & Go is used to create a list of constant values.

public enum Candy {
    SNICKERS(1.2),
    MARS_BAR(2.4),
    STARBURST(5.6),
    KIT_KAT(4.5);

    private float price;

    public Candy(float price) {
        this.price = price;
    }
}

In this example, I’m defining an enum in Java that declares different kinds of candy. I can’t construct a type of SNICKERS because it isn’t a variant of Candy. It’s equivalent to writing:

public static final SNICKERS = new Candy(1.2);

This post is a little short, but with the whole world in quarantine I hope to do a little more writing. I’m also thinking about writing things out of order because these beginning topics aren’t super interesting to me. Stay tuned to see where this goes!

Further Reading