CS 242: Algebraic data types

Now that we understand the essentials of the theory of type systems, the next big question is: where to? There’s many aspects of type systems we could potentially explore, but so little time. I’ve picked three particular topics in type systems (algebraic data types, recursive types, and polymorphic types) that are both practically useful in day-to-day programming, and also embody a wide range of core concepts in type theory.

ADTs by example

The basic idea behind algebraic data types (ADTs) is to represent complex data structures in our type system, more than just integers and functions. We want to represent relations between data, specifically the notions of “and” and “or”. We need types that represent a composite of A and B, or an option of A or B.

Records

The former idea is quite common in programming languages. C has structs:

typedef struct {
  int x;
  int y;
} point_t;

void main() {
  point_t origin;
  origin.x = 0;
  origin.y = 0;
  printf("(%d, %d)", origin.x, origin.y);
}

Python has tuples:

origin = (0, 0)
print(origin[0], origin[1])

These are both instances of the same core idea: types that contain multiple components. If the components are anonymous, like in the Python example, we call them tuples¹, and if the components have names, we call them records (or structs in the C case). Tuples are distinct from lists, as tuples have a fixed size. Records are distinct from dictionaries (aka maps, aka associative arrays) for the same reason. You have most certainly seen tuples or records before, so not much more detail is necessary. Here’s what they look like in OCaml:

type point = {
  x : int;
  y : int;
}

let origin: int * int = (0, 0) in
let (x, y) = origin in
Printf.printf "(%d, %d)" x y;

let origin: point = { x = 0; y = 0; } in
Printf.printf "(%d, %d)" origin.x origin.y

Two points of interest. First, in order to access elements of the tuple, we destructured the tuple into it’s components with let (x, y) = origin. This, and its more generalized notion of pattern matching are common features of functional programming languages (and sadly uncommon in other languages). Second, when constructing the point record, the record literal itself did not have to be annotated with the type name (e.g. point { x = 0; y = 0 }), and is instead inferred.

Variants

This latter idea, of having a type that represents one of many choices, is far less common in most traditional programming languages, but equally as important as records. In OCaml, this is usually called a “variant” type. The simplest example is the option type (OCaml):

type option = Some of int | None

let div (m : int) (n : int) : option =
  if n = 0 then None
  else Some (m / n)

let k = div 5 0 in
match k with
| Some k' -> Printf.printf "Success: %d" k'
| None -> Printf.printf "Failure :("

A value of the option type can be one two things: either a None, or a Some(n) for any integer n. In the div function, we use this to indicate the absence or presence of a result: if we divide by zero, then return None, else return Some(m/n).

That creates a value of the option type, but in order to use it, we have to be able to ask: is this result a some, or a none? For that, we can use the match statement, which allows us to define a branch for each possible value of the result. Here, we say “if k is a some, then get the integer result and print it, otherwise print failure.”

As an extended example, variants are amazingly useful for representing errors. Consider some alternative approaches to error handling. In C, programs traditionally use error codes:

#define ERROR_DIV_BY_ZERO -1

char* error_to_string(int err) {
  if (err == ERROR_DIV_BY_ZERO) {
    return "Div by zero";
  } else {
    return "<Unknown>";
  }
}

int div(int m, int n, int* result) {
  if (n == 0) {
    return ERROR_DIV_BY_ZERO;
  } else {
    *result = m / n;
    return 0;
  }
}

void main() {
  int result;
  int err = div(5, 0, &result);
  if (err < 0) {
    printf("Error: %s\n", error_to_string(err));
    exit(1);
  }
}

This interface is horrendous.

We have to pass a pointer to our result, only for it to possibly be filled in, and we could still ignore the error and use result’s undefined value.
We have to have a gross morass of #defines and error to string conversions.
We have to have a clear convention on error codes: is 0 success or failure? Is greater than 0, or less than 0 a success or a failure?

Some modern languages still get this wrong². Any language with a notion of null pointers (e.g. Java) often uses pointers as “implicit” option types—if the returned pointer in null, then the operation failed, otherwise it succeeded. By contrast, if you look at using our div function above:

