===========================================================================

ICFP 2017 Review #13A

---------------------------------------------------------------------------

Paper #13: Revisiting Parametricity: Inductives and Uniformity of Propositions

---------------------------------------------------------------------------

```
Overall merit: C. Weak paper, though I will not fight
strongly against it
Confidence: Y. I am knowledgeable in this area,
but not an expert
===== Paper summary =====
```

It is a well-known fact that parametricity for system F gives us theorems for free. What is less known is how to extend this result to richer languages. This paper presents a parametricity translation for a large fragment of Coq, and outlines the considerations and limitations of such translation, even fixing a bug in an already published result.

` ===== Comments to authors =====`

My main concern about this work is that it is staying in an uncomfortable middle ground: from a theoretical standpoint, it does not provide a proof of the abstraction theorem (even for a restricted set of terms); from a practical standpoint it does not provide enough information to quickly test the ideas presented in another setting.

About the second point, the paper mentions a translation that is otherwise not outlined in the paper, and is not included in the supplementary material. Moreover, in the one example included (Section 5) is not clear, at least to me, what is the free theorem being used and how.

As a last relevant point, I found the presentation hard to follow. The reader is asked to care about problems that are not yet in scope.

Minor observations:

- page 5: the first mention of \hat{s} comes out of the blue.
- page 7: the type of isZero_r is not a literal translation, but its beta-reduced form, right? It would be nice to guide the reader to understand the type being shown here.
- page 7: excess of \emph in "The deductive style has other adv..."
- page 9: it would be nice to find a less contrib example than depInd, more so given that the translation is quite complex and might use some intuition from the reader.
- page 12: Fig 1 should be placed closer to the text describing it.
- page 13: what's the point of R in IffProps?
- page 22: missing space in line 9.

===========================================================================

ICFP 2017 Review #13B

---------------------------------------------------------------------------

Paper #13: Revisiting Parametricity: Inductives and Uniformity of Propositions

---------------------------------------------------------------------------

```
Overall merit: C. Weak paper, though I will not fight
strongly against it
Confidence: X. I am an expert in this area
===== Paper summary =====
```

Various translations exist in the literature that take judgements of dependent type theory and translate them to their relationally parametric interpretation in the same dependent type theory.

These translations split every variable `x : T`

of the original judgement, producing two (for binary; or n, for n-ary parametricity) variables `x : T`

and `x_2 : T_2`

, plus a third variable `x_r : [[T]] x x_2`

which witnesses that x and x_2 are related according to the relation [[T]], which is the interpretation of the type T.

Terms `t : T`

are interpreted to terms `[[t]] : [[T]] t t_2`

. In particular, types T : Set are interpreted to [[T]] : T -> T_2 -> Sêt, where Sêt is some universe.

The parametric interpretation can then be used as a shortcut to prove theorems that would otherwise be tedious to prove, such as (see §5 of the paper) alpha-equivalence.

A disappointing property of existing translations is that the translation of a proposition `P : Prop`

is useless: it takes the from `[[P]] : P -> P_2 -> Prop`

, which is a rather uninformative (proof-relevant) theorem to have.

Indeed, regardless of what P and P_2 are, we have `λ p p_2.True : P -> P_2 -> Prop`

.

Of course, we would prefer to have instead a translation [[P]] witnessing that P and P_2 are in fact isomorphic (i.e. logically equivalent).

The authors demonstrate with a simple counterexample that this is quite simply not the case if we do not make additional assumptions, and so they investigated which additional assumptions we can make to automatically prove logical equivalence of P and P_2.

They introduce two additional properties that we can assume for the relational interpretations [[T]] of the types T that P depends on: [[T]] may be assumed to be one-to-one (essentially an injective partial function T -> T_2) or total (every element of T and T_2 is related to some element of T_2 / T respectively).

It is investigated for Pi-types, inductive propositions, and inductive types, which assumptions one needs to impose on the input types.

` ===== Comments to authors =====`

For this paper, I asked a sub-review, included below (except for the summary which is included above).

I also read the paper myself and will include my own assessment above.

Strong points:

Interesting topic: the problem being adressed is real and important

Practical applicability of the presented solution is convincingly demonstrated with a useful application in a real (and quite typical) Coq codebase.

Weak points:

Writing is unstructured and often too technical (e.g. I found many parts of section 3 impossible to follow)

