popl19-reviews-9.txt

POPL 2019 Paper #9 Reviews and Comments
===========================================================================
Paper #9 Gradual Type Theory


Review #9A
===========================================================================

Overall merit
-------------
A. Strong Accept

Reviewer expertise
------------------
Y. Knowledgeable

Paper summary
-------------
This paper presents an axiomatic characterization of gradual typing. Starting with a call-by-push-value setting, the paper presents axioms that that casts (and precision) must follow, and characterizes what all conforming implementations must then satisfy. This turns out to uniquely determine many aspects of the system, picking out a fairly traditional form of gradual typing as the only one to satisfy the desired axioms, which include \beta, \eta, and the dynamic gradual guarantee. The paper then shows that a standard operational interpretation makes sense for the theory, with contextual equivalence coinciding with equi-dynamism.

Strengths
---------
This paper makes a fundamental contribution in understanding gradual typing from the theoretical perspective. It demonstrates that from basic principles of what gradual typing _should_ mean, we can derive how to do it, justifying existing choices and showing the design space for more.

Weaknesses
----------
The paper is extremely dense and technical, and that even though much of the real work is deferred to the supplementary material.

Comments for author
-------------------
This is an excellent if difficult paper, and deserves acceptance.

## Smaller comments

line 135: eta is mostly used in one direction for optimization, and it's the other direction that fails for these cases, right?

687: shouldn't one of these be an upcast?

781: is the unforcedness of these choices connected to similar unforcedness of the treatment of flat contracts in the "blame completeness" of [Dimoulas et al]?

887: This `tycase` construct (and the whole discussion here more generally) is very reminiscent of the `type Dynamic` work.

1025 (but also elsewhere): using numeric citations as nouns is very confusing

1143: why isn't the transitive relation between V1 and V3 at some number larger than i?

1200: 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].



Review #9B
===========================================================================

Overall merit
-------------
C. Weak reject

Reviewer expertise
------------------
Z. No familiarity

Paper summary
-------------
The paper presents Gradual Type Theory, an axiomatic logic to reason about both CBV and CBN semantics. The GTT is formalized and proved sound for contextual equivalence.

Strengths
---------
The problem addressed in this work, i.e., checking program equivalence under both CBN and CBV semantics is very ambitious.

Weaknesses
----------
The writing of the paper can get improved so that it is more approachable to outsiders. There is no conclusion, no examples (after section 1), and the outline and contributions of the paper are not clearly stated.

Comments for author
-------------------
Being very familiar with the theory of gradual types, but not familiar with neither CBPV nor logical relations, it was very difficult for me to understand the technical contributions of this paper, so I can only provide shadow comments. 

The introductions sets the goal of the system (i.e. program equivalence) but
- It does not properly describe the problem: how does the combinator of gradual types, CBN, CBV interacts with program equivalence? Why can't I just use existing systems that check equivalence of CBN or CBV programs?
- There is no overview of the system: I suggest you add examples that your system accepts and rejects to provide an overview of your rules. 
- There are distracting details, e.g., the compositionality and dynamic gradual guarantee assumptions come too early, before the system (and the need for these assumptions) is explained. 
- The contributions and outline of this work are not clearly stated. 

Then, then paper jumps into the technical details, that, due to the lack of the overview/proper motivation, are difficult to follow by a non familiar reader. 
In short, for POPL acceptance the writing should get improved, so that at least the intuition of your system gets conveyed even to outsiders.  


- I found the title of the paper misleading: I expected that gradual type theory defines a unified theory for gradual typing and not a program equivalence logic. 
- Typo: pg 1: "vice-versa However"



Review #9C
===========================================================================

Overall merit
-------------
B. Weak accept

Reviewer expertise
------------------
X. Expert

Paper summary
-------------
This paper uses call-by-push-value (CBPV) to develop an axiomatic semantics for a gradual lambda calculus the authors call _Gradual Type Theory_ (GTT). GTT is built around the _dynamic gradual guarantee_: if you take a working program and replace some of its types with less precise (i.e., more dynamic) ones, then your program behaves the same. The core formalism is the axiomatic semantics and its corresponding theory of equality.

The core result is that languages with $\eta$ laws and the dynamic gradual guarantee must have the conventional semantics. To put it another way, if a gradually typed language's dynamic semantics doesn't use the conventional semantics, then either $\eta$ is violated or the dynamic gradual guarantee doesn't hold. This theorem (Theorem 3.5) is established in the axiomatic system. The paper then shows that a more or less conventional model satisfies these axioms.

Strengths
---------
The core theorem is a novel one and neatly characterizes a swath of the design space of gradual typing semantics.

