Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- We thank the reviewers for their work on our article and their
- detailed feedback.
- We wish to first address the two main points raised by the reviewers:
- A. The (informal and technical) meaning of the main result, the Full
- Abstraction theorem for the embedding of U into UL.
- B. The choice of paper structure given the page limits (and in
- particular the question of what presentation would make sense in
- absence of appendices).
- Then we will comment on some more local points raised by the review --
- feel free to skip this latter part.
- # Main questions
- A) The Full Abstraction result
- We made the mistake of using the "short" notation of equivalences, (e
- \simeq e'), used when the context and types are evident from the usage
- context, in Definition 1 and Definition 2, and the "long" notation of
- equivalences, (Gamma |- e \simeq e' : sigma), in Theorem 2. Theorem
- 2 is meant to state that if (e, e') are equivalent in the sense of
- Definition 1, then they are also equivalent in the sense of Definition
- 2. We thank reviewer 1 for noticing this unnecessary confusion, and
- will change the article to consistently use the long notation. Below
- is a longer explanation of the result of Theorem 1 -- feel free to
- skip it if the question was only on a notational level.
- Suppose a user is writing a fragment of program in U as part of
- a complete UL program. For example, maybe some of the library
- functions that they are calling are actually implemented in L (through
- a UL(..) boundary); library functions formally correspond to "free
- variables" in an open program. Suppose also that the user performs
- equational reasoning on their program fragment (for example, wondering
- if a given refactoring is correct) by thinking about
- indistinguishability: two fragments are "equivalent" if there is no
- way to use them in a program and observe a difference between the
- two. Finally, suppose that the user is only thinking about
- indistinguishability in U (maybe they do not actually know L). Then,
- our Full Abstraction theorem states that the equational reasoning they
- perform is in fact valid in the whole program UL: if they conclude
- that two fragments are equivalent as U terms (without thinking about
- L), they remain equivalent as UL terms. In other words, adding L code
- (reimplementing functions in L instead of U, for example) cannot break
- the expectations of U users -- in terms of equational reasoning at
- least.
- ¹: it is also the case that if two U terms are *distinguishable* as
- U programs (inequivalent), then they are distinguishable in UL. This
- is a much simpler result, coming from the fact that the execution
- behavior of pure-U programs is unchanged in UL -- a direct property of
- the way UL was constructed.
- "Indistinguishability", that is contextual equivalence, of U program
- fragments is formally defined with respect to whole-programs in U and
- in UL in Definitions 1 and 2 (we elaborate on these definitions below
- in our specific response to Review 1), and the theorem formally states
- that contextual equivalence in U implies contextual equivalent in UL.
- Note that "adding L to U preserves equational reasoning" may seem like
- a very limited formal statement (what about other forms of
- reasoning?), but that in our experience working with Full Abstraction
- in other contexts, it actually captures a lot of other "expectation
- preservation" properties that we don't know very well how to state
- formally -- a lot of the expectations that users have regarding
- program behaviors can be rephrased as equivalence quizzes "are the
- fragments X and Y indistinguishable?".
- B) The structure of the paper
- We have indeed found it challenging to present our work in the page
- limits requested for Fossacs submissions. It is not clear to us how
- much of the responsibility lies in the scientific work itself, in the
- choices of presentation, and in the choice of Fossacs space limits
- which are exactly twice smaller than most other conferences in our
- domain.
- We think of our work as presenting two distinct contributions:
- - a conceptual contribution, drawing attention to the question of
- usable designs for multi-language programs (by discussing the
- context and examples), and proposing a *formal* specification for
- a class of "adding language L to the system does not break user
- expectations"
- - a technical contribution, instantiating the conceptual proposal
- above by designing the language L, showing (through examples) that
- it is a useful side-kick to a typical ML-family programming language
- U, doing a metatheory of L and of UL together, and proving that they
- respect the formal specification (Full Abstraction).
- The conceptual contribution takes only 2 pages, and we are reluctant
- to shorten it more: the contexts and explanation are the part of this
- work that could inspire others to reuse our proposed formal
- criterion -- our goal in publishing this work.
- In the technical contribution, we have made the choice to delegate the
- technical proofs to the appendices, which Reviewer 1 apparently found
- problematic. We consider that the proof technique is not the main
- contribution of this work (it is not particularly technically
- challenging); we are happy to give access to a long preprint of this
- work with appendices (we already have a preprint on arXiv) for others
- to check our formal developments and reuse them in necessary, but we
- had decided to rather devote our exposition space to informal
- explanations of the language design of L, and the way UL is
- constructed from U and L (Reviewer 1 found this Section 3 confusing,
- possibly out of terseness).
- Review 2 asks what a final version of this work, without Appendices,
- would look like. Our base plan was to have something like the current
- submission, with Appendices omitted (and without references to them in
- the main document). We warmly welcome any suggestion on main-body
- content that could be moved out, or appendix-content that we should
- really try to include.
- Let us just review quickly the choices that were made for appendix
- content in the submission (feel free to skip that part):
- A. Quicksort, which takes a lot of space and has the "red wall"
- effect. We don't think this is essential content -- it was there to
- demonstrate use-cases of L, but we can rely on our reader's
- imagination instead.
- B. Internal syntax and typing. While this section is of interest to
- people designing languages with linear types, we think that users
- of the language or readers of the paper can skip it, as it can be
- summarized by "It is possible to show subject reduction for L."
- C. Reduction of Internal Terms. (With apologies for the macro mistake
- in the submission...). The most interesting part of this section
- are the reduction rules for linear memory operations (new/free,
- box/unbox), and the operational semantics of "copy". We will
- consider adding them to the main manuscript.
- D, E: static and dynamic semantics of UL. We could include an excerpt
- the type correspondence rules in the main manuscript (for example
- lump, product, function and bang), and the corresponding value
- correspondence rules (the function rules, which have to perform an
- eta-expansion, are interesting).
- F. The full abstraction proof. We are of the opinion that the proof
- itself needs not be include in the short conference presentation of
- this work (it is not as interesting or original than the rest of
- the work), but welcome further feedback from the reviewers.
- G and I. Parametricity, and the logical relation. The parametricity
- relation was built to substantiate, formally, the informal claim
- that the interaction between explicit lump types and type variables
- was a design improvement over previous multi-language designs
- (Perconti and Ahmed, 2014). This is an interesting result that
- required some amount of proving work but, in view of the space
- restrictions, we would not include it in the main article -- this
- is an unfortunate but classic case of removing scientific content
- to fit presentation constraints.
- H. Hybrid program examples. We have no space in the main article for
- further examples, and we hope that the hope remains readable
- without them.
- # Other questions
- ## Review 1
- > - Section 3.3. What is the intuition behind Definition 1 and
- > Definition 2?
- Contextual equivalence is a standard way to define a notion of
- equivalence of open term (with free/unbound variables) from a notion
- of equivalence on closed term at "ground" types in which equivalence
- is easy to define.
- (Typically, for a total language with only strongly terminating
- program, equivalence at closed program of boolean type is easy to
- define (they both return (true) or both return (false)). For
- a non-terminating language, termination properties must also be
- considered. For a language with input/output, the trace of
- user-observable actions during program execution must also be
- considered. These also correspond to natural choices of denotational
- semantics for these languages.)
- Consider a fixed language and an equivalence relation
- \emptyset |- t \simeq t' : tau
- where (tau) belong to a class of "ground" types for which equivalence is
- easy to define. Then contextual equivalence of two open terms
- (Gamma |- e : sigma) and (Gamma |- e' : sigma)
- is defined by:
- for any context (C) such as (C[e], C[e']) are closed terms at
- a ground type (tau), we have the closed program equivalence
- (\emptyset |- C[e] \simeq C[e'] : tau)
- In definition 1, the "language" considered is just U, and the
- equivalence on closed terms is: two terms at unit type are equivalent
- if they are equi-terminating.
- This closed-program equivalence is a standard choice, which is
- equivalent to taking, for example, the boolean type as ground, and
- asking that the two programs either both diverge or return the same
- boolean value -- consider the contexts
- (if {hole} then () else {infinite loop}) and
- (if {hole} then {infinite loop} else ()).
- In definition 2, the "language" considered is UL, and the notion of
- closed program equivalence is similar. For UL, we could consider
- comparing either two blue terms or two red terms (all terms have
- alternating layers of blue and red, but they either start with blue
- constructs or with red constructs), and having contexts that return
- either blue ground types or red ground types. But for the purpose of
- stating the full abstraction result, only the equivalence of blue
- terms matters.
- > - Section 3.3. In the sequents of Theorem 2 you use a notation that
- > has not been defined (the equivalence of e and e' typed by \sigma)
- Theorem 2 states that if two open U programs (e, e') are equivalent in
- the sense of Definition 1, then they are also equivalent in the sense
- of Definition 2.
- ## Review 2
- > Fig. 10 I am missing somewhere an stated invariant like
- >
- > if e : σ then ⟦e⟧ : ⟦σ⟧
- >
- > which I suppose is intended.
- Yes, and also for contexts -- the type of the hole also gets
- translated in the expected way. Thanks for pointing this out (and for
- the many other careful, very helpful comments).
Add Comment
Please, Sign In to add comment