The n-Category Café

A really minor comment: the definition of currying on page 57 gives the type as

$((X\otimes Y)\multimap Y)\multimap(Y\multimap(X\multimap Z))$

whilst virtually all the references on the web use the form

curry : ((a,b) -> c) -> (a -> b -> c)

(keeping it in the original notation CS people will be used to)

eg, see http://en.wikipedia.org/wiki/Currying http://www.cs.nott.ac.uk/~gmh/faq.html#currying

so you might want to explain why you’ve chosen an opposite definition. (In fact, you seem to have the opposite convention on pages 58-59 in calculi rules.) Also, you motivate product types with “This gives a less awkward way to deal with programs that take more than one argument.” I’d say you probably need to go deeper and say that product types make it easier for “functions” to output intermediate data structures so you can write programs piece by piece (as there’s no obvious “lack of ease” in having more than one argument in the curried style in the examples you’ve presented in the paper).

I only read Section 1.4. In general, I think it’s well-done (besides the parts that are obviously unfinished.) I like the clear and simple language, although it sometimes degenerates into excessive handwaviness, as I’ll elaborate.

Page numbers are what my PDF reader tells me. (Adding page numbers to the document itself might help reviewers.)

Section 1.4.1:

p. 52:

“While a Turing machine…” – This sentence is strangely non-parallel. I suggest contrasting Turing-machine-as-hardware with lambda-calculus-as-software.

“The most famous of these are Haskell and Lisp” – uh, I say this a Haskell guy, but the ML family of languages is just as famous as Haskell if not more so.

“So, everyone majoring in computer science at MIT…” – see http://www-tech.mit.edu/V125/N65/coursevi.html – you might want to fact-check this before the book goes out.

“In imperative programming, a program…” – this sentence is vague, and so is the rest of the paragraph. In particular, “how to change state” hides the real difference between imperative languages and functional languages. Languages in both paradigms let you write programs that manipulate state. The distinction is as to whether the state is *explicit* or not. If I were writing this I’d explain that the imperative paradigm concerns more operational, or procedural approaches to describing algorithms, and the functional paradigm emphasizes more mathematical, or declarative approaches.

Same para: “Functional programming is seemingly more limited…” – watch out when you use weasel words like “seemingly”. Whether functional programming seems more limited depends on your perspective. It may seem more limited to C programmers. But other people aren’t necessarily coming at it with that bias. It’s also odd and misleading to describe functional languages’ lack of implicit state as a “limitation”, since as you well know, languages with or without implicit state are equally computationally powerful.

There’s some confusion and vagueness in this section as to whether by “functional languages” you mean “purely functional languages”, which you surely do. An impure functional language (and some people say “if it isn’t pure, it isn’t functional”) like Lisp doesn’t have the nice theoretical properties you want. The only widely used programming language that does is Haskell 98 (not that anyone really programs in Haskell 98, but with the language extensions that most people do use, Haskell isn’t pure either…)

“In fact, the best-behaved functional programming languages…” – “best-behaved” is quite a subjective term. Programmers may well think that a strongly normalizing language (such as the simply-typed lambda-calculus) is *not* well-behaved – most programmers like being able to write nonterminating programs! I think this entire paragraph needs a lot of work. “Input into itself”, for example, is handwavy. You’re eliding a lot of subtlety here. At least to me, when I was learning this subject, the connection between types and the ability/lack thereof to write nonterminating programs was far from obvious.

“…the typed lambda calculus is just another way of talking about cartesian closed categories”: “Just another way” is rather dismissive. I suggest saying “Lambek found a way to interpret the typed lambda-calculus in terms of cartesian closed categories,” or something like that, that doesn’t imply that cartesian closed categories are the more privileged theoretical concept. Along the same lines, I think your assertion that “theoretical computer science has been closely entwined with category theory” is controversial. Certainly there has been a lot of work on the connections between CT and theoretical CS, but not all theoretical computer scientists think that CT is central to their work. It might be good to get more opinions on this.

“Combinatory logic is closely related to the lambda calculus…” – this is vague. Either explain that the two formalisms are related as being alternative minimalist Turing-complete computational systems (I don’t see what other relationship you might mean), or don’t say it at all.

p. 53

“Strips everything down to the bare minimum” is vague. Emphasize that combinatory logic is different because it avoids naming and the complicated machinery (substitution) associated with it – that would be easier to understand. “…In some ways more awkward…” – Again, this is weaselly. Some people think lambda calculus is more awkward because you need to worry about substitution. Don’t state opinions as facts.

“…it seems more efficient…” – Be bold and don’t say what “seeems” to be more efficient, say what you think *is* more efficient.

Section 1.4.2 (still on p. 53)

1st para: Rewrite to be parallel: “Mathematicians might apply… Functional programmers apply…” (Then you get the added bonus of active voice.)

“…suppose we have programs…” “…compute the obvious functions…” – I think you’re using “program” and “function” interchangeably. Use a consistent lexical set, or if you do mean something different, explain the difference between “program” and “function”.

You introduce equational reasoning here in a very vague way. Not all readers may be used to this style of writing programs.

p. 54

“To avoid problems…” – super-vague. Say *what* problems a non-confluent rewrite system causes. Or just declare that we want to talk about confluent rewrite systems, without justifying it.

Your definition of “confluence” is wrong or at least very misleading: when you say “back to the same expression”, I think you’re trying to say that when there’s a choice of rules to apply, you’ll still get the same normal form in the end, either way. But the resulting normal form is not the original expression, which “back to the same expression” implies. This whole paragraph is pretty handwavy.

I suggest putting in a citation for those who want further reading on rewrite systems: Baader and Nipkow’s _Term Rewriting and All That_ is a good one.

“We can handle…” Avoid noise words like “using”. “‘Currying’ is a trick that helps us handle functions…” In the next sentence, what’s “this”? Well, currying doesn’t turn a function of several arguments into anything – currying lets us *define* a function of several arguments as a function that (blah blah). So say that.

“…we can imagine a program plus that adds integers” – this paragraph seems to end a bit abruptly.

“…that branch to the left:” – I find that sentence unnecessary; you can just look at the picture.

p. 55

“…has no well-defined meaning.” – it’s nonsensical to talk about whether a program has a well-defined meaning unless you’ve defined the semantics for the language in which you’re programming. I would say this differently. It’s possible to define a very sensible language in which “(double Tuesday)” has a meaning, after all. Instead I would pick an example of an ill-typed program that’s actually *inconsistent*: for example, one that uses the same value in an integer context and a string context. Now, this could have a perfectly good meaning as well (say, in Tcl), but then you can point out that in most sensible languages it would be ill-typed because strings and integers have different machine representations.

“…instantly complain…” – it’s unclear what “instantly” means. Instead, I would emphasize the compile-time/run-time distinction.

It would be nice to give a nod to type inference in this section, so readers aren’t left with the impression that you always have to write explicit types in a functional language.

“in a variety of ways” – delete that phrase; the sentence has equivalent meaning without it.

“…there is a new type…” – the use of “new” is strange; a function type is no newer than its components. “another type”, perhaps?

“Any program is built…” – this sentence is extremely confusion. Rewrite it, preferably as two or three separate sentences.

“…a datum of type X…” – so f is like a constant function. Say that, perhaps.

p. 56

“…can be reinterpreted as…” – because you use the passive voice, I am confused by what you mean. Who does the reinterpreting? Saying it would clarify the idea.

“In functional programming, we take advantage…” – I have no idea what you’re trying to get at with this sentence.

“Computer scientists call…” – again, the “new”/”old” language is confusing. How about “building more complicated types from simpler types”?

“…a less awkward way…” – Again, don’t make unsubstantiated assertions. Whether currying is more awkward than tupling is a matter of taste.

Skipping to p. 58:

The void type (or unit type – which might be less confusing than “void type”, since the “void” type in C has a very different semantics than the unit type in Haskell or ML, and I think you really mean the latter) is useful in purely functional languages, too, not just in languages with side effects. See Pierce’s _Types and Programming Languages_. Also, “languages with side-effects” is a strange thing to say, because all programming languages allow you to write programs that have side effects. But a purely functional language provides a type system that controls and encapsulates effects. I would distinguish between pure/impure languages rather than languages with/without side effects.

