Paper #82 Revisiting Parametricity: Inductives and Uniformity of
Propositions
Y. Knowledgeable
Reynolds's relational parametricity work can be used to generate free
theorems for polymorphically typed languages. For the Coq proof
assistant which supports a rich dependently typed language, it is
possible to implement such a parametricity transaltion inside its
Calculus of Inductive Construction (CiC) language itself.
This paper presents a new parametricity translation for a subset of
CiC. The new translation can support not only inductive
definitions/propositions and pattern matching, but also a strong form
of logical equivalence for parametrically related propositions. Using
this new translation, the authors have successfully generated Coq
proofs automatically for certain theorems that would have taken a
significant amount of manual effort. One example is that big step
operational semantics respects alpha-equivalence; another example is
that observational equivalence also respects alpha-equivalence. The
authors plan to use these new parametricity results to help build
verified compilers.
Pros:
It is quite impressive that the proposed parametricity translation
can handle many different types of inductive definitions, including
those indexed inductive types and inductively defined predicates.
In addition to the conventional AnyRel translation, the paper presents
the first IsoRel translation which insists on using logically equivalent
propositions as related propositions.
Cons:
While building verified compiler is a great motivation, the free
theorems generated so far (e.g., bigstep operational semantics respect alpha
equivalence) are still not that interesting.
While the main topics addressed by the paper might be interesting to
those working on CiC, they are quite technical and may not be very appealing
to the general POPL community.
Many parts of the paper are quite difficult to follow.
Overall, while this paper might contain some technically interesting
results, it is still difficult to judge how useful these parametricity
translations really are in practice. The actual translation
functions are quite complex and, in many cases, impose significant
proof obligations (e.g. Total, OneToOne).
The paper can be significantly improved if the authors can provide more
evidence about the application of these new parametricity translations
to their verified compiler project. In particular, it will be really
useful to spend some parts of the paper to talk about the verified
compiler itself (e.g., what are the source and target languages,
how many compilation phases the authors attempt to verify, and
how many of these compilation correctness theorems can benefit
from the proposed parametricity translation).
Page 5, Section 2.1, please explain what are those variable subscripts
2, r, 4, 5. You do not want to lose readers at such an early stage.
Please don't assume that readers would already know AnyRel or read
Keller and Lasson [2012]. Please make your paper self-contained
(starting from Section 2.1).
Also, can you explain why there are five disjoint classes of variables?
Perhaps use some really simple examples to explain each of these classes
carefully.
Page 16, the example for W type is interesting, but please give the
type of the original W operator before showing IWP. More explanations
here will be very helpful to those readers who are not familiar with W.
Also, parsing the type for IWP is also not very easy, can you find
a better way to make large and long relational predicates a bit easier to parse?
I feel that Sections 3 and 4 are pretty hard going and many readers will
not be as motivated to read through all the details there until they see
the big picture in Section 5. Just as Theorem 1 on page 5 sets the big
picture for AnyRel, Section 5.1 really shows how IsoRel actually works.
The paper will probably become more readable if somewhere after Section 1
(but before Sectiom 2), you can give a high-level summary of AnyRel
definition (as done in Theorem 1) and IsoRel definition (as in Section 5.1).
This will help readers compare these two translations and understand why
we need to worry about Total and OneToOne.
Pag 24, Section 6 should be significantly expanded. It probably should
be explained earlier in a motivation section.
X. Expert
This paper gives a new internalised treatment of parametricity for a large
fragment of Coq's type theory which addresses concerns in the current state
of the art about polymorphic propositions and indexed inductive types. That
the difference is an improvement is demonstrated by giving an example which
becomes possible. The new mechanism is delivered via reflection in Coq.
Pro:
Contra:
The essence of the technique is to demand that parametricity relations
R : A -> B -> Propfor sufficiently small (i.e., in Prop or Set) A and B are the graphs of
isomorphisms. When A and B are themselves in Prop, proof irrelevance (taken
as an axiom) makes isomorphism degenerate to logical equivalence.
That choice is by contrast with Keller and Lasson's translation, which requires/ensures nothing about such relations, resulting in abstraction theorems of lower power.
The authors note, even so, that the graph-of-iso condition can often be profitably weakened and give equipment for doing so.
The presentation is pedagogically helpful, building up from a reconstruction
of the existing translation (ANYREL) to the extra conditions in their new
translation (ISOREL), exploring the delicate implications for the treatment
of inductive types as they go.
We start with an exploration of where in the sort hierarchy the predicates for each sort should inhabit. The authors break with Keller and Lasson by translating Set to predicates in Prop, with other sorts translating to families over themselves. This has implications for the translations of inductive sets and propositions which are subtle because Coq is subtle: it rules out the inductive construction of predicates for sets, as this makes the translation of large elimination rely on proof-relevant matching on propositions; fortunately, the predicates can (and should) be constructed by large elimination, in any case.
Meanwhile, the only way inductive propositions can be translated is by inductive predicates, exactly because large elimination to compute propositions would conflict with proof irrelevance. To my mind, this just adds further weight to the case for removing inductive propositions altogether, which would also make proof irrelevance for propositions achievable as a matter of definitional equality, rather than an axiom.
It is no criticism that the authors choose to work with Coq as it stands: that is how to contribute to engineering today. However, it is worth contributing some thought as to how Coq might be improved and which difficulties are artificial consequences of unfortunate legacy choices.
The development of the components of the ISOREL translation make key use of extensionality/proof irrelevance/uniqueness of identity proofs axioms. (It would be good if the authors summarized the requirements in one place.) It seems as if the approach might port readily to Altenkirch et al's Observational Type Theory, where the above hold without being taken as axioms.
The example at the end is a little delicate, as the authors confess, relying on a careful formulation to extract a useful logical equivalence result. It might help to introduce this example earlier, by way of motivation.
Please summarize dependency on axioms.
Related work on representation change might include Magaud/Bertot and Oury.
Might one consider reducing the rather hit-and-hope nature of stage 2 ISOREL
by a system of annotations, indicating which conditions one intends to impose on the relations? Is there any hope of clarifying the conditions on the original programs which allow abstraction theorems for the relaxed conditions? The examples PNone, PTot, POne are intriguing, but a stronger sense of how to classify such programs would be desirable.
It is, of course, reasonable to use fixpoints of indexed containers as indicative of inductive families in general. The complexity in the construction on page 20 is typical of translating naive pattern matching in terms of eliminators, but if you're assuming UIP, Sozeau's Equations package is known to automate the construction. You might save some space on such details.
X. Expert
The paper presents a new parametricity translation for a fragment of
Coq, the main feature is that it deals with the universe Prop in a
sensible way: instead of allowing Prop to be interpreted with any
relation in adds the condition that the only logically equivalent
propositions are related and that the relation is proof-irrelevant.
This makes it possible to deal with udnecidable relations
(codomain Prop) instead only decidable ones (codomain Bool).
The authors also point out and fix a problem in the existing
parametric translation of indexed families.
There are a number of interesting ideas in the paper. It seems to me
that the solution the authors develop is closely related to the
interpretation of the universe of proposition in models of HoTT. That
should be explored further.
One problem with the paper is that it attempts at the same time to
address a fundamental issue and develop a practical library for
Coq. Both goals are worthwhile but they lead to different
presentations.