From c573a92bef6374a3745a71aabc0776f4e86e36c4 Mon Sep 17 00:00:00 2001
From: Amal Ahmed <amal@ccs.neu.edu>
Date: Fri, 31 Jan 2020 13:30:23 -0500
Subject: [PATCH] intro edits

---
 jfp-paper/jfp-gtt.tex | 94 +++++++++++++++++++++++++++----------------
 1 file changed, 60 insertions(+), 34 deletions(-)

diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index dbf0c01..9d965a5 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -185,8 +185,8 @@ a function until it is called (and there are other possibilities, see
 e.g.  \cite{siek+09designspace,greenberg15spaceefficient}).
 %
 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.
+validate type-based reasoning has been limited to syntactic \emph{gradual type 
+soundness} and \emph{blame soundness} theorems.
 %
 In their strongest form, these theorems say: 
 ``If $t$ is a closed program of type $A$ then it diverges,
@@ -208,12 +208,20 @@ the language being defined.
 %% then ruling it out for typed programs).
 %
 
-We argue that these type soundness theorems are only indirectly
+\paragraph{Beyond Gradual Type Soundness: Preserving Typed Equivalence}
+We argue that existing gradual 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.  
-
-But what are there program equivalences that hold in statically typed portions
+not valid in the dynamically typed portion.  These typed equivalences are
+essential for ensuring that any reasoning about refactoring or optimization of
+code that is valid in a fully static setting is also valid for statically typed
+portions of a gradually typed program.  Thus, preserving appropriate typed
+equivalences---the ones that justify refactoring and optimization---should be one
+of the criteria that gradually typed languages should satisfy. 
+% However, reasoning about program equivalence is technically difficult and is
+% often neglected in the metatheory of gradual languages. 
+
+So what are the 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
@@ -222,6 +230,8 @@ certain constructions.
 %% $\eta$ equalities in our development unusual.  
 %
 %%Of course,
+
+\paragraph{$\eta$ Laws and their Significance.}
 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
@@ -246,10 +256,12 @@ of the terms involved.
 For instance, the $\eta$ principle for the boolean type $\texttt{Bool}$
 \emph{in call-by-value} is that for any term $M$ with a free variable $x :
 \texttt{Bool}$, $M$ is equivalent to a term that performs an if
