From 92f210faedb851ceff494d52d7bc1be483eb8abd Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Tue, 30 Oct 2018 00:54:50 -0400
Subject: [PATCH] small edits
---
paper/gtt.tex | 36 ++++++++++++++++++------------------
1 file changed, 18 insertions(+), 18 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index f0e16ed..97c1240 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -2896,12 +2896,12 @@ The casts' behavior is uniquely determined as follows: \ifshort (See the extende
\end{small}
\end{theorem}
In the case for an eager product $\times$, we can actually also show
-that running ${\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}$ and then
-${\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}$ is also an implementation of
-this cast, and therefore equal to the above. Intuitively, this is
-sensible because the only effect a downcast introduces is a run-time
-error, and if either downcast errors, both possible implementations
-will.
+that reversing the order and running ${\dncast{\u F A_2}{\u F A_2'}{\ret
+ x_2'}}$ and then ${\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}$ is also
+an implementation of this cast, and therefore equal to the above.
+Intuitively, this is sensible because the only effect a downcast
+introduces is a run-time error, and if either downcast errors, both
+possible implementations will.
%% For the function downcast, the structure of CBPV nicely requires
%% let-binding the result of the downcast, rather than running the
%% downcast each time the variable occurs, which is a plausible
@@ -3889,7 +3889,7 @@ are restricted to the substitution closures of
\begin{small}
\begin{array}{llll}
x : G \vdash \upcast{G}{\dynv}{x} : \dynv &
-\bullet : \u F \dynv \vdash \dncast{\u F G}{\u F \dynv}{x} : \u F \dynv &
+\bullet : \u F \dynv \vdash \dncast{\u F G}{\u F \dynv}{\bullet} : \u F \dynv &
\bullet : \dync \vdash \dncast{\u G}{\dync}{\bullet} : \dync &
x : U \u G \vdash \upcast{U \u G}{U \dync}{x} : U \dync
\end{array}
@@ -4220,15 +4220,15 @@ operational values and stacks.
%
\cbpvstar\ is almost a subset of GTT obtained as follows: We remove the
casts and the dynamic types $\dynv, \dync$ (the shaded pieces) from the
-syntax and typing rules in Figure~\ref{fig:gtt-syntax-and-terms}. There is no
-type dynamism, and the inequational theory of \cbpv* is the homogeneous
-fragment of term dynamism in
+syntax and typing rules in Figure~\ref{fig:gtt-syntax-and-terms}. There
+is no type dynamism, and the inequational theory of \cbpv* is the
+homogeneous fragment of term dynamism in
Figure~\ref{fig:gtt-term-dynamism-structural} (judgements $\Gamma \vdash
E \ltdyn E' : T$ where $\Gamma \vdash E,E' : T$, with all the same rules
in that figure thus restricted). The inequational axioms are the
-$\beta\eta$ rules for all type constructors in
-Figure~\ref{fig:gtt-term-dyn-axioms}, and the error properties (with the
-left-hand rule made homogeneous).
+Type Universal Properties ($\beta\eta$ rules)
+and Error Properties (with \textsc{ErrBot} made homogeneous) from
+Figure~\ref{fig:gtt-term-dyn-axioms}.
%
To implement the casts and dynamic types, we \emph{add} general
\emph{recursive} value types ($\mu X.A$, the fixed point of $X \vtype
@@ -4936,7 +4936,7 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
\pi'\dncast{\u B\with\u B}{\bool \to \u B}M \equidyn M\,\fls\\
\end{longonly}
- \inferrule*[right=$\dynv$I]
+ \inferrule*[right=$\dync$I]
{\Gamma \pipe \Delta \vdash M_{\to} : \dynv \to \dync\\
\Gamma \pipe \Delta \vdash M_{\u F} : \u F \dynv}
{\Gamma \pipe \Delta \vdash \dyncocaseFunF{M_{\to}}{M_{\u F}} : \dync}\\
@@ -9429,7 +9429,7 @@ even the dynamic types.
%
So even if a call-by-value language may have reference equality
functions, if it has the $\eta$ principle for strict pairs, then the
-pair cast must be that of theorem \ref{functorial-casts}.
+pair cast must be that of Theorem \ref{thm:functorial-casts}.
Next, we consider the applicability to non-eager languages.
%
@@ -9513,7 +9513,7 @@ their incompatibility theorem should be a consequence of our main
theorem in the following sense.
%
We showed that any contract semantics departing from the
-implementation in theorem \ref{thm:functorial-casts} must violate
+implementation in Theorem \ref{thm:functorial-casts} must violate
$\eta$ or graduality.
%
Their completeness property is inherently eager, and so must be
@@ -9531,11 +9531,11 @@ we give a uniform definition of all casts and derive implementations
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
+related to our model construction in Section
\ref{sec:contract}.
%
More specifically, many of the properties of casts needed to prove
-theorem \ref{thm:axiomatic-graduality} have direct analogues
+Theorem \ref{thm:axiomatic-graduality} have direct analogues
in Henglein's work, such as the coherence theorems.
%
We have not included these lemmas in the paper because they are quite
--
GitLab