Random code snippets, projects and musings about software from Eric Kidd, a developer and occasional entrepreneur. You're welcome to contact me!

Derivatives of algebraic data structures: An excellent tutorial

May 20, 2011 • by Eric Kidd

Last month, the folks at Lab49 explained how to compute the derivative of a data structure. This is a great example of how to write about mathematical subjects for a casual audience: They draw analogies to well-known programming languages, they follow a single, well-chosen thread of explanation, and there’s a clever payoff at the end.

The Lab49 blog post is, of course, based on two classic papers by Conor McBride, and Huet’s original paper The Zipper.

If you’re interested in real-world applications of this technique, there’s a great explanation in the final chapter of Learn You a Haskell for Great Good. If you’re interested in some deeper mathematical connections, see the discussion at Lambda the Ultimate.

Want to contact me about this article? Or if you're looking for something else to read, here's a list of popular posts.

Frank Atanassow wrote on May 20, 2011:

I only read the first half, and it looks like a nice tutorial, but it does not explain what it claims to explain, namely in what sense adt's are algebraic. Algebraic datatypes are not called algebraic because type constructors form an algebra, but rather because data constructors do. In fact, type constructors do not even form an algebra; they form a pseudo-algebra, which is a generalization of algebras. That is why properties like associativity of products only hold up to (unique, natural) isomorphism rather than up to type equality. If you want to explain the algebraic nature of Haskell datatypes with an allusion to differentiation, you can do it by defining a datatype, say, of polynomials.

Aleksey Khudyakov wrote on May 21, 2011:

This link leads to 403 page. Is this paper available anywhere else? http://www.cs.nott.ac.uk/~ctm/Dissect.pdf

Steve Massey wrote on May 22, 2011:

This is the same paper: http://strictlypositive.org/Dissect.pdf

Eric wrote on May 23, 2011:

Aleksey, Steve: Thank you! I fixed the link. Frank: Surely, among consenting category theorists, all isomorphic objects are identical. ;-) Thank you for the correction. The article isn't trying to explain algebraic data types by an analogy to differention. Rather, it's trying to explain type differentiation, and it needs to define a loose algebra of types to get there.

Frank Atanassow wrote on May 24, 2011:

@Eric I beg to differ. The article starts, "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?" So whereas they claim to explain in what sense an adt is algebraic, what they end up explaining is in what sense the kind * is algebraic.

More posts