From df7df59bc7f63aef7aee6ffd28dadb7bce911d2b Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Sun, 28 Oct 2018 18:57:22 -0400
Subject: [PATCH] revise the "applicability" section

---
 paper/gtt.tex | 67 +++++++++++++++++++++++++--------------------------
 paper/max.bib |  7 ++++++
 2 files changed, 40 insertions(+), 34 deletions(-)

diff --git a/paper/gtt.tex b/paper/gtt.tex
index 210f60c..6dbefa9 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -9348,42 +9348,41 @@ to reason about program transformations and optimizations in them.
 \fi
 
 The cast uniqueness principles given in theorem
-\ref{thm:functorial-casts} are theorems in the logic of Gradual Type
-Theory, so there is a question of what languages the theorem applies
-to.
+\ref{thm:functorial-casts} are theorems in the formal logic of Gradual
+Type Theory, and so there is a question of to what languages the
+theorem applies.
 %
 The theorem applies to any \emph{model} of gradual type theory, such
-as the models given in sections \ref{sec:contract}, \ref{sec:complex},
-\ref{sec:operational}.
-%
-We argue that this applies directly to languages that are
-call-by-value and call-by-name, not just call-by-push-value itself.
-%
-TODO: why
-
-Finally, we note that the case of the theorem for function types does
-\emph{not} apply to call-by-value languages where the restricetd
-$\eta$ principle for functions is not satisfied. In particular
-languages where functions can be tested for pointer equality. It is a
-well-known issue that the lazy semantics of functions and objects is
-not valid in the presence of pointer equality (TODO: cite semantic
-casts) and our uniqueness theorem provides a different perspective on
-this result.
-
-%
-However, we note that the cases of the theorem are completely
-\emph{modular} in that the proof for any individual connective
-$\to,\times,\ldots$ only relies on the $\eta$ principle for that
-connective.
-%
-This means that the case of the theorem for a particular connective
-applies to any model of any \emph{subsystem} of GTT that includes the
-$\eta$ principle for that connective.
-%
-For instance, if $\times\eta$ holds, then the product cast uniqueness
-theorem is provable, whether or not a dynamic computation type $\dync$
-is assumed to exist, or the $\to\eta$ principle holds.
-
+as the models we have constructed using call-by-push-value given in
+sections \ref{sec:contract}, \ref{sec:complex}, \ref{sec:operational}.
+%
+We conjecture that simple call-by-value and call-by-name gradual
+languages are also models of GTT, by extending the translation of
+call-by-push-value into call-by-value and call-by-name in the appendix
+to Levy's monograph \cite{levy03cbpvbook}.
+%
+In order for the theorem to apply, the language must validate an
+appropriate version of the $\eta$ principles for the types.
+%
+So for example, a call-by-value language that has reference equality
+of functions does \emph{not} validate even the value-restricted $\eta$
+law for functions, and so the case for functions does not apply.
+%
+It is a well-known issue that the lazy semantics of function casts is
+not compatible with the refinement property that graduality models in
+the presence of pointer equality, and our uniqueness theorem provides
+a different perspective on this phenomenon
+\cite{findlerflattfelleisen04, refined}.
+%
+However, we note that the cases of the uniqueness theorem, for each
+type connective are completely \emph{modular}: they rely only on the
+specification of casts and the $\beta,\eta$ principles for the
+particular connective, and not on the presence of any other types,
+even the dynamic types.
+%
+So while a call-by-value language that has reference equality of
+functions might still have the $\eta$ principle for strict pairs, so
+that case of the theorem still applies.
 
 % TODO: the following is all subsumed by using Levy's account of
 % "the lazy paradigm"
diff --git a/paper/max.bib b/paper/max.bib
index 5630140..0ff7d1f 100644
--- a/paper/max.bib
+++ b/paper/max.bib
@@ -1200,3 +1200,10 @@ pages="36--54",
   volume={25},
   pages={85-125}
 }
+@InProceedings{findlerflattfelleisen04,
+author="Findler, Robert Bruce and Flatt, Matthew and Felleisen, Matthias",
+title="Semantic Casts: Contracts and Structural Subtyping in a Nominal World",
+booktitle= ecoop,
+year={2004}
+}
+
-- 
GitLab