intro edits

jfp-paper/jfp-gtt.tex

@@ -25,13 +25,13 @@
 
 \title{Gradual Type Theory}
 
-\author[M.S. New, D.R. Licata and Amal Ahmed]
+\author[M.S. New, D.R. Licata and A. Ahmed]
        {Max S. New\\
         Northeastern University\\
         %% \email{maxnew@ccs.neu.edu}
        }
 
-\author[M.S. New, D.R. Licata and Amal Ahmed]
+\author[M.S. New, D.R. Licata and A. Ahmed]
        {Daniel R. Licata \\
         Wesleyan University\\
         %% \email{drlicata@wesleyan.edu}
@@ -58,14 +58,13 @@
 \begin{abstract}
   Gradually typed languages are designed to support both dynamically typed
   and statically typed programming styles while preserving the benefits of
-  each.  While existing gradual type soundness theorems for these
-  languages aim to show that type-based reasoning is preserved when
-  moving from the fully static setting to a gradual one, these theorems do
-  not imply that correctness of type-based refactorings and optimizations
-  is preserved.  Establishing correctness of program transformations is
-  technically difficult, because it requires reasoning about program
-  equivalence, and is often neglected in the metatheory of gradual
-  languages.  
+  each.  These languages come with gradual type soundness theorems that aim to 
+  show that type-based reasoning is preserved when moving from the fully static
+  setting to a gradual one.  Unfortunately, these theorems do not guarantee that
+  the correctness of type-based refactorings and optimizations is preserved. 
+  Establishing correctness of program transformations is technically difficult,
+  because it requires reasoning about program equivalence, and is often
+  neglected in the metatheory of gradual languages.  
 
   In this paper, we propose an \emph{axiomatic} account of
   program equivalence in a gradual cast calculus, which we formalize in a
@@ -75,12 +74,14 @@
   prove many theorems that justify optimizations and refactorings in
   gradually typed languages. For example, 
   \emph{uniqueness principles} for gradual type connectives show that if the
-  $\beta\eta$ laws hold for a connective, then casts between that
+  $\beta\eta$ laws hold for a connective, then casts to or from that
   connective must be equivalent to the so-called ``lazy'' cast semantics.
   Contrapositively, this shows that ``eager'' cast semantics violates the
   extensionality of function types.  As another example, we show that
   gradual upcasts are pure functions and, dually, gradual downcasts are
-  strict functions.  We show the consistency and applicability of our
+  strict functions.  
+
+  We show the consistency and applicability of our
   axiomatic theory by proving that a contract-based implementation using
   the lazy cast semantics gives a logical relations model of our type
   theory, where equivalence in GTT implies contextual equivalence of the
@@ -109,7 +110,7 @@ enable compiler optimizations, and underlie formal software verification.
 The difficulty is accommodating both of these styles and their benefits simultaneously:
 allowing the dynamic and static code to interact without forcing the
 dynamic code to be statically checked or violating the correctness of
-type-based reasoning.
+type-based reasoning in static code.
 
 The linchpin to the design of a gradually typed language is the
 semantics of \emph{runtime type casts}.  These are runtime checks that ensure
@@ -122,7 +123,7 @@ the language runtime must check if $x$ is a number, and otherwise
 raise a dynamic type error.
 %
 A programmer familiar with dynamically typed programming might object
-that this is overly strong: for instance if $f$ is just a constant
+that this is overly strong: for instance, if $f$ is just a constant
 function $f = \lambda x:\texttt{Num}. 0$ then why bother checking if
 $x$ is a number since the body of the program does not seem to depend
 on it?
@@ -149,7 +150,8 @@ programs: the two closures $\lambda x:\texttt{Num}. 0$ and $\lambda
 x:\texttt{Num}. x - x$ are indistinguishable to any other program in
 the language.
 %
-This is precisely the difference between gradual typing and so-called
+
+The above is precisely the difference between gradual typing and so-called
 \emph{optional} typing: in an optionally typed language (Hack,
 TypeScript, Flow), annotations are checked for consistency but are unreliable
 to the user, so provide no leverage for reasoning.  
@@ -186,12 +188,12 @@ The extent to which these different semantics have been shown to
 validate type-based reasoning has been limited to syntactic type
 soundness and blame soundness theorems.
 %
-In their strongest form, these theorems say ``If $t$ is a closed
-program of type $A$ then it diverges, or reduces to a runtime error
-blaming dynamically typed code, or reduces to a value that satisfies $A$ to a
-certain extent.''
+In their strongest form, these theorems say: 
+``If $t$ is a closed program of type $A$ then it diverges,
+   or reduces to a runtime error blaming dynamically typed code, or reduces to
+   a value that satisfies $A$ to a certain extent.''
 %
-However, the theorem at this level of generality is quite weak, and
+However, the theorem at this level of generality is quite weak, and 
 justifies almost no program equivalences without more information.
 %
 Saying that a resulting value satisfies type $A$ might be a strong
@@ -205,14 +207,17 @@ the language being defined.
 %% programs cannot go wrong'' depends on putting in an error outcome, and
 %% then ruling it out for typed programs).
 %