Technical choices are often motivated in a "x doesn't work, so we have to do y"-style, without much reflection about the big picture (see more about this below).

No formalisation of the translation, no proof of well-typedness of translated terms. Not even a comment on whether such a proof has been attempted or why it failed.

Some aspects of the approach feel hacky, particularly the post-processing "let's now remove every assumption that our generated proof isn't actually using" phase.

Missing related work. See below.

Summary assessment:

This paper presents a solution to an important problem, that is already practically useful.

However, I think there is still some work left on (1) finding ways to better motivate and explain the design, (2) developing more insights into the big picture of what you are doing and (3) improving the structure of the paper and the comparison to related work.

As such, I think this paper should not be accepted although I believe that if the authors are able to improve the above-listed weaknesses, a future version of the paper will stand a much better chance.

Major remarks:

You don't present a proof of well-typedness of translated terms, or even a formalisation of the translation.

Some of the work you build on does come with such a formalisation and proof (Bernardy et al., ICFP 2010), although IIUC you claim they missed a case.

The fact that they missed a case, shows the limits of on-paper proofs, but can also be seen as an argument that it's worth doing the exercise, to try and reduce the odds of it happening.

Anyway, have you attempted such a proof?

How hard do you expect it to be?- Missing related work.

There is an entire line of related work that you almost completely fail to mention: the work on dependently-typed parametricity using semantic models: - Izumi Takeuti. 2001. The Theory of Parametricity in Lambda Cube. Technical Report 1217. Kyoto University.
- Robert Atkey, Neil Ghani, and Patricia Johann. 2014. A Relationally Parametric Model of Dependent Type Theory. In Principles of Programming Languages. DOI:http://dx.doi.org/10.1145/2535838.2535852
- Jean-Philippe Bernardy, Thierry Coquand, and Guilhem Moulin. 2015. A Presheaf Model of Parametric Type Theory. Electronic Notes in Theoretical Computer Science 319 (2015), 67 – 82.
Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In Computer Science Logic (CSL).

You only discuss the last of the above related papers in one paragraph in the related work.

You say "Also, they enforced the property in the metatheory, whereas we build internally expressed proofs as a program translation.", but it's not clear whether you think this approach (metatheoretic parametricity proofs, sometimes with parametricity axioms available internally) is better or worse or whether each has their own advantages.Requiring relationships that are both total and one-to-one (i.e. isomorphisms) is a very strong requirement.

For example, one-to-one-ness doesn't seem to be satisfied in the Bessel-Descartes fable, right?

In some sense, this suggests to me that you're no longer proving parametricity but rather a form of univalence.

It's not clear to me from your paper whether you think these requirements are just sufficient or also necessary.

In other words: are they needed because of how your particular translation works or is there a reason why (for some example?) they're required in any possible translation?

General remarks:

I dislike your use of "x, x_2, x_r" in translated terms and would much prefer to see "x_1, x_2 and x_r".

This would distinguish "x_1" from "x" (as used in untranslated terms) and would be nicely symmetric.p.3,l.22: "polymorphic propositions": what does this mean?

p.3, l.41-p.4,l.2: I find it weird that you seem to be saying certain sorts of proofs don't need higher universes.

In my opinion, whether you need higher universes depends on how you are proving something, not what you are proving.p.4,l.11: "well-suited for defining logical relations": where have you talked about this before?

p.5, l.34: "show that having ... break the abstraction theorem for...": I think it's worthwhile to explain better why this is the case.

p.9, discussion of the index-equality proofs required: I wonder whether this requirement turns up if you do the regular translation after you desugar the indexed data type to a parametrised data type with embedded equality proofs for the indices?

I believe this is a way to try and make more sense of your requirements, similar to what my sub-reviewer suggested about Church encodings.p.12: what do you actually generate: Coq or Gallina?

p.14, l.7: a trivial consequence of the proof-irrelevance axiom: I thought you previously said your translation doesn't rely on axioms?

p.16, l.7-8: There's a reason Coq allows you to leave some arguments implicit.

ICFP papers are also allowed to do this, you know...p.20, l.4: "our reifier": what's a reifier?

p.23, l.39-..: I'm skeptical about some of the things you say about HoTT, like the fact that it doesn't support proof irrelevance.

IIRC, HoTT defines a notion of h-Props as precisely those sets that satisfy proof irrelevance and the HoTT book has quite a bit of discussion about this?

Also the suggestion that it's hard to use dependent pairs without inj_pair2 strikes me as a bit strong.