-statement on $x$: $M \equiv \kw{if} x (M[\texttt{true}/x])
-(M[\texttt{false}/x])$.
-%
-If we have an \texttt{if} form that is strongly typed (i.e., errors on
+statement on $x$: 
+
+\[ M \equiv \kw{if} x (M[\texttt{true}/x]) (M[\texttt{false}/x]).
+\]
+
+\noindent If we have an \texttt{if} form that is strongly typed (i.e., errors on
 non-booleans) then this tells us that it is \emph{safe} to run an if
 statement on any input of boolean type (in CBN, by contrast an if
 statement forces a thunk and so is not necessarily safe).
@@ -258,21 +270,29 @@ In addition, even if our \texttt{if} statement does some kind of
 coercion, this tells us that the term $M$ only cares about whether $x$
 is ``truthy'' or ``falsy'' and so a client is free to change e.g. one
 truthy value to a different one without changing behavior.
-%
+
 This $\eta$ principle justifies a number of program optimizations,
 such as dead-code and common subexpression elimination, and 
 hoisting an if
-statement outside of the body of a function if it is well-scoped
-($\lambda x. \kw{if} y \, M \, N \equiv \kw {if} y \, (\lambda x.M) \, (\lambda x.N)$).
+statement outside of the body of a function if it is well-scoped: 
+
+\[ \lambda x. \kw{if} y \, M \, N \equiv \kw {if} y \, (\lambda x.M) \, (\lambda
+x.N).
+\]
+
 %
-Any eager datatype, one whose elimination form is given by pattern
+\noindent Any eager datatype, one whose elimination form is given by pattern
 matching such as $0, +, 1, \times, \mathtt{list}$, has a similar $\eta$
 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.
 
-\subsection{An Axiomatic Approach to Gradual Typing.}
+Besides seeing $\eta$ laws are important for type-directed optimizations,
+but intuitively, in a gradually typed language
+FOO
+
+\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
@@ -292,9 +312,9 @@ provable equivalences/approximations.
 Due to its type-theoretic design, different axioms of program
 equivalence are easily added or removed.
 %
-Gradual type theory can be used both to explore language design questions and
-to verify behavioral properties of specific programs, such as correctness of
-optimizations and refactorings.
+The critical benefit of gradual type theory (GTT) is that it can be used both to
+explore language design questions and to verify behavioral properties of
+specific programs, such as correctness of optimizations and refactorings. 
 
 To get off the ground, we take two properties of the gradual language
 for granted.
@@ -309,7 +329,7 @@ but should have the same extensional behavior: of the cast semantics
 presented in \citet{siek+09designspace}, only the partially eager
 detection strategy violates this principle, and this strategy is not
 common.
-%
+
 The second property we take for granted is that the language satisfies
 the \emph{dynamic gradual guarantee}~\cite{refined} (``graduality'')---a
 strong correctness theorem of gradual typing--- which constrains how
@@ -369,7 +389,7 @@ not change.
 %% those systems by restricting GTT to only include the image of those
 %% embeddings.
 
-We then study what program equivalences are provable in GTT under
+Next, we study what program equivalences are provable in GTT under
 various assumptions.
 %
 Our central application is to study when the $\beta, \eta$ equalities
@@ -461,12 +481,12 @@ very type-based reasoning that gradual typing should provide.
 
 While criticisms of transient semantics on the basis of type soundness
 have been made before \citep{greenmanfelleisen:2018}, our development
-shows that the $\eta$ principles of types are enough to uniquely
+shows that the $\eta$ principles of types are enough to \emph{uniquely}
 determine a cast semantics, and helps clarify the trade-off between
 eager and lazy semantics of function casts.
 
-\textbf{Technical Overview of GTT.}  The gradual type theory developed
-in this paper unifies our previous work on
+\subsection{Technical Overview of GTT}  
+The gradual type theory developed in this paper unifies our previous work on
 operational (logical relations) reasoning for gradual typing in a
 call-by-value setting~\citep{newahmed18} (which did not consider a proof theory), and on an
 axiomatic proof theory for gradual typing~\citep{newlicata2018-fscd} in
@@ -493,15 +513,16 @@ call-by-push-value gradually typed languages.
 In the prior work \cite{newlicata2018-fscd,newahmed18}, gradual type
 casts are decomposed into upcasts and downcasts, as suggested above.
 %
-A \emph{type dynamism}
-relation (corresponding to type precision~\cite{refined} and na\"ive
-subtyping~\cite{wadler-findler09}) controls which casts exist: a type
-dynamism $A \ltdyn A'$ induces an upcast from $A$ to $A'$ and a downcast
-from $A'$ to $A$.  Then, a \emph{term dynamism} judgement is used for
-equational/approximational reasoning about programs.  Term dynamism
-relates two terms whose types are related by type dynamism, and the
+A \emph{type precision}
+relation $A \ltdyn A'$ (read: $A$ is more precise than $A'$, as in
+~\citet{refined} and na\"ive subtyping~\cite{wadler-findler09}) 
+controls which casts exist: a type 
+precision $A \ltdyn A'$ induces an upcast from $A$ to $A'$ and a downcast
+from $A'$ to $A$.  Then, a \emph{term precision} judgement is used for
+equational/approximational reasoning about programs.  Term precision
+relates two terms whose types are related by type precision, and the
 upcasts and downcasts are each \emph{specified} by certain term
-dynamism judgements holding.
+precision judgements holding.
 %
 This specification axiomatizes only the properties of casts needed to
 ensure the graduality theorem, and not their precise behavior, so cast
@@ -529,7 +550,9 @@ call-by-push-value, which corresponds to a behavioral property of
 \emph{thunkability} and
 \emph{linearity}~\cite{munchmaccagnoni14nonassociative}.  We argue in
 Section~\ref{sec:related} that this property is related to blame
-soundness.  Our gradual type theory naturally has two dynamic types, a
+soundness.  
+
+Our gradual type theory naturally has two dynamic types, a
 dynamic eager/value type and a dynamic lazy/computation type, where the
 former can be thought of as a sum of all possible values, and the latter
 as a product of all possible behaviors.  At the language design level,
@@ -546,7 +569,7 @@ correctness of specific programs.
 %% have ``shifted'' computation types (functions), while call-by-name
 %% languages do have ``shifted'' value types (datatypes), and in the mixed
 %% setting the properties of these types are clearer.
-\textbf{Contract-Based Models.}
+\subsection{Contract-Based Models}
 To show the consistency of GTT as a theory, and to give a concrete
 operational interpretation of its axioms and rules, we provide a
 concrete model based on an operational semantics.
@@ -594,7 +617,7 @@ functions.
 Our modular proof architecture allows us to easily prove correctness
 of $\beta, \eta$ and graduality for all of these interpretations.
 
-\textbf{Contributions.}
+\subsection{Contributions.}
 The main contributions of the paper are as follows.
 \begin{enumerate}
 \item We present Gradual Type Theory in Section \ref{sec:gtt}, a simple
@@ -637,6 +660,8 @@ The main contributions of the paper are as follows.
 \textbf{Extended version:} An extended version of the paper, which
 includes the omitted cases of definitions, lemmas, and proofs is
 available in \citet{newlicataahmed19:extended}.
+
+TODO: Compared to our previous paper on GTT \cite{newlicataahmed19}, we extend
 \end{shortonly}
 
 % While gradual typing has been researched quite extensively by proving
@@ -10110,6 +10135,7 @@ policies or endorsements, either expressed or implied, of the United
 States Air Force Research Laboratory, the U.S. Government, or Carnegie
 Mellon University.
 
+
 \bibliographystyle{jfp}
 \bibliography{max}
 
-- 
GitLab