@@ -616,8 +624,6 @@ Generalizing further, a stack out of an iterated function type $A_1
\subsection{Casts}
It is not immediately obvious how to add type casts to
call-by-push-value, but we can use previous work on call-by-value and
call-by-name gradual typing, combined with the embeddings of CBV and
...
...
@@ -706,6 +712,35 @@ TODO: do we actually know what would go wrong in that case?
%% Then for every type A, there are CBV coreflections (e(x) = inc; ret x | p(y) = dec; ret y)
\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 Type(s)}
\subsection{Embedding Call-by-Value}
...
...
@@ -723,6 +758,57 @@ 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}
...
...
@@ -743,7 +829,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}
...
...
@@ -754,11 +856,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