let k = div 5 0 in
match k with
| Some k' -> Printf.printf "Success: %d" k'
| None -> Printf.printf "Failure :("

We are disallowed from using the result value unless it succeeded. We simply cannot accidentally mess up the error handling. Moreover, we could use a more expressive result type to have richer kinds of errors:

type error = DivByZero | ...
type result = Ok of int | Error of error

let error_to_string e = match e with
| DivByZero -> "Div by zero"
| ...

let div (m : int) (n : int) : result =
  if n = 0 then Error (DivByZero)
  else Ok (m / n)

let k = div 5 0 in
match k with
| Ok k' -> Printf.printf "Success: %d" k'
| Error e -> Printf.printf "Failure: %s" (error_to_string e)

We can reuse the variant mechanism not just to represent our results, but also our errors too! One thing this makes clear: the power of a variant over the traditional notion of an “enum” (like you find in C) is that variants branches have fields. This enables rich, safe interfaces like the one above.

ADT theory

Hopefully that gives you an intuition for what ADTs are and how they work. Now, we’re going to explore a formalism that extends our simply typed lambda calculus from last week with ADTs.

Product types

First, we’re going to look at simplified records: pairs (or 2-uples). Before I provide you the solution, I want you to think for a moment—how would you implement pairs? What do you need to add to the syntax, statics, and dynamics?

As a general methodology for developing new language features, a given feature usually has two “forms” (syntax extensions): an introduction form, and an elimination form. Introductions create a thing, and elimination destroys the thing, usually providing value in the process. For example, functions are introduced by lambdas, and eliminated by function application.

For pairs, we’ll do the same thing. We need a form to create pairs, and to destroy pairs (i.e. access their elements).

$\begin{alignat*}{3} \msf{Type}~\tau ::= \qamp \ldots \\ \mid \qamp \tprod{\tau_1}{\tau_2} \qqamp \text{product} \\[1.2em] \msf{Direction}~d ::= \qamp L \mid R\\[1.2em] \msf{Expression}~e ::= \qamp \ldots \\ \mid \qamp \pair{e_1}{e_2} \qqamp \text{pair} \\ \mid \qamp \proj{e}{d} \qqamp \text{projection} \end{alignat*}$

We add a new “direction” syntax to specify which element of the pair we’re accessing. The operation of accessing an element of a pair is called a “projection.” For example, a function that returns that adds two pairs of integers:

$\funt{p_1}{\tprod{\tint}{\tint}}{ \funt{p_2}{\tprod{\tint}{\tint}}{ \pair{\proj{p_1}{L} + \proj{p_2}{L}}{\proj{p_1}{R} + \proj{p_2}{R}}}}$

We also added a new type: $\tprod{\tau_1}{\tau_2}$ . In the world of type theory, this is usually called a “product type.” The reasoning for the name will become more apparent when we discuss the “algebra” part of ADTs. In the meantime, we’ll need new static semantics:

$\ir{T-Pair} {\typeJC{e_1}{\tau_1} \s \typeJC{e_2}{\tau_2}} {\typeJC{\pair{e_1}{e_2}}{\tprod{\tau_1}{\tau_2}}} \s \ir{T-Project-L} {\typeJC{e}{\tprod{\tau_1}{\tau_2}}} {\typeJC{\proj{e}{L}}{\tau_1}} \s \ir{T-Project-R} {\typeJC{e}{\tprod{\tau_1}{\tau_2}}} {\typeJC{\proj{e}{R}}{\tau_2}}$

Read them carefully to make sure you parse the syntax. The rules themselves should seem fairly commonsense–if a pair is composed of two expressions with types $\tau_1$ and $\tau_2$ , then the pair type is $\tprod{\tau_1}{\tau_2}$ . If a pair has type $\tprod{\tau_1}{\tau_2}$ and you’re taking out the left element, then the result is of type $\tau_1$ , vice versa for the right element. Lastly, the dynamic semantics:

$\ir{D-Pair$_1$}{\steps{e_1}{e_1'}}{\steps{\pair{e_1}{e_2}}{\pair{e_1'}{e_2}}} \s \ir{D-Pair$_2$}{\val{e_1} \s \steps{e_2}{e_2'}}{\steps{\pair{e_1}{e_2}}{\pair{e_1}{e_2'}}} \s \ir{D-Pair$_3$}{\val{e_1} \s \val{e_2}}{\val{\pair{e_1}{e_2}}} \nl \ir{D-Project$_1$}{\steps{e}{e'}}{\steps{\proj{e}{d}}{\proj{e'}{d}}} \s \ir{D-Project$_2$}{\val{\pair{e_1}{e_2}}}{\steps{\pair{e_1}{e_2}.L}{e_1}} \s \ir{D-Project$_3$}{\val{\pair{e_1}{e_2}}}{\steps{\pair{e_1}{e_2}.R}{e_2}}$

There are a good number of rules, but as usual, most of the clutter just comes from precise treatment of eager vs. lazy evaluation. Here, we specify that a pair is only a value if both of its components are values. The projection rules should be self-explanatory at this point.

Sum types

As with products, we will present a simplified version of variants, usually called “sum types.” And as before, we will start by defining the syntax of the introduction and elimination forms, and then defining their semantics.

$\begin{alignat*}{3} \msf{Type}~\tau ::= \qamp \ldots \\ \mid \qamp \tsum{\tau_1}{\tau_2} \qqamp \text{sum} \\[1.2em] \msf{Expression}~e ::= \qamp \ldots \\ \mid \qamp \inj{e}{d}{\tau} \qqamp \text{injection} \\ \mid \qamp \case{e}{x_1}{e_1}{x_2}{e_2} \qqamp \text{case} \end{alignat*}$

This syntax looks a little more intimidating! First, to introduce a value of sum type, we use an “injection”. For example, $\inj{2}{L}{\tsum{\tint}{(\tfun{\tint}{\tint})}}$ creates a value that could be an integer, or could be a function (but it’s actually an integer). Then we use a $\msf{case}$ statement like a more limited match to conditionally run code based on the value of a sum type. For example, a function that either returns a number or calls a function:

$\funt{x}{\tsum{\tint}{(\tfun{\tint}{\tint})}}{\case{x}{n}{n}{f}{(\app{f}{0})}}$

We need to add typing rules for our new syntax:

$\ir{T-Inject-L} {\typeJC{e}{\tau_1}} {\typeJC{\inj{e}{L}{\tsum{\tau_1}{\tau_2}}}{\tau_1 + \tau_2}} \s \ir{T-Inject-R} {\typeJC{e}{\tau_2}} {\typeJC{\inj{e}{R}{\tsum{\tau_1}{\tau_2}}}{\tau_1 + \tau_2}} \nl \ir{T-Case} {\typeJC{e}{\tsum{\tau_1}{\tau_2}} \s \typeJ{\ctx,\hasType{x_1}{\tau_1}}{e_1}{\tau} \s \typeJ{\ctx,\hasType{x_2}{\tau_2}}{e_2}{\tau}} {\typeJC{\case{e}{x_1}{e_1}{x_2}{e_2}}{\tau}}$

The first two rules are fairly simple—if an injection says “this $e$ is a sum type $\tsum{\tau_1}{\tau_2}$ ”, then double-check the type of $e$ and roll with it, no further questions asked. Case statements are more tricky. First, we check that the expression we’re casing on is actually a sum type $\tsum{\tau_1}{\tau_2}$ . Then we have two expressions with variable bindings, and type-checking rules reminiscent of the original rule for lambdas. For $e_1$ , we have to check what type it returns assuming $\hasType{x_1}{\tau_1}$ , getting some $\tau$ . We then check the type of $e_2$ assuming $\hasType{x_2}{\tau_2}$ . Importantly, the two expressions have to return the same type. This is implicitly written in the rule by using the same variable name $\tau$ for both judgments.

Lastly, the dynamic semantics:

