popl20response.md

Thank you for your reviews. After a shorter general response, there are point-by-point responses for those inclined to read them.

As far as motivation (Reviewer A): there are currently a range of interesting program analyses formulated as sequential effect systems. Currently, none of them can handle control flow more complicated than while loops or simple recursion. Exceptions and generators, which are now widespread, have never been addressed in any sequential effect system. While there is perhaps a case to be made that delimited continuations might be "more" than we should address directly (Reviewer B), it seems that growing interest in algebraic effects (tunneling algebraic effects are essentially tagged delimited continuations) and the impending addition of explicit delimited continuations to the JVM (see Project Loom https://wiki.openjdk.java.net/display/loom/Main) would suggest that in addition to playing a role in deriving rules for "weaker" control operators, they are also of growing direct interest.

The shared concern of Reviewers B and C is clarify of exposition. Clearly the style of exposition I've used works for some readers (e.g., Reviewer A), but not for others --- this dichotomy has persisted through several rounds of reviewing even with significant rewrites of the middle section of the paper. The core tension I've been struggling to resolve is the competition for space between intuition and expounding lower-level technical details.

Adding more concrete examples has been suggested a couple times, and I've responded by trying to add small examples and make existing ones more concrete (I see the comments that this latest rounds has not succeeded in the latter), because the alternative seems to be compromising on background material (which people seem to need) or technical exposition (which seems like a bad idea). Adding a larger quantity of concrete examples would seem to require a substantial amount of space; my ideal approach would work through:

• Ordinary effect quantales (roughly, background section material) Prompts and aborts (addressing
• early-return and exceptions) Continuation types / replacing contexts / invoking continuations
• (without addressing where they come from) Prophecies without control (i.e., just capturing
• continuations involving only underlying effects)
  • This includes introducing the idea that a continuation type models the fact that given a continuation E of type cont τ χ τ', invoking it with a value v of type τ will result in a term E[v] of type τ' and effect χ, and the purpose of the current prophecy structure is to be able to construct this typing derivation for a captured continuation.
• Prophecies capturing aborts Prophecies capturing continuations involving continuation invocation
• (with only abort/replace) Prophecies capturing further uses of call/cc (i.e., the reason
• prophecies contain full effects) Nested continuation capture and aborts/continuations "jumping
• over" the nearest same-tagged prompt due to being nested in a different prompt's continuation (i.e., the need for blocking until a tag)

So a question: other than trying hard to reduce verbosity and perhaps cutting the typesetting of call/comp rules, are there any places in the paper you felt the content did not need to be there, or at least seemed less important than missing examples?

POPL 2020 Paper #120 Reviews and Comments

Paper #120 Lifting Sequential Effects to Control Operators

Review #120A

Overall merit

B. Weak Accept

Reviewer expertise

Y. Knowledgeable

Paper summary

This is a paper shows how to design type-and-effect systems for languages with both sequential (i.e. noncommutative) effects and delimited control operator. It does so in a quite general way, by considering notions of control operator through macros, and abstract effects as modeled by effect quantales. The obtained type system is reasonably simple, and derived rules are given for various control operators. Type preservation and progress are the main technical results of the paper.

Strengths

The paper is beautifully written, in such a way as to allow even the non-specialist to understand the details. The type system described in Section 4 is quite simple and natural, and can arguably form the basis of a type system for concrete functional languages. Comparison with related work is comprehensive, and satisfactory. Thank you!

Weaknesses

The paper does not give any compelling case for mixing sequential effects with delimited control. Why would the PL community be interested in this contribution? Is there any specific programming language in which keeping track of effects the way the proposed type system can do would be beneficial?

There are a range of program analyses characterized as sequential effect systems (cited in the introduction and later in the paper), for properties such as flow-sensitive lock ownership tracking, reasoning about program traces, atomicity, and more. Without the work described in this paper, none of this applies to program with more sophisticated (single-threaded) control than loops or recursion. None of the prior work on sequential (flow-sensitive) effect systems can handle exceptions. None can handle generators. Yet these are increasingly popular features. This paper's contribution make it possible to take those analyses and apply them to programs that use these features, or delimited continuations. And by targeting delimited continuations and deriving rules for such constructs rather than addressing each control flow construct individually, we (1) ensure the derived rules will compose with each other and (2) ensure that if new control constructs arise, as long as they are expressible via delimited continuations (we are aware of no counterexamples to this currently) we can derive rules for those that compose with rules for existing constructs.

Moreover, there is increasing interest in languages that do have delimited continuations! The solution to a recent modularity problem with algebraic effects --- tunneling --- is in fact an implementation of tagged delimited continuations. And major platforms are adding delimited continuations: this is an explicit goal of OpenJDK's Project Loom (https://wiki.openjdk.java.net/display/loom/Main), which is far enough along that there are prototypes available for download.

Review #120B

Overall merit

C. Weak Reject

Reviewer expertise

Y. Knowledgeable

Paper summary

Suppose we have an effect system Q for an effectful language. We extend the language with some new control structures, such as call/cc. Can we appropriately extend the effect system Q to a richer one C(Q) which can be used for the extended language? The authors give an answer for a version of call/cc with multiple tags.

Starting from an effect quantale Q for the underlying effects, the authors construct an elaborate new structure C(Q) that can deal with the intricacies of non-local control. However, C(Q) is not an effect quantale -- first it would have to be quotiented by a suitable equivalence relation.

The system is demonstrated on the example of deriving the effects for a loop, implemented using call/cc and co., from first principles.

Strengths

The approach is generic, i.e., we can start with any effect quantale Q and derive the corresponding C(Q).

Weaknesses

The system is extremely elaborate, which raises serious doubts about its usability. The authors do their best to explain what is going on, but I am afraid that at least for me that's not good enough. I was unable to penetrate the complexity of the system, in part because some things remain unexplained, or at least not explained sufficiently to be understandable (see comments below).

It is also a bummer that C(Q) ends up not being an effect quantale. The authors say they could have quotiented it to become one, but they do not discuss what happens after quotienting (maybe the whole thing trivializes), nor how the quotient would affect applicability of their effect system in practice (it may induces some nasty questions about computing the equality and the partial order of effects).

I have submitted this paper several times now, with significant rewriting of the middle section. This is actually the first time I have not presented the result as an effect quantale --- each prior time I presented the quotienting as part of the construction C(Q) rather than factoring it out. And each time there was nearly universal consensus among reviewers that the quotienting added more inessential complexity to the exposition, often coupled with complaints that requiring the result to be an effect quantale was too limiting on philosophical grounds. I'm not particularly tied to including the quotient in C(Q)'s definition or as a separate transformation.

The supplementary content includes discussion of the quotient, noting that it does not trivialize (unless the underlying effect quantale was already trivial). The quotient doesn't affect computability in a meaningful way --- the quotient is essentially element-wise over-approximation, similar to depth subtyping of records, or the way a set of Java exceptions are checked for containment (A $\sqsubseteq$ B if every exception type in A has a supertype in B). The main hurdle for implementations is that prophecy sets are allowed to be countably infinite, though in examples I've looked at they appear to be regular (since the only time C(Q) creates an infinite set is from the infinite union in the iteration operator). I can't claim that will hold for all examples, though.

Comments for author

I have great difficulties understanding the paper. Whenever this happens I worry greatly that I am not an appropriate referee and that I am out of my league. However, I am not entirely ignorant about effect systems, having published work on them, as well as on topics related to delimited continuations, so I think it's not entirely my fault. Please take the following comments as an explanation of why I failed to penetrate the paper, so that you can think of ways of improving it.

This paper feels like it is not yet finished work. You central construction C(Q) is not what you set out to do (if it is, you certainly managed to give me the wrong expectation), namely an effect quantale. You say you can quotient it -- but then you would have to study the quotient and address possible algorithmic issues. Namely, once you have the quotient, can you still compute whether two (representatives of equivalence classes of) effects are equal, or related by the induced ≤ relation?

This was mostly addressed above, but for a bit more detail: to compare effects according to ≤, for prophecy sets and control effect sets, for each element of the "smaller" effect, the implementation would have to find an element of the same component in the "larger" effect with a greater effect (and result type). Control effect sets (after quotienting) are always finite. Prophecy sets are countably infinite, but the only way an infinite prophecy set is generated is by use of the closure operator, which only generates infinite unions. I hypothesize (but have not proven) that checking the case where the lesser effect contains such an infinite union, simply finding a corresponding piece in each larger union would be adequate, and make the number of checks finite for any given effect.

I find the complexity of your system completely overwhelming. If there is no simpler way to achieve your goals, perhaps we should just stop using call/cc, like we stopped using goto many years ago. I do not see anyone developing an effect system for goto... Be that as it may, here are some technical comments and remarks to show where I got lost in the text.

A surface-level effect system for call/cc is only one application of this, with the second being to derive rules for weaker control structures like generators that are already widely used in practice. Note also that as mentioned above, delimited continuations are being added in more places, and combining algebraic (computational) effects with sequential (static) effect systems faces the same problems as call/cc.

Line 126: if you're going to make references to other people's work, then make them for real, and reference the things you care about. Here you references three works on deadlock freedom, but in line 27 you reference a different set of works. So it all looks pretty random and unnecessary. If you feel like you're doing it just to satisfy referee's whims, then I suggest you do not do it at all and stand your ground. A good middle ground is to collect related work in one place and do a proper comparison there, but then you do not have to litter the entire paper with random citations that serve no purpose.

Lines 134--140: you did not explain the basic judgement form Γ ⊢ e : τ | χ. I have to guess that it means: in context Γ expression e has type τ and it may cause effects χ. This is how you start losing your readers.

Line 242: In Section 2.2 you set out to review tagged delimited continuations. You tell the experience reader they can skip the section -- that's not me, although I am "knowledgeable" about the topic. So presumably the section is for the rest of us, the non-experienced readers. However, in line 242 you make a terse reference to Figure 1, without any further explanation of what is what. As a non-experienced reader I would appreciate having my memory refreshed. Instead the entire section 2.2 is just an overview of the myriad of possibilities on how one might design delimited continuations -- so perhaps this is for the expert after all?

A fair point. I should discuss Figure 1. Some of the discussion there is indeed intended for experts, contrary to the start of that section's claim; I have previously had several reviewers who insisted that using a different delimited continuation basis (e.g., shift/reset, shift0/reset0) would simplify the system, even though all are inter-expressible and would face the same problems solved in this system.

Lines 246--260: Figure 1 is not explained, and I feel like it is not my fault for starting to get lost here. Some things are clear, for instance the abstract syntax of expressions E, but how should I understand the basic judgement forms? There are two of them, one has a single arrow → and the other a double arrow ⇒. What is δ in E-PRIMAPP, and what is Values? If you're not going to explain these things, you should give a reference (but it's better to explain at least somewhat). Agreed, sorry. The single arrow is for local reductions, the double arrow is for reductions involving evaluation context manipulation.