Here again are a few comments, this time about computation.

Bottom of page 55 where you explain that datatypes are objects and morphisms are equivalence classes of programs: depending on how it fits with your overall scheme, you might want to mention that the rewrite rules are 2-cells between programs, so you can view the datatypes-programs-rewrite rules as a 2-category.

Page 58: call it “unit type” whose only element is “unit” (write it as empty tuple perhaps?) and mention that this is “sort of like the void type in C/C++/Java”. Please do not propagate the horrible misnomer “void type” (after all, the type is not void, is it?)

There are two main uses for the unit type: (1) to indicate that no result is returned, and (2) for thunking.

Speaking of thunking, you have the opportunity to explain the difference between eager evaluation (call-by-value) and lazy evaluation (call-by-name), and relate these two concepts to two symmetric monoidal closed structures (please verify, I might be slightly wrong here):

(a) call-by-name is like Sets with products and exponentials so that you actually get a CCC (eta-reduction is valid)

(b) call-by-value is like Sets and partial functions, where the structure is that of a smash product and the space of partial maps. Eta reduction is not valid because, while a term t might diverge, lambda x. t x does not.

I do not understand why you insist on confluent and terminating rewrite rules. That automatically prevents you from having a Turing complete programming language, which is sort of a bummer. You could just say that in name of simplicity you assume the rewrite rules to be determinstic (but that computer scientists also deal with non-deterministic computation), and that in principle a computation can be diverging (infinite), and that there is no way around it if we want a Turing complete language.

I spotted a small typo: Roberto di Cosmo’s last name is incorrectly spelled “di Cosimo” through the paper.

At the top of page 2 there is a minor typo.
The second sentence reads: “The idea is that a proof is process going us go from one …”. It should probably read “… process taking us from one …”

WOW! Thank you all for coming out of the woodwork and posting these wonderfully detailed, wonderfully helpful comments.

I won’t thank you all by name now: I’ll do that in the paper. I may have more questions later. But, I really must thank Tim Chevalier by name right now for his line-by-line dissection of suboptimal wordings — and even better, suggested improvements. It takes a lot of work to go through prose and write up detailed comments like this. I do it for my grad students. It’s a real pleasure and an honor to have someone do it for me.

Mike Stay does programming and computer science for a living, but I don’t… so to me, it’s a slippery and mysterious business — unlike, say, mathematical physics, where I’ve put in enough time to have a feel for it. To get happy with this paper I really had to take everything he wrote in this section and rewrite it line by line, simply to see if I understand it. (If I can’t say something in my own voice, I don’t understand it.) I’m in the middle of that process now. So far I feel quite uncomfortable, because there’s a lot I don’t understand. That’s probably why a lot of my sentences have weaselly wordings.

So, getting all this feedback helps a lot.

By the way, I’ll be glad to use the term ‘unit type’ instead of ‘void type’ — ‘void’ makes me think of the empty set, or more generally initial objects, instead of unit objects.

I have some minor observations about the latest draft of the logic section. The first few are historical points. The last two are points about your discussion of the sequent calculus.

1. (p 35)

“One reason is that some logicians deny that certain familiar principles are actually valid. But there are also subtler, more interesting reasons.”

I would consider changing that last sentence to “But there are other reasons as well.” After all, Martin-Lof’s reasons for rejecting classical reasoning are very subtle and very interesting, both mathematically and philosophically!

2. (p 35)
“For example, around 1907 Brouwer [51] began developing ‘intuitionistic logic’. “

It is true that Brouwer developed intuitionism as a philosophy of mathematics, but I don’t think it is correct to say that he had any *direct* role in the development of intuitionistic logic. This distinction should go to his student Heyting, along with Kolmogorov in Russia. As far as I understand, Brouwer was resolutely “anti-formalist” and actually did not approve of Heyting’s formalization of intuitionism in logical terms. If I were writing this paper, I would want to avoid all of these historical fine points and just say something like the following:

“For example, in the late 1920s and early 1930s logicians and mathematicians, under the influence of Brouwer’s “intuitionistic” philosophy of mathematics, began to develop formal logics that rejected the inference from “it is not the case that it is not the case that X” to “X”. For obvious reasons, these logics were dubbed “intuitionistic.”

3. (p 36)

“In the 1930’s, this idea was made precise by Godel [47] and Gentzen [44].”

While it is true that Godel and Gentzen made this idea precise in the 1930’s, you might also want to mention that Kolmogorov, working independently of this entire tradition, made it precise in 1925! I believe that you can find this result in his paper “On the principle of the excluded middle” which is collected in Van Heijenoort’s “From Frege to Godel” anthology.
(You might also mention that this paper contains the earliest formalization of intuitionistic logic, predating Heyting’s by about five years.)

Incidentally, when these results of Godel and Gentzen are mentioned by historians of logic, they almost always also mention the closely related theorem proved by Glivenko in 1929: http://en.wikipedia.org/wiki/Glivenko’s_theorem.

4. (p 38)

“Gentzen listed enough inference rules to describe the whole classical propositional calculus, and a subset that give the intuitionistic propositional calculus.”

I’m no expert, but I am fairly certain that one can’t “just” take a subset of the inference rules for the classical sequent calculus in order to get the intuitionistic sequent calculus. One must also restrict the form that sequents can take (at most one conclusion) along with stipulating a new rule for introducing the “or” connective on the left. Maybe you are trying to say something different though? If you are, I think this sentence needs restating.

Similarly, the sentence directly after the one I just quoted seems to say something false. First of all, you are talking about the “classical” sequent calculus, not “classical logic.” Second, the “intuitionistic” sequent calculus does not allow for multiple formulas on the right of the turnstile in a sequent, so it does not even make sense to say that such an equivalence holds in the “intuitionistic” sequent calculus. But again, perhaps I am misunderstanding what you are trying to say.

5. (p 39)

Your discussion of the sub-formula property and of cut-elimination seems excessively handwavy. That is, you say what the sub-formula property is but when it comes time to say why it is so important, you just way your hands and mutter some vague stuff about the set of proofs for a given sequent. Similarly, you say what cut-elimination is but when it comes time to say why it is so important, you just mutter some vague stuff about proof-theorists being obsessed with the theorem. You should say why the subformula property makes proof search behave nicely. You should say why proof-theorists are “obsessed” with cut-elimination (for instance, the relation between cut-elimination and consistency). If you think briefly mentioning these things might take you too far afield, I suggest that you just write

“Since any proposition has just finitely many subformulas, this makes the set of possible proofs of a given sequent quite manageable. For more on this point and it’s application to automated deduction, we recommend [references]”

Similarly:

“From the two sequents on top, the cut rule gives us the sequent below. Note that the intermediate step A does not appear in the sequent below. It is ‘cut out’. So, the cut rule lacks the subformula property. One of Gentzen’s great achievements was to show that any proof in the classical propositional (or predicate) calculus that can be done with the cut
rule can also be done without it. This is called ‘cut elimination’. To see why cut-elimination is such a deep and important result, we recommend [references].”

In the actual paper, it *seems* like you are handwaving because you don’t know how to succinctly explain (1) why the sub-formula property is important and (2) why proof-theorists are so concerned with cut-elimination. If you are going to handwave, you should make it seem like you are doing so because you don’t want to get sidetracked with details that you could otherwise easily fill in. I didn’t get this sense when I read the portions about cut-elimination and the sub-formula property.

Having said all this, let me say that I am extremely excited about this paper and can’t wait to see the finished version!

First, I’d like to say that I’m also very excited about this paper! I agree with most of the comments so far, particularly Andrej and Derek. Here are a few more comments of my own…

In table 1.4, you say “programs executing in parallel”, and I believe this is the first occurrence of this operational notion of parallelism. It’s not clear to me that we need or ought to consider products of programs as being “parallel” in the familiar computational sense, although they could be considered parallel in the sense that they are semantically independent. In any case, if you want to use this characterization, it should probably be introduced/justified in the text.

