From 78d72e9c5d1ee254348e9fcd9571c4422e00eb98 Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Tue, 30 Oct 2018 00:30:58 -0400
Subject: [PATCH] add references to rule names in text

---
 paper/gtt.tex | 110 ++++++++++++++++++++++++++------------------------
 1 file changed, 58 insertions(+), 52 deletions(-)

diff --git a/paper/gtt.tex b/paper/gtt.tex
index e7541a8..f0e16ed 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1457,7 +1457,7 @@ types will arise from type dynamism and casts.
 The \emph{type dynamism} relation of gradual type theory is written $A
 \ltdyn A'$ and read as ``$A$ is less dynamic than $A'$''; intuitively,
 this means that $A'$ supports more behaviors than $A$.
-\citet{newahmed18,newlicata2018-fscd} analyze this as the existence of an \emph{upcast}
+Our previous work~\citep{newahmed18,newlicata2018-fscd} analyzes this as the existence of an \emph{upcast}
 from $A$ to $A'$ and a downcast from $A'$ to $A$ which form an
 embedding-projection pair (\emph{ep pair}) for term error approximation
 (an ordering where runtime errors are minimal): the upcast followed by the
@@ -1479,15 +1479,18 @@ Section~\ref{sec:dynamic-type-interp}.
 This extends in a straightforward way to CBPV's distinction between
 value and computation types in Figure~\ref{fig:gtt-type-dynamism}: there
 is a type dynamism relation for value types $A \ltdyn A'$ and for
