response2.md

We thank the reviewers for their very helpful feedback and will revise the paper accordingly.

1. Reviewer C says "Moreover, the paper doesn't produce any particular equalities that one might want to reason with while programming."

We would push back on this criticism: we show soundness of an entire class of equalities that are useful for program reasoning by programmers and compilers alike: things like lifting an if statement (or more generally any pattern match) out of a lambda are very common in refactoring and optimization, and induction is fundamental for any program verification.

In terms of "actionable" theorems, we show that upcasts form complex values and downcsats form complex stacks, which also justifies refactorings and optimizations. For instance, upcasts, as complex values, can be freely (de)-duplicated, discarded if not used, and lifted out of loops as if they were values. Downcasts, as complex stacks, are strict in their input, which aids strictness analysis, as in optimizers for lazy langauges.

2. Reviewer C asks about the meaning of L514 and whether or not our syntactic theory of term dynamism and equivalence is not only sound but complete for contextual equivalence.

Our sentence is a bit awkwardly worded, but we mean that if two terms are equidynamic, then in operational models they should be contextually equivalent. We do include beta-eta in the definition of term dynamism in figure 4, where they are labeled as axioms of term dynamism, but this is not enough to prove completeness for an effectful language like cbpv: for instance, both sequential and non-deterministic languages should model all of axioms. To ask if our syntax is complete for contextual equivalence we need to fix a particular model. The syntax is not intended to be complete for any particular model, in order that it apply to as many models as possible. This is what allows us to interpret the model with incompatible definitions of the dynamic type and extend it with new axioms based on that model like those given in figure 5.

3. Reviewer C asks "Do these theorems hold when you distinguish between different errors via, e.g., blame labels?"

It seems likely, but it's not yet clear how to formalize these properties with multiple blame labels. For instance, the dynamic gradual guarantee allows for a more precisely typed program to error with a blame label different from the less precise program. So if our ordering models the dynamic gradual guarantee, this means that blame(l) would be a least element of our ordering for every label l so any two blame errors would be equivalent.

On the other hand the uniqueness theorems seem that they should hold when all of the casts involved have the same label; we plan to explore this in future work, building on the unpublished tech report: https://newtraell.cs.uchicago.edu/research/publications/techreports/TR-2004-02

4. Reviewer D asks to clarify lines 116-117.

Yes, we mean that the typed equivalences should hold in the statically typed portions of the code; the dynamic type casts ensure that the equivalences hold in statically typed portions of the code even if they interact with (more) dynamically typed code. We expect that it will be rare for gradually typed programs to be completely typed (e.g. this is very rare in Typed Racket).

5. Reviewer D asks about languages where dynamism doesn't go all the way up to ? if we can still reduce everything to upcasts and downcasts.

The use of ? in the factorization of a cast A => B can be replaced with any type D that is more dynamic than both A and B, so ?, if it is present, always works. We would be curious to know of any systems where a cast A => B was allowed but they have no common dynamism-supertype.

6. Reviewer C says that we "restrict to non-effectful programs" and finds it surprising because "blame is an effect".

This is not what we intended by that comment in the intro (which is only explaining that the eta rule in traditional call-by-value is restricted to values). In this paper, we do treat dynamic type errors as an effect, and as Reviewer D notes, this is one of the main reasons we use CBPV: to have an axiomatic theory that is valid in the presence of arbitrary effects.

7. Reviewer A asks "(l35) eta is mostly used in one direction for optimization, it's the other direction that fails for these cases right?"

Yes, in the "eager" cast semantics, the eta law for functions should be an ordering V <= \x -> V x but it's debateable whether this means that the right should be allowed to be optimized to the left. This would make the semantics of the program dependent on the precise behvior of the optimizer, so it would be very hard to change the optimizer without either making code error that didn't before or vice-versa (because whether or not an optimization is triggered can be very sensitive to small changes).

8. Reviewer C comments on some missing related work.

We apologize for the oversight and will add appropriate discussion; for Henglein, a significant difference is that the equational theory there is based on a rewriting system with cast rules for each pair of types, whereas in our approach those rules are a theorem following from the universal characterization of casts. For others TODO?

9. Reviewer B: we apologize that the presentation was not accessible and will work to give a better high-level introduction in the revisions. The reason existing work does not suffice is that gradual typing introduces a dynamic type ? and type casts, and the question is how to enrich the equational theories of CBV and CBN with these features.