Lambda the Ultimate

MSFP rejected this paper, for pretty much the same (good) reasons already brought up here: as written, the paper was way too imprecise.

And the referees were right! I was too close to the topic to properly see it, but this write-up was simply not ready for publication. This is one thing I really like about parts of the PL community: refereeing is taken very seriously and standards are high. And because the referees take their job seriously (or at least the 3 that looked at my paper), the feedback was fantastic.

It has happened to me three times now that a paper where I am co-author gets rejected and, after reading the referee reports, my conclusion is that I agree with the referees. This does not always happen, naturally, but my current sample set makes me happy to continue submitting papers to conferences such as MSFP.

In any case, by late June or mid-July, an updated version of the paper should be available, with all this feedback taken into account.

The paper was originally written using set-theoretical and combinatorial language only (like the [Berg89] book) but then we decided that for MSFP we could safely assume categorical knowledge. We had originally tried to give more 'intuition', and unfortunately that came out as vagueness. We rewrote parts of the paper in a more categorical style, but did not redo the earlier parts. Clearly we should have done that too.

We will fix the vagueness - whether the paper gets accepted to MSFP or not. Hopefully we can do that in the coming week, and we'll update the version on the web site.

To answer some of your questions: The species 0 is the functor that maps all sets to the empty set (and all arrows to the identity). The species \epsilon of "elements" is the functor that maps any set U to the set U, and is the identity on arrows (ie keeps the arrows as is); in other words the structures on U are the elements of U. We carelessly described functors by their images on objects, in other words the "set encoding" of a data-structure [the arrows being bijections]. Think of the usual coding of a pair (a,b) as the set {{a},{a,b}}, or the disjoint sum of sets U and V as the set {(0,u)|u\in U} union {(1,v)|v\in V} [where you have to encode that as a set too]. So the low-level set maps are hideous, and that's why one wants to immediately move away from that. But the low-level maps are often closer to actual implementation details! So unlike some of the literature on models of data-structures as Functors, we wanted to keep a bit of that visible since B-species and L-species offer different perspectives on memory hierarchies [for example, something we left out: using 5-sorted species, we can model the 5 levels of memory (register, L1, L2, main memory, on-disk) ].

For composition, we should have written (F o G)[A] = (F(G[A]]) as the "on objects" definition. Graphs and nodes are then the usual visual abstraction that one always does when doing set-theory: you associate an abstract object (like a graph) to a particular set-encoding.

Cardinality restriction can be defined precisely as
F_n[U] = if |U| = n then F[U] else \emptyset

Thanks for elaborating on the definitions. As I spend more time with this, I'd be happy to provide more feedback directly if you'd like (just email me: tim@epicgames.com).

There is an impressive amount of information in this paper. This is an important field for future data structure work, so I see a lot of value in presenting the material in a way that's accessible to technical people in other disciplines.

[Sorry for the noise on LtU] Did my email make it through?

I still can't see the difference between composition and functorial composition. The definitions in the paper are F(G[A]) and F[G[U]], which (to me) look identical. (Is there a difference between brackets and parentheses?) I'm guessing the difference has to do with U being the "underlying set", but I have no sense of what that means.

I have uploaded a new version of the paper where the definitions are much more precise [at least on the object part of the functor, the arrow part is usually straightforward]. You guys really hammered the point home that the ``intuitive'' definitions were simply insufficient [they below in a much longer expository paper, along with many more pictures, but skipping the formal definition was a mistake].

Composition is really substitution - F\circ G is really an F-structure on a set of G-structures obtained by partitioning the underlying set. It corresponds to composition of power series. This is what people mean when they say "a List of Trees". Functorial composition corresponds to putting an F-structure on the set of all G-structures on the underlying set, which corresponds to composition of series coefficients. The neutral element for Functorial composition is the species of pointed sets, while X is the unit for composition.

Set is used (as a category) because it is a very well-understood category with many useful properties for ``encoding'' data-structures. It is not the only category that can be used -- but you need at least a CCC (and possibly more, I have not checked all the details) to make things work. But the main point is that sets are used as in the standard ``encoding'' of classical mathematics in set-theory. So while the result is a set, that is as useful to the theory as saying that all Haskell ever manipulates is bit patterns. This is true, but not the point. One needs to abstract away from the 'implementation mechanism'.

Species allow you to built multisets, lists and trees -- why would you want to use those for further encodings? I don't quite understand this part of the question.

It has recently been shown that generalized species (see reference in the paper) form a CCC. I am reasonably sure that the category of generalized species is rich enough to built most of the theory of species atop that.

Having said that, I am less sure that species built on categories other than Set would have the fundamental property of corresponding exactly to analytic functors (ie those functors which have series expansions). The proof of that theorem seem more Set-oriented than the rest of the development of the theory.

Could you be more precise about your notion of 'factorization'? Note that species (like regular functors) really are about abstract notions of types and containers. They are explicitly quite independent of representation and implementation issues. To me, species neither helps nor hinders efficient representations, that is an orthogonal issue. But if I understood better your notion of 'factorization', I might be able to say something more cogent.

You can generally expect analytic solutions for species equations whenever the analogue equation has an analytic solution. In the case of your equation, the result is not very interesting as a type constructor as there is no type variable in the answer. In other words, you get a structure as solution, which is the same structure that you get interpreting the continued fraction as a structure, but it has no places to put data in it. This is to be expected, since it is the generalization of a 'constant', so it is pure structure.

However, for other equations, if the analytic equation has an analytic solution (in terms of continued fractions or series), then you can expect the species equation to also have a solution.

Jacques,

Thanks again for your detailed answers. i'll give more factorization examples in a later posting. But, as "closed" structures, these are actually of great interest to me. Set theory without atoms is closed. Here's a finite approximation for a free theory (that needs to be whacked down by a structural equivalence corresponding to the set theoretic axioms)

S ::= { S* }

A similar equation characterizes Conway games -- which are extraordinarily expressive.

G ::= { G* | G* }

All of the reflective soln's i've devised for various computational calculi are closed. For example a "closed" π-calculus

P,Q ::= 0
x?(y).P
x!(P)
P|Q
@x
x,y ::= 'P'

This is expressive enough to encode the ordinary π-calculus; and yet, there is no "hole" for data. The solution to the equation is pure structure. (Note: i've also shown a solution for an FM-style set theory with atoms that follows this same procedure.)

Finally, every such structure i've investigated has a representation in terms of a 2-level type decomposition + a 'knot tying' eqn. So, you can always get from a "pure structure" spec of this form to something that "carries data".

Best wishes,

--greg