Lines 246--260: still staying with Figure 1, you pulled a bait & switch here. Your formal semantics has the call/comp construct which in section 3 you remove. If you're not going to consider call/comp then do not include it because it is both a little bit dishonest and it just puts additional strain on the reader's brain.

call/comp is considered in the technical appendix. It appears in the main paper because I have previously had several reviewers insist it was critical because some of the inter-expressibility results depend on it (even though most people have never heard of it). In particular, it's necessary both for establishing semantic completeness with respect to some denotational models, and it's involved in ensuring correct space efficiency when macro-expressing other delimited control operators.

Lines 326--330: perhaps you should pick an example in which you do not shoot yourself in the foot by giving the wrong semantics of exceptions? In any case, this example is already too elaborate for a "warming up" section. It would be quite OK to have just, say, two exceptions and a concrete piece of code that I can think about.

Lines 437--440: here you set out to explain the crucial concept (P_X, C_X, Q_X). However, you then refer to unexplained concepts that you equip with derision quotes, namely the "regular" executions and the "resolved" behavior. What are these? I do not see a formal explanation anywhere in the subsequent text. Your readers will try hard to understand what you did, but they cannot do so if the explanation refers to undefined concepts? Sorry, my intuition about call/cc is not good enough to be able to guess what "resolved" behavior is supposed to be.

