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
     insight, even if it hasn't been stated exactly that way
     before. There are several papers already remarking on the issues
     presented by, e.g., function proxies (e.g., Siek's work on
     Reticulated Python is motivated by Python's extensive use of
     reference equality and other $\eta$-breaking operations; Tanter's
     work on Confined Gradual Typing has a similar motivation)."

   - "The paper claims that "the linchpin to the design of a gradually
     typed language is the semantics of _runtime type casts_"
     (L34). This unsupported claim goes directly counter to the
     intuition of Garcia et al.'s AGT, which says that the linchpin of
     the design is the Galois connection giving meaning to imprecision
     in types. Further, the paper goes on to suggest that grad..."

     Is this a fing joke? Our point is that gradual typing is that
     static reasoning principles are ensured by the dynamic type
     casts. AGT produces these casts by its Galois Connection but the
     casts are still central to the design of the system. The latest
     work you cited changes the input language in order to produce
     different runtime type checking.

   - We think you are misinterpreting what the comment about L124 is
     saying: we are saying that the "full" eta law `M = \x -> M x` for
     functions in CBV can be true if the program's context is pure or
     if `M` is pure, so it is used sometimes to reason about programs
     in a restricted context.

     Our development does not at all restrict to non-effectful
     programs: the CBPV axiomatic theory is compatible with a broad
     class of effects: state, continuations, I/O and that is the main
     reason that we use it.
     In our *specific* model, we have two effects: divergence and an
     uncatchable error, but the soundness of GTT for proving
     contextual approximation would still hold if we were to use a
     language with more effects.

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

     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
     terms which aren't equidynamic? It's not obvious from the
     presentation of the definitions that you're including $\beta\eta$
     in $\sqsubseteq$... but you are, right? In which case
     equidynamism should be not only sound but _also complete_ for
     contextual equivalence (L758).

     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 include beta-eta in the definition of term dynamism in figure
     4, where they are labeled as axioms of term dynamism.

     It does not make sense to ask if our syntax is complete for
     contextual equivalence without fixing a particular operational
     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.

   - Do these theorems hold when you distinguish between different
     errors via, e.g., blame labels?

     For many of our theorems the distinction is small. The
     dynamic gradual guarantee allows for a term with more precise
     types to error with a different blame label, so any system we
     made that axiomatized the ordering in the gradual guarantee would
     necessarily have that any two errors would be equi-dynamic
     regardless of their blame label, so it doesn't change much to
     just consider them equal in our axioms.

     On the other hand, it seems sensible that our cast uniqueness
     theorems should hold in the presence of multiple blame labels if
     formalized correctly. For instance in the product cast uniquenes
     theorem:
     
        <{A1' x A2'} <-< {A1 x A2}>y
        = split y to (y1,y2). (<A1' <-< A1>y1, <A2' <-< A2>y2)
	
     the correct blame-sensitive statement would be that these hold
     when both sides all use the same blame label. It is not clear to
     us how to formalize this exactly, but this was attempted in some
     unpublished work by Findler-Blume-Felleisen where the ordering
     was parameterized by which error was considered the "current
     blame label":
     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
     the program" as you say, but we also want to emphasize that the
     static equivalences hold even in the presence of interaction with
     (more) dynamically typed code, which is exactly what the casts
     ensure.

4. Reviewer C says that we are overly specific in our view of gradual
   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
cannot ever be used. For instance in OCaml an eta reduction is not
necessarily an equivalence because of reference equality of functions,
but in a specific portion of a program where reference equality of
functions is not being used programmers will refactor in ways that are
only justified by eta principles. What we have shown is that anything
besides the cast semantics *breaks the eta principle in a new way*. So
this means that in order