\documentclass{article}
\usepackage{float}
\usepackage{amsmath,amssymb, amsthm}
\usepackage{tikz-cd}
\usepackage{mathpartir}
\usepackage{rotating}
\newtheorem{theorem}{Theorem}
\newtheorem{definition}{Definition}
\newcommand{\vtype}{\,\,\text{val type}}
\newcommand{\ctype}{\,\,\text{comp type}}
\newcommand{\ctx}{\,\,\text{ctx}}
\newcommand{\stoup}{\,\,\text{stoup}}
\newcommand{\pipe}{\,\,|\,\,}
\newcommand{\hole}{\bullet}
\renewcommand{\u}{\underline}
\newcommand{\ltdyn}{\sqsubseteq}
\newcommand{\gtdyn}{\sqsupseteq}
\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
\newcommand{\ltdynv}{\mathrel{\sqsubseteq_V}}
\newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
\newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
\newcommand{\dyn}{{?}}
\newcommand{\dynv}{{?}}
\newcommand{\dync}{\u {\text{?`}}}
\newcommand{\uarrow}{\mathrel{\rotatebox[origin=c]{-30}{$\leftarrowtail$}}}
\newcommand{\darrow}{\mathrel{\rotatebox[origin=c]{30}{$\twoheadleftarrow$}}}
\newcommand{\upcast}[2]{\langle{#2}\uarrow{#1}\rangle}
\newcommand{\dncast}[2]{\langle{#1}\darrow{#2}\rangle}
\newcommand{\err}{\mho}
\newcommand{\roll}{\text{roll}\,\,}
\newcommand{\unroll}{\text{unroll}\,\,}
\newcommand{\Set}{\text{Set}}
\newcommand{\relto}{\to}
\newcommand{\M}{\mathcal{M}}
\newcommand{\sq}{\square}
\newcommand{\lett}{\text{let}\,\,}
\newcommand{\too}{\text{to}\,\,}
\newcommand{\case}{\text{case}\,\,}
\newcommand{\ret}{\text{ret}\,\,}
\newcommand{\thunk}{\text{thunk}\,\,}
\newcommand{\force}{\text{force}\,\,}
\begin{document}
\title{Gradual Call-By-Push-Value}
\author{Max S. New, Daniel R. Licata and Amal Ahmed}
\maketitle
There are 5 basic judgments of call-by-push-value: value types,
computation types, values (many value types as input, value type as
output), terms (many value types as input, computation type as output)
and stacks (many value types and one computation type as input,
computation type as output) (also equality?).
%
We combine the term and stack judgments into one term judgment with a
``stoup'': i.e. at most one variable (the hole).
%
Gradual Call-by-push-value adds an ordering form for each of these
judgments: value type dynamism, computation type dynamism, value
dynamism, term (and stack) dynamism.
\begin{figure}[H]
\begin{mathpar}
A \vtype \and
\inferrule
{}
{A_1 \ltdyn A_2}\\
\underline{B} \ctype\and
\inferrule
{}
{\underline{B}_1 \ltdyn \underline{B}_2}\\
\Gamma \ctx
\Phi : \Gamma_1 \ltdyn \Gamma_2\\
\inferrule
{\Gamma \ctx \and A \vtype}
{\Gamma \vdash v : A}
\inferrule
{\Phi : \Gamma_1 \ltdyn \Gamma_2 \and A_1 \ltdyn A_2}
{\Phi \vdash v_1 \ltdyn v_2 : A_1 \ltdyn A_2}\\
\Delta \stoup
\Psi : \Delta_1 \ltdyn \Delta_2\\
\inferrule
{\Gamma \ctx \and B \ctype}
{\Gamma \vdash M : \underline B}
\inferrule
{\Phi : \Gamma_1 \ltdyn \Gamma_2 \and
\Psi : \Delta_1 \ltdyn \Delta_2 \\
\Gamma_1\pipe\Delta_1 \vdash M_1 : \u B_1\\
\Gamma_2\pipe\Delta_2 \vdash M_2 : \u B_2\\
\u B_1 \ltdyn \u B_2}
{\Phi\pipe\Psi \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2}\\
\end{mathpar}
\caption{GCBPV Judgment Presuppositions}
\end{figure}
Call-by-push-value includes 5 kinds of substitution: we can substitute
values for variables in values, terms and stacks and we can plug
terms and stacks into the hole $\hole$ of a stack.
%
Furthermore, there are the 2 forms of identity: value variable usage
in a value and hole usage in a stack.
%
The orderings of GCBPV are all congruences with respect to these
notions of composition and their corresponding identities.
%
Additionally, there are rules making each of the orderings into
\emph{preorders}: i.e., there are reflexivity and transitivity rules
for each.
\begin{figure}[H]
\begin{mathpar}
\inferrule
{}
{\cdot \ctx}
\inferrule
{\Gamma \ctx \and A \vtype}
{\Gamma, x : A \ctx}\\
\inferrule
{}
{\cdot \stoup}
\inferrule
{\u B \ctype}
{\hole : \u B \stoup}\\
\inferrule
{}
{\Gamma,x:A,\Gamma' \vdash x : A}
\inferrule
{}
{\Phi,x_1 \ltdyn x_2 : A_1 \ltdyn A_2,\Phi' \vdash x_1 \ltdyn x_2 : A_1 \ltdyn A_2}\\
\inferrule
{\forall{x' : A' \in \Gamma'}.~ \Gamma \vdash \gamma (x') : A'\and
\Gamma \vdash v : A
}
{\Gamma \vdash v[\gamma] : A}
\inferrule
{\Phi' \vdash v_1 \ltdyn v_2 : A_1 \ltdyn A_2\\
\forall (x_1' \ltdyn x_2' : A_1' \ltdyn A_2' \in \Phi'). \Phi \vdash \gamma_1(x_1') \ltdyn \gamma_2(x_2') : A_1' \ltdyn A_2'
}
{\Phi \vdash v_1[\gamma_1] \ltdyn v_2[\gamma_2] : A_1 \ltdyn A_2}\\
\inferrule
{\forall{x' : A' \in \Gamma'}.~ \Gamma \vdash \gamma(x') : A'\and
\Gamma\pipe \Delta \vdash M : \u B
}
{\Gamma\pipe\Delta \vdash M[\gamma] : \u B}
\inferrule
{\Phi'\pipe\Psi \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2\\
\forall (x_1' \ltdyn x_2' : A_1' \ltdyn A_2' \in \Phi'). \Phi \vdash \gamma_1(x_1') \ltdyn \gamma_2(x_2') : A_1' \ltdyn A_2'
}
{\Phi\pipe\Psi \vdash M_1[\gamma_1] \ltdyn M_2[\gamma_2] : \u B_1 \ltdyn \u B_2}\\
\inferrule{}{\Gamma\pipe \hole : \u B \vdash \hole : \u B}
\inferrule{}{\Phi\pipe \hole \ltdyn \hole : \u B_1 \ltdyn \u B_2 \vdash \hole \ltdyn \hole : \u B_1 \ltdyn \u B_2}
\inferrule
{\Gamma\pipe\Delta \vdash M : \u B \and \Gamma \pipe \hole : \u B \vdash S : \u C}
{\Gamma\pipe\Delta \vdash \u B \vdash S[M/\hole] : \u C}
\inferrule
{\Phi\pipe\Psi \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2 \and \Phi \pipe \hole \ltdyn \hole : \u B_1 \ltdyn \u B_2 \vdash S_1 \ltdyn S_2 : \u C_1 \ltdyn \u C_2}
{\Phi\pipe\Psi \vdash \u B_1 \ltdyn \u B_2 \vdash S_1[M_1/\hole]\ltdyn S_2[M_2/\hole] : \u C_1 \ltdyn \u C_2}
\end{mathpar}
\caption{GCBPV Basic Judgmental Rules 1 (Contexts, Identities, Substitutions)}
\end{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{}
{A \ltdyn A}
\inferrule
{A_1 \ltdyn A_2 \and A_2 \ltdyn A_3}
{A_1 \ltdyn A_3}\\
\inferrule
{}
{\u B \ltdyn \u B}
\inferrule
{\u B_1 \ltdyn \u B_2 \and \u B_2 \ltdyn \u B_3}
{\u B_1 \ltdyn \u B_3}\\
\inferrule
{}
{\Phi_{\Gamma} : \Gamma \ltdyn \Gamma}
\inferrule
{\Phi : \Gamma_1 \ltdyn \Gamma_2 \and \Phi' : \Gamma_2 \ltdyn \Gamma_3}
{\Phi'' : \Gamma_1 \ltdyn \Gamma_3}\\
\inferrule
{\Gamma \vdash v : A}
{\Gamma \ltdyn \Gamma \vdash v \ltdyn v : A \ltdyn A}
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : A_1\ltdyn A_2 \and
\Phi' \vdash v_2 \ltdyn v_3 : A_2\ltdyn A_3 \and
}
{\Phi'' \vdash v_1 \ltdyn v_3 : A_1 \ltdyn A_3}\\
\inferrule
{\Gamma \vdash M : \u B}
{\Gamma \vdash M \ltdyn M : \u B \ltdyn \u B}
\inferrule
{\Phi \vdash M_1 \ltdyn M_2 : \u B_1\ltdyn \u B_2 \and
\Phi' \vdash M_2 \ltdyn M_3 : \u B_2\ltdyn \u B_3 \and
}
{\Phi'' \vdash M_1 \ltdyn M_3 : \u B_1 \ltdyn \u B_3}\\
\inferrule
{\Gamma\pipe \hole : \u B \vdash M : \u C}
{\Gamma\pipe \hole : \u B \vdash M \ltdyn M : \u C \ltdyn \u C}
\inferrule
{\Phi \pipe \hole : \u B_1\ltdyn \u B_2 \vdash S_1 \ltdyn S_2 : \u C_1\ltdyn \u C_2 \and
\Phi'\pipe \hole : \u B_2\ltdyn \u B_3\vdash S_2 \ltdyn S_3 : \u C_2\ltdyn \u C_3 \and
}
{\Phi''\pipe \hole : \u B_1\ltdyn \u B_3 \vdash S_1 \ltdyn S_3 : \u C_1 \ltdyn \u C_3}
\end{mathpar}
\caption{GCBPV Basic Judgmental Rules 2 (Reflexivities, Transitivities)}
\end{figure}
A na\"ive attempt to add casts in the style of cbn gradual type theory
(TODO: cite) would be to add an upcast and downcast \emph{values} for
every value type dynamism judgment and upcast and downcast
\emph{stacks} for every computation type dynamism judgment.
%
However, this does not match pre-existing work on gradual typing: if a
downcast is a value, then that means a type error is a value?
%
Dually, if a function upcast were a stack, that would mean it
\emph{has} to call the function it is casting, but if the downcast on
the input fails, the function will never be invoked.
%
We have forgotten the translation of call-by-name into
call-by-push-value: the call-by-name casts would not be stacks $\u B
\multimap \u C$ but \emph{co-Kleisli} arrows $U(\u B) \to \u C$.
%
While this gives us a correct translation of cbn GTT, it violates the
judgmental approach since now casts need the presence of the $U$ type
in order to be defined.
%
Furthermore, our original na\"ive attempt had something going for it:
upcasts in call-by-value \emph{are} pure functions and downcasts in
call-by-name \emph{are} linear, but there is no way to prove this if
we assume casts are given by Kleisli and co-Kleisli morphisms.
Fortunately, there is a simple resolution to all of these problems
that is actually \emph{simpler} than our na\"ive approach: value type
dynamism induces a pure value upcast and computation type dynamism
induces a linear stack downcast, and \emph{no other casts are
primitive}.
%
The downcast on value types and upcast on computation types will then
be \emph{derived} using the $F,U$ adjoint type constructors, which
will both be defined to be \emph{monotone} with respect to type
dynamism.
\begin{figure}[H]
\begin{mathpar}
\inferrule
{\Gamma \vdash v : A_1 \and A_1 \ltdyn A_2}
{\Gamma \vdash \upcast{A_1}{A_2} v : A_2}
\inferrule
{A_1 \ltdyn A_2}
{x_1 : A_1 \vdash x_1 \ltdyn \upcast{A_1}{A_2} x_1 : A_1 \ltdyn A_2}
\inferrule
{A_1 \ltdyn A_2}
{x_1 \ltdyn x_2 : A_1 \ltdyn A_2 \vdash \upcast{A_1}{A_2} x_1 \ltdyn x_2 : A_2}\\
\inferrule
{\Gamma\pipe \Delta \vdash M : \u B_2 \and \u B_1 \ltdyn \u B_2}
{\Gamma\pipe \Delta \vdash \dncast{\u B_1}{\u B_2} M : \u B_1}
\inferrule
{\u B_1 \ltdyn \u B_2}
{\cdot\pipe \hole : \u B_2 \vdash \dncast{\u B_1}{\u B_2}{\hole} \ltdyn \hole : \u B_1 \ltdyn \u B_2}
\inferrule
{\u B_1 \ltdyn \u B_2}
{\cdot\pipe \hole \ltdyn \hole : \u B_1 \ltdyn \u B_2 \vdash {\hole} \ltdyn \dncast{\u B_1}{\u B_2} \hole : \u B_1}
\end{mathpar}
\caption{Upcasts and Downcasts (Would be simpler with a Stoup)}
\end{figure}
\subsection{Exponentials}
Next, we add the $\u F$ and $U$ types that mediate between the worlds
of values and computations. The $\u F$ type takes a value type and
makes the computation type of ``things that may eventually return
values of type $A$''. In CBPV, the $\u F$ type is a lot like the
monadic type in Moggi's metalanguage in that a call-by-value ``term''
is interpreted as a computation whose type is $\u F A$. To produce an
$\u F A$ we return a value, and to consume one, we let-bind its
eventual value to a variable and proceed. The $\beta$ rule says that
returning a value and then let-binding it should be that same as
substituting the value in and the $\eta$ rule says that any term where
an $\u F$ type is in elimination position is equivalent to let-binding
it.
On the other side, the $U$ type constructor turns a computation into a
\emph{thunked} value that can be \emph{forced} to perform its effect
(in a term judgment of course).
In \emph{Gradual} call-by-push-value, following the dogma of gradual
type theory, we simply ``make everything monotone''.
%
With this, we can get our ``missing'' downcasts between value types
and upcasts between computation types: they are in the image of $\u F,
U$ respectively.
%
Both constructors define \emph{monotone functors} and it is a general
theorem that monotone functors preserve representability, so we get
that for $\u F$ and $U$ types, we have both an upcast and a downcast
from a preordering.
\begin{figure}[H]
\begin{mathpar}
\inferrule
{A \vtype}
{\u F A \ctype}
\inferrule
{A_1 \ltdyn A_2}
{\u F A_1 \ltdyn \u F A_2}\\
\inferrule
{\Gamma \vdash v : A}
{\Gamma\pipe\cdot \vdash \ret v : \u F A}
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : A_1 \ltdyn A_2}
{\Phi\pipe\cdot \vdash \ret v_1 \ltdyn \ret v_2 : \u F A_1 \ltdyn \u F A_2}\\
\inferrule
{\Gamma \pipe\Delta \vdash M : \u F A\and
\Gamma, x : A \vdash N : \u B}
{\Gamma \pipe \Delta \vdash \lett x = M; N : \u B}
\inferrule
{\Phi \pipe\Psi \vdash M_1 \ltdyn M_2 : \u F A_1 \ltdyn \u F A_2 \\
\Phi, x_1\ltdyn x_2 : A_1 \ltdyn A_2 \pipe \cdot \vdash N_1 \ltdyn N_2 : \u B_1 \ltdyn \u B_2}
{\Phi \pipe \Psi \vdash \lett x_1 = M_1; N_1 \ltdyn \lett x_2 = M_2; N_2 : \u B_1 \ltdyn \u B_2}\\
\inferrule
{}
{\lett x = \ret v; N \equidyn N[v/x]}
\inferrule
{}
{\lett x = \ret y; N \equidyn N[y/x]}
\inferrule
{\Gamma\pipe\Delta \vdash N : \u F A}
{M[N/\hole] \equidyn \lett x = N; M[\ret x/\hole]}
\inferrule
{\Gamma \pipe \hole : \u F A \vdash M : \u B}
{M \equidyn \lett x = \hole; M[\ret x/\hole]}
\\
\inferrule
{\u B \ctype}
{U \u B \vtype}
\inferrule
{\u B_1 \ltdyn \u B_2}
{U \u B_1 \ltdyn U \u B_2}\\
\inferrule
{\Gamma\pipe \cdot \vdash M : \u B}
{\Gamma \vdash \thunk M : U \u B}
\inferrule
{\Phi\pipe \cdot \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2}
{\Phi \vdash \thunk M_1 \ltdyn \thunk M_2 : U \u B_1 \ltdyn U \u B_2}\\
\inferrule
{\Gamma \vdash v : U \u B}
{\Gamma\pipe \cdot \vdash \force v : \u B}
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : U \u B_1 \ltdyn U \u B_2}
{\Phi\pipe \cdot \vdash \force v_1 \ltdyn \force v_2 : \u B_1 \ltdyn \u B_2}\\
\inferrule
{}
{\force \thunk M \equidyn M}
\inferrule
{}
{\force \thunk \hole \equidyn \hole}\\
\inferrule
{}
{\thunk \force v \equidyn v}
\inferrule
{}
{\thunk \force x \equidyn x}
\end{mathpar}
\caption{Adjunction Constructors (Stoupified) Beta and Eta are presented with and without cuts}
\end{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{\Gamma, x : A_1 \vdash \upcast {A_1} {A_2} x : A_2}
{\Gamma\pipe \hole : \u F A_1 \vdash \lett x = \hole; \ret \upcast {A_1} {A_2} x : \u F A_2}
\inferrule
{A_1 \ltdyn A_2}
{\cdot \pipe \hole : \u F A_1 \vdash \hole \ltdyn \lett x = \hole; \ret \upcast {A_1} {A_2} x : \u F A_1 \ltdyn \u F A_2}
\inferrule
{A_1 \ltdyn A_2}
{\cdot \pipe \hole \ltdyn \hole : \u F A_1 \ltdyn \u F A_2 \vdash \lett x_1 = \hole; \ret \upcast {A_1} {A_2} x_1 \ltdyn \hole : \u F A_2}
\inferrule
{\Gamma \pipe \hole : \u B_2 \vdash \dncast {\u B_1} {\u B_2} \hole : \u B_1}
{\Gamma, x: U \u B_2 \vdash \thunk \dncast {\u B_1} {\u B_2} \force x : U \u B_1}
\inferrule
{\u B_1 \ltdyn \u B_2}
{x : U \u B_2 \vdash \thunk \dncast {\u B_1}{\u B_2} \force x \ltdyn x : U \u B_1 \ltdyn U \u B_2}
\inferrule
{\u B_1 \ltdyn \u B_2}
{x_1 \ltdyn x_2 : U \u B_1 \ltdyn U \u B_2 \vdash x_1 \ltdyn \thunk \dncast {\u B_1}{\u B_2} \force x_2 : U \u B_1}
\end{mathpar}
\caption{Functoriality Preserves Representability (Theorem Statments)}
\end{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule*
{\hole \ltdyn \lett x = \hole; \ret x \and
\inferrule*
{\hole \ltdyn \hole \and
\inferrule*
{x : \u F A_1 \vdash x \ltdyn \upcast {A_1}{A_2} x}
{x : \u F A_1 \vdash \ret x \ltdyn \ret \upcast {A_1}{A_2} x}
}
{\hole:\u F A_1 \vdash \lett x = \hole; \ret x \ltdyn \lett x = \hole; \ret \upcast {A_1} {A_2} x}
}
{\cdot \pipe \hole : \u F A_1 \vdash \hole \ltdyn \lett x = \hole; \ret \upcast {A_1} {A_2} x : \u F A_1 \ltdyn \u F A_2}
\inferrule*
{\inferrule*
{\hole \ltdyn \hole \and
\inferrule
{{x_1 \ltdyn x_2 : A_1 \ltdyn A_2 \vdash \upcast {A_1} {A_2} x_1 \ltdyn x_2}}
{x_1 \ltdyn x_2 : A_1 \ltdyn A_2 \vdash \ret \upcast {A_1} {A_2} x_1 \ltdyn \ret x_2}}
{\lett x_1 = \hole; \ret \upcast {A_1} {A_2} x_1 \ltdyn\lett x_2 = \hole; \ret x_2}
\and
\hole \ltdyn \lett x_2 = \hole; \ret x_2
}
{\cdot \pipe \hole \ltdyn \hole : \u F A_1 \ltdyn \u F A_2 \vdash \lett x_1 = \hole; \ret \upcast {A_1} {A_2} x_1 \ltdyn \hole : \u F A_2}
\inferrule
{\inferrule
{\inferrule
{{x : U \u B_2 \vdash \force x \ltdyn \force x : U \u B_1 \ltdyn U \u B_2}}
{x : U \u B_2 \vdash \dncast {\u B_1}{\u B_2} \force x \ltdyn \force x : U \u B_1 \ltdyn U \u B_2}}
{x : U \u B_2 \vdash \thunk \dncast {\u B_1}{\u B_2} \force x \ltdyn \thunk \force x : U \u B_1 \ltdyn U \u B_2}
\and \thunk \force x \ltdyn x
}
{x : U \u B_2 \vdash \thunk \dncast {\u B_1}{\u B_2} \force x \ltdyn x : U \u B_1 \ltdyn U \u B_2}
\inferrule
{x_1 \ltdyn \thunk \force x_1\and
\inferrule
{\inferrule
{\inferrule
{{x_1 \ltdyn x_2 : U \u B_1 \ltdyn U \u B_2 \vdash x_1 \ltdyn x_2 : U \u B_1 \ltdyn U \u B_2}}
{x_1 \ltdyn x_2 : U \u B_1 \ltdyn U \u B_2 \vdash \force x_1 \ltdyn \force x_2 : \u B_1 \ltdyn \u B_2}}
{x_1 \ltdyn x_2 : U \u B_1 \ltdyn U \u B_2 \vdash \force x_1 \ltdyn \dncast {\u B_1}{\u B_2} \force x_2 : \u B_1}}
{x_1 \ltdyn x_2 : U \u B_1 \ltdyn U \u B_2 \vdash \thunk \force x_1 \ltdyn \thunk \dncast {\u B_1}{\u B_2} \force x_2 : U \u B_1}
}
{x_1 \ltdyn x_2 : U \u B_1 \ltdyn U \u B_2 \vdash x_1 \ltdyn \thunk \dncast {\u B_1}{\u B_2} \force x_2 : U \u B_1}
\end{mathpar}
\caption{Functoriality Preserves Representability (Proofs)}
\end{figure}
\subsection{Dynamic Types}
\begin{figure}[H]
\begin{mathpar}
\inferrule{}{\dynv \vtype}
\inferrule{}{\dync \ctype}
\inferrule{A \vtype}{A \ltdyn \dynv}
\inferrule{\u B \ctype}{\u B \ltdyn \dync}
\end{mathpar}
\caption{Dynamic Types}
\end{figure}
\section{Connectives and Contract Uniqueness Theorems}
Next we consider the contract uniqueness theorems for the connectives
of call-by-push-value.
%
First, an abstract perspective on the following theorems.
%
The primitive rules of upcasts and downcasts covariantly assign an
upcast $\upcast {A}{A'}$ to any value type dynamism judgment $A \ltdyn
A'$ and contravariantly assign a downcast $\dncast {\u B}{\u B'}$ to
any computation type dynamism judgment $\u B \ltdyn \u B'$.
%
Next, note that \emph{every} type constructor in call-by-push-value is
jointly functorial in its arguments, with the domain of the function
type being the only contravariant position of any of the connectives
(though if we have EEC connectives, it's more complex).
%
When these two variances align, the contract uniqueness theorem is
very simple.
%
We call any connective where all \emph{covariant} arguments are of the
same \emph{sort} (i.e., value vs computation type) and all
\emph{contravariant} arguments are of the opposite sort a \emph{nice}
connective.
%
Then every nice connective has a nice uniqueness theorem for its
same-sorted cast, i.e., upcasts for value types and downcasts for
computation types.
The only two connectives in CBPV that are not \emph{nice} are the $\u
F$ and the $U$ types since each are covariant in their argument but
swap sorts.
%
And correspondingly, neither of these types has a fully general
contract uniquness theorem.
%
That is, for a base value type dynamism $X_1 \ltdyn X_2$, we have no
contract uniqueness theorem for the downcast given by $\u F X_1 \ltdyn
\u F X_2$.
%
However, that's not to say that $\u F$ and $U$ have \emph{no}
associated uniqueness principles: instead, we will show in what
follows that the application of $\u F$ or $U$ to any connective can be
shown to have a uniqueness principle.
%
Unlike with functoriality, we do not know the general principle, but
it seems closely related to work on so-called ``direct models'' of
effectful computation, i.e. Freyd Categories, Fuhrmann's Abstract
Kleisli Categories and Munch-Maccagnoni's duploids.
\begin{theorem}[Admissibility of (Almost All) Downcasts]
Any upcast or downcast associated to a cut-free type dynamism
judgment (i.e., one only built out of monotonicity rules) in gradual
call-by-push-value is equivalent to a term whose only upcasts and
downcasts are those that are ``axiomatically undetermined'': defined in
figure \ref{axiomatically-free}.
\end{theorem}
\begin{proof}
We prove the theorem by induction on dynamism derivations with $4$
mutually recursive cases
\begin{mathpar}
\inferrule{A \ltdyn A'}{\upcast A {A'}}
\inferrule{A \ltdyn A'}{\dncast{\u F A}{\u F A'}}
\inferrule{\u B \ltdyn \u B'}{\dncast{\u B}{\u B'}}
\inferrule{\u B \ltdyn \u B'}{\upcast{U \u B}{U \u B'}}
\end{mathpar}
The cases are all in other sections, we record them here to state
precisely the inductive structure of the proof and cover the trivial
cases (units).
\begin{enumerate}
\item Value Types
\begin{enumerate}
\item $1 \ltdyn 1$: upcast is identity, by decomposition theorem,
similarly for downcast.
\item $A_1 \times A_2 \ltdyn A_1' \times A_2'$: see multiplicatives and use the inductive hypothesis.
\item $0 \ltdyn 0$: By $\eta$ for $0$, must be $\case x \{ \}$,
similarly the downcast must be equivalent to $\lett x = \bullet; \case x \{ \}$.
\item $A_1 + A_2 \ltdyn A_1' + A_2'$: see additives and use
inductive hypothesis
\item $U \u B \ltdyn U \u B'$: by inductive hypothesis on $\u B
\ltdyn \u B'$, there is an upcast $U \u B \ltdyn U \u B'$. For
the downcast, we need a downcast $\dncast{\u F U \u B}{\u F U \u
B'}$, for which we use the inductive hypothesis for $\u B
\ltdyn \u B'$ and the functoriality of $U, \u F$ (see the
exponential section).
\end{enumerate}
\item Computation Types.
\begin{enumerate}
\item $\top \ltdyn \top$: by $\eta$ for $\top$, the downcast must by $\{\}$. Similarly, the upcast must be $\thunk\{\}$
\item $\inferrule{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2'}{A_1 \times
A_2 \ltdyn A_1' \times A_2'}$ See additives section and use the
inductive hypotheses
\item $\inferrule{A \ltdyn A' \and \u B \ltdyn \u B'}{A \to \u B
\ltdyn A \to \u B'}$ See multiplicatives section and use the
inductive hypotheses.
\item $\inferrule{A \ltdyn A'}{\u F A \ltdyn \u F A'}$ for the
downcast, use the inductive hypothesis. For the upcast, use the
inductive hypothesis and see the exponential section.
\end{enumerate}
\end{enumerate}
\end{proof}
\begin{figure}
\begin{mathpar}
1 \ltdyn \dynv
\dynv \times \dynv \ltdyn \dynv
\dynv + \dynv \ltdyn \dynv
U \dync \ltdyn \dynv\\
\dync \wedge \dync \ltdyn \dync
\dynv \to \dync \ltdyn \dync
\u F \dynv \ltdyn \dync
\end{mathpar}
\caption{Cut-Free Type Dynamism (with $\dynv, \dync$)}
\end{figure}
\begin{figure}
\begin{mathpar}
\upcast{T}{\dynv}
\upcast{U \u M}{U \dync}
\dncast{\u M}{\dync}
\dncast{\u F T}{\u F \dynv}
\end{mathpar}
\caption{Axiomatically Undetermined Upcasts, Downcasts}
\label{axiomatically-free}
\end{figure}
\subsection{Additive Connectives: Positive Sum, Negative Product}
First, we introduce the sum type, which is a \emph{value} type
constructor.
%
It has two value constructors $\sigma$ and $\sigma'$ for the left and
right injections.
%
It's universal property is given by case analysis.
%
It should have this universal property \emph{any} time it appears as a
variable, which means that we need case analysis values, computations
and stacks.
%
Having two different, seemingly unrelated forms of pattern matching
looks problematic, but they are not unrelated, we can show that
substituting a value with a pattern match into a term is equivalent to
first lifting the pattern match out of the term and then substituting.
%
This theorem is key to the proof that complex values can be
eliminated.
We also have the \emph{computation product}, which is a cartesian
product and we write $\wedge$.
%
Unlike the positive, value product, this is defined by the
projections.
%
Its constructor is analogous to the elimination form for the sum.
Both satisfy contract uniqueness principles.
%
First, we have the ``natural'' uniqueness principles: the upcast
between sums is a pattern match and then cast and dually the downcast
for products is a copattern match and then cast.
%
Second we have the ``expat'' uniquness principles that are a bit more
complex.
%
The expat uniqueness principles are in the ``wrong'' category: i.e.,
it is the downcast for the sum type (a value type) under an $\u F$,
and vice-versa the upcast for the product under a $U$.
\begin{align*}
M[\case v \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \}/x_+ ]
&=
M[\case y \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \}/x_+][v/y]\\
&\equidyn
(\case y \{ \\ &\qquad
\sigma x \mapsto M[\case \sigma x \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \}/x_+]\\ &\qquad
\pipe \sigma' x' \mapsto M[\case \sigma' x' \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \}/x_+]\\ &\quad
\})[v/y] \\
&\equidyn
(\case y \{ \\ &\qquad
\sigma x \mapsto M[v_k /x_+]\\ &\qquad
\pipe \sigma' x' \mapsto M[v_k'/x_+]\\ &\quad
\})[v/y] \\
&=
\case v \{ \sigma x \mapsto M[v_k/x_+] \pipe \sigma' x' \mapsto M[v_k'/x_+] \}
\end{align*}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{A \vtype \and A' \vtype}
{A + A' \vtype}
\inferrule
{A_1 \ltdyn A_2 \and A_1' \ltdyn A_2'}
{A_1 + A_1' \ltdyn A_2 + A_2'}\\
\inferrule
{\Gamma \vdash v : A}
{\Gamma \vdash \sigma_{A,A'} v : A + A'}
\inferrule
{\Gamma \vdash v' : A'}
{\Gamma \vdash \sigma'_{A,A'} v' : A + A'}
\inferrule
{v_1 \ltdyn v_2 : A_1 \ltdyn A_2 \and A_1' \ltdyn A_2'}
{\sigma v_1 \ltdyn \sigma v_2 : A_1 + A_1' \ltdyn A_2 + A_2'}
\inferrule
{v_1' \ltdyn v_2' : A_1' \ltdyn A_2' \and A_1 \ltdyn A_2}
{\sigma' v_1' \ltdyn \sigma' v_2' : A_1 + A_1' \ltdyn A_2 + A_2'}
\inferrule
{\Gamma \vdash v : A + A'\and
\Gamma, x:A \vdash v_k : A_3\and
\Gamma, x':A' \vdash v_k' : A_3}
{\Gamma \vdash \case v \{\sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k'\} : A_3}
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : A_1 + A_1' \ltdyn A_2 + A_2'\\
\Phi, x_1\ltdyn x_1:A_1 \ltdyn A_1 \vdash v_{k,1} \ltdyn v_{k,2} : A_3 \ltdyn A_4\\
\Phi, x_1'\ltdyn x_1':A_1' \ltdyn A_1' \vdash v_{k,1}' \ltdyn v_{k,2}' : A_3 \ltdyn A_4}
{\Phi \vdash \case v_1 \{\sigma x_1 \mapsto v_{k,1} \pipe \sigma' x_1' \mapsto v_{k,1}'\}
\ltdyn \case v_2 \{\sigma x_2 \mapsto v_{k,2} \pipe \sigma' x_2' \mapsto v_{k,2}'\} : A_3 \ltdyn A_4}
\inferrule
{\Gamma \vdash v : A + A'\and
\Gamma, x:A\pipe \Delta \vdash M : \u B\and
\Gamma, x':A' \pipe \Delta \vdash M' : \u B}
{\Gamma\pipe \Delta \vdash \case v \{\sigma x \mapsto M \pipe \sigma' x' \mapsto M'\} : \u B}
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : A_1 + A_1' \ltdyn A_2 + A_2'\\
\Phi, x_1\ltdyn x_1:A_1 \ltdyn A_1 \pipe \Psi \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2 \\
\Phi, x_1'\ltdyn x_1':A_1' \ltdyn A_1'\pipe\Psi \vdash M_1' \ltdyn M_2' : \u B_1 \ltdyn \u B_2}
{\Phi\pipe\Psi \vdash \case v_1 \{\sigma x_1 \mapsto M_1 \pipe \sigma' x_1' \mapsto M_1'\}
\ltdyn \case v_2 \{\sigma x_2 \mapsto M_2 \pipe \sigma' x_2' \mapsto M_2'\} : \u B_1 \ltdyn \u B_2}
\case \sigma v \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \} \equidyn v_k[v/x]\\
\case \sigma' v' \{ \sigma x \mapsto v_k \pipe \sigma' x' \mapsto v_k' \} \equidyn v_k'[v'/x']\\
\case \sigma v \{ \sigma x \mapsto M \pipe \sigma' x' \mapsto M' \} \equidyn M[v/x]\\
\case \sigma' v' \{ \sigma x \mapsto M \pipe \sigma' x' \mapsto M' \} \equidyn M'[v'/x']\\
\inferrule
{x_+ : A + A'}
{v \equidyn \case x_+ \{ \sigma x \mapsto v[\sigma x/x+_] \pipe \sigma' x' \mapsto v[\sigma' x'/x_+] \}}
\inferrule
{x_+ : A + A'}
{M \equidyn \case x_+ \{ \sigma x \mapsto M[\sigma x/x+_] \pipe \sigma' x' \mapsto M[\sigma' x'/x_+] \}}
\end{mathpar}
\caption{Binary Sum}
\end{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{B \ctype \and B' \ctype}
{B \wedge B' \ctype}
\inferrule
{B_1 \ltdyn B_2 \and B_1' \ltdyn B_2'}
{B_1 \wedge B_1' \ltdyn B_2 \wedge B_2'}
\inferrule
{\Gamma\pipe\Delta \vdash M : \u B\and
\Gamma\pipe\Delta \vdash M' : \u B'}
{\Gamma\pipe \Delta \vdash \pair M {M'} : \u B \wedge \u B'}
\inferrule
{\Phi\pipe\Psi \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2 \\
\Phi\pipe\Psi \vdash M_1' \ltdyn M_2' : \u B_1' \ltdyn \u B_2'}
{\Phi\pipe \Psi \vdash \pair {M_1} {M_1'} \ltdyn \pair {M_2} {M_2'} : \u B_1 \wedge \u B_1' \ltdyn \u B_2 \wedge \u B_2'}
\inferrule
{\Gamma \pipe \Delta \vdash M : \u B \wedge \u B'}
{\Gamma \pipe \Delta \vdash \pi M : \u B}
\inferrule
{\Gamma \pipe \Delta \vdash M : \u B \wedge \u B'}
{\Gamma \pipe \Delta \vdash \pi' M : \u B'}
\inferrule
{\Phi \pipe \Psi \vdash M_1 \ltdyn M_2 : \u B_1 \wedge \u B_1' \ltdyn \u B_2 \wedge \u B_2'
\and \u B_1 \ltdyn \u B_2 \and \u B_1' \ltdyn \u B_2'}
{\Phi \pipe \Psi \vdash \pi M_1 \ltdyn \pi M_2 : \u B_1 \ltdyn \u B_2}
\inferrule
{\Phi \pipe \Psi \vdash M_1 \ltdyn M_2 : \u B_1 \wedge \u B_1' \ltdyn \u B_2 \wedge \u B_2'
\and \u B_1 \ltdyn \u B_2 \and \u B_1' \ltdyn \u B_2'}
{\Phi \pipe \Psi \vdash \pi' M_1 \ltdyn \pi' M_2 : \u B_1 \ltdyn \u B_2}
\pi \pair M {M'} \equidyn M\and
\pi' \pair M {M'} \equidyn M'\\
\inferrule
{M : \u B \wedge \u B'}
{M \equidyn \pair {\pi M}{\pi' M}}
\end{mathpar}
\caption{Binary Computation Product}
\end{figure}
\begin{figure}[H]
\begin{mathpar}
\begin{array}{rcl}
\upcast{A_1 + A_1'}{A_2 + A_2'} x_{+,1} &\equidyn&
\case x_{+,1} \{ \sigma x \mapsto \upcast {A_1} {A_2} \pipe \sigma' x' \mapsto \upcast {A_1'} {A_2'} \}\\
\dncast{\u F(A_1 + A_1')}{\u F(A_2 + A_2')} \bullet &\equidyn& \lett x_{+,2} = \bullet;
\case x_{+,2} \{\\&&\quad
\sigma x_2 \mapsto \dncast{\u F A_1}{\u F A_2}\ret x_2\\&&\quad
\pipe \sigma' x_2' \mapsto \dncast{\u F A_1'}{\u F A_2'}\ret x_2'\\&&\quad
\}\\
\dncast{\u B_1 \wedge \u B_1'}{\u B_2 \wedge \u B_2'}\bullet &\equidyn& \pair {\dncast{\u B_1}{\u B_2}\pi\bullet}{\dncast{\u B_1'}{\u B_2'}\pi'\bullet}\\
\upcast{U({\u B_1 \wedge \u B_1'})}{U({\u B_2 \wedge \u B_2'})}x_{\wedge} &\equidyn&
\thunk\{\\&&\quad
\pi\mapsto{\force \upcast{U \u B_1}{U \u B_2}\thunk \pi\force x_{\wedge}} \pipe\\ &&\quad
\pi'\mapsto{\force \upcast{U \u B_1'}{U \u B_2'}\thunk \pi'\force x_{\wedge}}
\}
\end{array}
\end{mathpar}
\caption{Binary Sum and Binary Computation Product Contract Uniqueness Theorems}
\end{figure}
\subsection{Nice Multiplicatives: Value Products and Functions}
Next, we consider the two ``nice'' multiplicative connectives ($\u F$
and $U$ are also multiplicatives but they are ``bad'' because they
don't have a uniqueness principle for their casts).
%
L
\begin{figure}[H]
\begin{mathpar}
\inferrule
{A \vtype \and \u B \ctype}
{A \to \u B \ctype}
\inferrule
{A_1 \ltdyn A_2 \and \u B_1 \ltdyn \u B_2}
{A_1 \to \u B_1 \ltdyn A_2 \to \u B_2}
\inferrule
{\Gamma, x : A \pipe \Delta \vdash M : B}
{\Gamma \pipe \Delta \vdash \lambda x:A. M : A \to \u B}
\inferrule
{\Phi, x_1 \ltdyn x_2 : A_1 \ltdyn A_2 \pipe \Psi \vdash M_1 \ltdyn M_2 : B_1 \ltdyn B_2}
{\Phi \pipe \Psi \vdash \lambda x_1:A_1. M_1 \ltdyn \lambda x_2:A_2. M_2 : A_1 \to \u B_1 \ltdyn A_2 \to \u B_2}
\inferrule
{\Gamma \pipe \Delta \vdash M : A \to \u B\and
\Gamma \vdash v : A}
{\Gamma \pipe \Delta \vdash M(v) : \u B}
\inferrule
{\Phi \pipe \Psi \vdash M_1 \ltdyn M_2 : A_1 \to \u B_1 \ltdyn A_2 \to \u B_2 \and
\Phi \vdash v_1 \ltdyn v_2 : A_1 \ltdyn A_2}
{\Phi \pipe \Psi \vdash M_1(v_1) \ltdyn M_2(v_2) : \u B_1 \ltdyn \u B_2}
\inferrule
{}
{(\lambda x. M)v \equidyn M[v/x]}
\inferrule
{M : A \to \u B}
{M \equidyn \lambda x. M x}
\end{mathpar}
\caption{Function Type}
\end{figure}
\begin{figure}[H]
\begin{mathpar}
\inferrule
{A \vtype \and A' \vtype}
{A \times A \vtype}
\inferrule
{A_1 \ltdyn A_2 \and A_1' \ltdyn A_2'}
{A_1 \times A_1' \ltdyn A_2 \to A_2'}
\inferrule
{\Gamma \vdash v : A \and \Gamma \vdash v' : A'}
{\Gamma \vdash (v,v') : A \times A'}
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : A_1 \ltdyn A_2 \and \Phi \vdash v_1' \ltdyn v_2' : A_1' \ltdyn A_2'}
{\Phi \vdash (v,v') \ltdyn (v,v') : A_1 \times A_1' \ltdyn A_2 \times A_2'}
\inferrule
{\Gamma \vdash v : A \times A'\and
\Gamma,x:A,x':A' \vdash v_k : A_k}
{\Gamma \vdash \lett (x,x') = v; v_k : A_k}
\inferrule
{\Gamma \vdash v : A \times A'\and
\Gamma,x:A,x':A'\pipe\Delta \vdash M : \u B}
{\Gamma\pipe\Delta \vdash \lett (x,x') = v; M : \u B}
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : A_1 \times A_1' \ltdyn A_2 \times A_2'\\
\Phi,x_1\ltdyn x_2:A_1\ltdyn A_2,x_1'\ltdyn x_2':A_1'\ltdyn A_2' \vdash v_{k,1} \ltdyn v_{k,2} : A_{k,1} \ltdyn A_{k,2}}
{\Phi \vdash \lett (x_1,x_1') = v_1; v_{k,1} \ltdyn \lett (x_2,x_2') = v_2; v_{k,2} : A_{k,1} \ltdyn A_{k,2}}
\inferrule
{\Phi \vdash v_1 \ltdyn v_2 : A_1 \times A_1' \ltdyn A_2 \times A_2'\\
\Phi,x_1\ltdyn x_2:A_1\ltdyn A_2,x_1'\ltdyn x_2':A_1'\ltdyn A_2'\pipe \Psi \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2}
{\Phi\pipe\Psi \vdash \lett (x_1,x_1') = v_1; M_1 \ltdyn \lett (x_2,x_2') = v_2; M_2 : \u B_1 \ltdyn \u B_2}
\inferrule
{}
{\lett (x,x') = (v,v'); v_k \equidyn v_k[v/x,v'/x']}
\inferrule
{}
{\lett (x,x') = (v,v'); M \equidyn M[v/x,v'/x']}\\
\inferrule
{y : A \times A'}
{v \equidyn \lett(x,x') = y; v[(x,x')/y]}
\inferrule
{y : A \times A'}
{M \equidyn \lett(x,x') = y; M[(x,x')/y]}
\end{mathpar}
\caption{Value Product Type}
\end{figure}
Next, we consider the contract uniqueness theorems for the
multiplicatives.
%
For the natural contracts, again everything works swimmingly.
%
For the product type, we just substitute in the upcasts.
%
Similarly, for the function downcast, we substitute in the upcast on
the domain and plug into the downcast for the result type.
\begin{figure}[H]
\begin{mathpar}
\inferrule
{}
{\dncast {A_1 \to \u B_1}{A_2 \to \u B_2} \bullet \equidyn \lambda x:A_1. \dncast {\u B_1}{\u B_2} (\bullet(\upcast {A_1} {A_2} x))}
\inferrule
{}
{\upcast{A_1 \times A_1'}{A_2 \times A_2'}} x_{\times} \equidyn
\lett (x,x') = x_{\times}; (\upcast {A_1}{A_2} x, \upcast {A_1'}{A_2'} x')
\end{mathpar}
\caption{Function and Product Contract ``Natural'' directions}
\end{figure}
\begin{figure}
\begin{mathpar}
\begin{array}{rcl}
\dncast{\u F (A_1 \times A')}{\u F(A_2 \times A')}\bullet &\equidyn&
\lett x_{\times} = \bullet; \\&&
\lett (x_2,x') = x_{\times};\\&&
\lett x_1 = \dncast{\u F A_1}{\u F A_2}\ret x_2;\\&&
\ret (x_1,x')\\
\dncast{\u F (A \times A_1')}{\u F(A \times A_2')}\bullet &\equidyn&
\lett x_{\times} = \bullet; \\&&
\lett (x,x_2') = x_{\times};\\&&
\lett x_1' = \dncast{\u F A_1'}{\u F A_2'}\ret x_2';\\&&
\ret (x,x_1')\\\\
\upcast{U(A_1 \to \u B)}{U(A_2 \to \u B)}f_{\to} &\equidyn&
\thunk\lambda (x_2 : A_2). \lett x_1 = \dncast{\u F A_1}{\u F A_2}\ret x_2; (\force f_{\to})(x_1)\\
\upcast{U(A \to \u B_1)}{U(A \to \u B_2)}f_{\to} &\equidyn&
\thunk\lambda (x : A). \force \upcast{U \u B_1}{U \u B_2}\thunk ((\force f_{\to})(x_1))\\\\
\dncast{\u F (A_1 \times A_1')}{\u F(A_2 \times A_1')}
&\equidyn& \dncast{\u F (A_1 \times A_1')}{\u F(A_2 \times A_1')} \dncast{\u F (A_2 \times A_1')}{\u F(A_2 \times A_2')}\\
&\equidyn& \dncast{\u F (A_1 \times A_1')}{\u F(A_1 \times A_2')} \dncast{\u F (A_1 \times A_2')}{\u F(A_2 \times A_2')}\\\\
\upcast{U(A_1 \to \u B_1)}{U(A_2 \to \u B_2)}
&\equidyn& \upcast{U(A_1 \to \u B_2)}{U(A_2 \to \u B_2)}\upcast{U(A_1 \to \u B_1)}{U(A_1 \to \u B_2)}\\
&\equidyn& \upcast{U(A_2 \to \u B_1)}{U(A_2 \to \u B_2)}\upcast{U(A_1 \to \u B_1)}{U(A_2 \to \u B_1)}
\end{array}
\end{mathpar}
\caption{Function and Product "Expat" Directions, one side at a time}
\end{figure}
\subsection{Exponentials}
To summarize what we've done so far: we show that all of the ``nice''
connectives give an obvious uniquness principle for their ``natural''
cast: nice value connectives give upcasts and nice computation
connectives give downcasts.
The $\u F$ and $U$ types are \emph{not nice} in that they both have a
\emph{covariant} argument of \emph{the opposite sort}.
%
The reason this is troublesome is when we go to make a semantics, for
a nice type like product if we try to design an upcast, the type
constructor says:
\begin{mathpar}
\inferrule
{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2'}
{A_1 \times A_2 \ltdyn A_1' \times A_2'}
\end{mathpar}
and since $A \ltdyn A'$ denotes an upcast $\upcast{A}{A'}$, and
$\times$ is covariant, we can apply the functoriality of $\times$.
However, $\u F$ and $U$ are \emph{covariant} types, but if we look one
level up we don't get a useful assumption:
\begin{mathpar}
\inferrule
{A \ltdyn A'}
{\u F A \ltdyn \u F A'}
\end{mathpar}
So given an upcast $\upcast A {A'}$ we are tasked with constructing a
downcast $\dncast{\u F A}{\u F A'}$, but since $\u F$ is covariant
there is no way to proceed.
%
But to summarize the previous sections, we've shown that we can derive
implementations for upcasts/downcasts for $\u F$ and $U$ on a
case-by-case basis for each connective.
So instead of the above we had
\begin{mathpar}
\inferrule*
{\inferrule{A_1 \ltdyn A_1'\and A_2\ltdyn A_2'}{A_1\times A_2 \ltdyn A_1' \times A_2'}}
{\u F(A_1 \times A_2) \ltdyn \u F (A_1' \times A_2')}
\end{mathpar}
And at this point we have shown this is true for every connective
\emph{except} the exponentials themselves.
%
So in order to produce a ``full'' implementation, we need to know what
the casts between $U \u F A$s and $\u F U \u B$s look like
respectively.
%
Fortunately, at this point there \emph{is} an obvious answer because
now we have doubly negated: since $U$ and $\u F$ are both functors we
can get candidates by applying their functoriality twice.
%
And this is correct because as we explained earlier, all functors
preserve representability.
However, here is a more direct syntactic proof.
\begin{figure}
\inferrule
{A_1 \ltdyn A_2}
{x_1 : U \u F A_1 \vdash \upcast{U\u F A_1}{U\u F A_2}x_1 \equidyn \thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1)}
\inferrule
{\inferrule
{y_2 \ltdyn \upcast{A_1}{A_2}y_1}
{\thunk (\lett y_1 = \force x_1; \ret y_1) \ltdyn \thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1)}}
{x_1 : U \u F A_1 \vdash \upcast{U\u F A_1}{U\u F A_2}x_1 \ltdyn \thunk \upcast{U\u F A_1}{U\u F A_2}(\lett y_1 = \force x_1; \ret y_1) \ltdyn \thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1)}
\inferrule
{\inferrule
{x_1 \ltdyn \force\upcast{U\u F A_1}{U\u FA_2}x_1 \ltdyn x_1\and
y_1 \ltdyn y_2 \vdash \upcast{A_1}{A_2}y_1 \ltdyn y_2
}
{\thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1) \ltdyn \thunk (\lett y_2 = \force\upcast{U\u F A_1}{U\u F A_2} x_1; \ret y_2)}}
{x_1 : U \u F A_1 \vdash \thunk (\lett y_1 = \force x_1; \ret \upcast{A_1}{A_2}y_1) \ltdyn \thunk (\lett y_2 = \force\upcast{U\u F A_1}{U\u F A_2} x_1; \ret y_2) \ltdyn \upcast{U\u F A_1}{U\u F A_2}x_1}
\caption{Exponential Interaction}
\inferrule
{\u B_1 \ltdyn \u B_2}
{\bullet:\u F U \u B_2 \vdash \dncast{\u FU\u B_1}{\u FU\u B_2}\bullet \equidyn \lett x = \bullet; \ret \thunk \force x : \u F U \u B_1}
\end{figure}
\section{Concrete Syntactic Models}
To determine what sorts of dynamic type we want for different
applications, we consider the models.
%
There are many choices we could make: should there be a most dynamic
value type or computation type or both?
%
For each of those choices, can we support the full range of
call-by-push-value connectives, or just the call-by-value or
call-by-name fragments?
%
And which of the dynamic types support interoperability between
call-by-value and call-by-name?
We'll start with the most novel model, which has dynamic value and
computaiton types and supports the full range of call-by-push-value
connectives.
%
We'll call the syntax ?`GCBPV?
A model of ?`GCBPV? consists of a preorder-enriched cbpv model with
specified interpretations of $\dynv, \dync$ and the following
precision judgments. Note that we don't need $0 \ltdyn \dynv$ and
$\top \ltdyn \dync$ because those are uniquely determined by the
universal property.
%
An interpretation of a value type dynamism $A \ltdyn A'$ should be a
pure upcast $e : A \to A'$ and an effectful downcast $p : \u F A'
\multimap \u F A$ such that they are adjoint $F(e)\dashv p$ and the
downcast retracts the upcast $p \circ F(e) = id_{\u F A}$.
%
An interpreetation of a computation type dynamism $\u B \ltdyn \u B'$
should be a stack downcast $p : \u B' \multimap \u B$ and a delaying
upcast $e : U \u B \to U \u B'$ such that they are adjoint $e \dashv
U(p)$ and again the downcast retracts the upcast $U(p) \circ e = id_{U
\u B}$.
\begin{mathpar}
1 \ltdyn \dynv
\dynv \times \dynv \ltdyn \dynv
\dynv + \dynv \ltdyn \dynv
U \dync \ltdyn \dynv\\
\dync \wedge \dync \ltdyn \dync
\dynv \to \dync \ltdyn \dync
\u F \dynv \ltdyn \dync
\end{mathpar}
Next, we will use poset CBPV as a metalanguage and compile GCBPV into
poset CBPV with recursive types.
%
As a domain equation we can write this as a pair of mutually recursive equations:
\begin{mathpar}
\dynv = 1 + (\dynv \times \dynv) + (\dynv + \dynv) + U \dync\\
\dync = (\dync \wedge \dync) \wedge (\dynv \to \dync) \wedge \u F \dynv
\end{mathpar}
\begin{mathpar}
\dynv(X, \u Y) = 1 + (X \times X) + (X + X) + U \u Y
\dync(X, \u Y) = (\u Y \wedge \u Y) \wedge (X \to \u Y) \wedge \u F X
\dynv = \mu X. \dynv(X, \u \mu \u Y. \dync(X, \u Y))
\dync = \mu \u Y. \dync(\mu X. \dynv(X, \u Y), \u Y)
\end{mathpar}
We call the cases of $\dynv$ the ``tag types'' and abbreviate them $T$
because they are the tags of the sum, and the cases of the $\dync$ the
``message types'' and abbreviate them $\u M$ because they are the
possible messages of the ``coinductive'' dynamic type.
%
We implement the appropriate casts and their adjoints as follows
\[ \upcast T \dynv x = \roll \sigma_T x \]
\[ \dncast {\u F T} {\u F \dynv} \hole = \lett x = \hole; \case \unroll x \{ \sigma_T y \mapsto y; \sigma_{T'} y \mapsto \err \} \]
\[ \dncast {\u M} \dync \hole = \pi_{\u M} \u \unroll \hole \]
\[ \upcast {U \u M} {U \dync} x = \u \roll \thunk [ \pi_{\u M} \mapsto \force x; \pi_{\u M'} \mapsto \err ] \]
Note that these both satisfy adjunction and retraction.
\begin{mathpar}
\inferrule
{\text{retract: need to show}}
{\dncast {\u F T} {\u F \dynv}\ret \upcast T \dynv y \equidyn y}
\inferrule
{}
{\lett x = \ret \roll \sigma_T y; \case \unroll x \{ \sigma_T y \mapsto y; \sigma_{T'} y \mapsto \err \}
\equidyn \case \unroll \roll\sigma_T y \{ \sigma_T y \mapsto y; \sigma_{T'} y \mapsto \err \}
\equidyn y}
%% \inferrule
%% {\text{projection: need to show}}
%% {\lett y = \dncast{\u F T}{\u F \dynv}\ret x; \ret \upcast T \dynv y \ltdyn x}
%% \inferrule
%% {{\lett y = \dncast{\u F T}{\u F \dynv}\ret x; \ret \roll\sigma_T y \ltdyn \ret x}}
\end{mathpar}
\end{document}
%% Local Variables:
%% compile-command: "pdflatex gcbpv.tex"
%% End: