some prose

paper/gtt.tex

@@ -108,7 +108,8 @@
 %% DEFINITIONS
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-\newcommand{\cbpv}{$\text{CBPV}_{\mu,\nu,\err,\ltdyn}$}
+\newcommand{\cbpv}{\text{CBPV}_{\mu,\nu,\err,\ltdyn}}
+\newcommand{\cbpvtxt}{$\cbpv$}
 \newcommand{\sem}[1]{\llbracket#1\rrbracket}
 \newcommand{\hetplug}[1]{\langle#1\rangle}
 \newcommand{\nats}{\mathbb{N}}
@@ -513,8 +514,9 @@ embeddings.
 
 Our proof architecture is as follows:
 \begin{tikzcd}
-GTT \arrow[d] \\
-CBPV \arrow[d] \\
+GTT \arrow[d,"contract insertion"] \\
+\cbpv^* \arrow[d,"complex value elimination"] \\
+\cbpv \arrow[d,"logical relation"] \\
 LR \simeq CtxApprox
 \end{tikzcd}
 Our gradual type theory with casts and syntactic theory of term
@@ -741,6 +743,38 @@ principles of each type, given in figure TODO ref.
 
 \section{Contract Translation to Call-by-push-value}
 
+To show the soundness of our model, and demonstrate its relationship
+to operational definitions of the gradual guarantee, we develop a
+\emph{model} of GTT using observational error approximation of a
+\emph{non-gradual} call-by-push-value language.
+%
+We call this the \emph{contract translation} because it translates the
+builtin casts of the gradual language into ordinary terms implemented
+in a non-gradual language.
+%
+While contracts are typically implemented in a dynamically typed
+language, our target is typed, meaning we retain the type information
+that might be used in later stages of compilation.
+%
+We could always erase the types of our typed language (cbpv's
+operational semantics is perfectly sensible on untyped terms) and get
+a more typical contract translation.
+
+As described in the previous section, almost all of the contract
+translation is uniquely determined already: casts between function
+types must wrap inputs and outputs, pairs cast each component, etc.
+%
+The \emph{only} part of the translation that is not predetermined is
+the interpretation of the dynamic type and the ``tagging/untagging''
+casts between the dynamic type and basic tag types.
+%
+For this reason, our translation is \emph{parameterized} by an
+interpretation of the dynamic type.
+%
+To interpret the dynamic type in our target language, we use a version
+of call-by-push-value with \emph{recursive} and \emph{corecursive}
+types, whose rules are presented in TODO.
+
 Our target call-by-push-value language is almost a subset of GTT:
 there are no casts, we remove complex values, only allowing
 constructors, similarly for complex stacks, and the inequational
@@ -774,8 +808,8 @@ with more general types for \emph{recursive} value types and
 \end{figure}
 
 \begin{definition}[Dynamic Type Interpretation]
-  A $\dynv,\dync$ interpretation $\rho$ consists of first a \cbpv
-    value type $\rho(\dynv)$, a \cbpv computation type $\rho(\dync)$.
+  A $\dynv,\dync$ interpretation $\rho$ consists of first a \cbpvtxt
+    value type $\rho(\dynv)$, a \cbpvtxt computation type $\rho(\dync)$.
     This is extended in the obvious way to interpretations of all
     ground types $\sem G \rho$ and $\sem {\u G} \rho$.
 
@@ -943,13 +977,13 @@ booleans.
   Then the following are all true
   \begin{enumerate}
   \item If $\Gamma \vdash M : \u B$ in GTT, then $\sem{\Gamma}\rho
-    \vdash \sem M \rho : \sem {\u B} \rho$ in \cbpv.
+    \vdash \sem M \rho : \sem {\u B} \rho$ in \cbpvtxt.
   \item If $\Gamma \vdash V : A$ in GTT, and $\sem\Gamma\rho, x:\sem
-    A\rho \vdash M : \u B$ in \cbpv, then
-    $\sem\Gamma \vdash M\hetplug {V/x}\rho : \u B$ in \cbpv.
+    A\rho \vdash M : \u B$ in \cbpvtxt, then
+    $\sem\Gamma \vdash M\hetplug {V/x}\rho : \u B$ in \cbpvtxt.
   \item If $\Gamma \pipe \u B \vdash S : \u B'$in GTT, and
-    $\sem\Gamma\rho \vdash M : \sem{\u B}\rho$ in \cbpv then
-    $\sem{\Gamma}\rho \vdash S\hetplug{M}\rho : \sem {\u B} \rho$ in \cbpv.
+    $\sem\Gamma\rho \vdash M : \sem{\u B}\rho$ in \cbpvtxt then
+    $\sem{\Gamma}\rho \vdash S\hetplug{M}\rho : \sem {\u B} \rho$ in \cbpvtxt.
   \end{enumerate}
   \begin{enumerate}
   \item If $\Gamma \ltdyn \Gamma' \vdash M \ltdyn M' : \u B \ltdyn \u B'$,