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.