Typos and general nitpicking:

"typehood judgements": never heard this term before. You seem to mean well-typedness judgements?

p.7, l.11: " to only create proofs": "only to create proofs"

p.7, l.27: "resultant": resulting

p.8, l.38: the second O on this line should be O_2, I think.

p.9, l.34: break line before "If an inductive ...": here, but also elsewhere, you often put a lot of stuff into one paragraph, but I recommend you apply the principle of "one paragraph, one idea"

p.11, l.12: "3rd" is typeset weird here. You should use "3\textsuperscript{rd}" instead of "3$^{rd}$".

p.12: "Using reification and reflection (Malecha and Sozeau)": this citation sounds to me as if these guys invented reification and reflection, which they did not IIUC.

In principle I am enthousiastic about this direction of research. The authors make the correct and important observation that the current interpretation of propositions is useless. (Also for multi-element types, we will sometimes want to find an isomorphism, rather than a mere relation, but it is legitimate to not consider that in a first approach of the problem.) This has to my knowledge not been adequately addressed so far in any publication. Homotopy type theory (HoTT) does automatically produce equivalences, but also requires equivalences as input, which is more than sometimes necessary. The authors show that additional assumptions are needed and choose, I believe, the right direction when they investigate the structure of P : Prop to find out what assumptions are needed precisely. I find it surprising that considering the one-to-one and totality properties yields good results here; this approach is to my knowledge new not only in published work but also in the WIP that I am aware of.

The reasons why I give a C rating nonetheless, are:

- A lack of structure and readability
- The absence of reflection on the achieved results and of an attempt to transfer high-level understanding: technical (Coq)-proofs and counterexamples establish the validity of the results, but as a human reader I am also interested in the deeper reasons why the achieved results are what they are.

In short, I think this is a relatively weak presentation of a valuable piece of work.

While reading the paper, I repeatedly found myself wondering in puzzlement: what are we doing now and why? So I made an outline of the structure and found out that some section titles do not match the content of the section. I include the outline, with structure-related and other remarks, below.

This is related to point 1, of course. My primary issue was that it is next to impossible to quickly reread something that you recall having read earlier.

The text on p7, ln 41-42, is very important. Yet after having read the full paper, I had much trouble retrieving it, and even more trouble in retrieving its argumentation. There are two claims here: (1) the deductive-style translation is necessary for inductive types if Sêt = Prop, and (2) the inductive-style translation is necessary for inductive propositions. Each claim has its own argumentation. If you would, e.g., state these claims as two lemmas (\begin{lemma} ... \end{lemma}), each with a proof, then they influence the page lay-out and allow me to quickly find them back.

In order to prove logical equivalence of related propositions P and P_2, the authors investigate the structure of P and make assumptions based on that. So the structure of P gives rise to the assumptions that are made. The specifics of this interaction are

*the*central theoretical contribution of this paper, yet they are spread throughout, in subsentences in the middle of proofs that do not have a corresponding theorem featured as such. If I want to check the assumptions made for the universal quantifier, I have to reread the entire reasoning to find e.g. the clause 'Using the CompleteRel property of B_r, ...' (p14, ln 36).

I suggest instead to anounce every proof in the paper with some theorem environment, in which the assumptions are clearly listed. Since the interaction between proposition structure and assumptions is so central to the paper, I would moreover recommend to add a clear table or (if the results turn out to be too capricious to fit a table) a dedicated section that reviews the interaction and discusses it.

Some key recommendations:

- Use the page-layout (theorem environments, more fine-grained use of ((sub)sub)sections, enumerations, ...) to allow the reader to quickly look up important points and their justification after the first read.
- Identify what is important in the paper and summarize it before or after its argumentation.

In general, a proof serves two purposes: to establish that a claim is true, and to allow the reader to understand why. I think an important virtue of proof-assistants is that they allow to separate those concerns: you can convince Coq that your results are true, and dedicate your paper to teaching the reader a *feel* for why they are true. This may mean that instead of giving a fully general and technical proof, you give an illuminating example that makes the general theorem credible.

It especially means that you should not talk to your reader the way you talk to Coq. A good example where you do this is on p16, ln 9-10. Here, you explicitly 'introduce' a variable and explicitly invoke the substitution rule. In Coq, in order to prove a universally quantified theorem, you use Intro. But when explaining to a human that something holds for all y, you say 'pick any y', not 'we introduce y'. Similarly, you need not tell a human reader when to substitute one thing for another; instead you can just explain why indices are equal and perhaps remind us of the equality when the substitution needs to happen.

The entire proof about IWP (which, by the way, could use a corresponding theorem) - as well as many proofs in the paper - reads like a direct English-language transcript of a Coq proof. I think instead of giving a solid but extremely technical proof, you should seize the opportunity to help your reader *understand* why you need all the assumptions, and only the assumptions, that you make.

The HoTT-book may serve as a guide here: it does an excellent job of doing type theory without treating its reader like a proof assistant.

As mentioned before, I think you need to gather somewhere the specifics of the interaction between proposition structure and assumptions. But I suggest you moreover discuss these gathered results: what do they mean, how do they arise, what are the patterns and how can we understand this? In rare occasions, truth is just ugly and there is nothing to say, but I am not convinced that this is the case here. In fact I think interesting further structure can be identified, see also my comments on §4.

One thing that I think may be illuminating, is to consider Church encoding. For types, this is problematic as Set is predicative, but indexed inductive propositions may (if I'm not mistaken) be Church-encoded using only Pi-types and Prop. E.g. we can encode le : nat -> nat -> Prop as

`le m n = (P : nat -> nat -> Prop) -> ((k : nat) -> P k k) -> ((k l : nat) -> (P k l) -> (P k (S l))) -> P m n `

This may allow you to explain the assumptions made for indexed inductive propositions, in terms of the ones made for Pi-types. For inductive Sets, the same would be possible if Set were impredicative, see e.g. Robert Atkey, Neil Ghani, Patricia Johann, POPL 2014, 'A relationally parametric model of dependent type theory'.

- Here, I think the writing is quite good.
- The fable about Bessel and Descartes is as much about parametricity as it is about univalence. So perhaps it is, today, not the best example to illustrate the idea of parametricity?
- Instead of repeating "the existing translation (Keller and Lasson 2012)" you could use \citeauthor{...} to write, as of the second mention, "Keller and Lasson's translation".
- p3, ln 8: I see what you mean, but I think a clarification of the example is desirable.
- p3, ln 11-12: I would say 'logical equivalence of the related propositions' and 'triviality of the relation'. Currently it sounds like the relation needs to be logically equivalent, which is meaningless.
- p3, ln 32-34: I read this sentence 10x on the first read without understanding what is meant, and then again after reading the whole paper and I still find it very dense. This is just too complicated a claim for a single sentence. Since the general treatment follows in section 3, perhaps you can do with a non-general example for now?
- p3, ln 41-43: This claim is vague to the point of meaninglessness. The following sentence ('For example, one can define...') makes your point much better. I think you can delete this one.

Ok.

- p5, abstraction theorem: For types, readability may increase if you instantiate them on the left of the = sign, e.g. [[s]] x x_2 = x -> x_2 -> ŝ. (This is a matter of taste.)
- p5, ln 34: I suggest "... breaks the abstraction theorem
*above*for the ...". Also, by referring Keller&Lasson, you make it seem like a deep result. In as much space, you can explain what the problem is: give the translation of Type_i : Type_{i+1} and note that it is ill-typed. - I think a refresher of Coq's universe structure is worthwhile. We have, if I'm correct, Prop : Type_1, Set = Type_0 : Type_1 : Type_2 : ...

- This section consists entirely of 2.2.1. The title of 2.2.1 suits better than this one. So I suggest to make it '2.2 The previous translations of inductives: comparison' AND to add multiple subsection titles.

```
My summary of the section:
- you review Keller&Lasson's and Bernardy et al.'s translations
- you show that deductive-style is more suitable for inductive types (and necessary with Sêt = Prop)
- you show that inductive style is necessary for inductive props
```

- p6, ln 44.5 : We do not apply n_r to the match term; rather, we apply the match term to n_r. Also, while I do not object to providing background literature, you again make the situation seem complicated by refraining from giving an explanation on the spot. The situation is simple (or it would be in Agda, the Coq return clause surprises me in that it does not take a function, so I may be missing something here): since n_r is already in scope when you type 'match', it does not change type within the matcher. By making the match term return lambda-terms, you can use the return-clause to tell Coq how to adapt the argument's type to every case.
- p7, ln 13: 'iff it's type is a proposition' would be more readable.
- p7, ln 31-33: As mentioned: I suggest to have 2 lemma-environments and 2 proof-environments here.
- p7, ln 33-35: Since both styles are supposed to be isomorphic, and deductive-style allows proof by computation, I expect a Coq tactic that takes care of proofs for the inductive-style is feasible? (This is a somewhat off-topic discussion.)

```
My summary of the section:
you fix the subtle flaw and add an additional equality constraint
```

- Note that my summary does not match the section's title. A deductive-style translation appears in §2.2, so fixing the flaw is all you do. Then the title should be clear about that. The way it is now, it leaves me wondering: "Where is the section on inductive-style translation of indexed-inductive propositions?" The first paragraph of the section is not clear on the section's subject either.
- p8, ln 21 on the right: It's the first time I see the phrase 'member of a family'. I originally read this as referring to a vector, rather than a type of vectors of a given length. I would suggest 'different indices', 'different instantiations of the type family' or just 'different types'. This holds for all uses of the word 'member'. If you insist on the terminology, I suggest adding a clarification at least once.
- p9, ln 13: You can use Coq parts in an English sentence, but better not English in a Coq expression.
p9, ln 40: This example is (1) proof-irrelevant, which is not a requirement here, and (2) contrived and practically useless, disallowing the reader to appeal to their intuition. I suggest to use for example (forgive me my flawed Coq grammar)

`Inductive Contains (A : Set) : \forall (n : nat) (v : Vec A n) (a : A), Set := hdContains : \forall (n : nat) (a : A) (v : Vec A n), Contains (S n) (consV a v) a tlContains : \forall (n : nat) (a : A) (v : Vec A n) (Contains n v b), Contains (S n) (consV a v) b`

- p10, ln 5-7: Even if the implementation does not have implicit arguments (that's how I understood it), perhaps you would consider using them in the paper anyway? Or writing underscores for inferrable arguments? This type is not readable as it is. Also, what does Req stand for? Quickly mentioning the meaning of an acronym, promotes it from a random sequence of letters to something that makes sense.
p10, ln 11: So 'singleton' is Coq terminology for a type with at most one element?

- p10, ln 33.5: What do you mean precisely by 'complex'? It certainly is complex in terms of readability, but at the same time I have the impression that it is entirely straightforward, in the sense that this section introduces no remarkable new ideas? The word complex seems to announce a new idea.
As for the depIndRec example, I would suggest the following (corresponding to the Contains example):

`Definition getIndex (A : Set) (n : nat) (v : Vec A n) (a : A) (c : Contains n v a) : Fin n := match c with | hdContains _ _ _ => fzero | tlContains _ _ _ c' => fsucc (getIndex _ _ _ c')`

Figure 1 could be made more readable by using underscores or implicit arguments.

- The last paragraph is very cryptic. What do you mean by 'generating'? You say it 'needs' to do so; why is that the case? Do we require propositional or definitional equalities? Do you mean fix F = F (fix F), as you say (then how does this relate to the translation), or rather something like [[fix F]] = [[F]] _ _ [[fix F]]?

- I was surprised by the last sentence. Is Coq's type inference untrusted?

- The section title is vague and there is no clarifying first paragraph. This section contains the technical meat of the IsoRel translation. I suggest merging it with §4 (which just wraps up the loose ends) and naming it "The IsoRel Translation". The section should start with an overview, and the content between title 3 and title 3.1 deserves its own title and section number. The start of §3 is also a good place for the content that is now between title 4 and title 4.1; that way the reader knows where we are going and what is the role of [[_]]iso (which, in fact, is NOT the IsoRel translation, which is obtained by pruning [[_]]iso).
- p13, ln 34: Here you could mention univalence.
- p13, ln 40-41: This is what we need more of: transfer of understanding.
- p14, ln 3-9: Some flashforward on why we need uniqueness of proof-irrelevant relations, would be useful.
- p14, ln 19-20: The Curry-Howard correspondence is commonly known in type theory and I see little reason to emphasize it here.

`My summary: how to assert IffProps and CompleteRel for universally quantified propositions`

- first line: 'This includes the case when' should be 'The same holds when'. Although A:Prop implies A:Set, a context that has A:Prop is different from a context that has A:Set.
- ln 33: 'relations in the family B_r' -> I think you could just say 'B_r', or perhaps 'instantiations of B_r'. Talk about families, in my opinion, makes things sound more complex than necessary.
- ln 40: I suggest 'λ_.False', rather than 'False'

- This is very hard to follow. Abbreviating IWP I A B AI BI to, say, W', everywhere, and similarly IWP_r
to W'_r, would already be a vast improvement. Using underscores or implicit arguments could also/alternatively help. Perhaps working with something less general than IWP may actually contribute more to the reader's understanding (you have the Coq-proof to establish the truth of the general claim); however, I acknowledge that it is not easy to cook up an example here that shows the relevant behaviour in I, A and (most difficultly) B and at the same time is easy and intuitive to think about. Perhaps you could use 3 examples which demonstrate the role of the assumptions on I, A and B separately; and then state the general result, with or without proof? - p14, ln 46.5: I suggest 'indexed inductive propositions', rather than 'indexed induction'. I had originally read over the fact that this section was about propositions.
- p15, ln 9-10: The naming is illogical to me. I would call the constructor 'node' or 'iwp-node' or (as it is) 'iwp', and the argument 'node' could be called 'branches' or 'children'.
- p15, ln 18-22: I'm not positive that I understood this well. The way I understand it, you proved properties about IWP, but not about general indexed-inductive types, because these are very often encodable in terms of IWP? That would make sense, it's just not clear to me whether that is what you are saying.
- p15, ln 30: 'only one direction': You can omit the word 'only', this is all very symmetric and proving one direction convinces everyone that the other also holds.
- p15, ln 36: I'm not an English native, but 'RHS conjunct' sounds weird to me, I would say 'right hand conjunct'.
- p16, ln 14-19: While it is wise to start in a simple setting, I would be surprised if your results completely broke down when allowing proof-relevant relations between types. However, you would soon need to consider higher-dimensional parametricity (double translations like [[ [[t]] ]], see the papers in Guilhem Moulin's PhD thesis, cited below, especially the first and the last one). What I'm saying is that I think you should be careful with words like 'need', referring to a necessity. I doubt that proof-irrelevance is a necessity here, but it does avoid opening the Pandora box of higher-dimensional parametricity.

J.-P. Bernardy and G. Moulin. A computational interpretation of para-

metricity. In Proceedings of the 27th Annual IEEE Symposium on Logic

in Computer Science, pages 135–144, 2012. doi: 10.1109/LICS.2012.25.

URL http://dx.doi.org/10.1109/LICS.2012.25.

J.-P. Bernardy and G. Moulin. Type theory in color. In Proceedings of the

18th ACM SIGPLAN International Conference on Functional Programming,

ICFP ’13, pages 61–72. ACM, 2013. doi: 10.1145/2500365.2500577.

URL http://doi.acm.org/10.1145/2500365.2500577.

J.-P. Bernardy, T. Coquand, and G. Moulin. A presheaf model of para-

metric type theory. volume 319, pages 67–82, 2015. doi: http://dx.doi.

org/10.1016/j.entcs.2015.12.006. URL http://www.sciencedirect.

com/science/article/pii/S1571066115000730. The 31st Confer-

ence on the Mathematical Foundations of Programming Semantics

(MFPS XXXI).

```
My summary: We will require props to be total & one-to-one rather than equivalent & complete
In fact, you explicitly say so: "In this section, we consider the subtyping rule"
```

- Note that the content of the section, does not match the section title. Also, it seems out of place. I would explain the idea of this section immediately after the last of the 4 definitions of IffProps, CompleteRel, Total, OneToOne.
- The intro of this section is also confusing. You say "We consider all the ways to construct new types in the universe Set ...", and you don't say where, making me assume that it will be the content of this section (as also the title suggests). But that is not the case; rather, it is the content of §3.4 and §3.5. Perhaps §3.4 and §3.5 should become two parts of a single section?
- It seems that the OneToOne property is completely trivial for propositions and hence Total alone asserts logical equivalence? If so, you should say so.

`My summary: When is a Pi-type one-to-one or total?`

- ln 6.5: A relation between function types, or a relation on functions, but not a relation between functions (OR you should say that it takes 8 arguments and returns a proof of relatedness of functions).
- Please state the theorem in an environment. "[[the Pi-type]] is one-to-one if ... and total if ...".
- This section fails to explain any underlying idea: there is no general proof; no concrete proof for an intuitive example. The only 'hard' argument we get is a counterexample of something more general than the asserted theorem. An example of a simple remark that would help is the following: "If A_r is not one-to-one, then it can introduce conflicts by relating different elements of A (with possibly different images) to the same element of A_2."

```
My summary: When is an indexed inductive type one-to-one or total?
I'll admit that I didn't work through the details here.
```

- The use of I for an inductive type (here and in other places) is confusing, as earlier (and in §3.5) I is used as the index type of an indexed inductive type/proposition.
- GoodRel is a vague name. What about Isomorphism?
- State the theorem, and compare it to the theorem for inductive propositions. It is harder to prove totality of a relation between types, than totality of a relation between propositions. Hence, it requires a superset of assumptions!
- I would prefer human-language mathematics over a list of combinators.
- As mentioned before, a glance at the Church encoding of an indexed-inductive type, even if it is ill-typed with predicative Set, could relate the results of §3.5 to those of §3.4.

`My summary: This section explains the implementation approach you took.`

- I think §4 with parts §4.1 and §4.2 should be a subsection of §3; and §4.3 should be a separate subsection of §3.
- p19, ln 34-40: From a practical viewpoint, the 2-stage approach (first apply [[_]]iso, then prune) is absolutely valid, since it works. However, the theorem behind it - 'If you remove all unused assumptions from a theorem produced by [[_]]iso, then the theorem remains true' - is not very informative. An approach that is theoretically more interesting and perhaps also practically useful, could be to have 4 translations:
- [[_]], the AnyRel translation,
- [[_]]iso, the IsoRel translation which asserts the Total and OneToOne properties for types and props,
- [[_]]tot, a translation which only asserts the Total property for types and props,
- [[_]]1-1, a translation which only asserts the OneToOne property for types and (trivially) for props.

These translations would be defined mutually recursively, and e.g. the definition of [[_]]iso would use whichever of the four translations is necessary for each subterm. I did not spell this out, but if this kind of translation is achievable I think that would be very valuable. Some advantages are: - The translation reflects what I think is the core theoretical contribution of this paper, namely how the definition of a proposition determines what assumptions are needed on input relations for the output relation to be Total,
- No pruning is involved; no unnecessary work is done.
- It relates to modal type theory, where variables are annotated with a modality that expresses how the judgement's RHS depends on them. Here, the modalities would express things like 'If we want [[_]]iso for the RHS of the judgement, we need [[_]]tot for this variable'. That could point the way to future theoretical work on this subject.

- Actually I think terminology is a bit confusing. Currently, IsoRel refers to the composition of both stages, whereas [[_]]iso refers to only the first stage (and hence is unpronounceable). It seems more logical to me to call the first stage IsoRel, and the composition something like MinimalRel. Then §4 would be called 'MinimalRel translation', §4.1 would be 'Stage 1: The IsoRel translation' and §4.2 would be 'Stage 2: Eliminating unused hypotheses'. In any case, I would avoid titles consisting purely of a mathematical symbol.

See my remarks above

- This could become 'Limitations of MinimalRel'
- Please take care to distinguish the proof irrelevance axiom (any two proofs of the same proposition are equal) from uniqueness of identity proofs (UIP; any two proofs of equality are equal). HoTT does not exclude a universe of propositions (see ch. 3 "Sets and logic" in the HoTT-book), but equality will not in general be a proposition.

- I think this section is very good as it is, although the very short and non-applied §5.1 is a bit awkward and seems out-of-place here.

- p23 ln 39-40: You could call HoTT more general than [[_]]iso (the first stage) in that it uses equivalences instead of isomorphisms. However, it is not more general than MinimalRel, which, unlike HoTT, appropriately weakens the required assumptions. This is a clear advantage of your work over anything that I am aware of.
- p23, ln 45-47: Again, univalence refutes UIP, not Prop. Even with UIP, higher inductive types are possible, but they will represent setoids instead of groupoids; they are then often called quotient types.
- p24, ln 2: HoTT-book-style HoTT makes the use of dependent pairs quite hard, I agree on that. However, Cubical type theory (Cohen, Coquand, Huber, Mörtberg, 2016, Cubical Type Theory: a constructive interpretation of the univalence axiom) addresses that.

This can be omitted in my opinion.

===========================================================================

ICFP 2017 Review #13C

---------------------------------------------------------------------------

Paper #13: Revisiting Parametricity: Inductives and Uniformity of Propositions

---------------------------------------------------------------------------

```
Overall merit: B. OK paper, but I will not champion
it
Confidence: X. I am an expert in this area
===== Paper summary =====
```

Free theorems for functional programs are all very well, but one might

expect that they would really be useful when generating proofs in a

proof assistant. This paper continues a line of work initiated by

Bernardy et al in synactic generation of proofs of Reynolds'

abstraction theorem for dependently typed proofs and programs. The

core of this paper is a discussion of a Coq tactic that generates

proofs given terms. The major contributions of this paper are:

Extension of previous translations to handle a larger range of

Coq's indexed inductive types. A detailed comparison between two

methods of relational translation is made, with discussion of what

works and what does not. A special, but representative case (W types)

is formalised in Coq to show that the translation should always work

(the actual tactic may fail during proof generation).A new translation (the "IsoRel" translation) that has the desirable

property that two propositions (i.e. objects of the Coq sort 'Prop')

are related only when they are are equivalent propositions. This is in

contrast to the original translation (Bernardy et al, Lasson and

Keller), which stated that all propositions were related. This is a

much weaker property, and makes the translation effectively useless

when translating propositions. Unfortunately, the cost of this extra

strength is that relations between normal types are restricted to

isomorphisms. A slightly ad-hoc claim is made that some of these

assumptions of isomorphism can often be dropped in practice.

An application of the generation of abstraction proofs is given,

demonstrating its use in a compiler correctness project. It is claimed

that this use (would have) saved many hours of work.

` ===== Comments to authors =====`

Things I liked:

The new translation properly handles (indexed) inductive types, and

there is a detailed discussion of the issues involved.The discussion in the paper is based on a working tool for

constructing Coq proofs, which has been shown to work in practice.The ability to transfer proofs between situations is really

powerful, and gives, concretely some of the promised abilities of

homotopy type theory. This is illustrated by an example in Section 5.The paper is generally quite clear, though I found the language a

little too roundabout in places.

Things that could be improved:

The custom equality types in section 2.3 (on page 10) seem to be

solving the same problem as McBride's heterogeneous (or "John Major")

equality:https://coq.inria.fr/distrib/current/stdlib/Coq.Logic.JMeq.html

`JMEq`

allows the statement of equalities between types that are not

yet known to be definitionally equal. It is specifically designed for

this kind of case of telescoping dependent indexes in inductive

types. Would using `JMEq`

simplify your translation. `JMEq`

supposes

proof irrelevance, but you are already doing this.

- The iso translation is justified by essentially: we tried to prove

it without these assumptions and got stuck, so we added these

assumptions (isomorphisms) and proved that they are preserved by all

the type constructors. Is there a more high-level reason why

isomorphisms are the right thing here?

Some possibly related work:

Edmund Robinson: Parametricity as

Isomorphism. Theor. Comput. Sci. 136(1): 163-181 (1994)

The introduction keeps referring to "undecidable relations" when

talking about relations that are expressed in Coq as functions into

Prop. I understand that the point is that the 'AnyRel' translation

does the right thing for relations with codomain 'bool', and that

these are decidable. But the fact that the relations in Prop might be

undecidable isn't what makes the translation difficult, right?The "Eliminating Unused Hypotheses" process described in Section

4.2 seems very ad-hoc.The authors appear to have made everything fit the page limit by

removing all vertical space around displayed pieces of Coq code. I

found this quite difficult to read, despite the syntax highlighting.In general, the writing is a bit wordy in places and could really

do with some editing. For example, page 2, lines 39 to 41 has a

sentence that starts with "As a result, .." and ends with "... true

and false" and contains two colons and several clauses. It could be

simplified by (a) deleting the word "much"; (b) deleting "which is not

a universe, and"; (c) deleting "they are mere ...".

I found that the prolix writing style made it quite difficult to

determine what was going on in some places. The constant back and

forth references to "explain below" (where?) and so on were also

distracting.

Also, I think the sectioning could be improved. The discussion of the

translation of inductive types (Sections 2.2-2.6) should be split out

from the basic 'AnyRel' translation in 2.1 in order to cleanly

separate what is new from what is not.

===========================================================================

Comment

---------------------------------------------------------------------------

**PAGE LIMIT EXCEEDED**: The submitted version of this paper exceeds the limit of 24 pages (not including references) that was specified in the call for papers. However, the main body of the paper does fit within the specified limit. For this reason, reviewers are instructed to treat the appendix to this paper as it had been submitted as supplementary material. In particular, this means that **reviewers may choose not to look at the material in the appendix**.