response.md

We thank the reviewers for their feedback.
We labeled each question with "Reviewer A|B|C|D" so ctrl-f your
designation to see your responses

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

The 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-sequential 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.

2. 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 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, but we don't
know how to formalize it currently, but would likely build on the
approach in the unpublished tech report:
https://newtraell.cs.uchicago.edu/research/publications/techreports/TR-2004-02

3. 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, we want to emphasize that 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, and it is very rare in Typed Racket for this to be
the case.

4. 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 ? is the most convenient since if its present it 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.

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

This is taken out of context, 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
effects.

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

This is a completely incorrect criticism.
We show 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.

Furthermore, we show that upcasts form complex values and downcsats
form complex stacks, which also justifies a great deal of refactorings
optimizations since for instance complex values can be freely
(de)-duplicated, discarded if not used and lifted out of loops as if
they were values.
Since downcsats are complex stacks/linear they are strict in their
input, which aids strictness analysis, which is a major input for
optimizers for lazy langauges.

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" 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).