+
 We argue that these type soundness theorems are only indirectly
 expressing the actual desired properties of the gradual language,
 which are \emph{program equivalences in the typed portion of the code} that are
-not valid in the dynamically typed portion. 
+not valid in the dynamically typed portion.  
 
-Such program equivalences typically include $\beta$-like principles,
-which arise from computation steps, as well as \emph{$\eta$ equalities},
-which express the uniqueness or universality of certain constructions.
+But what are there program equivalences that hold in statically typed portions
+of the code but not in dynamically typed portions?  They typically include
+$\beta$-like principles, which arise from computation steps, as well as
+\emph{$\eta$ equalities}, which express the uniqueness or universality of
+certain constructions. 
 %% The reader unfamiliar with proof theory may find the centrality of
 %% $\eta$ equalities in our development unusual.  
 %
@@ -220,7 +225,7 @@ which express the uniqueness or universality of certain constructions.
 The $\eta$ law of the untyped $\lambda$-calculus, which
 states that any $\lambda$-term $M \equiv \lambda x. M x$, is
 restricted in a typed language to only hold for terms of function type $M
-: A \to B$ ($\lambda$ is the unique/universal way of making an element
+: A \to B$ (i.e., $\lambda$ is the unique/universal way of making an element 
 of the function type).  
 %
 This famously ``fails'' to hold in call-by-value languages in the
@@ -233,7 +238,8 @@ simple call-by-value languages\footnote{This does not hold in languages
   equality. We discuss the applicability of our main results more generally in Section \ref{sec:related}.} (e.g. SML) if we have a ``value
 restriction'' $V \equiv \lambda x. V x$.
 %
-This illustrates that $\eta$/extensionality rules must be stated for
+
+The above illustrates that $\eta$/extensionality rules must be stated for
 each type connective, and be sensitive to the effects/evaluation order
 of the terms involved.
 %
@@ -266,7 +272,7 @@ principle which enables similar reasoning, such as proofs by induction.
 The $\eta$ principles for lazy types \emph{in call-by-name} support dual
 behavioral reasoning about lazy functions, records, and streams.
 
-\textbf{An Axiomatic Approach to Gradual Typing.}
+\subsection{An Axiomatic Approach to Gradual Typing.}
 In this paper, we systematically study questions of program equivalence
 for a class of gradually typed languages by working in an
 \emph{axiomatic theory} of gradual program equivalence, a language and
@@ -10138,11 +10144,11 @@ structure~\cite{ahman+16fiberedeffects}.
 
 \paragraph{Acknowledgments}
 We thank Ron Garcia, Kenji Maillard and Gabriel Scherer for helpful
-discussions about this work. We thank the anonymous reviewers for
+discussions about this work. We thank the anonymous POPL 2019 reviewers for
 helpful feedback on this article. This material is based on research
-sponsored by the National Science Foundation under grant CCF-1453796
-and the United States Air Force Research Laboratory under agreement
-number FA9550-15-1-0053 and FA9550-16-1-0292.
+sponsored by the National Science Foundation under grants CCF-1910522,
+CCF-1816837, CCF-1453796 and the United States Air Force Research Laboratory
+under agreement number FA9550-15-1-0053 and FA9550-16-1-0292.
 %% The U.S. Government is
 %% authorized to reproduce and distribute reprints for Governmental
 %% purposes notwithstanding any copyright notation thereon.