Reynolds overplayed?

[dvanhorn]

The story of pushdown a la Reynolds is pleasant in this one particular instance, but it's not clear if that persists given a language with more sophisticated control. Reynolds specifically points out two different metalanguages that yield different interpreter semantics, but here there is but one, with no other control feature inherited. If say call/cc were added to the interpreter and implemented using call/cc, how would that compare to using abstract-machine-based AAM to attempt pushdown analysis of such a language? In short, the pleasant surprise is pleasant but possibly overemphasized in the story.

The call/cc question is something to consider, but rewriting for the control monad would destroy the reliance on the meta-interpreter stack. (That observation is probably worth making in the paper.)

IMO: The Reynolds thing is (a) important and (b) only occupies one short section of the paper.

Perhaps the solution is to acknowledge how much is not inherited from the meta-language: memory, GC, state, etc. and it's hard to imagine how these things could be inherited in an abstract interpreter. The reviewer is right that it's a delicate thing to relying on the meta-stack, but it's still pretty amazing that you can.

[labichn]

This is one of the points I think we should address in depth. My thought when I read this yesterday is that the control operator call/cc (and any other desired control operators) can be modeled as a monadic effect, regardless of the choice of implementation language. If a particular stack implements call/cc, any object-language semantics may use the effect to implement any desired behavior, including an object-language-level call/cc. Each new monad transformer stack gives rise to a new host semantics, exposing some set of effects and behavior from which any object-language semantics may inherit. Is it wrong to call this a new meta-language?

We do lose the correspondence between the Racket stack and the object-language stack with a ContT stuck in, but I think this is true with any non-trivial transformer stuck in (e.g. ListT). And we'll certainly still capture the same object-level semantics as an AAM-style analysis.

[davdar]

This is an interesting idea. My first reaction was "we would have to rework the caching algorithm to accommodate having ContT in the transformer stack"... but maybe we don't! Might be worth playing around with to see if this is true or not. If it is true (no reworking necessary), we can state this in the response and back it up. If it isn't true (reworking is necessary), we can state this as well, and say this is a sensible limitation of our current caching algorithm.

[labichn]

I can confirm no reworking is necessary, both for ContT and CCT (delimited control).

[dvanhorn]

I'm closing this since we renamed the paper as a major step toward de-emphasizing. This stuff about control operators can be examined in an extended version of the paper if you're still interested.