The reviewers were right to reject my paper

I submitted two papers to POPL 2018. The first, “Type-Preserving CPS Translation of Σ and Π Types is Not Not Possible”, was accepted. The second, “Correctly Closure-Converting Coq and Keeping the Types, Too” (draft unavailable), was rejected.

Initially, I was annoyed about the reviews. I’ve since reconsidered the reviews and my work, and think the reviewers were right: this paper needs more work.

In short and in my own words, the reviews criticized my work as follows:

1. The translation requires ad-hoc additions to the target language.
2. There is no proof of type soundness of the target language.
3. The work ignores the issue of computational relevance, compiling irrelevant things like functions in Prop.
4. The key insight is poorly explained, lost in the details of the Calculus of Inductive Constructions (CIC).

Initially, I thought that the reviews were unfair. I had worked out type-preserving closure conversion for much of CIC! We have an argument for why the target ought to be sound, but a formal proof would be too much. It took many dissertations to work out the soundness of CIC! As for computational relevance, well sure, we’re compiling too much, but we’re preserving all the information! Computational relevance is hard; one dissertation has been written on the subject and another is in the works. Figuring out computational relevance is important, but will be a separate project in itself! As for ad-hoc, well, I disagree, but maybe I communicated badly; that’s on me.

And that’s, essentially, what I wrote in my rebuttal. However, now I’m reconsidering my position.

But first, some context.

In this POPL submission, I developed a type-preserving closure conversion for CIC. An early version of this work was presented as a student research competition poster at POPL 2017, which you can find at here. In this paper, I scaled that work from the Calculus of Constructions to CIC; I added inductive types, guarded recursion, the universe hierarchy, and Set vs Prop. To do that, I made some compromises. I decided not to formally prove soundness, but give an argument thusly: use types that can be encoded in CIC, give a syntactic guard condition that seems plausible, but might have minor bugs that need to be repaired (which is the pragmatic approach to termination taken by Coq). As mentioned before, proving CIC sound was quite a challenge, and I felt it unrealistic to try to prove this target language sound. I also ignored computational relevance for two reasons. First I couldn’t find a great formal description of how to treat Type; there seems to be some kind of static analysis involved in giving it semantics via extraction. Second, after reading a lot about relevance, I think Set vs Prop is sort of the wrong way to encode it anyway, so I’d want to compile those into distinct concepts in the long run. So I decided to do CIC since it’s a more realistic source, but treat soundness of the target and relevance as future work.

To judge this work, we have to look at the type-preserving compilation literature. Since the reviews came out, I’ve been rereading the literature as I work on my thesis proposal, and talking to my committee; this helped put the reviews in a new context for me. The de-facto standard by which we judge type-preserving compilation work is “System F to Typed Assembly Language”. That work does not compile a realistic programming language; it compiles System F. Essentially it shows how to preserve one feature—parametric polymorphism—into a statically typed assembly language. And it took four of the best in our field to do that and do it “right”. While they do not handle a practical source language, they do handle a complicated type theoretic feature, preserve it through a realistic compiler to an assembly like language, and prove type soundness of that target language.

Judged by this standard, I can see the reviewers’ criticism as this: this paper was focusing on the wrong things. I am an academic, not an engineer. Instead of trying to handle all of CIC so that I have a practical source language, I should focus on compiling the new type theoretic feature—full spectrum dependent types—and doing that right. I should carve off the subset that I know how to do well, how to explain well, and how to prove correct. I should leave scaling to all the pragmatic features of CIC as future work, so that I have time to figure out how to do those features right.

So, thank you POPL anonymous reviewers for evaluating my work. You’ve given me a new perspective on my work and I think I know how to improve it.