The Algebra of Algebraic Data Types

Derivatives of types to come in part II or III (or just watch the talk on YouTube: http://www.youtube.com/watch?v=YScIPA8RbVE)

There are a couple of posts by Dan Piponi where he explores how to count inhabitants of types when you properly account for ⊥:

    http://blog.sigfpe.com/2008/02/how-many-functions-are-there-from-to.html

    1 in a total language (like Agda) or in mathematics.
    3 in a lazy language (like Haskell) when working completely lazily.
    4 in Haskell, when using seq to enforce strictness.
    3 in a strict language (like ML).

    http://blog.sigfpe.com/2008/01/what-does-topology-have-to-do-with.html
    http://blog.sigfpe.com/2008/02/what-is-topology.html
    http://blog.sigfpe.com/2008/03/what-does-topology-have-to-do-with.html

Edit: Aha, I just realized who you are, and that we've met before..!

And I would go as far as to claim that for our purposes, `Either Void ()` can indeed be made isomorphic with `()`, since the functions the converts between them will be total: they will provide a unique canonical term of the one for every canonical term of the other. It makes no sense to say that it's not total on the grounds that “it is not accounting for the extra inhabitant, the bottom”, because bottom is not a canonical term of any type.

So the isomorphism is very real, and can be trusted as such. It's better to maintain an attainable definition of totality in a language, and a distinction between canonical and non-canonical terms, than to just say “There is no total function, because Bottom!”, whence we lose important distinctions for reasoning and gain nothing.

For these reasons, I tend to use the term “inhabited by” to refer to canonical terms.

Fast and loose reasoning is morally correct.

As to how the number of terms in a given type follows in CH, it's just the number of possible proofs for the corresponding proposition.

Category theory does just that by treating all of these things as special kinds of categories and reading off universal properties which link rings, algebraic data types, logic, sets, topological spaces, etc. etc.

As to the practical advantage - does there have to be one? Isn't the fact that it's intellectually gratifying enough?

If you insist, though - I sometimes see the kind of laws I presented used in actual Haskell code. For example, in the Data.Lens package[0] you can consider a lens on a a structure of type a to be composed of a getter and a setter of values of type b

    data Lens a b = Lens (a -> b, a -> b -> a)

    data Lens a b = Lens (a -> (b, b -> a))

    data Store b a = Store (b, b -> a)
    data Lens a b = Lens (a -> Store b a)

[0] https://github.com/ekmett/lens

[1] http://stackoverflow.com/questions/8766246/what-is-the-store...

Normally, when we use lists, we do something to the head and recurse on the tail. This allows us to easily move forwards through the list, but what if we sometimes want to go backwards? It's very easy to come up with a structure that lets us do this: we just keep track of the previous elements of the list as well as the remaining ones. This is exactly what a zipper over a list is:

    zipper [a] <=> ([a], [a])

This is a very simple and elegant idea, but also very easy to come up with yourself; no need for any algebra. However, there is an interesting observation to be made: a zipper corresponds to the derivative of a type! I think crntaylor is going to cover the mechanics of this in a future post.

This gives us a couple of useful insights. For one, it means we can apply the derivative operation repeatedly to get as many "cursors" into our type as we want. We could have a zipper with two positions in the list, or three positions in the list, or whatever. Additionally, it also tells us how to generalize zippers to other types like trees. At least to me, this is not obvious and the algebra really helps here.

So we can go from the very simple structure of using ([a], [a]) to represent a position in [a] to having an arbitrary number of positions in arbitrary types like trees. I think that's pretty cool.

Another fun example is packing seven binary trees into one, using complex numbers. This is a bit more involved, so I'll let much better writers than me cover it: there's the original paper[1] as well as a nice blog post[2] about it. I think it's a very cool demonstration of how this sort of algebraic reasoning can be useful even with a fairly trivial algebraic structure.

[1]: http://www.cs.toronto.edu/~yuvalf/7trees.pdf

[2]: http://blog.sigfpe.com/2007/09/arboreal-isomorphisms-from-nu...

Also, recognizing this sort of structure can help us organize our programs. Often, even trivial abstractions are useful just for organizing code even if you don't get any especial insight from them. For example, monoids are very trivial, but are extremely useful for writing libraries.

Also, I think this is exactly the sort of abstraction which would make writing generic programs much easier, but I do not know enough about generic programming to be sure. (Here it's "generic" in the Haskell sense--programs that operate based on a type's structure and apply to many different types rather than generic in the Java sense, which is just parametric polymorphism.) Just something else to look into if you're curious.

So, I'll do my best to explain why this is "practical," as someone who spent a long time trying to establish a relationship between "mathematician jfarmer" and "programmer jfarmer."

For me, the #1 practical benefit is clarity. For example, you say that "the algebra of data types, as described, is simply the algebra of natural numbers."

Is this really true? The mathematician's move would be to abstract out this common "algebra" and isolate that structure and that structure alone. The algebra of data types and the algebra of the natural numbers then become instances of this more universal algebra.

In other words, the picture you have is that "A is an instance of B" of really it's that A and B are instances some third thing, C, that isolates their shared algebraic structure. If you're curious, the shared algebraic structure is called a semiring (http://en.wikipedia.org/wiki/Semiring).

Why is this helpful? Because it makes for clearer explanations. We can understand what facts/theorems are true because of this shared structure vs. what is true because of the particularities of one of the more specific structures. We can prove things about semirings per se which will be true for any particular semiring. We then have a new strategy available to us: if we can show some structure is a semiring, a whole universe of facts become available to us without any additional work.

Moreover, from this perspective, whole classes of seemingly-distinct algorithms become instances of a more abstract algorithm depending on which semiring we're operating over.

For example, the probabalistic and and non-probabalistic versions of a CKY parser are instance of the same algorithm which vary only according to which semiring they're executed over. ({TRUE, FALSE}, OR, AND) and ([0,∞), +, * ), respectively.

That's not just a curiosity; it's an entirely new axis of thought that reveals connections between what previously seemed like similar-but-unrelated pieces of software. It opens up the possibility of writing a function that takes a semiring specification* as input and returns a function for the "instantiated" algorithm over that semiring.

* : This example requires more than just a semiring, but I'm just trying to illustrate the point.