If you want to see how crazy this can get, know that you can actually take the derivative of a type (with respect to another type), and this yields useful information.
This interpretation of the derivative of a formal power series was known in combinatorics long before people were studying algebraic data types in programming, so I am surprised that McBride presents it as novel.
Pedants would add that the analogy with number of inhabitants is all a little screwed up in Haskell since bottom is an implicit inhabitant of all data types, which means that e.g. Either Void () has a different number of inhabitants than () and so they cannot strictly speaking be made isomorphic.
Strict languages can sidestep this problem to an extent but still end up with "wrong" numbers of inhabitants for e.g. T -> (), since (\_ -> ()) is different from (\_ -> undefined).
So the only guys living in pure algebraic bliss are the total functional programmers like the Agda aficionados.
He does it by counting the number of functions () -> () (where () is of course inhabited by both () and ⊥), and concludes that the number of functions () -> () depends on the semantics of the language:
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).
He then goes on to analyse the relationship between point-set topology and computability, showing that the set of computable functions is in a 1-1 correspondence to the set of continuous functions, under the appropriate topology:
True. But for the purpose of reasoning, it's totally normal to ignore the “obviously wrong but admitted anyway” inhabitants like bottom.
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.
Ok, pardon my ignorance, but I'm curious if anyone can comment on how this does or doesn't relate to the Curry-Howard correspondence ? The very limited amount of introductory type theory that I've read (mostly Benjamin Pierce's TAPL and Software Foundations) seems to treat Curry-Howard as a deep and fundamental cornerstone, but the only places I've seen the algebraic properties of types explored is in blog posts (http://blog.lab49.com/archives/3011).
Is there some connection I just haven't figured out yet due to mathematical immaturity? I'm struggling to see the relationship between types as sums, products and exponents, and types as conjunction, disjunction and implication.
The answer you're looking for is in category theory. For a long time people ad hoc recognized that "products" and "sums" exist in many different domains, but there wasn't a universal method to construct them.
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.
One way to understand it is to think of the “type” side of things (sums, products, exponents) as the sort of things that one needs in order to prove the “propositional” side of things (disjunction, conjunction, implication). So, a term of a sum type will serve as a proof for the corresponding disjunction proposition, and so forth.
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.
I'm a beginner Haskeller and I'm really enjoying this blog so far. After reading through a few tutorials, it's refreshing to get some theoretical background to it all. It helps make the language more intuitive, even if it's not teaching concrete uses of the theory. Subscribed!
So the algebra of data types, as described, is simply the algebra of natural numbers. I guess this can't be the whole story because it does not describe types which can get an infinite number of values.
But still I wonder, what is the practical advantage of using this simple mathematical structure? What does it buy us? Not trying to be snarky, I just don't see the point.
Indeed, it's not the whole story. Infinite types and recursive types will come along in part 2!
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)
which is refactored, using the law (a -> b, a -> c) == a -> (b,c), to look like
data Lens a b = Lens (a -> (b, b -> a))
which allows for a more efficient 'modify' operation. It also allows you to notice that lenses are related to the 'Store' comonad[1]:
data Store b a = Store (b, b -> a)
data Lens a b = Lens (a -> Store b a)
on which a lot of the Data.Lens internals are based.
Thanks for explaining and for the examples. I would like to clarify that by 'practical advantage' I do not mean 'how does this help us write a web app' (although that would be nice), I mean 'how does this help us better understand programming'. In my experience, if you find that a problem admits a mathematical structure, but the structure is very simple, then often the structure does not lead to interesting insights -- it is just a form of taxonomy.
This happens for example in my field (theoretical physics), where some objects can be described in fancy ways using category theory. These descriptions do not lead to any practical results, like discovering new mathematical properties of the objects involved. Personally I do not find these descriptions gratifying because, again, they are just taxonomy.
There usually needs to be some minimal amount of mathematical structure (like group structure, manifold structure, etc.) in order to be able to say something new and non-trivial about the problem at hand.
Does it help if I tell you that types form a semiring[0]?
Note that the natural numbers also form a semiring (with 0 as the additive identity and 1 as the multiplicative identity). The natural numbers can be embedded in the semiring of types, but they are a strict subset - there are types that don't correspond to natural numbers (which addressed the point on the great-grandparent post).
There's a great paper by Fiore and Leinster[1] called "Objects of Categories as Complex Numbers" which shows how you can treat elements of some semirings as complex numbers for the purposes of proving arithmetic statements about them, and then convert the proofs that use complex numbers into valid proofs in the semiring.
I started programming in high school as a hobby and went on to study mathematics and linguistics at the University of Chicago, where I graduated in 2006. The date is just to give a sense of the timeline: it wasn't until 2-3 years ago that these worlds felt meaningfully compatible to me.
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.
A fun example is zippers. A zipper over some structure is a purely functional way to keep track of your "position" inside the structure, which ideally lets you move around it easily.
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])
So if we have the list [1,2,3,4], the zipper would let us represent [1,2,^3,4] where ^ is our position; it would look something like ([2, 1], [3, 4]). We could then move forwards to ([3,2,1], [4]) or backwards to ([1], [2,3,4]).
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.
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.
Do you know of any more of this cool stuff? I've already looked at 'Seven Trees In One' and zippers and want to go further. I'm just learning combinatorics and classes and want to relate it to programming structure.
You can read Huet's seminal paper on zippers [1]. I found that Edward Z Yang's article[2] explains well the more general zippers.
The generic operation of differentiation to create the the type of zipper is explained in this article[3] from Conor McBride.
Another fun fact about zippers is that they have a comonadic structure, ie from a zipper you can build a zipper of zippers that reifies the concept of moving the cursor. That comonadic structure can express "locality of rules" in cellular automata. This classic article[4] by Dan Piponi uses a 1D automaton. As an exercise, I described an implementation of Conway's game of life in a comonadic manner in [5].
following your explanation it seems like the type constructors are more responsible for determining whether it is sum or product type instead of the data constructors. this tripped me up when i was trying to figure out why function types didn't have a size of a * b, and instead b^a. then i remembered that Add takes the same amount of arguments as Mul in the type constructor despite it being a sum type. i would hint more that what determines the size of a type isn't the type constructor but more the different data constructors, e.g.:
data T a b = Foo a | Bar a b | Baz b | Qux (a -> b) <=> T = a + a*b + b + b^a
i'm already anticipating your recursive type post :)
data Rec a b = One a | Two a b (Rec a b) | Three b <=> T = a + a * b * T + b
T - T * a * b = a + b
T * (1 - a * b) = a + b
T = (a + b) / (1 - a * b)
... in haskell's ADT's how do you get the inverses of a type? then we could solve for the size of the recursive type Rec a b.
See McBride's paper http://strictlypositive.org/diff.pdf , or this guy who is discovering it by himself: http://stackoverflow.com/questions/9190352/abusing-the-algeb...