This explanation has been rewritten since the previous submission, and I see I omitted a key point about call/cc: it is typically used to implement new control abstractions (rather than being used arbitrarily throughout code). The notion of "resolved behavior" is intended to refer to the boundaries of these abstractions. For example, outside a try-catch that catches all exceptions, there's no need to reason about exceptions. In this calculus, these correspond to prompt boundaries: all behaviors that target a given prompt (aborts to it, continuation capture up to it) are confined to the dynamic extent of the prompt; the effect of an expression containing a prompt will never explicitly mention non-local control behaviors targeting that prompt, as those behaviors are entirely contained within the expression and do not escape.

Lines 442-468: I stared at Figure 2 for a while. I wish you told me that: UnderlyingfEffect is the effect quantale E from section 2, but you switched notation; when you write set Prophecy and set ControlOperator on the fourth line, the keyword set is probably irrelevant; while option UnderlyingEffect is the option type, etc. It is not easy to find in the text the explanation of the boxed things, those should be more prominent. I wish there were some sort of an overview telling me what is what in Figure 2. There's a bunch of equations, what are they about? What is the NoUnderlyingTop and UnderlyingTop? An overview would be good. It defines the grammar of effects, sequencing and join operations on those effects (primarily in the double-box, with equations above it defining components thereof), and a partial order below the double-box. The $\approx$ is the equivalence relation used in quotienting C(Q) to make it a proper effect quantale. NoUnderlyingTop means no use of top from the underlying effect quantale appears anywhere in the effect(s). UnderlyingTop means it does. $\approx$ considers any two effects mentioning the underlying top --- anywhere --- equivalent, because both indicate a possible error with respect to the underlying effect quantale. When the underlying effect quantale's top does not appear in one of the effects, effects are equivalent if they each overapproximate the other using the partial order on the last line of the figure, which is the component-wise application of the partial orders earlier in the figure for prophecies, control effects, or (optional) underlying effects.