Weaknesses
----------
It's not clear how the core theorem is actionable.

The paper presumes a notion of gradual typing that is not universally accepted.

It's not entirely clear who the paper's audience is.

The cost of abstraction in this paper is very steep, and it's not entirely clear what the generality is _for_.

Comments for author
-------------------
My fundamental criticism is that the ideas of this paper fall into two categories: things that experts on gradual typing already know (e.g., cast semantics that munge proxies disrupt $\eta$) and things that are new but aren't obviously actionable ($\eta$ + dynamic gradual guarantee => conventional cast semantics). My concern is that the audience who will get something out of this paper is restricted to people who are (a) adept with CBPV and (b) know nothing about gradual types. I think the best way to improve the paper would be to use GTT to design a new gradual programming language, making use of Theorem 3.5 and the equational reasoning you've developed. You could further broaden your audience (and not lose much) by abandoning CBPV and using a simpler semantic framework. As it stands, the theorem and equations are underwhelming. My score is a B because (a) I believe the theorems and (b) I may be wrong about the narrowness of the paper's potential audience and applications.

Gradual typing experts will be surprised by the paper's particular notion of what gradual typing is. I would not refer to the dynamic gradual guarantee as "now standard", considering that a number of reasonable systems reject it (e.g., systems for information flow or polymorphism, or in type systems attached to existing dynamic languages). In fact, the correctness criteria of gradual typing seem to be very much in flux. While Theorem 3.5 covers quite a bit of space, it covers only that design space that has both the dynamic gradual guarantee and $\eta$ rules. From a practical perspective, that's a very narrow space!

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 gradual typing is always between "static and dynamic typing" (L36; similarly at L360), when recent examples (information flow, effects) directly falsify that. You later claim that AGT is based on the operational semantics of languages (L1180), when it's based on a proof _relating_ the static semantics to the operational semantics.

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 does insufficient justice to Henglein's seminal work. Henglein's early paper not only introduces all of the ideas of gradual typing through, say, Herman et al.'s work on space efficiency, it also gives an equational theory, contra the discussion around L63. Moreover, the paper doesn't produce any particular equalities that one might want to reason with while programming.

The suggestion to restrict to non-effectful programs (L124) is a surprising one, since blame is an effect. (While most formal models treat it as uncatchable and therefore a more benign idempotent effect, real implementations would certainly not do so.). Study of lazy gradual type systems seems to be more or less abandoned since Degen and Thiemann's work (2010, 2012). While the generality bought from CBPV is nice, in principle, I don't see the point. Not only is blame an effect (and therefore plays poorly in practice with laziness), but laziness and dynamic checking cannot be both _complete_ and _meaning preserving_ (Degen and Thiemann 2012).

Please name your rules. For example, I would name the rules in Figure 3: refl, trans, var, subst, stoup, msubst, monopair, monosplit, monoret, monobind, monolam, monoapp. Having these names would have significantly eased my time reading.

I was repeatedly flummoxed by observations like "it is very natural to make the dynamic type the minimal type with injections from $G$: i.e., the sum of all value ground types" (L816-817). What you're describing are _type tags_, but it sounds as though you've just discovered or invented or justified them for the first time.

L17 Your "equational analogue of Wadler-Findler's blame soundness theorem" only covers one direction, since you only have $\sqsubseteq$, i.e., naive subtyping. The abstract seems to overclaim at L18, since we are only given intuition---not a theorem---at the paragraph at L1199.

L475 "that it is true" ?

L559 It would be worth spending some more time discussing why $\mho \sqsubseteq M$ for all well formed $M$. (NB that the rule here seems to have a typo, writing $M'$ above the line and $M$ below.) The intuition I found was that failures $\mho$ represent being "too" precise.

L898 do you mean $\lfloor A \rfloor$ instead of $G$ in the rule for variables?

Questions for authors’ 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).

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



Review #9D
===========================================================================

Overall merit
-------------
A. Strong Accept

Reviewer expertise
------------------
X. Expert

Paper summary
-------------
The paper defines gradual typing from the perspective of what axioms should be satisfied; if the axioms hold, various transformations preserve meaning.  Only certain cast strategies (cast semantics) validate both "graduality" (the dynamic gradual guarantee) and the axioms, suggesting that those strategies may be preferable.  The paper "instantiates" the model with different interpretations of the unknown type ?.  The work is based on call-by-push-value (CBPV), subsuming some previous work, and leading to a characterization of casts in terms of distinctions made by CBPV.

Strengths
---------
The use of CBPV to cover a wide range of semantics, teasing out subtle properties of casts; careful formulations and writing; a fresh perspective on gradual type system design.

