The Algebra of Data, and the Calculus of Mutation

April 18th, 2009

With the spreading popularity of languages like F# and Haskell, many people are encountering the concept of an algebraic data type for the first time.  When that term is produced without explanation, it almost invariably becomes a source of confusion.  In what sense are data types algebraic?  Is there a one-to-one correspondence between the structures of high-school algebra and the data types of Haskell?  Could I create a polynomial data type?  Do I have to remember the quadratic formula?  Are the term-transformations of (say) differential calculus meaningful in the context of algebraic data types?  Isn’t this all just a bunch of general abstract nonsense?

We’ll investigate these questions, and perhaps demystify this important concept of functional languages.

Algebraic Expressions at the Level of Types

To understand the concept of algebraic data types, simply stated, we need to unify the set of concepts that we associate with algebra, and the set of concepts that we associate with data types.

In an algebraic expression, we might encounter a humble lone variable:


In a data type expression, we might encounter a humble lone type:


Algebraic expressions can also be compositions of other expressions, so for example we might see:


And similarly for data types:


To explain: the product of two types denotes the type of pairs of those types.  In some languages, this might instead be written as pair<int,int> but as we’ll soon see, it’s useful to think of this as a product.

Of course, the algebraic expression above could be simplified to x**2 (“x squared”) and so you could also write int**2.

Now, in an algebraic expression you might also see:


And the same concept exists for data types:


The sum of two types denotes the type of variants which can have values either of the left type or the right (but not both).  The sum in the above type might seem superfluous, because whether a value of the above sum type has the left or the right type, it’ll be an int.  However, there’s some additional useful information in knowing whether the left or right was chosen.

Consider, for example, a data type representing the balance of a bank account:

type balance = int + int

We might interpret values on the left as positive balances, and values on the right as negative balances.  So if we wrote a function to describe a balance for screen-reading, it might look like:

