define dynamic type interp, state correctness for translation

Conclusion: we should break the contract interpretation into 2 steps:
1. Eliminate the casts using an interpretation for the dyn type tags
2. Complex Value/Stack elimination

paper/gtt.tex

@@ -108,6 +108,9 @@
 %% DEFINITIONS
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
+\newcommand{\cbpv}{$\text{CBPV}_{\mu,\nu,\err,\ltdyn}$}
+\newcommand{\sem}[1]{\llbracket#1\rrbracket}
+\newcommand{\hetplug}[1]{\langle#1\rangle}
 \newcommand{\nats}{\mathbb{N}}
 \newtheorem{principle}{Principle}
 \newcommand{\vtype}{\,\,\text{val type}}
@@ -145,10 +148,13 @@
 \newcommand{\bigstepzero}{\bigstepsin{0}}
 
 \newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
+\newcommand{\pairWtoXYtoZ}[4]{\{ #1 \mapsto {#2} \pipe #3 \mapsto {#4}\}}
 \newcommand{\tru}{\texttt{true}}
 \newcommand{\fls}{\texttt{false}}
 \newcommand{\inl}{\texttt{inl}}
 \newcommand{\inr}{\texttt{inr}}
+\newcommand{\intag}[1]{\texttt{in}_{#1}}
+\newcommand{\els}{\kw {else}}
 
 \newcommand{\dyn}{{?}}
 \newcommand{\dynv}{{?}}
@@ -480,7 +486,7 @@ approximation ``up to cast''.
 
 Each paper had certain limitations: \cite{cbn-gtt} only dealt with the
 negative fragment of call-by-name, and did not have an accompanying
-operational semantic interpreation.
+operational semantic interpretation.
 %
 On the other hand, \cite{cbv-gt-lr} dealt with positive and negative
 types in call-by-value, but only allowed for contextual equivalence
@@ -735,6 +741,246 @@ principles of each type, given in figure TODO ref.
 
 \section{Contract Translation to Call-by-push-value}
 
+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
+theory only relates terms that have the same input and output
+environment.
+%
+We also remove the dynamic types $\dynv, \dync$, but we replace them
+with more general types for \emph{recursive} value types and
+\emph{corecursive} computation types.
+
+\begin{figure}
+  \begin{mathpar}
+    \inferrule
+    {\Gamma \vdash V : A[\mu X. A/X]}
+    {\Gamma \vdash \roll{\mu X. A} V : \mu X.A}
+
+    \inferrule
+    {\Gamma \vdash V : \mu X. A\and
+      \Gamma, x : A[\mu X.A/X] \vdash M : \u B}
+    {\Gamma \vdash \pmmuXtoYinZ V x M : \u B}
+
+    \inferrule
+    {\Gamma \vdash M : \nu \u Y. \u B}
+    {\Gamma \vdash \unroll M : \u B[\nu \u Y. \u B]}
+
+    \inferrule
+    {\Gamma \vdash M : \u B[\nu \u Y. \u B]}
+    {\Gamma \vdash \roll{\nu \u Y. \u B} M : \nu \u Y. \u B}
+  \end{mathpar}
+  \caption{Recursive, Corecursive Types}
+\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)$.
+    This is extended in the obvious way to interpretations of all
+    ground types $\sem G \rho$ and $\sem {\u G} \rho$.
+
+    The interpretation furthermore has for each value ground type, an
+    interpretation of the upcast and the downcast with $\rho(\dynv)$
+    such that the upcast is thunkable and the pair satisfy
+    retraction and projection:
+    \begin{mathpar}
+      \inferrule
+      {}
+      {x : \sem G \rho \vdash \rho_{up}(G) : \u F \rho (\dynv)}
+
+      \inferrule
+      {}
+      {y : \rho(\dynv) \vdash \rho_{dn}(G) : \u F \sem G \rho }
+
+      \inferrule*[Right=Thunkability]
+      {}
+      {x : \sem G \rho \vdash \bindXtoYinZ {\rho_{up}(G)} x' \ret\thunk\ret x' \equidyn \ret\thunk \rho_{up}(G) : \u F U \u F \rho(\dynv)}
+
+      \inferrule*[Right=Retraction]
+      {}
+      {x : \sem G\vdash  \ret x\equidyn  \bindXtoYinZ {\rho_{up}(G)} y \rho_{dn}(G)  : \u F \sem G \rho}
+
+      \inferrule*[Right=Projection]
+      {}
+      {y : \rho(\dynv) \rho \vdash \bindXtoYinZ {\rho_{dn}(G)} x \rho_{up}(G) \ltdyn \ret y : \u F \rho(\dynv)}
+    \end{mathpar}
+
+    And for each computation ground type, an interpretation of the
+    downcast and upcast with $\rho(\dync)$ such that the downcast is
+    linear and the pair satisfy retraction and projection:
+    \begin{mathpar}
+      \inferrule
+      {}
+      {w : U \rho (\dync) \vdash \rho_{dn}(\u G) : \sem {\u G} \rho}
+
+      \inferrule
+      {}
+      {z : U \sem {\u G} \rho \vdash \rho_{up}(\u G) : \rho(\dync)}
+
+      \inferrule*[right=Linearity]
+      {}
+      {th : U\u F U \rho(\dync) \vdash \bindXtoYinZ {\force th} w \rho_{dn}(\u G) \equidyn \letXbeYinZ {\thunk (\bindXtoYinZ {\force th} {w'} \force w')} w \rho_{dn}(\u G)}
+
+      \inferrule*[right=Retraction]
+      {}
+      {z : U \sem {\u G} \rho \vdash \force z \equidyn
+        \letXbeYinZ {\rho_{up}(\u G)} w \rho_{dn}(\u G)
+        : \sem {\u G} \rho}
+
+      \inferrule*[right=Projection]
+      {}
+      {w : U \rho(\dync) \vdash
+        \letXbeYinZ {\thunk \rho_{dn}(\u G)} z \rho_{up}(\u G)
+        \ltdyn
+        \force w
+        : \rho(\dync)
+      }
+    \end{mathpar}
+\end{definition}
+
+Next, we show several possible interpretations of the dynamic type
+that all by construction satisfy the gradual guarantee.
+%
+First, we give the most ``natural'' translation.
+%
+An intuition is that to implement the value dynamic type $\dynv$ we
+need a pure function from each of the value tag types $G$, so the
+easiest way to achieve this is by making $\dynv$ a sum of the $G$s,
+with the downcast failing if it is the wrong case.
+%
+For the computation dynamic type, we need a linear function to each of
+the computation tag types $\u G$, so the easiest way to achieve this
+is by making $\dync$ a product of the $\u G$s, with the upcast failing
+on the other tags.
+
+\begin{definition}[Natural Dynamic Type Interpretation]
+  The following defines a $\dynv-\dync$ dynamic type interpretation.
+  %
+  First, we define $\rho(\dynv), \rho(\dync)$ as mutually recursive
+  and corecursive types, respectively.
+  \begin{align*}
+    \rho(\dynv) &= 1 + (\rho(\dynv) \times \rho(\dynv)) + (\rho(\dynv) + \rho(\dynv)) + U\rho(\dync) \\
+    \rho(\dync) &= (\rho(\dync) \with \rho(\dync)) \with (\rho(\dynv) \to \rho(\dync)) \with \u F \rho(\dynv)
+  \end{align*}
+  and define for each $G$,
+  \begin{align*}
+    \rho_{up}(G) &= \ret \intag{G} x\\
+    \rho_{dn}(G) &= \caseofXthenYelseZ y {\intag{G} x. \ret x}{\els. \err}
+  \end{align*}
+  and for each $\u G$
+  \begin{align*}
+    \rho_{dn}(\u G) &= \pi_{\u G}\force w\\
+    \rho_{up}(\u G) &= \pairWtoXYtoZ {\u G} {\force z} {\els} {\err}
+  \end{align*}
+\end{definition}
+\begin{proof}
+  We 
+\end{proof}
+
+The inclusion of sums, and negative products as tags on the dynamic
+type is uncommon in dynamically typed languages.
+%
+Instead, sums can be encoded using a pair of some atomic enumeration
+type and the payload.
+%
+The next interpreation we present is based on this idea.
+%
+We use booleans as the atomic enumeration for simplicity, but we could
+of course use some larger type of machine integers in an
+implementation.
+%
+Similarly, we can interpret the negative product type as a function.
+%
+Both of these encodings (sums as pairs, lazy pairs as functions)
+correspond to valid type isomorphisms in dependent type theory, where
+pairs are interpreted as a sigma type and functions as a pi type.
+%
+In addition, we can drop the $1$ case by interpreting it as one of the
+booleans.
+
+\begin{definition}[Sums-as-pairs Dynamic Type Interpretation]
+  The following defines a dynamic type interpretation.
+  \begin{align*}
+    \rho(\dynv) &= (1 + 1) + (\rho(\dynv) \times \rho(\dynv)) + U\rho(\dync) \\
+    \rho(\dync) &= (\rho(\dynv) \to \rho(\dync)) \with \u F \rho(\dynv)
+  \end{align*}
+  and define for each $G$,
+  \begin{align*}
+    \rho_{up}(1) &= \intag{2}\inl()\\
+    \rho_{up}(\dynv + \dynv) &= \caseofXthenYelseZ x {\inl y_1. \intag{\times}(\inl(), y_1)}{\inr y_2. \intag{\times}(\inr(), y_2)}\\
+    \rho_{up}(G) &= \intag{G} x \qquad \text{otherwise} \\
+  \end{align*}
+  and for each $\u G$
+  \begin{align*}
+    \rho_{dn}(\dync \with \dync) &= \lambda (bit:\dynv). \\% TODO: implement
+    \rho_{dn}(\u G) &= \pi_{\u G}\\
+    \rho_{up}(\u G) &= \pairWtoXYtoZ {\u G} {\force z} {\els} {\err}
+  \end{align*}
+\end{definition}
+
+\begin{definition}[CBV Dynamic Type Interpretation]
+  If we restrict the types of the gradual language to just the
+  call-by-value types, the following suffices
+  \begin{align*}
+    \rho(\dynv) &= 1 + (\rho(\dynv) + \rho(\dynv)) + (\rho(\dynv) \times \rho(\dynv)) + U(\rho(\dync))\\
+    \rho(\dync) &= \rho(\dynv) \to \u F \rho(\dynv)
+  \end{align*}
+\end{definition}
+
+\begin{definition}[CBN Dynamic Type Interpretation]
+  If we restrict the types of the gradual language to just the
+  call-by-name types, the following suffices
+  \begin{align*}
+    \rho(\dynv) &= (1 + 1)\\
+    \rho(\dync) &= (\rho(\dync) \with \rho(\dync)) \with (U\rho(\dync) \to \dync)
+    \with \u F \rho(\dynv)
+  \end{align*}
+\end{definition}
+
+\begin{theorem}[Type Preservation of Contract Translation]
+  Let $\rho$ be a dynamic type interpretation.
+  %
+  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.
+  \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.
+  \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.
+  \end{enumerate}
+  \begin{enumerate}
+  \item If $\Gamma \ltdyn \Gamma' \vdash M \ltdyn M' : \u B \ltdyn \u B'$,
+    then
+    \[
+    \sem{\Gamma}\rho \vdash \sem{M}\rho \ltdyn \sem{M'[\upcast{\Gamma}{\Gamma'}\Gamma']}
+    \]
+  \end{enumerate}
+\end{theorem}
+
+\begin{theorem}[Interpretation of Casts]
+  \begin{enumerate}
+  \item If $A \ltdyn A'$, then $\sem{\upcast A {A'}}\rho$ is
+    thunkable, and $\sem{\upcast A {A'}}$ and $\sem{\dncast {\u F
+        A}{\u F A}}$ are a value embedding-projection pair.
+  \item If $\u B \ltdyn \u B'$, then $\sem{\dncast {\u B} {\u
+      B'}}\rho$ is linear, and $\sem{\dncast {\u B} {\u B'}}\rho$ and
+    $\sem{\upcast {U \u B} {U \u B'}}$ are a computation
+    embedding-projection pair.
+  \end{enumerate}
+\end{theorem}
+\begin{theorem}[Coherence]
+  TODO
+\end{theorem}
+
+When combined with the logical relation interpretation of CBPV, this
+is our graduality theorem.
+\begin{theorem}[Dynamism Preservation of Contract Translation (Graduality Part 1)]
+  
+\end{theorem}
+
 \subsection{Call-by-push-value operational semantics}
 
 We present the operational semantics for our CBPV in figure TODO ref.