Lambda the Ultimate

I think the stuff on generating functions corresponding to various data structures will still yield good ideas, if I ever get around to understanding it (if it is obvious to you that the generating function for recursively specified non-null lists is x/(1-x), I suppose you might be disappointed). Perhaps there is some connection with the way Conor McBride and company take derivatives of types ...

There is a connection, though I am fuzzy on it. The recent work by McBride et al. on container types makes use of functors which are close to André Joyal's analytic functors, and the latter somehow generalize generating functions from the theory of species to the setting of categories.

This is an area which is growing in importance, and promises to make working with types only a little harder than doing arithmetic on numbers. See, for example,

M.P. Fiore.  Isomorphisms of generic recursive polynomial types.   In 31st Symposium on Principles of Programming Languages (POPL 2004), pages 77-88.  ACM Press, 2004.

I see that you are familiar with this notion of generating function. My next question: do you (a) know it from the Burge book or did you (b) see it elsewhere ... or is it (c) just *that* obvious to someone with the right background? Casing on your choice for answer (and assuming no match error): (a) do you agree that Burge was pretty well ahead of his time? (I rarely see this book cited, oddly enough.) (b) can you tell me where else you saw material on gen. funs.? (i.e., besides perhaps connections in Joyal and Fiore, which I will pursue) (c) uh, gee, I guess you *are* the bright boy then :) .

x + x^2 + x^3 + ...

Alas, I am not bright enough to connect such disparate topics on my own, and I know about generating functions and datatypes because have seen them mentioned before in the same context. The first place I saw generating functions mentioned was probably Baez and Dolan's HDA3, and I subsequently leafed through Combinatorial Species and Tree-like Structures by Bergeron et al. Since then I have seen mention of it here and there in the categorical CS literature. Sadly, Joyal's article on analytic functors is entirely in French, so I was a bit stymied there.

BTW, I found this book online, which looks pretty neat and accessible, though, not surprisingly, it doesn't seem to mention datatypes:

generatingfunctionology by Herbert S. Wilf

This paper:

∂ for data by Abbott, Altenkirch, Ghani, and McBride

has a nice explanation of the intuition of differentiating data types. It uses constructive set theory instead of category theory, which makes it a little more accessible than some of their other papers, for me anyway. Although I started getting confused when it talked about shapes and positions. (Maybe I need to read some of Jay's papers.)

Their idea uses Huet's zipper structures (unfortunately only available in JFP). A zipper is a data structure representing a context with a single hole. (Huet's paper shows some nice applications of zippers to data structure traversals.)

From the introduction on page 2: if we represent a binary tree with a hole in it like so:

data Tree' = Left Tree | Right Tree
data Zipper = [Tree']

where Tree' represents (a) which direction you have to go at each step in the traversal of the tree to find the hole and (b) the rest of the tree not on the path of the traversal, then we can fill the hole with:

plug :: Zipper -> Tree -> Tree
plug [] t = t
plug ((Left rrest) : z) t = Node (plug z t) rrest
plut ((Right lrest) : z) t = Node lrest (plug z t)

So here's the cool part: in general an n-ary tree will have some type T = μX.F X, where for binary trees F X = 1 + X², for ternary trees F X = 1 + X³, and so on. The type of the zipper structure is then Z = List(F' T), where for binary trees F' X = 2 × X, for ternary trees F' X = 3 × X, and so on.

Apparently they derive the rules from calculus for differentiating general polynomials, as well as the chain rule, and then a couple other rules for initial algebras and final coalgebras. They claim the connection is not just coincidental, but my calculus is rusty, and my type theory near nonexistent. So I'm still trying to slog through it. :)

Is The Derivative of a Regular Type is its Type of One-Hole Contexts relevant? Was it ever mentioned on LtU?

As I wrote down the rules corresponding to the empty type, the unit type, sums and products, I was astonished to find that Leibniz had beaten me to them by several centuries: they were exactly the rules of differentiation I had learned as a child.

The |x| < 1 condition is a red herring in this case. It is quite standard to work with generating functions in the context of the ring of formal power series k[[x]] with coefficients in a field k. (You can generalize the heck out of this definition.) A formal power series is a polynomial except for the fact that we don't require the elements of its coefficient sequence to become zero after a certain point. We define addition in this ring in the obvious way and multiplication by convolution of the coefficient sequences, just like you would in a polynomial ring.




In the present context, it makes sense to view a formal power series such as 1 + x + x^2 + ... as a polymorphic type, parameterized by its element type, x. You interpret 1 as the empty type, + as union and multiplication as Cartesian multiplication. Thus the above power series reads 'This type is empty, or equal to x, or equal to a pair of x's, or ...' I'm pretty sure Frank, etc understand this, so this is merely clarification for those of you who might still be a bit confused.




(First post, by the way.)

OK, I hereby offer a free Haskell t-shirt to the first person to come up with a useful type-theoretic interpretation of the long division algorithm :) .

Heh, I might take you up on this! My work is closely related to this area, and I think it might not be long before I could give some reasonable interpretations of division.