On page 56, you say “In computer science this corresponds to the fact that programs are data…” I’m not sure I’d say this. Generally speaking, when programmers use the phrase “programs as data”, they’re referring to the direct manipulation or inspection of the representation or specification of a program. The classic examples of this are Lisp macros and manipulation of machine code (JIT compilation, for example). This is a somewhat different notion than currying and first-class functions, and is also often called metaprogramming.

It doesn’t help that the standard name in computer science for a function from a program representation to the program itself is also called “eval”. For this reason, a computer scientist might find it unfortunate that categorists use the name “eval” for the arrow $(Z^Y \times Y) \rightarrow Z$. We would mostly prefer to call this arrow “apply”. It is very, very important to understand the distinction between the programmer’s eval and apply, and this often causes problems for new programmers.

I strongly disagree with the idea that the unit type is not useful! Mostly it seems not useful because programmers are unused to thinking so abstractly. From the categorical point of view, all zero-parameter data constructors (e.g., True and False, each of the integers) are categorical elements (arrows $I \rightarrow X$), and these show up all over the place. In my opinion, this leads to useful insights, such as that the standard type of boolean values is $2 \cong 1 + 1$. You said this yourself on page 55, so I’m surprised that you’re so quick to slander the terminal object.

Regarding termination, I would not be so quick to introduce inconsistency. There’s interesting recent work on total functional programming, and I can imagine a bright future where we no longer say “Turing complete” (as though it’s a good thing), and just say “inconsistent”.

If you really do want to get Turing completeness, you might want to mention the standard semantic trick of using total functions between pointed objects, as Andrej mentioned, but I very strongly agree with Derek that this obscures the connections with logic.

Finally, as Derek suggests, I do urge you to at least mention polymorphic functions as natural transformations, as well as the connection between control operators and duality.

May be you can take a look at the work of L. Meertens. http://www.cs.uu.nl/research/techreps/RUU-CS-89-09.html.

In that report Meertens proposes a calculus of programs using compositional structures which seem to link up nicely with your treatement of CT.

kr

Twan

Considering your links to physics (and stuff types), I am surprised to find no references to
J.-Y. Girard, ‘Normal functors, power series and λ-calculus’, Ann. Pure Appl. Logic 37 (1988) 129–177
or to Hasegawa’s “Two Applications of Analytic Functors”.

Where are the 2-morphisms? Disclosure: parts of my active research involves program transformation and program generation. Another view of inference rules (instead of dinatural transformations) involves 2- and 3-cells in categories, see Giraud’s Three dimensions of Proofs.

Since products and coproducts are so nicely dual, and generalize nicely [to records and labeled unions respectively] in the indexed case, it is a bit surprising that does not make an appearance. I know they are less important in other areas than in computation, so maybe they really belong on the “extension” of the Rosetta stone…

Minor comment: on p.48, the two natural transformations involving (W,X,Y,Z) both have an extra ).

Another possible use of (n-)categories in computer science is to provide static analysis tools for programs. For example, in Polygraphic programs and polynomial-time functions, written with Guillaume Bonfante, we give tools to study complexity.

For that, we use an encoding of programs where computations are 3-dimensional objects. Indeed, a first-order functional program can be seen as a 3-category freely generated by: one 0-cell; elementary types as 1-cells; constructor and function symbols as 2-cells; computation rules as 3-cells.

Then we prove that well-chosen functorial interpretations of the underlying 2-category give space bounds on the results of computation, while “derivations” of the same 2-category yield information on the time complexity. The same tools were already used to prove termination of 3-dimensional rewriting systems there.

The paper is not written using n-categories explicitely. One of the reasons is that I do not know how to define “derivations” of n-categories yet. Please note that the paper is currently under revision before publication and thus some minor modifications could occur in the near future.

(Just a remark: the paper Jacques Carette’s cites (thanks!) is a preliminary version. The final published version is there.)

In case anyone wonders why I’m not commenting more on this thread: it’s not lack of interest, I’m just spending all my time trying to finish the paper on time! I’m taking all your wonderful suggestions into account, and I’ll try to say more in a few days…