From 62e965766c63ac26efaaf88fb0d04531145f307e Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Thu, 25 Oct 2018 12:19:18 -0400
Subject: [PATCH] more on eager and lazy semantics in the intro
---
paper/gtt.tex | 69 +++++++++++++++++++++++++++++++++++++++++----------
1 file changed, 56 insertions(+), 13 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index bb7a081..663dd2e 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -569,24 +569,67 @@ axioms of gradual type theory.
This mean the language violates either compositionality, the gradual
guarantee, or one of the $\beta, \eta$ axioms---and in practice, it is
usually $\eta$.
-%
+
For instance, a transient semantics, where only the top-level
connectives are checked, violates $\eta$ for strict pairs:
\begin{small}
- \[ {x : A_1 \times (A_2 \times A_3)} \vdash \letXbeYinZ x {(x_1,(x_2,x_3))} 0 \neq 0 \]
+ \[ {x : A_1 \times A_2} \vdash \letXbeYinZ x {(x_1,x_2)} 0 \neq 0 \]
+\end{small}
+because the top-level connectives of $A_1, A_2$ are only checked when
+the pattern match is introduced. As a concrete counterexample to
+contextual equivalence, let $A_1, A_2$ all be \texttt{String}. Then
+because only the top-level connective is checked, $(0,1)$ is a valid
+value of type $\texttt{String} \times \texttt{String}$, but pattern
+matching on the pair ensures that the two components are checked to be
+strings, so $\letXbeYinZ {(0,1)} {(x_1,x_2)} 0 \mapsto \err$, whereas
+with no pattern match a value is returned. This means simple program
+changes such as changing a function of two arguments to take a single
+pair of those arguments that are valid in a typed language are
+invalidated by the transient semantics.
+%
+In summary, transient semantics is ``lazier'' than the types dictate,
+catching errors only when the term is inspected.
+
+As a subtler example, in call-by-value ``eager cast semantics'' the
+$\beta, \eta$ principles for all of the eager datatypes ($0, +, 1,
+\times$, lists, etc.) will be satisfied, but the $\eta$ principle for
+the function type $\to$ is violated, i.e., there are values $V : A \to
+A'$ for which $V \neq \lambda x:A. V x $.
+%
+For instance, take an arbitrary function value $V : A \to
+\texttt{String}$ for some type $A$, and let $V' = \obcast{A \to
+ \dyn}{A \to \texttt{String}}$ be the result of casting it to have a
+dynamically typed output.
+%
+Then in eager semantics, the following programs are not equivalent:
+\begin{small}
+ \lambda x:A. V' x \neq V' : A \to \dyn
\end{small}
-because the top-level connectives of $A_2, A_3$ are checked when the
-pattern match is introduced.
%
-Next, in a typical CBV ``eager cast semantics'' the $\beta, \eta$
-principles for all of the eager datatypes ($0, +, 1, \times$, lists,
-etc.) will be satisfied, but the $\eta$ principle for the function
-type $\to$ is violated, i.e., there are values $V : A \to A'$ for
-which $V \neq \lambda x:A. V x $.
+We cannot observe any difference between these two programs by
+applying them to arguments, however, they are distinguished from each
+other by their behavior when \emph{cast}.
+%
+Specifically, if we cast both sides to $A \to \texttt{Number}$, then
+$\obcast{A\to \texttt{Number}}{A\to\dyn}(\lambda x:A.V' x)$ is a
+value, but $\obcast{A \to \texttt{Number}}{A\to \dyn}V'$ reduces to an
+error because $\texttt{Number}$ is incompatible with
+$\texttt{String}$.
+%
+However this type error might not correspond to any actual typing
+violation of the program involved.
+%
+For one thing, the resulting function might never be executed.
+%
+Furthermore, in the presence of effects, it may be that the original
+function $V : A \to \texttt{String}$ never returns a string (because
+it diverges, raises an exception or invokes a continuation), and so
+that same value casted to $A \to \texttt{Number}$ might be a perfectly
+valid inhabitant of that type.
%
-We argue that ``eager'' cast semantics is in fact overly eager: in
+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 program equivalences that gradual typing should provide.
+very type-based reasoning that gradual typing should provide.
The reader unfamiliar with proof theory may find the centrality of
$\eta$ equalities in our development unusual.
@@ -771,13 +814,13 @@ of $\beta, \eta$ and graduality for all of these interpretations.
The main contributions of the paper are as follows.
\begin{enumerate}
-\item We present Gradual Type Theory in \secref{sec:gtt}, a simple
+\item We present Gradual Type Theory in section \ref{sec:gtt}, a simple
axiomatic theory of gradual typing. The theory axiomatizes three
simple assumptions about a gradual language: compositionality,
graduality, and type-based reasoning in the form of $\eta$
equivalences.
\item We prove many theorems in the formal logic of Gradual Type
- Theory in \secref{sec:theorems-in-gtt}. Chief among these are the
+ Theory in section \ref{sec:theorems-in-gtt}. Chief among these are the
uniqueness implementation theorems for casts which show that for
each type connective of GTT, the $\eta$ principle for the type
ensures that the casts must implement the lazy contract
--
GitLab