$\ir{D-Inject$_1$} {\steps{e}{e'}} {\steps{\inj{e}{d}{\tau}}{\inj{e'}{d}{\tau}}} \s \ir{D-Inject$_2$}{\val{e}}{\val{\inj{e}{d}{\tau}}} \nl \ir{D-Case$_1$} {\steps{e}{e'}} {\steps {\case{e}{x_1}{e_1}{x_2}{e_2}} {\case{e'}{x_1}{e_1}{x_2}{e_2}}} \nl \ir{D-Case$_2$} {\val{e}} {\steps {\case{(\inj{e}{L}{\tau})}{x_1}{e_1}{x_2}{e_2}} {\subst{x_1}{e}{e_1}}} \nl \ir{D-Case$_3$} {\val{e}} {\steps {\case{(\inj{e}{R}{\tau})}{x_1}{e_1}{x_2}{e_2}} {\subst{x_2}{e}{e_2}}}$

As an exercise, you should read through these yourself and see if you can understand the semantics. A goal of this course is to equip you with the necessary tools and methodologies to explore programming languages on your own, so this is a valuable lesson for improving your fluency in the langauge of PL.

ADT metatheory

Now that we’ve changed our simply typed lambda calculus, we’re going to have to re-prove our type safety theorems. After all, we could have introduced potentially incorrect/breaking changes. However, one of the neat things about structural induction proofs is that they are naturally extensible. Rather than having to go through the entire language again, I can just prove the cases of the theorem for each new rule I provided. Below, I’ll walk through a proof of progress for sum types as an example.

Theorem: if $\hasType{e}{\tau}$ then either $\val{e}$ or there exists an $e'$ such that $\steps{e}{e'}$ .

Proof: by structural induction (extending from last time).

T-Inject-L: if $\typeJC{\inj{e}{L}{\tsum{\tau_1}{\tau_2}}}{\tsum{\tau_1}{\tau_2}}$ then either $\val{(\inj{e}{L}{\tsum{\tau_1}{\tau_2}})}$ or there exists an $e'$ such that $\steps{\inj{e}{L}{\tsum{\tau_1}{\tau_2}}}{e'}$ .

First, by the premises of T-Inject-L, $\typeJC{e}{\tau_1}$ .

Second, by the inductive hypothesis, either $\val{e}$ or $\steps{e}{e'}$ .

Third, casing on each possibility for $e$ :
1. If $\val{e}$ , then by D-Inject-2, $\val{\inj{e}{L}{\tsum{\tau_1}{\tau_2}}}$ .
2. If $\steps{e}{e'}$ , then by D-Inject-1, $\steps{\inj{e}{L}{\tsum{\tau_1}{\tau_2}}}{\inj{e'}{L}{\tsum{\tau_1}{\tau_2}}}$ .
Hence the theorem holds for both cases.
T-Inject-R: proof is same as T-Inject-L, but for $\typeJC{e}{\tau_2}$ and $d = R$ .
T-Case: if $\typeJC{\case{e}{x_1}{e_1}{x_2}{e_2}}{\tau}$ then either $\val{(\case{e}{x_1}{e_1}{x_2}{e_2})}$ or there exists an $e'$ such that $\steps{\case{e}{x_1}{e_1}{x_2}{e_2}}{e'}$ .

First, assume the premises of T-Case (listed above).

Second, assume the inductive hypothesis for $e, e_1, e_2$ .

