From d9f2cdd7099fed604aefede64d8e454884d0ccd4 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 12 Jul 2018 12:02:14 +0100
Subject: [PATCH] section 2 edits
---
paper/gtt.tex | 26 +++++++++++++++-----------
1 file changed, 15 insertions(+), 11 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index eca72e8..4465558 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1092,8 +1092,7 @@ lemmas, and proofs.
\subsection{Background: Call-by-Push-Value}
-GTT is an extension of CBPV, so we combine the rules for the two systems;
-the syntax and typing for CBPV are the unshaded rules in
+GTT is an extension of CBPV, so we first present CBPV as the unshaded rules in
Figure~\ref{fig:gtt-syntax-and-terms}. CBPV makes a distinction between
\emph{value types} $A$ and \emph{computation types} $\u B$, where value
types classify \emph{values} $\Gamma \vdash V : A$ and computation types
@@ -1362,7 +1361,7 @@ embedding-projection pair (\emph{ep pair}) for term error approximation
downcast is a no-op, while the downcast followed by the upcast might
error more than the original term, because it imposes a run-time type
check. Syntactically, type dynamism is defined (1) to be reflexive and
-transitive (a preorder), (2) where every type constructor is monotone is
+transitive (a preorder), (2) where every type constructor is monotone in
all positions, and (3) where the dynamic type is greatest in the type
dynamism ordering. This last condition, \emph{the
dynamic type is the most dynamic type}, implies the existence of an
@@ -1484,14 +1483,14 @@ B'$ and $x : U \u B' \vdash V_d : U \u B$, where both the upcast and the
downcast again may a priori be (co)effectful, in the sense that they may
not reflect all effects of their input.
-However, this analysis ignores an important property of CBV casts:
+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, an
upcast from $A$ to $\dynv$ is often implemented as a sum/recursive type
injection, which are value constructors. Previous work on a logical
relation for call-by-value gradual typing~\cite{newahmed18} proved that all
-upcasts had this property (but this depended on the only effects being
+upcasts had this property (but their proof depended on the only effects being
divergence and type error). In GTT, we can make this property explicit
in the syntax of the casts, by making the upcast $\upcast{A}{A'}$
induced by a value type dynamism $A \ltdyn A'$ itself a complex value,
@@ -1503,8 +1502,8 @@ We can also make a dual observation about CBN casts. The
\emph{downcast} arising from $\u B \ltdyn \u B'$ has a stronger property
than being a computation $x : U \u B' \vdash M : \u B$ as suggested
above: it can be taken to be a stack $\bullet : \u B' \vdash \dncast{\u
- B}{\u B'}{\bullet} : \u B$, because a downcasted computation (behaves
-like it) evaluates the computation it is ``wrapping'' exactly once. One
+ B}{\u B'}{\bullet} : \u B$, because a downcasted computation
+evaluates the computation it is ``wrapping'' exactly once. One
intuitive justification for this point of view, which we make precise
below, is to think of the dynamic computation type $\dync$ as a
recursive \emph{product} of all possible behaviors that a computation
@@ -1699,7 +1698,12 @@ judgement $E \ltdyn E' : T \ltdyn T'$ between terms $E : T$ and $E' :
T'$ where $T \ltdyn T'$---i.e. relating two terms at two different
types, where the type on the right is more dynamic than the type on the
right. This judgement structure allows simple axioms characterizing the
-behavior of casts~\cite{newlicata2018-fscd}. Here, we break this judgement up into
+%
+behavior of casts~\cite{newlicata2018-fscd} and axiomatizes the
+graduality property~\cite{refined}.
+%
+Here, we break this judgement up into
+%
value dynamism $V \ltdyn V' : A \ltdyn A'$ and computation dynamism $M
\ltdyn M' : \u B \ltdyn \u B'$. To support reasoning about open terms,
the full form of the judgements are
@@ -1780,15 +1784,15 @@ specification of casts leaves some behavior undefined: for example, we
cannot prove in the theory that $\dncast{\u F 1+1}{\u
F\dynv}\upcast{1}{\dynv}$ reduces to an error. We choose this design
because there are valid models in which it is not an error, for instance
-if the unique value of $1$ is represented as the boolean \kw{true}. In
+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 any
-context.
+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