-computation types $\u B \ltdyn \u B'$, which (1) each are preorders, (2)
-every type constructor is monotone, where the shifts $\u F$ and $U$
-switch which relation is being considered, and (3) the dynamic 
-types $\dynv$ and $\dync$ are the most dynamic value and computation
-types respectively.  For example, we have $U(A \to \u F A') \ltdyn
-U(\dynv \to \u F \dynv)$, which is the analogue of $A \to A' \ltdyn
-\dynv \to \dynv$ in call-by-value: because $\to$ preserves
-embedding-retraction pairs, it is monotone, not contravariant, in the
-domain~\cite{newahmed18,newlicata2018-fscd}.
+computation types $\u B \ltdyn \u B'$, which (1) each are preorders
+(\textsc{VTyRefl}, \textsc{VTyTrans}, \textsc{CTyRefl}, \textsc{CTyTrans}),
+(2) every type constructor is monotone
+(\textsc{$+$Mon}, \textsc{$\times$Mon}, \textsc{$\with$Mon} ,\textsc{$\to$Mon})
+where the shifts $\u F$ and $U$ switch which relation is being
+considered (\textsc{$U$Mon}, \textsc{$F$Mon}), and (3) the dynamic types
+$\dynv$ and $\dync$ are the most dynamic value and computation types
+respectively (\textsc{VTyTop}, \textsc{CTyTop}).  For example, we have
+$U(A \to \u F A') \ltdyn U(\dynv \to \u F \dynv)$, which is the analogue
+of $A \to A' \ltdyn \dynv \to \dynv$ in call-by-value: because $\to$
+preserves embedding-retraction pairs, it is monotone, not contravariant,
+in the domain~\citep{newahmed18,newlicata2018-fscd}.
 
 \begin{figure}
 \begin{small}
@@ -1590,7 +1593,8 @@ However, this analysis ignores an important property of CBV casts in practice:
 \emph{upcasts} always terminate without performing any effects, and in
 some systems upcasts are even defined to be values, while only the
 \emph{downcasts} are effectful (introduce errors).  For example, for many types $A$, the
-upcast from $A$ to $\dynv$ is an injection into a sum/recursive type, which is a value constructor.  Previous work on a logical
+upcast from $A$ to $\dynv$ is an injection into a sum/recursive type,
+which is a value constructor.  Our previous work on a logical
 relation for call-by-value gradual typing~\cite{newahmed18} proved that all
 upcasts were pure in this sense as a consequence of the embedding-projection pair properties (but their proof depended on the only effects being
 divergence and type error).
@@ -1616,26 +1620,26 @@ can introduce errors, because the upcast of an object supporting some
 ``methods'' to one with all possible methods will error dynamically on
 the unimplemented ones.
 
-These observations are expressed in the (shaded) rules for casts in
+These observations are expressed in the (shaded) \textsc{UpCast} and
+\textsc{DnCasts} rules for casts in
 Figure~\ref{fig:gtt-syntax-and-terms}: the upcast for a value type
 dynamism is a complex value, while the downcast for a computation type
 dynamism is a stack (if its argument is).  Indeed, this description of
 casts is simpler than the intuition we began the section with: rather
 than putting in both upcasts and downcasts for all value and computation
 type dynamisms, it suffices to put in only \emph{upcasts} for
-\emph{value} type dynamisms
-and \emph{downcasts} for \emph{computation} type dynamisms, because of
-monotonicity of type dynamism for $U$/$\u F$ types.  The
-\emph{downcast} for a \emph{value} type dynamism $A \ltdyn A'$, as a
-stack $\bullet : \u F A' \vdash \dncast{\u F A}{\u F A'}{\bullet} : \u F
-A$ as described above, is obtained from $\u F A \ltdyn \u F A'$ as
-computation types.  The upcast for a computation type dynamism $\u B
-\ltdyn \u B'$ as a value $x : U \u B \vdash \upcast{U \u B}{U \u B'}{x}
-: U \u B'$ is obtained from $U \u B \ltdyn U \u B'$ as value types.
-Moreover, we will show below that the value upcast $\upcast{A}{A'}$
-induces a stack $\bullet : \u F A \vdash \ldots : \u F A'$ that behaves
-like an upcast, and dually for the downcast, so this formulation 
-implies the original formulation above.
+\emph{value} type dynamisms and \emph{downcasts} for \emph{computation}
+type dynamisms, because of monotonicity of type dynamism for $U$/$\u F$
+types.  The \emph{downcast} for a \emph{value} type dynamism $A \ltdyn
+A'$, as a stack $\bullet : \u F A' \vdash \dncast{\u F A}{\u F
+  A'}{\bullet} : \u F A$ as described above, is obtained from $\u F A
+\ltdyn \u F A'$ as computation types.  The upcast for a computation type
+dynamism $\u B \ltdyn \u B'$ as a value $x : U \u B \vdash \upcast{U \u
+  B}{U \u B'}{x} : U \u B'$ is obtained from $U \u B \ltdyn U \u B'$ as
+value types.  Moreover, we will show below that the value upcast
+$\upcast{A}{A'}$ induces a stack $\bullet : \u F A \vdash \ldots : \u F
+A'$ that behaves like an upcast, and dually for the downcast, so this
+formulation implies the original formulation above.
 
 We justify this design in two ways in the remainder of the paper.  In
 Section~\ref{sec:contract}, we show how to implement casts by a
@@ -1831,33 +1835,35 @@ terms for related variables.  We will implicitly zip/unzip pairs of
 contexts, and sometimes write e.g. $\Gamma \ltdyn \Gamma$ to mean $x
 \ltdyn x : A \ltdyn A$ for all $x : A$ in $\Gamma$.
 
-The main point of our rules for term dynamism is that \emph{there
-  are no type-specific axioms in the definition} beyond the
-$\beta\eta$-axioms that the type satisfies in a non-gradual language.
-Thus, adding a new type to gradual type theory does not require any a
-priori consideration of its gradual behavior in the language definition;
-instead, this is deduced as a theorem in the type theory.  The basic
-structural rules of term dynamism in
-Figure~\ref{fig:gtt-term-dynamism-structural} say that it is reflexive
-and transitive, that assumptions can be used and substituted for, and
-that every term constructor is monotone (the congruence rules are
-derived in a mechanical way from the corresponding typing rules).
+The main point of our rules for term dynamism is that \emph{there are no
+  type-specific axioms in the definition} beyond the $\beta\eta$-axioms
+that the type satisfies in a non-gradual language.  Thus, adding a new
+type to gradual type theory does not require any a priori consideration
+of its gradual behavior in the language definition; instead, this is
+deduced as a theorem in the type theory.  The basic structural rules of
+term dynamism in Figure~\ref{fig:gtt-term-dynamism-structural} say that
+it is reflexive and transitive (\textsc{TmDynRefl},
+\textsc{TmDynTrans}), that assumptions can be used and substituted for
+(\textsc{TmDynVar}, \textsc{TmDynValSubst}, \textsc{TmDynHole},
+\textsc{TmDynStkSubst}), and that every term constructor is monotone
+(the \textsc{Cong} rules).
 \begin{longonly}
 While we could add congruence rules for errors and casts,
 these follow from the axioms characterizing their behavior below.  
 \end{longonly}
 
-Type dynamism is reflexive, and we will often abbreviate a homogeneous
-term dynamism by writing e.g. $\Gamma \vdash V \ltdyn V' : A \ltdyn A'$
-for $\Gamma \ltdyn \Gamma \vdash V \ltdyn V' : A \ltdyn A'$, or $\Phi
-\vdash V \ltdyn V' : A$ for $\Phi \vdash V \ltdyn V' : A \ltdyn A$, and
-similarly for computations.  The entirely homogeneous judgements $\Gamma
-\vdash V \ltdyn V' : A$ and $\Gamma \mid \Delta \vdash M \ltdyn M' : \u
-B$ can be thought of as a syntax for contextual error approximation (as we
-prove below).  We write $V \equidyn V'$ (``equidynamism'') to mean term dynamism relations
-in both directions (which requires that the types are also equidynamic
-$\Gamma \equidyn \Gamma'$ and $A \ltdyn A'$,
-typically because they are identical), which is a syntactic judgement for contextual equivalence.
+We will often abbreviate a ``homogeneous'' term dynamism (where the type
+or context dynamism is given by reflexivity) by writing e.g. $\Gamma
+\vdash V \ltdyn V' : A \ltdyn A'$ for $\Gamma \ltdyn \Gamma \vdash V
+\ltdyn V' : A \ltdyn A'$, or $\Phi \vdash V \ltdyn V' : A$ for $\Phi
+\vdash V \ltdyn V' : A \ltdyn A$, and similarly for computations.  The
+entirely homogeneous judgements $\Gamma \vdash V \ltdyn V' : A$ and
+$\Gamma \mid \Delta \vdash M \ltdyn M' : \u B$ can be thought of as a
+syntax for contextual error approximation (as we prove below).  We write
+$V \equidyn V'$ (``equidynamism'') to mean term dynamism relations in
+both directions (which requires that the types are also equidynamic
+$\Gamma \equidyn \Gamma'$ and $A \ltdyn A'$), which is a syntactic
+judgement for contextual equivalence.
 
 \ifshort \vspace{-0.1in} \fi
 \subsection{Term Dynamism: Axioms}
@@ -1893,11 +1899,11 @@ if the unique value of $1$ is represented as the boolean \texttt{true}. In
 Section~\ref{sec:dynamic-type-interp}, we show additional axioms that
 fully characterize the behavior of the dynamic type.
 
-The axioms in the middle of the figure, which are taken directly from
-CBPV, assert the $\beta\eta$ rules for each type as (homogeneous) term
-equidynamisms---these should be understood as having, as implicit
-premises, the typing conditions that make both sides type check, in equidynamic
-contexts.
+The type universal properties in the middle of the figure, which are
+taken directly from CBPV, assert the $\beta\eta$ rules for each type as
+(homogeneous) term equidynamisms---these should be understood as having,
+as implicit premises, the typing conditions that make both sides type
+check, in equidynamic contexts.
 
 The final axioms assert properties of the run-time error term $\err$: it
 is the least dynamic term (has the fewest behaviors) of every
-- 
GitLab