Lines 551--557: There's nothing wrong with C(Q) not being an effect quantale, but they way you wrote the paper you made me expect that you wanted one. More importantly, you propose a quotienting relation ≈ such that C(Q)/≈ is an effect quantale. The quotienting could in principle destroy the structure of C(Q), how do we know this does not happen? If your effect system is to be applied in practice, does the ≈ relation present any difficulties of an algorithmic nature? Please discuss.

I discussed this a bit above. For a bit more on omitting algorithmic discussions, they do not appear in the paper because:

• I have not implemented this yet
• Decidability seems less critical to me than it might in other cases, since some examples (notably Koskinen and Terauchi's trace effects, or Skalka et al.'s history effects) are already undecidable just as a basic effect quantale. Skalka works around this by producing an inference system that generates only effects from a decidable fragment, but this is fairly brittle and unlikely to extend well to contexts like this. This is perhaps worth mentioning in the paper, though.

Of course I could try to establish results relative to qualifications on decidability of questions on the underlying effect quantale (for example, my speculation above that subeffecting could be implemented effectively by exploiting the structure of the prophecy sets actually created by the effect system and closure operator, as long as the over-approximation could be checked in the underlying effect quantale), but I'd rather address this in conjunction with work on effect inference.

Lines 589--614: One again, Figure 3 contains unexplained entities. In T-CALLCONT, what is NonTrivial? Are the lines 589--594 premises of the rule on line 589? Does the rule on line 589 have a name? Wait! The line on 589 may be just a divider between the equations above and the rules below? That's just formatting then? Yes, it's just formatting. NonTrivial is explained in lines 716-721 on page 15.

