edits to response

popl19/response2.md

@@ -12,7 +12,7 @@ generally any pattern match) out of a lambda are very common in
 refactoring and optimization.
 
 In terms of "actionable" theorems, we show that upcasts form complex
-values and downcsats form complex stacks, which also justifies 
+values and downcasts 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
@@ -68,19 +68,20 @@ very rare in Typed Racket).
    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. We don't konw
+with any type D that is more dynamic than both A and B. We don't know
 of any systems where a cast A => B is 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.
+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.
+The comment in the intro where we say "restrict to non-effectful code" concerns
+the eta rule (explaining the eta rule in traditional call-by-value is restricted
+to values or non-effectful code). 
+
 
 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?"
@@ -104,4 +105,4 @@ specification of casts.
 
 We will also add a discussion of Degen and Thiemann's work, which is
 related: their completeness property inherently violates CBN eta
-principles, so is incompatible with "lazy" checking.
\ No newline at end of file
+principles, so is incompatible with "lazy" checking.