From 2eeed410fb6256e6f39e56ece8802640ca946114 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 29 Oct 2018 09:43:29 -0400
Subject: [PATCH] add in some refs to type tags throughout
---
paper/gtt.tex | 41 +++++++++++++++++++++++------------------
1 file changed, 23 insertions(+), 18 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 6dbefa9..ae21b62 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1434,7 +1434,7 @@ or whether we should have \emph{both} a dynamic value type and a dynamic
computation type.
%
Our modular, type-theoretic presentation of gradual typing allows us to
-easily explore these options, though we find that (surprisingly) having
+easily explore these options, though we find that having
both a dynamic value $\dynv$ and a dynamic computation type $\dync$
gives the most natural implementation (see
Section~\ref{sec:dynamic-type-interp}). Thus, we add both $\dynv$ and
@@ -1583,17 +1583,17 @@ not reflect all effects of their input.
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
+\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
relation for call-by-value gradual typing~\cite{newahmed18} proved that all
-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
+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).
+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,
-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 erroring otherwise, and so should not be a complex value.
+rather than computation. On the other hand, many downcasts between value
+types are implemented as a case-analysis looking for a specific
+tag and erroring otherwise, and so are not complex values.
We can also make a dual observation about CBN casts. The
\emph{downcast} arising from $\u B \ltdyn \u B'$ has a stronger property
@@ -1602,7 +1602,7 @@ 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
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
+in section \ref{sec:contract}, is to think of the dynamic computation type $\dync$ as a
recursive \emph{product} of all possible behaviors that a computation
might have, and the downcast as a recursive type unrolling and product
projection, which is a stack. From this point of view, an \emph{upcast}
@@ -1639,10 +1639,9 @@ downcasts are complex stacks.
However, one goal of
GTT is to be able to prove things about many gradually typed languages
at once, by giving different models, so one might wonder whether this
-design rules out potential models where casts are effectful. In
+design rules out useful models of gradual typing where casts can have more general effects. In
Theorem~\ref{thm:upcasts-values-downcasts-stacks}, we show instead that
-this design is forced for all casts, as long as the casts between ground
-types and the dynamic types have this property.
+our design choice is forced for all casts, as long as the casts between ground types and the dynamic types are values/stacks.
%% Counterexample
@@ -3833,7 +3832,7 @@ casts between \emph{ground} types and $\dynv$/$\dync$. For this section, we def
\[
G ::= 1 \mid \dynv \times \dynv \mid 0 \mid \dynv + \dynv \mid U \dync
\qquad
- \u G ::= \top \mid \dync \with \dync \mid \dynv \to \dync \mid \u F \dynv
+ \u G ::= \dynv \to \dync \mid \top \mid \dync \with \dync \mid \u F \dynv
\]
\begin{longonly}
@@ -4130,9 +4129,14 @@ in a non-gradual language.
While contracts are typically implemented in a dynamically typed
language, our target is typed, retaining type information similarly to
manifest contracts \cite{greenberg-manifest}.
+%
+We give implementations of the dynamic value type in the usual way as
+a recursive sum of basic value types, i.e., using type tags, and we
+give implementations of the dynamic computation type as the dual: a
+recursive product of basic computation types.
-Writing $\sem{M}$ for the contract translation, the remaining sections
-of the paper establish:
+Writing $\sem{M}$ for any of the contract translations, the remaining
+sections of the paper establish:
\begin{theorem}[Equi-dynamism implies Observational Equivalence]
If $\Gamma \vdash M_1 \equidyn M_2 : \u B$, then for any closing
GTT context $C : (\Gamma \vdash \u B) \Rightarrow (\cdot \vdash \u F
@@ -4153,7 +4157,8 @@ of the paper establish:
\end{enumerate}
\end{theorem}
-As a consequence we will also get consistency of dynamism:
+As a consequence we will also get consistency of our logic of
+dynamism:
\begin{corollary}[Consistency \iflong of GTT \fi]
$\cdot \vdash \ret \kw{true} \ltdyn \ret \kw{false} : \u F(1+1)$ is not
provable in GTT.
@@ -9484,7 +9489,7 @@ for each type \cite{henglein94:dynamic-typing}.
%
Because of this, the theorems proven in that paper are more closely
related to our model construction in section
-\ref{sec:contract-models}.
+\ref{sec:contract}.
%
More specifically, many of the lemmas proven in the extended version
of the paper have direct analogues in Henglein's work.
--
GitLab