Fossacs 2018 author response

gistfile1.txt

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).