Line 902--904: Your system is very complex. One way of verifying that it holds water is to provide theorems showing that it has good properties, which is exactly what the Type preservation theorem sets out to do. However, the theorem has unexplained components, again. I am guessing that ⊢ σ : Σ says that σ is a state of state type Σ. But then what is Σ ; Γ in Σ ; Γ ⊢ e : τ | χ? I thought the typing judgement took the form Γ ⊢ e : τ | χ. Next, the q_1, ..., q_n above the arrow are unexplained, I suppose they must be elements of Q. This should have been explained. The actual soundness proof is parameterized by a pluggable notion of state, state type, primitives, and assignment of types and elements of the underlying effect quantale to primitives. The details of the parameterization are somewhat intricate (though orthogonal to the main contributions of this paper, and explained carefully in [Gordon 2017]), but the high points should have been here in this paper.

Review #120C

Overall merit

D. Strong Reject

Reviewer expertise

Y. Knowledgeable

Paper summary

Many effect type systems in the literature conservatively approximate the set of effects that may happen when a computation is run. Sequential effect type systems aim to additionally capture the order in which effects may occur. This paper strives to extend existing work on sequential effect typing to account for first-class control operators.

Strengths

• interesting problem

Weaknesses

• poor presentation makes it painful to read the paper

Comments for author

I found the paper to be reasonably well-motivated, and technically it may be sound, but because the presentation is so poor I did not make it to the end. There are large blocks of sometimes vague and overly-verbose text interspersed with rather inscrutable figures whose meaning can only be discerned by reading several chunks of rather disconnected text.

Given that this is a PC paper it must be held to higher standards, and as such I'm unwilling to waste as much time wrestling with it as as I might a poorly presented non-PC paper.

To be fair, it starts and finishes well. It's the technical part in the middle (particularly Sections 3 and 4) that needs a lot of work to make it readable. Where I really started to get lost was when trying to follow Figure 2 and the accompanying text.

I think the paper can be drastically improved by first running through a collection of small but representative examples, before presenting the technical details. Overall it needs to be much more structured and the text needs to be made a lot crisper and more concise. The figures contain too much information in one place that is not remotely self-contained.

l166--l167: The nilpotency of top seems quite restrictive. Can you give an example of how top is used? It is used as a means of rejecting certain improper combinations of effects. For example, an effect system enforcing that certain operations occur in a certain order (say, ABC repeatedly) would give the sequencing of A and C directly effect top. It is also propagated by the iteration operator: iterating an effect that indicates lock acquisition yields top, because if we repeat a lock acquisition an arbitrary number of times we don't know how many times to release it.

l169: I recommend you follow Knuth's advice and never begin a sentence with a symbol.

l224: "lense"

2.2:

• It would be kind to the reader to spell out the syntax before you introduce a semantics.

• It would also be nice if you'd explain basic features of the semantics such as what $\sigma$ stands for. Just referring to Flatt et al.'s paper is insufficient.

• There seems to be little point in including call/comp in the evaluation contexts given that you don't include its semantics and say in the text that you defer its treatment to later. As noted in response to Reviewer B, this has been insisted upon by several prior reviewers.

l287: "For now, ignore..." This is a warning sign that there's something wrong with your presentation. You can maybe get away with something like this once, but it continues and gets much worse later in the paper.

l356: This example is poorly explained. You should describe the full effect of this code.

l361: "ellided"

l436--l440: I found the sequence of quoted terms that are apparently aimed at providing intuition for the meaning of a continuation effect entirely unenlightening.

Figure 2: The box syntax is rather distracting, and even more so when it appears in a figure with nested boxes!

I agree this is not ideal, but the alternative is to make the syntax more verbose (a prior version appended "until t" in place of solid boxes, which made things much harder to parse). On the other hand, it's possible I'm over-accustomed to it from reading recent program logic papers that make heavy use of this style of notation for shared invariants.

l480: Which other components?

l510: "Initially, readers may assume" is another warning sign that there's something wrong with the presentation