extend rebuttal

popl19/corrections.org

 * Typos
   - 111: missing a turnstile, would be better to have on its own line.
+  - 687: one of these should be an upcast
+  - l475: "that it is true" that what is true?
+  - l559: the rule err <= M uses M below and M' above.
+  - l898: G should be floor A
 * Clarity
+  - multiple reviewers: there isn't a "we did this" part of the intro
   - numeric citations as nouns: L1025 and "elsewhere".
   - 108: *dynamic* gradual guarantee
   - "AGT is based on operational semantics more than it's based on
@@ -8,3 +13,16 @@
     semantics.  I got the point eventually, but it was a little
     jarring."
   - CBPV mnemonic: liFt, thUnk
+  - You correctly saw the need for a section to give background on
+    CBPV, but it's also important to clearly summarize the two papers
+    you're generalizing.
+* Proper Attribution
+  - Blame soundness as a concept is not due to Wadler and Findler, but
+    to [Tobin-Hochstadt and Felleisen 2006] , although you may be
+    thinking of a more specific result here from Wadler and
+    Findler. The argument in this paragraph (the continuation cannot
+    affect the result and thus does not deserve blame) is very similar
+    to the criteria given in "blame correctness" by [Dimoulas et al
+    2011].
+  - Our work on constructing models of the dynamic type should cite
+    some of the obvious stuff on type tags, type Dynamic, etc.

popl19/outline-response.org

 * Reviewer A (Accept)
-  - 
+  - (l35) eta is mostly used in one direction for optimization, it's
+    the other direction that fails for these cases right?
+    - Ans: 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.
+  - 781: is the unforcedness of these choices connected to similar
+    unforcedness... Could you be more specific about what you mean? It
+    sounds intriguing but we don't understand the question. Is the
+    paper being referred to Dimoulas et al 2011?
+  - 1143: why isn't the trans relation at some number larger than i:
+    this is technical but standard: the short explanation is that `i`
+    here is only a bound on exploring the behavior of V1 (i.e. the
+    left-hand side), so it doesn't change when we go from V2 to V3.
+  - 1200: we 
 * Reviewer B (Weak Reject)
 * Reviewer C (Weak Accept)
 ** Things I will respond to
+   - "cast semantics that munge proxies disrupt \eta"
+     - A: we think it is oversimplifying our discussion of eta to say
+       that the observation that eager semantics has already been
+       shown. The two examples given involving reference equality are
+       situations where the eta principle is not present, not where it
+       is broken by the cast semantics, as we discussed. If you can
+       point us to work where the this has been noted before, we would
+       be happy to see it.
    - "But beyond these criticisms of the paper's scholarly situation,
      there's more: the core result---that $\eta$ isn't compatible with
      some of the trickier forms of gradual checking---is hardly a new
@@ -45,11 +70,16 @@
    - "Moreover, the paper doesn't produce any particular equalities
      that one might want to reason with while programming."
 
-     This is ridiculous, we show an entire class of equalities that
-     are useful for program reasoning by programmers and compilers
-     alike: things like lifting an if statement out of a lambda and
-     knowing it's safe are very common in refactoring and
-     optimization.
+     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.
+
+   - "Degen and Thiemann's work": we thank the reviewer for pointing
+     out this related work. Our perspective on their result is that
+     their definition of "completeness" is inherently call-by-value in
+     that it requires breaking eta equalities that a lazy language is
+     intended to provide.
 ** Questions for Response
    - What do you mean that you have a syntactic judgment for
      contextual equivalence? (L514) Are there contextual equivalent
@@ -101,6 +131,14 @@
      https://newtraell.cs.uchicago.edu/research/publications/techreports/TR-2004-02
 
 * Reviewer D (Accept)
+** Other Qs
+   - For "less gradual" languages in which dynamism doesn't go up to
+     ?...upcasting all the way to ? makes me a little worried.
+     - 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.
 ** Questions for Response
    - 
    - The typed equivalences should hold "within the static portions of
@@ -113,7 +151,6 @@
    typing: that we only consider languages that have eta laws and the
    dynamic gradual guarantee.
 
-
 This seems like a narrow view of programming language semantics. Often
 in practice languages will not satisfy idealized properties because of
 certain known features. This does not mean that these principles

popl19/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
@@ -42,3 +44,42 @@ 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.
\ No newline at end of file