From d65d1ef932847b458622cb210cd809ce17eb1d59 Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Tue, 10 Jul 2018 12:34:43 -0400
Subject: [PATCH] edits
---
paper/gtt.tex | 35 +++++++++++++++++------------------
1 file changed, 17 insertions(+), 18 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index b61ca79..dd1a532 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1174,7 +1174,7 @@ computations may be surprising to those familiar only with
call-by-value, because at higher computation types effects have a
call-by-name-like equational theory. For example, at computation type
$A \to \u B$, we have an equality $\print c; \lambda x. M = \lambda
-x.print c; M$. Intuitively, the reason is that $A \to \u B$ is not
+x.\print c; M$. Intuitively, the reason is that $A \to \u B$ is not
treated as an \emph{observable} type (one where computations are run):
the states of the operational semantics are only those comptuations of
type $\u F A$ for some value type $A$. Thus, ``running'' a function
@@ -1220,11 +1220,11 @@ bijective with computations $x : A \vdash M : \u B$.
To compress the presentation in Figure~\ref{fig:gtt-syntax-and-terms},
we use a typing judgement $\Gamma \mid \Delta \vdash M : \u B$ with a
-``stoup''~\citep{girard?}, a typing context $\Delta$ that is either
+``stoup'', a typing context $\Delta$ that is either
empty or contains exactly one assumption $\bullet : \u B$, so $\Gamma
\mid \cdot \vdash M : \u B$ is a computation, while $\Gamma \mid \bullet
: \u B \vdash M : \u B'$ is a stack. The \ifshort{(omitted) }\fi typing
-rules for $\top$ and $\with$ treat the stack input variable additively
+rules for $\top$ and $\with$ treat the stoup additively
(it is arbitrary in the conclusion and the same in all premises); for a
function application to be a stack, the stack input must occur in the
function position. The elimination form for $U \u B$, $\force{V}$, is
@@ -1251,9 +1251,9 @@ while a CBN function $B \to B'$ is translated to $U \u B^n \to \u B'^n$
with a thunked argument. Sums $B_1 + B_2$ are translated to $\u F (U \u
{B_1}^n + U \u {B_2}^n)$, making the ``lifting'' in lazy sums explicit.
Call-by-push-value \emph{subsumes} call-by-value and call-by-name in
-that these embeddings are \emph{full and faithful}: two CBV programs are
+that these embeddings are \emph{full and faithful}: two CBV or CBN programs are
equivalent if and only if their embeddings into CBPV are equivalent, and
-every CBPV program with a CBV/CBN type can be back-translated to CBV.
+every CBPV program with a CBV or CBN type can be back-translated.
%% While these rules are very intuitive when the input and output types
%% of the stack are $\u F A$ for some value type (which is always the
@@ -1344,7 +1344,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$.
-\cite{nl18cbngtt,icfp} analyze this as the existence of an \emph{upcast}
+\cite{newahmed18,newlicata2018-fscd} analyze 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 an ordering on terms
where runtime type errors are minimal: the upcast followed by the
@@ -1374,7 +1374,7 @@ 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{fscd,icfp}.
+domain~\cite{newahmed18,newlicata2018-fscd}.
\begin{figure}
\begin{small}
@@ -1437,14 +1437,13 @@ domain~\cite{fscd,icfp}.
\subsection{Casts}
\label{sec:gtt-casts}
-Even given previous work on call-by-value~\cite{newahmed18} and
-call-by-name~\cite{fscd} gradual typing, it is not immediately obvious
-how to add type casts to CPBV, because CBPV exposes finer judgemental
-distinctions than previous work considered. However, we can arrive at a
-first proposal by considering how previous work would be embedded into
-CBPV.
+It is not immediately obvious how to add type casts to CPBV, because
+CBPV exposes finer judgemental distinctions than previous work
+considered. However, we can arrive at a first proposal by considering
+how previous work would be embedded into CBPV.
%
-In the previous work on both CBV and CBN, every type dynamism judgement
+In the previous work on both CBV and
+CBN~\cite{newahmed18,newlicata2018-fscd} every type dynamism judgement
$A \ltdyn A'$ induces both an upcast from $A$ to $A'$ and a downcast
from $A'$ to $A$.
%
@@ -1466,8 +1465,8 @@ the upcast and downcast to a priori be effectful computations.
%
Dually, a CBN cast typically can be represented by a CBN function of
type $B \to B'$, whose CBPV analogue is a computation of type $U \u B
-\to \u B'$, or equivalently a computation $x : U \u B \vdash M : \u B'$,
-or a value $x : U \u B \vdash \thunk{M} : U \u B'$. This suggests that a
+\to \u B'$, which is equivalent with a computation $x : U \u B \vdash M : \u B'$,
+and with a value $x : U \u B \vdash \thunk{M} : U \u B'$. This suggests that a
\emph{computation} type dynamism $\u B \ltdyn \u B'$ should induce an
embedding-projection pair of \emph{values} $x : U \u B \vdash V_u : U \u
B'$ and $x : U \u B' \vdash V_d : U \u B$, where both the upcast and the
@@ -1487,7 +1486,7 @@ in the syntax of the casts, by making the upcast $\upcast{A}{A'}$
induced by a value type precision $A \ltdyn A'$ itself a complex value,
rather than computation. On the other hand, a downcast between value
types is typically implemented as a case-analysis looking for a specific
-tag, and therefore can error, and so should not be a complex value.
+tag, and erroring otherwise, and so should not be a complex value.
We can also make a dual observation about CBN casts. The
\emph{downcast} arising from $\u B \ltdyn \u B'$ has a stronger property
@@ -1513,7 +1512,7 @@ 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 of type dynamism for $U$/$\u F$ types. The
+monotonicity of type dynamism for $U$/$\u F$ types. The
\emph{downcast} for a \emph{value} type precision $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
--
GitLab