Skip to content
Snippets Groups Projects
Commit 3d521ac3 authored by Max New's avatar Max New
Browse files

start popl reviews

parent 3ca81af2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
popl19/corrections.org 0 → 100644
+ 10
− 0
View file @ 3d521ac3
* Typos
- 111: missing a turnstile, would be better to have on its own line.
* Clarity
- numeric citations as nouns: L1025 and "elsewhere".
- 108: *dynamic* gradual guarantee
- "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."
- CBPV mnemonic: liFt, thUnk
popl19/outline-response.org 0 → 100644
+ 126
− 0
View file @ 3d521ac3
* Reviewer A (Accept)
-
* Reviewer B (Weak Reject)
* Reviewer C (Weak Accept)
** Things I will respond to
- "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."
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.
** 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)
** 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
popl19/popl19-reviews-9.txt 0 → 100644
+ 233
− 0
View file @ 3d521ac3
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?
popl19/response.md 0 → 100644
+ 44
− 0
View file @ 3d521ac3
We thank the reviewers for their feedback.
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.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment