From 13031b747b88d6d1f368bed3c070c4c68680e78f Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 29 Oct 2018 16:00:25 -0400
Subject: [PATCH] rewrite agt and gradualizer comparison

---
 paper/gtt.tex | 91 ++++++++++++++++++++++++---------------------------
 1 file changed, 42 insertions(+), 49 deletions(-)

diff --git a/paper/gtt.tex b/paper/gtt.tex
index 2ac5411..1d381bb 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -479,7 +479,7 @@ $\dyn$ and then down to $B$: $\obcast{B}{\dyn}\obcast{\dyn}{A} t$.
 %
 These casts often have quite different performance characteristics,
 but should have the same extensional behavior: of the cast semantics
-presented in \cite{siek+09designspace}, only the partially eager
+presented in \citet{siek+09designspace}, only the partially eager
 detection strategy violates this principle, and this strategy is not
 common.
 %
@@ -682,10 +682,10 @@ The $\eta$ principles for lazy types \emph{in call-by-name} support dual
 behavioral reasoning about lazy functions, records, and streams.
 
 \textbf{Overview of GTT.}  This paper unifies two strands of previous
-work.  The first~\cite{newahmed18} develops operational (logical
+work.  The first~\citep{newahmed18} develops operational (logical
 relations) reasoning for gradual typing in a call-by-value setting, but
 does not develop an axiomatic proof theory for it.  The
-second~\cite{newlicata2018-fscd} develops an axiomatic gradual type
+second~\citep{newlicata2018-fscd} develops an axiomatic gradual type
 theory, but for only function and pair types in call-by-name (whereas
 all existing gradual languages are call-by-value), and gives
 denotational but not operational models of the axioms.
@@ -852,9 +852,9 @@ The main contributions of the paper are as follows.
 \end{enumerate}
 
 \begin{shortonly}
-\textbf{Extended version:} As supplementary materials, we attach an
-extended version of the paper, which has omitted cases of definitions,
-lemmas, and proofs.  
+\textbf{Extended version:} An extended version of the paper, which
+includes the omitted cases of definitions, lemmas, and proofs is
+available as \citet{newlicataahmed19:extended}.
 \end{shortonly}
 
 % While gradual typing has been researched quite extensively by proving
@@ -9474,7 +9474,7 @@ equivalences can only be achieved by certain cast semantics.
 
 \citet{Degen2012TheIO} give an analysis of different cast semantics
 for contracts in lazy languages, specifically based on Haskell, so
-call-by-need with \texttt{seq}.
+call-by-need with \seq.
 %
 They propose two properties ``meaning preservation'' and
 ``completeness'' that they show are incompatible and identify which
@@ -9539,48 +9539,41 @@ coercion calculus.
 \paragraph{Gradual Typing Frameworks}
 \fi
 
-Our approach to systematically producing a gradual type theory from a
-type theory by adding dynamic types, casts and dynamism orderings is
-similar in spirit to ``frameworks'' for gradual typing, specifically
-AGT \cite{AGT} and the Gradualizer \cite{gradualizer16,gradualizer17}.
-%
-These two frameworks systematically produce a gradual language from a
-statically typed language, and both produce a surface language with a
-type system, whereas we consider only the inequational theory of
-intrinsically typed terms of a cast calculus.
-%
-The major point of departure for this work is that both AGT and the
-Gradualizer are based on the \emph{operational semantics} of the
-statically typed language, whereas our approach is to ``gradualize''
-the axiomatic semantics of the typed language.
-%
-This means our approach accomplishes something quite different: their
-frameworks produce specific implementations, whereas GTT axiomatizes
-the commonalities across different implementations.
-% AA: Perhaps the above point should also be made in the intro. 
-Furthermore, while both the AGT and Gradualizer approaches prove various
-gradual typing correctness theorems by construction (gradual type
-safety, conservativity, gradual guarantee), neither considers the
-program equivalences that we argued are the raison d'\^etre of gradual
-typing in the first place.
-%
-In fact, both systems \emph{fail} to preserve these equivalences.
-%
-AGT reproduces the ``eager'' semantics of function casts,
-breaking $\eta$ for functions.
-%
-Gradualizer produces the ``lazy'' semantics and thus should validate the
-$\eta$ equality, though this does not seem to be a central component of
-the language: a different version could produce the ``eager'' semantics
-and satisfy all of their criteria.
-%
-Both systems, however, fail to preserve the program equivalences of
-parametric polymorphism, and in addition fail to meet gradual typing
-criteria for stateful references.
-%
-The ``reason'' that these violations occur is that they are not safety
-properties of the operational semantics, which is the only input to
-these frameworks.
+In this work we have applied a method of ``gradualizing'' axiomatic
+type theories by adding in dynamism orderings and adding dynamic
+types, casts and errors by axioms related to the dynamism orderings.
+%
+This is similar in spirit to two recent frameworks for designing
+gradual languages: Abstracting Gradual Typing (AGT) \citep{AGT} and the
+Gradualizer \citep{gradualizer16,gradualizer17}.
+%
+All of these approaches start with a typed language and construct a
+related gradual language.
+%
+A major difference between our approach and those is that our work is
+based on axiomatic semantics and so we take into account the equality
+principles of the typed language, whereas Gradualizer is based on the
+typing and operational semantics and AGT is based on the type safety
+proof of the typed language.
+%
+Furthermore, our approach produces not just a single language, but
+also an axiomatization of the structure of gradual typing and so we
+can prove results about many languages by proving theorems in GTT.
+%
+The downside to this is that our approach doesn't directly provide an
+operational semantics for the gradual language, whereas for AGT this
+is a semi-mechanical process and for Gradualizer, completely
+automated.
+%
+Finally, we note that AGT produces the ``eager'' semantics for
+function types, and it is not clear how to modify the AGT methodology
+to reproduce the lazy semantics that GTT provides.
+%
+More generally, both AGT and the Gradualizer are known to produce
+violations of parametricity when applied to polymorphic languages,
+with the explanation being that the parametricity property is in no
+way encoded in the input to the systems: the operational semantics and
+the type safety proof.
 %
 In future work, we plan to apply our axiomatic approach to gradualizing
 polymorphism and state by starting with the rich \emph{relational logics
-- 
GitLab