Weaknesses
----------
Introductory sections don't clearly structure the paper's contributions; later sections are dense (possibly unavoidable).

Comments for author
-------------------
I will preface this review by admitting that I spent less time on the paper than I would like, skimming a lot (especially the last few pages).  To the extent that an "X" rating should mean "high confidence", my confidence is somewhat lower than that.

However, based on what I have read, the parts of the technical development that I can follow (particularly around CBPV, type dynamism, and term dynamism) are solid.  The flaws that are apparent to me are mostly around presentation of the early sections.  Modulo those issues I think the paper should be accepted, and even if the presentation didn't change at all, the underlying work seems important enough to deserve acceptance.

I'll try to explain why.  Gradual typing research has been characterized by explosive but not always orderly growth.  Some principles have been generated (discovered) but at a lower rate than the gradual type systems.  The value of this paper's approach, as I understand it, is to turn around the "design system, check for good properties" by assuming the good properties and figuring out (parts of) the system in reverse.

The dynamic semantics of gradual typing is all about casts, which are effectful in the sense that some of them can fail.  A key insight of the paper is that call-by-push-value, with its value/computation distinction, can be used as a consistent basis for various flavors of gradual type systems.

So, as far as I can tell, the content seems strong and I am complaining primarily about presentation (and, relative to most papers, my complaints are minor).

First complaint:

The introduction doesn't clearly structure what the author(s) see as the contributions.  Line 165 says "One of our main contributions (Section 2) is to..." but what are the other main contributions?  It's not immediate.  The paper is building on/subsuming two previous papers, but I didn't see a delineated introduction to those papers.  (Confusingly, the work in this paper is called "GTT" and is explicitly based on call-by-push-value, but one of the previous papers [26] is called "Call-by-name Gradual Type Theory" and mentions a CBPV formulation as future work, so...GTT in this paper is a new thing, but generalizes previous work also called GTT.)  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.

Second complaint:

Lines 116-117: "it disables the very program equivalences that gradual typing should provide"

This feels like overreaching.  Why should gradual typing always be expected to provide those equivalences?  From a logical perspective, gradual typing simply ruins the interpretation of programs as proofs.  Classic program equivalences correspond to proof reductions and proof expansions—but if a program can't be interpreted as a proof, why should I expect proof/program reduction (or expansion) to always work?

I certainly accept that having η-equivalences, etc., is good, but I'm not convinced it's _essential_, which the paper seems to assume.

The paper also says (lines 74-75) that "the actual desired properties of the gradual language" are "program equivalences in the typed portion of the code that are not valid in the dynamically typed portion", which makes sense to me: only the "static" part of the program can be expected to enjoy the usual program equivalences.  If the entire program is static (which is, to me, the proper goal for users of gradual typing), all of it will enjoy the equivalences.

If I read lines 116-117 with an implied "within the static portions of a program", am I reading it correctly?


Not a complaint, a question (unlikely to affect my decision): For "less gradual" languages in which dynamism doesn't go all the way up to ?—where you have a gradual type coming from a proper subset of all static types—does all this work carry over?  I feel like the answer should be yes, but the technique of upcasting all the way to ? makes me a little worried.


Minor comments:

Line 93 implies that "graduality" is another name for the dynamic gradual guarantee.  Line 108 says "the gradual guarantee"; is this the dynamic gradual guarantee, the entire gradual guarantee, or something else?  The sentence can be technically true if it's the *dynamic* guarantee (because the guarantee is the conjunction of its parts) but it's not clear.

Line 111: I assume the meaning is "under the assumption x : ..., the term let ...  is not equivalent...", but the paper simply writes the assumption followed by the term.  Based on later notation, I think this is just a missing turnstile.

Line 128: "Performing an if statement" sounds odd; at this point in the paper it's not obviously CBPV, where "statement" is plausible as a computation, and both "perform" and "statement" are unexpected in the context of an ordinary CBV functional language.  Line 130 uses "run", not "perform".

Line 269: I would give the mnemonic "liFt / thUnk".

Line 365: I'm not surprised that using CBPV would lead to two unknown types; CBPV distinguishes stuff that is usually not distinguished, so a thing with one name can easily become two things.

Line 1180: AGT is based on operational semantics more than it's based on axiomatic semantics, but it's primarily based on typing—*static* semantics.  I got the point eventually, but it was a little jarring.

The supplementary material follows the same structure as the paper, which makes non-obvious what is "new" compared to the main paper.
In some places (e.g. page 57), lines run off the page.

Questions for authors’ response
---------------------------------
Not absolutely essential, ignore if other reviewers have more pressing questions:
Is my interpretation of lines 116-117 as "within the static portions" (mostly) correct?