Third, casing on each possibility for $e$ :
1. If $\val{e}$ , then by inversion of T-Inject-L and T-Inject-R, because $\typeJC{e}{\tsum{\tau_1}{\tau_2}}$ , two possible values for $e$ :
  1. $\inj{e'}{L}{\tsum{\tau_1}{\tau_2}}$ : then by D-Case-2:
    $\steps {\case{(\inj{e}{L}{\tau})}{x_1}{e_1}{x_2}{e_2}} {\subst{x_1}{e}{e_1}}$
  2. $\inj{e'}{R}{\tsum{\tau_1}{\tau_2}}$ : then by D-Case-3:
    $\steps {\case{(\inj{e}{R}{\tau})}{x_1}{e_1}{x_2}{e_2}} {\subst{x_2}{e}{e_2}}$
2. If $\steps{e}{e'}$ , then by D-Case-1:
  $\steps {\case{e}{x_1}{e_1}{x_2}{e_2}} {\case{e'}{x_1}{e_1}{x_2}{e_2}}$
Hence, in each case, there exists an $e'$ that the $\msf{case}$ steps to, and the progress theorem holds.

Algebra of ADTs

Product types and sum types are collectively called “algebraic” data types because they have algebraic properties similar to normal integers. It’s a neat little construction that might help you understand the relation between products/sums, although it probably won’t change much in the design of your programs.

Generally, you can understand the algebraic properties in terms of the number of values that inhabit a particular type. For example, the type $\tbool$ is inhabited by two values, true and false. We write this as $\mag{\tbool} = 2$ . To fully develop the algebra, we first need to add two concepts to our language:

$\begin{alignat*}{3} \msf{Type}~\tau ::= \qamp \ldots \\ \mid \qamp \tvoid \qqamp \text{void type} \\ \mid \qamp \tunit \qqamp \text{unit type} \\[1em] \msf{Expression}~e ::= \qamp \ldots \\ \mid \qamp () \qqamp \text{unit value} \end{alignat*}$

Above we introduce the void and unit types³. The idea behind these types is that there are 0 expressions that have the type $\tvoid$ , and there is 1 expression that has the type $\tunit$ (the unit value). With these in the language, now we have an identity for both of our data types:

$\begin{align*} |\tprod{\tau}{\tunit}| &= |\tau| \\ |\tsum{\tau}{\tvoid}| &= |\tau| \end{align*}$

For example, if $\tau = \tbool$ , then the terms that have the type $\tprod{\tbool}{\tunit}$ are $(\msf{true}, ())$ and $(\msf{false}, ())$ . In an information-theoretic sense, adding the unit type (or the $1$ type) to our pair provides no additional information about our data structure. The number of terms inhabiting the type remain the same. Similarly, for the sum case, the type $\tsum{\tbool}{\tvoid}$ has two values: $\inj{\msf{true}}{L}{\tsum{\tbool}{\tvoid}}$ and $\inj{\msf{false}}{L}{\tsum{\tbool}{\tvoid}}$ . There are no values of type $0$ , so there are no other possible injections.

More generally, the sum and product type operators follow these basic rules:

$\begin{align*} |\tprod{\tau_1}{\tau_2}| &= |\tau_1| \times |\tau_2| \\ |\tsum{\tau_1}{\tau_2}| &= |\tau_1| + |\tau_2| \end{align*}$

These rules then give rise to a number of algebraic properties. For example:

$\begin{align*} |\tprod{\tau_1}{\tau_2}| &= |\tprod{\tau_2}{\tau_1}| \tag*{(commutativity)} \\ |\tprod{(\tprod{\tau_1}{\tau_2})}{\tau_3}| &= |\tprod{\tau_1}{(\tprod{\tau_2}{\tau_3})}| \tag*{(associativity)} \\ |\tau_1 \times (\tau_2 + \tau_3)| &= |(\tau_1 \times \tau_2) + (\tau_1 \times \tau_3)| \tag*{(distributivity)} \end{align*}$

One way to interpret this is as calculuating information content. A pair of two numbers is logically same as the same pair reversed. As in, there’s not a real difference between { int x; int y; } and { int y; int x }. For more on this, I recommend The algebra (and calculus!) of algebraic data types (uses Haskell syntax, but ideas are the same).

“Tuple” is a generalization of single, double, triple, quadruple, quintuple, etc. to $t$ -uple, a composite of $t$ elements. Hence, tuple. ↩
It’s always a strong statement to say something is categorically “wrong” in a programming language, but I feel pretty strongly about this one. ↩
While the void type does not exist in OCaml, the unit type is used frequently to represent side effects. For example, Printf.printf returns a unit type. ↩

Sections