From 29c2dad50e47407676ed53eb672b6ff4f0c7e109 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 30 Oct 2018 14:23:52 -0400
Subject: [PATCH] fix the fixme, and blame soundness ref
---
paper/abstract.tex | 3 +--
paper/gtt.tex | 16 ++++++++--------
2 files changed, 9 insertions(+), 10 deletions(-)
diff --git a/paper/abstract.tex b/paper/abstract.tex
index 2a88a27..9799d91 100644
--- a/paper/abstract.tex
+++ b/paper/abstract.tex
@@ -22,8 +22,7 @@ connective must be equivalent to the so-called ``lazy'' cast semantics.
Contrapositively, this shows that ``eager'' cast semantics violates the
extensionality of function types. As another example, we show that
gradual upcasts are pure functions and, dually, gradual downcasts are
-strict functions, an equational analogue of Wadler-Findler's blame
-soundness theorem. We show the consistency and applicability of our
+strict functions. We show the consistency and applicability of our
axiomatic theory by proving that a contract-based implementation using
the lazy cast semantics gives a logical relations model of our type
theory, where equivalence in GTT implies contextual equivalence of the
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 5af4f97..f0280c8 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -466,8 +466,7 @@ $\lambda x. M x$ will only print when given an argument. But this can be
accomodated with one further modification: the $\eta$ law is valid in
simple call-by-value languages\footnote{This does not hold in languages
with some intensional feature of functions such as reference
- equality. We discuss the applicability of this theorem more generally
- in section \ref{sec:related}} (e.g. SML) if we have a ``value
+ equality. We discuss the applicability of our main results more generally in section \ref{sec:related}} (e.g. SML) if we have a ``value
restriction'' $V \equiv \lambda x. V x$.
%
This illustrates that $\eta$/extensionality rules must be stated for
@@ -689,11 +688,12 @@ valid inhabitant of that type.
In summary the ``eager'' cast semantics is in fact overly eager: in
its effort to find bugs faster than ``lazy'' semantics it disables the
very type-based reasoning that gradual typing should provide.
-% FIXME
-While these criticisms of transient and eager cast semantics are
-well-known (cite?), a novel consequence of our development is that
-\emph{only} the lazy cast semantics satisifies both graduality and
-$\eta$.
+
+While criticisms of transient semantics on the basis of type soundness
+have been made before \citep{greenmanfelleisen:2018}, our development
+shows that the $\eta$ principles of types are enough to uniquely
+determine a cast semantics, and helps clarify the trade-off between
+eager and lazy semantics of function casts.
\textbf{Technical Overview of GTT.} The gradual type theory developed
in this paper unifies our previous work~\citep{newahmed18} on
@@ -9608,7 +9608,7 @@ principles of local state.
\fi
We do not give a treatment of runtime blame reporting, but we argue that
the observation that upcasts are thunkable and downcasts are linear is
-directly related to blame soundness~\cite{wadler-findler09} in that if
+directly related to blame soundness~\cite{tobin-hochstadt06,wadler-findler09} in that if
an upcast were \emph{not} thunkable, it should raise positive blame and
if a downcast were \emph{not} linear, it should raise negative blame.
%
--
GitLab