From: ITP 2014 Date: Fri, Mar 21, 2014 at 1:08 PM Subject: ITP 2014 notification for paper 5 To: Jason Gross Dear Jason, we are pleased to inform you that your paper Experience Implementing a Performant Category-Theory Library in Coq has been accepted for presentation at the conference. The reviews and comments are attached below. Please consider all comments and follow the reviewers' requests in revising and improving your paper. The deadline for the final camera ready version of your paper is: Friday, April 18. (anywhere on the planet) When preparing your camera-ready version, please use the Springer LNCS format. Instructions and style files may be found at: http://www.springer.com/computer/lncs/lncs+authors Please conform to the page limits: 16 pages for full papers and 6 pages for rough diamonds. We will be contacting you again closer to the deadline with further instructions for copyright forms and submitting your files. Best Regards, Gerwin & Ruben (ITP'14 Program Co-chairs) ----------------------- REVIEW 1 --------------------- PAPER: 5 TITLE: Experience Implementing a Performant Category-Theory Library in Coq AUTHORS: Jason Gross, Adam Chlipala and David Spivak OVERALL EVALUATION: 2 (accept) REVIEWER'S CONFIDENCE: 5 (expert) ----------- REVIEW ----------- This is a large scale experiment in developing a library for category theory. Moreover, it is one of the first libraries that builds on the novel library for homotopy type theory. This is an important experiment which has already helped to isolate efficiency problems in the current implementation of Coq. I appreciate the points made in section 2.3 (Arguments vs Fields). However, it should be emphasized that this library has not been applied to specific examples. In such examples, one could expect the alternative choice to be better suited. It would be very interesting to formalize some basic applications of category theory and see how this library holds up. Next to the comparison in 2.3, the authors should also consider the work on packed classes by the ssreflect team. However, such an experiment will certainly give enough material for an entire new article. In the context of homotopy type theory, one naturally considers the 2-category(!) Cat, in particular, the use of UIP does not seem natural here. For a formalization in agda see: Wilander, Olov. An E-bicategory of E-categories exemplifying a type-theoretic approach to bicategories. Technical report, University of Uppsala, 2005. p7. You avoid setoids by assuming axioms: funext and higher inductive types (quotients). You are anticipating a new generation of proof assistants where these features are natively present. This is a practical attitude, but you should be very careful not to suggest to have solved the problem of extensionality. Small suggesions: Please be specific about which homotopy library you are using. There are at least two. The abstract nonsense joke seems stale for this audience. Giving a brief motivation for category theory would also help gauging the effectiveness of the present library for these applications. p8. Including the example of the interval and the proof of functional extensionality is cute, but may be a bit heavy for the ITP audience (imagine an interested HOL user). You could consider presenting either the propositional truncation or quotients instead. p9 disjoint union -> sum The problems with duality feel like a unification problem, rather than a problem of definitional equality. What would happen if you treat it as such? It would be nice to know the effect of using fast projections. ----------------------- REVIEW 2 --------------------- PAPER: 5 TITLE: Experience Implementing a Performant Category-Theory Library in Coq AUTHORS: Jason Gross, Adam Chlipala and David Spivak OVERALL EVALUATION: 1 (weak accept) REVIEWER'S CONFIDENCE: 4 (high) ----------- REVIEW ----------- This paper describes a category theory library developed in the Coq proof assistant, built on top of the homotopy type theory library. Category theory is an important target for formalization, and the exposition nicely makes an effort to reflect on broad design considerations. As such, the paper is a landmark and a good reference for the topic. There are two things that prevent this from being a great paper. First, although the paper is about a formalization of category theory, it does not discuss much category theory itself, beyond the basic definition of a category and the notion of a dual category. There is a lot more to category theory than that! One has to look at the list at the end of the paper, or browse through the theory files, to get a sense of what has actually been formalized. It would have been nice to have a synoptic overview. Could it be that there is really nothing interesting to say about the details? More to the point, it is very hard to read through the library and figure out what has been proved, and where. The problem is just that the development is factored into so many abstract pieces that it is hard to see what is going on. The paper doesn't provide much help in navigating the library and making sense of what is there, and it really should, if the presentation is supposed to be useful to others. Second, there are times when the exposition raises interesting issues, but the details are murky. I came way from the paper with the feeling of not quite understanding what the authors are trying to convey. I will try to indicate some specific difficulties below. The strong points outweigh the shortcomings, however, and I recommend publication. Specific comments: p 2 l 3: "transliterate": "translate" or "transfer" is probably more accurate. p 2 third full paragraph and footnote 1: I am not sure what is going on here. It would be nice to hear the details. p 4 l 9: "We might formalize" makes it sound as though you didn't take this approach, though from the later discussion, it seems that you did. Please clarify. p 5: the discussion, and second definition, are very confusing. It would be helpful that with the first approach, you say something like C : Cat and the Objects and Morphisms are bundled as projections of C; in the second, you say C : Cat Obj Hom The discussion of universes is hard to make sense of. p 6, "argument to a dummy function": it would be nice to see an example of this approach and how it works. p 8, higher inductive types. "In type theory with higher inductive types ...." Is there a clear notion of what "type theory with higher inductive types" is, and a reference for that? Are the authors actually using a version of Coq that implements HIT's? If so, please give the details. If not, please explain how you are simulating them in Coq. The last paragraph on page 8 is suggestive, but here is another place where the details are not at all clear. p 12, section 3.2: what is the eta rule for equality needed for, or good for? p 13, top: what are you proving anything at all about proofs of equality? Aren't you formalizing ordinary 1-category theory? Is your library compatible with proof irrelevance? What is going on here? p 13, first line of Section 4.2: "for goals around 150,000 words long": do they really get that long? Where? How? References: is there a web reference for [19]? The authors seem to have overlooked some formalizations of category theory that should be mentioned, for example: Altucher and Panangaden, "A mechanically assisted constructive proof in category theory" Agerholm, "Experiments in Formalizing Basic Category theory in Higher Order Logic and Set Theory" O'Keefe, "Towards a Readable Formalisation of Category Theory" There's also plenty of category theory in Mizar and there's a fairly recent Isabelle AFP entry by Alexander Katovsky. I'm sure this isn't by any means an exhaustive list. ----------------------- REVIEW 3 --------------------- PAPER: 5 TITLE: Experience Implementing a Performant Category-Theory Library in Coq AUTHORS: Jason Gross, Adam Chlipala and David Spivak OVERALL EVALUATION: 1 (weak accept) REVIEWER'S CONFIDENCE: 5 (expert) ----------- REVIEW ----------- This paper describes a fairly comprehensive Coq formalization of concepts and definitions of category theory (CT). The work does an original take on the subject, based on concepts and axioms from homotopy type theory (HoTT). The paper focuses mainly on pragmatics of the development, in particular on many adjustments that had to be made to the formalization to overcome significant performance problems of the Coq system. While formalization of category theory is a old, recurring topic, this work does explore fresh ideas, such as the use of HoTT equality for the equational theory of morphisms, HoTT sets for the Set category, and HoTT quotients for constructing colimits in this category. The work is substantial, and includes ingenious support for much of the traditional CT notation. The pragmatics discussion is very lively and some of it should be of interest to anyone concerned with the implementation of Martin-Lof type theory. However, it remains that many of the points made in the paper are extremely specific to the Coq system, and even down to specific sub-versions, and as such will be lost on most of the ITP audience. Claims about the generality, expressiveness and performance of the library are severely undermined by the absence of a mention of ANY application of this library, or for that matter of any major important internal CT theorem (such as Freyd's adjoint functor construction). Indeed, I could not find any such in the development source tree; but a library is only ever as good as its applications. Several CT formalizations do come with such applications (Rezk completion for Ahrens et. al, Freyd for the age-old Saibi work, or domain theory for the unpublished followup by Benton et al. on their TPHOLs 2009 work); one would expect at least as much from new work in the area. The actual code does reveal that the intended scope is univalent HoTT: the "Category" structure in the paper is called "PreCategory" in the code (contrary to usage), while "Category" means roughly skeletal category (consistently with univalence). This is not explained in the paper. There is also some interesting boilerplate to support concepts and notation, such as overloading for various forms of comma categories, that are not described in the paper. Some of the pragmatic lessons drawn are quite compelling, for instance the caution on excessive number of hidden parameters tos definitions (this has been pointed out previously, e.g., by Garillot et al. in TPHOLs 2009, but still merits wide dissemination). However, the performance analysis p. 10 on Coq inefficiency in typing C^op lemmas is likely to be incorrect. The paper assumes this is due to Coq comparing normal forms; the opposite seems far more probable. Coq typing is optimistic: its heuristic tries hard to make comparisons succeed early, keeping defined constants intact and then backtracking lazily over the decision not to unfold them. When lazy reduction is disabled (as in the HoTT branch this development is using), comparison failure becomes exponential in the number of definitions involved. To accept an x : object C as an object C^op, Coq must first fail to equate C with C^op, before computing the object projection and succeeding. The authors must have realized this, since the development is replete with parsing-expanded Notations (e.g., in the definition of C^op). It is curious then that this is not mentioned, and indeed that they complain instead of the large goal sizes, presumably generated by the abuse of such Notation.