Paper #82 Revisiting Parametricity: Inductives and Uniformity of

Propositions

- Weak reject - will not argue against

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.

- Accept - will argue for

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:

- thorough and enlightening reconstructive analysis of the state of the art
- clearly demonstrated improvement over the state of the art
- implementation in Coq, usable now
- comprehensive and cogent presentation
- significant amount of formalization

Contra:

- to some extent, this paper makes an industry out of legacy Coq awkwardness

without really challenging it - the construction is not entirely axiom-free
- the technique does not extend above Set without needing conflicting axioms
- the example is rushed, despite its fragility

The essence of the technique is to demand that parametricity relations

`R : A -> B -> Prop`

for 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.

- Weak accept - will not argue for

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.