{\Phi\mid\Psi\vdash\pi' M \ltdyn\pi' M' : \u B_2 \ltdyn\u B_2'}
\end{mathpar}
\caption{GTT Term Dynamism (Compatibility Rules)}
\end{small}
\end{figure}
\begin{figure}
\begin{mathpar}
\inferrule
{\Gamma\vdash V : A \and A \ltdyn A'}
{\Gamma\vdash\upcast A {A'} V : A'}
\inferrule
{}
{x : A \vdash x \ltdyn\upcast A {A'} x : A \ltdyn A'}
\inferrule
{}
{x \ltdyn x' : A \ltdyn A' \vdash\upcast A {A'} x \ltdyn x' : A'}
\inferrule
{\Gamma\pipe\Delta\vdash M : \u B' \and\u B \ltdyn\u B'}
{\Gamma\pipe\Delta\vdash\dncast{\u B}{\u B'} M : \u B}
\inferrule
{}
{\bullet : \u B' \vdash\dncast{\u B}{\u B'}\bullet\ltdyn\bullet : \u B \ltdyn\u B'}
\inferrule
{}
{\bullet\ltdyn\bullet : \u B \ltdyn\u B' \vdash\bullet\ltdyn\dncast{\u B}{\u B'}\bullet : \u B}
\end{mathpar}
\caption{Casts in GTT}
\end{figure}
\subsection{Dynamic Types and Errors}
Since our language has two different kinds of types, we have several
...
...
@@ -788,6 +1275,57 @@ by taking just the subset of types that are sensible in Call-by-value.
The key feature of call-by-value is that all of its types are
interpreted as value types in call-by-push-value.
\begin{figure}
\begin{mathpar}
\begin{array}{lrcl}
\text{Types}& A &\bnfdef& 1 \alt (A + A) \alt (A \times A) \alt (A_1,\ldots,A_n) \to A\\
\text{Values}& V &\bnfdef&\upcast{A}{A'}V \alt () \alt\inl V \alt\inr V \alt (V,V) \alt\lambda (x_1:A_1,\ldots,x_n:A_n). M\\
\text{Terms}& M &\bnfdef&\err V \alt\alt\dncast{A}{A'}V \alt\caseofXthenYelseZ V {\inl x_1. M_1}{\inr x_2. M_2}\alt\pmpairWtoXYinZ V x y M \alt V(V_1,\ldots,V_n) \alt\bindXtoYinZ M x M \alt\letXbeYinZ V x M
\end{array}
\end{mathpar}
\begin{mathpar}
\inferrule
{\Gamma\vdash V : A \and A \ltdyn A'}
{\Gamma\vdash\upcast A {A'} V : A'}
\inferrule
{\Gamma\vdash V : A' \and A \ltdyn A'}
{\Gamma\vdash\dncast A {A'} V : A}
\inferrule
{}
{x : A' \vdash\dncast A A' x \ltdyn x : A \ltdyn A'}
\inferrule
{}
{x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn\dncast A {A'} x : A}
\end{mathpar}
\caption{CBV GTT}
\end{figure}
\begin{figure}
\begin{mathpar}
\inferrule
{A \ltdyn A' \and B \ltdyn B'}
{f : A \to B \vdash\dncast{A\to B}{A' \to B'} f \equidyn\lambda (x:A). \bindXtoYinZ{f(\upcast{A}{A'}x)} y \dncast{B}{B'} y}
\inferrule
{
f \ltdyn\lambda (x:A). \bindXtoYinZ{f(x)} y y
\and
\inferrule
{\inferrule
{\inferrule{f \ltdyn f'\and x \ltdyn\upcast{A}{A'}x}{{f(x)}\ltdyn f'(\upcast{A}{A'}x)}\and{y \ltdyn y' \vdash y \ltdyn\dncast{B}{B'} y}}
{x \ltdyn x : A \vdash\bindXtoYinZ{f(x)} y y \ltdyn\bindXtoYinZ{f'(\upcast{A}{A'}x)} y' \dncast{B}{B'} y}
}
{\lambda (x:A). \bindXtoYinZ{f(x)} y y \ltdyn\lambda (x:A). \bindXtoYinZ{f'(\upcast{A}{A'}x)} y' \dncast{B}{B'} y}
}
{f \ltdyn f' : A \to B \ltdyn A' \to B'
\vdash f \ltdyn\lambda (x:A). \bindXtoYinZ{f'(\upcast{A}{A'}x)} y' \dncast{B}{B'} y'}
\end{mathpar}
\caption{Uniqueness Principle for CBV Functions}
\end{figure}
\section{Theorems in Gradual Type Theory}
...
...
@@ -808,7 +1346,23 @@ Gradual Type Theory.
\subsection{Upcasts are Thunkable, Downcasts are Linear, a posteriori}
While we have shown
\begin{theorem}{Upcasts are (Complex) Values, Downcasts are (Complex) Stacks}
If the tagging upcasts are complex values and untagging downcasts
are stacks, then all upcasts are complex values and all downcasts
are complex stacks.
\end{theorem}
\begin{proof}
\end{proof}
\subsection{Retract Axiom}
In the call-by-name version of GTT (\cite{GTT}), there was an explicit
axiom that states that every pair of upcasts and downcasts forms a
section-retraction pair: i.e., that the downcast applied to the upcast
is the identity.
%
\subsection{Uniqueness Principles for Casts}
...
...
@@ -819,11 +1373,95 @@ principles of each type, given in figure TODO ref.
\begin{figure}
\begin{mathpar}
TODO
\upcast{0}{A}V \equidyn\absurd V\\
\dncast{\u F 0}{\u F A}\equidyn\err\\
\dncast{1}{\u B}\equidyn\{\}\\
\upcast{U 1}{U \u B}\equidyn\thunk\err\\
\end{mathpar}
\caption{Uniqueness Principles for Casts}
\end{figure}
To prove these uniqueness theorems, we use the fact that the
specification of upcasts and downcasts by their right and left
$\ltdyn$ rules defines them \emph{uniquely} up to $\equidyn$.
%
In category-theoretic terms this says that the upcasts and downcasts
have a \emph{universal property}, and so we can show that something
else is equivalent to the upcast or downcast by showing that it has
the \emph{same} property.
%
\begin{lemma}{Specification for Casts is a Universal Property}
If $A \ltdyn A'$ and $x : A \vdash V_u[x] : A'$ is a value such that
the following judgments are provable:
\begin{mathpar}
\inferrule
{}
{x : A \ltdyn x' : A' \vdash V_u[x] \ltdyn x' : A'}
\inferrule
{}
{x_2 : A \ltdyn x : A \vdash x_2 \ltdyn V_u[x] : A \ltdyn A'}
\end{mathpar}
then we can prove $x : A \vdash V_u[x]\equidyn x : A$.
Similarly, if $\u B \ltdyn\u B'$ and $\bullet : \u B' \vdash S_d :
\u B$ is a stack such that the following are provable:
\begin{mathpar}
\inferrule
{}
{\bullet\ltdyn\bullet : \u B' \vdash S_d \ltdyn\bullet : \u B \ltdyn\u B'}
\inferrule
{}
{\bullet\ltdyn\bullet : \u B \ltdyn\u B' \vdash\bullet\ltdyn S_d : \u B}
\end{mathpar}
then we can prove $\bullet : \u B' \vdash S_d \equidyn\dncast{\u B}{\u B'}\bullet : \u B$
\end{lemma}
\begin{proof}
\begin{mathpar}
\inferrule*[right=substitution]
{x_1 \ltdyn x_2 \vdash x_1 \ltdyn\upcast{A}{A'}x_2 : A \ltdyn A' \and x_1 \ltdyn x_2' : A \ltdyn A' \vdash V_u[x_1] \ltdyn x_2' : A'}
{x_1 : A \ltdyn x_2 : A \vdash V_u[x_1] \ltdyn\upcast{A}{A'} x_2 : A'}
\end{mathpar}
The other direction is essentially the same, but swapping $V_u$ and
the upcast.
\end{proof}
The other key ingredient to the uniqueness theorems is the
\emph{$\eta$ principle} and \emph{congruence rules} for each type.
%
The reason for this is that to show that an implementation of a cast
$x : A \vdash V_u : A'$ is correct, we have to show that it is less
than and greater than \emph{variables}: $x : A \ltdyn V_u[x]$ and $x
\ltdyn x' \vdash V_u[x]\ltdyn x'$.
%
Since we know nothing about a variable except it's type, the only way
to proceed is to $\eta$ expand it.
%
The uniqueness principles for casts arise when the two sides of the
cast have the \emph{same} top-level connective, and thus the
\emph{same}$\eta$ principle, so we $\eta$ expand both the lower
bounding and upper bounding variable, and the cast itself is a kind of
$\eta$-expansion \emph{up to cast at smaller type}.
% TODO: can we take advantage of duality???
%% With the large number of connectives comes a large number of proofs.
%% %
%% For each connective, we need four proofs: left and right rules for the
%% upcast and left and right rules for the downcast.
%% %
%% However, we can take advantage of the duality between upcasts and
%% downcasts and the duality between $\ltdyn$ and $\gtdyn$ to save some
%% effort, so that if we constrain our proof, we can mechanically turn a
%% single case, say the left rule for upcast into proofs of the other 3
%% cases.
%% %
%% In order for this duality to be \emph{perfect}, we use the version of
%% casts that are \emph{not} assumed to be
\section{Contract Translation to Call-by-push-value}
To show the soundness of our model, and demonstrate its relationship
...
...
@@ -2113,6 +2751,23 @@ the limit as $i \to \infty$.
equivalent to the graduality ordering.
\end{proof}
In fact, we can prove the converse, that at least for the term case,
our LR is \emph{complete} with respect to contextual graduality
\begin{lemma}{Logical Preorder is Complete wrt Contextual Preorder}
For any $\apreorder$, if $\Gamma\vDash M \ctxize\apreorder N \in
\u B$, then $\Gamma\vDash M \ilrof\apreorder\omega{} N \in\u B$.
\end{lemma}
\begin{proof}
Let $S_1\ilrof\apreorder i {\u B} S_2$ and $\gamma_1\ilrof
\apreorder i \Gamma\gamma_2$. We need to show that
\[
S_1[M[\gamma_1]]\ix\apreorder i S_2[N[\gamma_2]]
\]
We use \emph{reflexivity} of the relation:
TODO: adapt the old proof of this below
\end{proof}
This establishes that our logical relation can prove graduality, so it
only remains to show that our \emph{inequational theory} implies our
logical relation.
...
...
@@ -2192,7 +2847,40 @@ limit is a consequence.
TODO
\end{lemma}
% Lemma: relation is a module of the ordering/infinite relation
\begin{lemma}{$\precltdyn$ and $\ltdynsucc$ are Models of CBPV}
\begin{enumerate}
\item If $\Gamma\vdash M_1\ltdyn M_2 : \u B$, then
\[\Gamma\vDash M_1\ix\precltdyn\omega M_2\in\u B \]
and
\[\Gamma\vDash M_1\ix\ltdynsucc\omega M_2\in\u B \]
\item If $\Gamma\vdash V_1\ltdyn V_2 : A$, then
\[\Gamma\vDash V_1\ix\precltdyn\omega V_2\in A
\]
\[\Gamma\vDash V_1\ix\ltdynsucc\omega V_2\in A
\]
\item If $\Gamma\pipe\bullet : \u B \vdash S_1\ltdyn S_2 : \u C$ , then
\[\Gamma\pipe\bullet : \u B \vDash S_1\ix\precltdyn\omega S_2\in\u C \]
and
\[\Gamma\pipe\bullet : \u B \vDash S_1\ix\ltdynsucc\omega S_2\in\u C \]
\end{enumerate}
\end{lemma}
\begin{theorem}{$\ctxize\ltdyn$ is a Model of CBPV}
\begin{enumerate}
\item If $\Gamma\vdash M_1\ltdyn M_2 : \u B$, then
\[\Gamma\vDash M_1\ctxize\ltdyn M_2\in\u B \]
\item If $\Gamma\vdash V_1\ltdyn V_2 : A$, then
\[\Gamma\vDash V_1\ctxize\ltdyn V_2\in A \]
\item If $\Gamma\pipe\bullet : \u B \vdash S_1\ltdyn S_2 : \u C$, then
\[\Gamma\pipe\bullet : \u B \vDash S_1\ctxize\ltdyn S_2\in\u C \]
\end{enumerate}
\end{theorem}
\begin{proof}
TODO: prose
Logical by prev lemma
Logical => Contextual by soundness
Contextual of the 2 => Contextual ltdyn by earlier lemma