string describe(balance b) {
   if (b.is_left()) {
      return “The bank owes you $” + b.left();
   } else {
      return “You owe the bank $” + b.right();

For many people, sum types are less obvious than product types.  It may help to consider that, just as pair<int,int> corresponds to product types, boost::variant<int,int> corresponds to sum types.  C-style unions also serve a similar function.

Now, we can use these type-composition functions to make arbitrarily complex expressions:


Just as we could use them to make arbitrarily complex algebraic expressions:


But there is perhaps a simpler algebraic concept to consider:


What does the natural number “one” mean at the level of types?  This is called the “unit type” and it has only one value, written ().  It doesn’t do much good to have a value of the unit type — you already know what it must be.  However, it can become useful in composition, for example if you consider the simple identity:


Now “two” becomes the type of bits (or boolean values) — because a value of this type could either be the (trivial) unit value on the left, or the one on the right.  This view may help to understand variant types better, consider:

int+int = 2*int

In other words, the sum type of two ints is the same thing as the product type of a boolean value and a single int (the boolean value tells you whether the int is the one on the left or the right of the sum).

Furthermore, as you might expect:

1*int = int

In other words, having a pair of a unit value and an int is the same as having an int (the unit value adds no information here — you already know what it must be).

Now there’s one other natural number that deserves special consideration:


This is a special kind of type — it’s known as the “void” type (slightly different than the void type in programming languages like C, you’ll have to forgive this overloading of terms).  Unlike the unit type, which has a single value, the void type has no values.  It’s impossible to construct a value of this type.

That means, for example, that:


Because if you have a sum type with unit on the left and void on the right, no values of this type can possibly be on the right (again, it’s impossible to construct a value of the void type) — so it’s safe to assume that you can simplify this sum type to just be the unit type.

By a similar argument:


Because to construct a pair, you have to construct both of its members — if you can’t construct one member of the pair (again, it’s impossible to construct a value of the void type) then you can’t construct the whole pair.

Now, these types that we’ve covered so far are quite useful, and it’s hopefully pretty clear how they map to simple algebraic expressions.  However, it might be pointed out that there are more complex types, and more complex algebraic expressions to consider (even though the expressions above can get quite complex).

For example, how might the type of a list of integers be described (a list<int>) as an algebraic expression?  To help motivate this answer, consider the possible lists of integers we might produce.  For example, a list of integers could be an empty list, or it might be just one integer, or it might be two, or three, etc.  Each “or” here should be thought of as a sum, so that (with the unit type representing the trivial empty list) we come to a type represented by an infinite sum:


Now, as an algebraic expression we might be happy with this, or we might convert it to the “big-sigma” notation.  However, in the world of types, this kind of infinite expansion is described with a recursive type.  A recursive type associates the expansion with a symbol and consolidates the type to an expression where that symbol may be used.  For the case of our list of ints, this is written:


This can be pronounced “mu X, one plus int times X.”  Forget the “mu” if Greek symbols bother you; all it really means is “look out, here comes a recursive type.”  The most important idea is that the type should be thought of as the infinite expansion you get when you repeatedly substitute the entire recursive type for X (the recursion variable).  For example, performing that substitution once in the above type will produce:


and again:


Using the normal distributive properties of * and +, this can be reduced to:


And in the limit that we perform this substitution continually, we will produce the same infinite sum that we expected for this list of ints.

Although this formalism may seem somewhat removed from the language of types in F#, you can quickly recover it if you replace the keyword “type” for “mu,” “=” for “.”, “|” for “+”, recognize that empty constructors are constructors on the unit type, and ignore constructor names.  For example:

type IntList = Nil | Cons of int*IntList



Again, the type of lists of integers that we have already identified (modulo the choice of “X” or “IntList” for the recursion symbol).

This machinery of recursive types takes some getting used to, but it can produce the same infinite series that we expect in algebra, and it’s very convenient for recursive types with multiple branches of recursion, for example the type of binary trees of integers:


In other words, a binary tree is either a leaf (storing an int) or it’s a branch (storing a pair of binary trees).

It seems like we can describe a very rich category of types with these tools (for more detail, see “the bible of type theory”).  What’s more, our existing knowledge of algebra can be ported to this world of types, where we find many familiar structures.  But this formalization of types goes even deeper, and there are more concepts left to unify.

for Data

In the world of functional programming, destructive mutation is discouraged or even banned outright.  From a formal perspective, an update should produce a new copy of the original value, with both versions available for some later use.  This view has simplified many otherwise thorny problems, and it makes programs much simpler to reason about.

We have previously discussed ways to recover mutation-like functions, inspired by the most famous data structure of its kind: the Zipper.

In 2001, Conor McBride made a remarkable discovery about algebraic data types, and the concept of a zipper, which he elaborated four years later (along with coauthors Abbot, Ghani, and Altenkirch).

Central to this discovery is the concept of a one-hole context.  A one-hole context can be thought of as a data type “with a hole in it.”  This is a concept closely linked to the concept of mutation, as a value can be “updated” by “plugging in” that hole.

Consider as a very simple example, a 3-tuple of integers.  Its type is int*int*int, or int**3.  Now, we might have a value of this type:

(98, 76, 54)

We might want to “update” one of these values, or at least single one out for updating.  We can do this by “poking a hole” in the data structure where a particular value goes.  In other words, we might choose to update the first, second, or third components of this 3-tuple (using “_” to represent a hole):

(_,  76, 54)
(98, _,  54)
(98, 76, _)

These three cases represent the only ways that we could “poke a hole” in this 3-tuple data, and we can capture that idea in a corresponding data type.  Because there are three ways to poke a hole, the type should be a three-way sum.  Each possibility leaves two integers (in different configurations), and so we can pretty straightforwardly deduce this type of one-hole contexts:


In other words, the first int*int corresponds to the type of “(_, 76, 54)“, the second int*int corresponds to the type of “(98, _, 54)“, and the third int*int corresponds to the type of “(98, 76, _)“.

It’s useful to simplify the type of this expression, and so we might shrink it to (explicitly naming squares):


and then combining like terms:


In other words, the type of one-hole contexts of 3-tuples of ints is one of three int-pairs.

Now here’s an odd thing, we started out with the type:


and taking its one-hole context we derived the type:


That looks an awful lot like the derivative of differential calculus!

In fact that’s exactly what McBride discovered, that the derivative of an algebraic data type is its type of one-hole contexts!  Extended to recursive types (see McBride’s paper for more details) we can use the derivative to mechanically produce functions for updating and iterating over arbitrary data structures.

Further Reading

Predating McBride’s work, Andre Joyal explored the concept of combinatorial species (built on the concept of generating functions — a formalism similar in purpose to algebraic data types), where the use of the derivative was also discovered.

McBride is also the co-creator of the programming language Epigram, a programming language with a powerful theory of types.

In the next article, we’ll look at implementing this notion of differentiation of data types with a brief Haskell program.

16 Responses to “The Algebra of Data, and the Calculus of Mutation”

  1. falcon Says:

    I have gone through most of TAPL and read quite a lot about functional programming (from a novice’s perspective)…I have NEVER seen this explanation. This is one of the best things I have read in a very long time. Amazing and thanks!

  2. choy Says:

    I’ve always wondered why they’re called Algebraic Data Types. And I never quite understood how the zipper could be considered a derivative of a data type. Your illuminating tutorial has cleared up a lot for me.

  3. Sandro Says:

    Excellent explanation. I hadn’t given much thought to the deep connections functional programming has to algebra, despite constantly using the algebraic terminology. Your explanation is clear and compelling. Thanks!

  4. Copplepot Says:

    Thank you for this article! It clarified several concepts that I have been carrying around ill-formed. I had been looking for something like this article for years.

  5. Will Pearson Says:

    Thanks, I had come across some hints of this, but it is very useful to have it all laid out.

  6. Ricardo Herrmann Says:

    This is a great article for much of us that have learned functional programming in an ad-hoc way, thanks for the clear exposition of this topic.

  7. links for 2009-04-19 « Blarney Fellow Says:

    [...] The Algebra of Data, and the Calculus of Mutation » Lab49 Blog (tags: fp haskell) [...]

  8. Yevgeniy Says:

    Thank you for the article. It is clear and insightful. I have not thought that natlist = 1 / (1 – nat) :-)

    I always thought that the types were called “algebraic” because of the universal algebra (branch of mathematics), not regular algebra that deals with polynomials, etc. Namely, an algebraic datatype is a free algebra (mathematical structure) generated by its constructors.

  9. Raoul Duke Says:

    echoing the thanks!

    assuming, that is, you aren’t just lying through your teeth to confuse newbies. :-)

  10. Brohohibe Says:

    This is a great article, but the notation would be clearer if you used (^) for exponentiation instead of (**), since there’s already so much (*) going on. Or perhaps even just actual superscripts.

  11. Eric Says:

    A very nice piece, Mr Thielen. One question: We know that the derivative of a type is the type of its one-holed contexts. Do we know what relationship links a type to the type of its multi-holed contexts?

  12. Kalani Thielen Says:

    Eric, the n-hole context of a type is its nth-derivative.

    Consider the example of int**3, how many ways can you poke two holes in a triple? Here “_1″ means the first hole and “_2″ means the second hole:

    (int, _1, _2) +
    (int, _2, _1) +
    (_1, int, _2) +
    (_2, int, _1) +
    (_1, _2, int) +
    (_2, _1, int)

    Because holes have the unit type, this becomes int+int+int+int+int+int, or 6*int (which is the second derivative of int**3). If you poke three holes, the three-hole context has type 1+1+1+1+1+1 or 6 (the third derivative of int**3). If you poke four holes, the four-hole context has type 0 (i.e.: you can’t poke four holes in a triple).

  13. Jeremy Kimball Says:

    Wow…awesome writeup, Kalani!

    It all seems so simple now…any further reading recommendations on this topic? I’m actually curious about what other algebraic concepts are valid here…

  14. Kalani Thielen Says:

    Thank you Jeremy,

    In addition to the papers mentioned above, Conor McBride has this page on his website where he has continued to investigate this topic.

    It’s also worth repeating that the subject of generating functions touches on many of the same themes (generating functions are often studied in “discrete math” classes, and roughly correspond to the kinds of datatypes used in the article above). The book generatingfunctionology covers this topic in detail.

    Oleg Kiselyov has made the point that the Zipper is the delimited continuation of a traversal function (he argues that the derivative-type above is the “reification” of this delimited continuation as a data type).

    Chung-chieh Shan explores the logical interpretation of delimited continuations, also making the observation that negative types correspond to full-continuations expecting a value of that type (this concept of continuations as values of negative type has also been covered elsewhere, but I’m not turning up any references at the moment).

    sigfpe observes that the interpretation of infinitesimal values in differential calculus holds for types (i.e.: infinitesimal types are linear types). Thomas Ehrhard and Laurent Regnier further this idea to a differential lambda calculus.

    Edward Kmett tries to lift automatic differentiation to the level of types. He also delves deeper into the differentiation of types, finding corresponding concepts for e and sinh/cosh.

    That’s about all I could come up with off the top of my head. This is still a very active topic of research, and there are a lot of angles that people have explored.

  15. Differentiating Types in Haskell » Lab49 Blog Says:

    [...] the last article, we explored the concept of data-types as algebraic expressions, and the idea that the derivative [...]

  16. Rick Minerich's Development Wonderland : Discoveries This Week 05/10/2009 Says:

    [...] Kalani Thielen’s “The Algebra of Data, and the Calculus of Mutation” [...]