Derivatives of algebraic data structures: An excellent tutorial

Posted by Eric Kidd Fri, 20 May 2011 20:01:00 GMT

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.

Tags ,  | 5 comments

Comments

  1. Frank Atanassow said about 4 hours later:

    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.

  2. Aleksey Khudyakov said about 18 hours later:

    This link leads to 403 page. Is this paper available anywhere else?

    http://www.cs.nott.ac.uk/~ctm/Dissect.pdf

  3. Steve Massey said 1 day later:

    This is the same paper:

    http://strictlypositive.org/Dissect.pdf

  4. Eric said 2 days later:

    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.

  5. Frank Atanassow said 4 days later:

    @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.

(leave url/email »)

   Preview comment