To get an exact correspondence between types and algebras, one needs to restrict to algebras which, syntactically, are close to linear theories. In such a setting, the exponential actually behaves much like division, although it splits into two operators called residuals, which will be familiar to anyone who has seen the Lambek calculus. I think this is enough to `divide' monomials; if I can figure out how to handle arbitrary polynomials, then the expansion of a natural number (expressed in some base) as a power series suggests a framework for doing long division...

I will, of course, have to insist on a black shirt. :) Did you ever find a place that makes those?

Frank, I'm replying to you since you seem to have a good idea of the correspondence between generating functions and type definitions. We have (and correct me if I am wrong) the following correspondence:



1 empty type

+ disjoint union

* Cartesian product




The question arises of how to deal with coefficients. I cannot think of a natural way to interpret anything but (nonnegative) integer coefficients so let's go with that: Distributivity implies nx = (1 + ... + 1)x = x + ... + x, so we are FORCED to interpret nx as the disjoint union of n copies of x. But it is a well-known fact from the theory of ordinary generating functions that any formal power series (with integer coefficients) with a nonzero constant term has an inverse, e.g. (1 + 2x + 4x^2 + 8x^3 + ...)(1 - 2x) = 1. With the above correspondence in mind, this is clearly absurd since the Cartesian product of two countable, nonempty sets is nonempty; we don't even need the axiom of choice for this countable case. Cartesian products distribute over disjoint unions up to isomorphism (count the cardinalities to see this) so what's the problem? I haven't read any papers or books on generating functions in this context so I'm a bit confused.

First of all, I actually know very little about generating functions, though they are on my list of things to look into. (In particular, I didn't know that theorem about inverses you mention.)

The short answer to your question is, I don't know.

The long answer is that the "correspondence" between arithmetic (say, for rings) and types is not well developed yet, so using it naively is likely to yield contradictions like the one you demonstrate.

Let me point out a few places where your reasoning seems specious.

First, as I said, the correspondence holds best for non-commutative linear theories, where one should read the equality symbol as "canonically isomorphic". (By "best", I mean that this restriction on theories appears to be sufficient, but not necessary to establish a correspondence.) So if your argument depends on up-to-iso properties such as commutativity of product or distributivity of products over sums (note that it involves duplication of a variable), it is likely to yield nonsense.

Second, your example of an inverse (1 - 2x) involves subtraction, and I don't know an interpretation for that; set minus is too strict because ti depends on set equality. The coexponential behaves a bit like subtraction, but any category with both exponentials and coexponentials is trivial (collapses to a poset)—in particular, the category Set has exponentials, so it can't have coexponentials. (Of course, one expects even more strongly than subtraction that coexponentials should interpret logarithms, so they are probably not the right choice here anyway.)

Third, I don't know even if every ring can be assigned a type-theoretical meaning, but if so, I doubt it will be as an object of Set, and probably not even as one in a topos, at least if you interpret "equality" as "canonically iso". I think what is actually required is some kind of asymmetric *-autonomous category because this has the right linearity properties.

(Given these considerations, it is probably not a good thing for authors to use the term "polynomial functor". This class of functors is often used to describe the ones which generate ML-like datatypes, but in fact the correspondence with polynomials is pretty weak.)

"First of all, I actually know very little about generating functions, though they are on my list of things to look into. (In particular, I didn't know that theorem about inverses you mention.)"

The book by Wilf you mentioned is a good starting point. In particular, I am confident it mentions the theorem I mentioned. In fact it's pretty easy to see why it's true; let me try to work it out here.



Theorem. Let k[[x]] be the ring of formal power series with coefficients in a field k. Let f be an element of k[[x]]. Then f is invertible if and only if f has a nonzero constant term.


Proof. Necessity is obvious since if f has a zero constant term then fg will have a zero constant term for any g in k[[x]]. Conversely, suppose that f has a nonzero constant term. Write f = a_0 + a_1 x + ... a_n x^n + ... where a_i is in k. We seek a formal power series g in k[[x]] such that fg = 1. If we write g = b_0 + b_1 x + ... + b_n x^n + ... then we have fg = (a_0 b_0) + (a_0 b_1 + a_1 b_0) x + (a_0 b_2 + a_2 b_0 + a_1 b_1) x^2 + .... We want a_0 b_0 = 1, a_0 b_1 + a_1 b_0 = 0, a_0 b_2 + a_2 b_0 + a_1 b_1 = 0, ... and since a_0 is nonzero we may take b_0 = 1/a_0 (since k is a field). The nth equation is to be solved for b_n and since the coefficient of b_n in this equation is a_0 (which is nonzero) and the earlier coefficients are already determined (by induction on n), we can indeed solve for b (since k is a field).


I just realized that I misquoted this theorem earlier since I said it works when you take coefficients in any ring. In fact it only works for a formal power series whose constant coefficient is a unit in the coefficient ring. (This is the natural generalization of the above theorem.)



"The long answer is that the "correspondence" between arithmetic (say, for rings) and types is not well developed yet, so using it naively is likely to yield contradictions like the one you demonstrate."



I agree; I was intentionally being rather cavalier in my manipulations to see where the correspondence would "naively" lead us.



"First, as I said, the correspondence holds best for non-commutative linear theories, where one should read the equality symbol as "canonically isomorphic". (By "best", I mean that this restriction on theories appears to be sufficient, but not necessary to establish a correspondence.) So if your argument depends on up-to-iso properties such as commutativity of product or distributivity of products over sums (note that it involves duplication of a variable), it is likely to yield nonsense."



That makes sense to me; thanks for pointing that out.



"Second, your example of an inverse (1 - 2x) involves subtraction, and I don't know an interpretation for that; set minus is too strict because ti depends on set equality."



Indeed, this is a huge problem. However, we are quickly imposing requirements that rapidly diminish the number of useful theorems in the theory of generating functions that could be used to investigate type theory. At best we'd like a partial correspondence between analytic and formal power series since this allows us to use e.g. complex analysis to tackle combinatorial (or in our case, type theory) problems. However, we obviously cannot have that in the present context. Barring that, we'd at least like a coefficient ring (or commutative rig -- see work by Baez) with "enough" units. We don't have that here either; the empty type is quite obviously the only unit with respect to the Cartesian product.



All this really makes me question the usefulness of this approach. I'd love to be proven wrong, however, since I absolutely love generating functions.