\documentclass{article}
\usepackage{float}
\usepackage{amsmath,amssymb}
\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 multiplicative and additive connectives of
gradual call-by-push value, and their corresponding contracts.
%
We start with the additives because they are comparatively easier.
\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{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}
\section{Call by Value $\ltdyn$ Call by Name}
Can we model the idea that ``call by value errors more than call by
name'' using type dynamism/ep pairs? Some basic calculations work
out...
\section{Focusing on an implementation}
Call-by-push-value with complex values and stacks is odd from an
operational perspective.
%
Values, rather than being simple trees built out of their
constructors, can perform pattern matching on free variables, which
would mean that they seemingly need ot be reduced operationally, when
they are expected to be inert.
%
Dually, stacks, rather than being simple composites of
\emph{destructors}, can also consist of $\lambda$s and code tuples,
which are expected to \emph{delay} evaluation of their bodies in an
operational semantics, whereas they are expected to \emph{force} the
evaluation of the term plugged into the hole.
%
Levy resolves these seeming oddities by showing that as long as the
values and stacks occur inside a larger term, the ``complex'' portions
can be \emph{compiled away}.
%
Today, many years later, with the benefit of much hindsight, we can
see Levy's proof as an application of the method of \emph{focusing}.
Here we adapt that proof to get an operational semantics for
\emph{Gradual} CBPV that will .
%
If we focus even more intensely we can make all upcasts between
positive connectives implicit, but allowing positive variables rules
out that possibility.
\begin{figure}[H]
\mbox{Values: $\Gamma \vdash V : A$}\\
\begin{mathpar}
\inferrule
{\Gamma \vdash \hat V : A_1 \and A_1 \ltdyn A_2}
{\Gamma \vdash \upcast {A_1}{A_2} \hat V : A_2}
\end{mathpar}
\mbox{Value Constructors: $\Gamma \vdash\hat V : A$}\\
\begin{mathpar}
\inferrule
{x : A \in \Gamma}
{\Gamma \vdash x : A}
\inferrule
{\Gamma \vdash V : A \and\Gamma \vdash V' : A'}
{\Gamma \vdash ( V, V') : A \times A'}
\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
{}
{\Gamma \vdash () : 1}
\inferrule
{\Gamma \vdash M : \u B}
{\Gamma \vdash \thunk M : U \u B}
\end{mathpar}
\mbox{Terms: $\Gamma \vdash M : \u B$}
\begin{mathpar}
\inferrule
{}
{\Gamma \vdash \err_{\u B} : \u B}
\inferrule
{\Gamma \vdash V : A}
{\Gamma \vdash \ret V : \u F A}
\inferrule
{\Gamma \vdash V : U \u B\and
\Gamma \pipe [ \u B ] \vdash S : \u C
}
{\Gamma \vdash \force V; S : \u B}
\inferrule
{\Gamma, x : A \vdash M : \u B}
{\Gamma \vdash \lambda x : A. M : A \to \u B}
\inferrule
{}
{\Gamma \vdash [] : \top}
\inferrule
{\Gamma \vdash M : \u B\and
\Gamma \vdash M' : \u B'}
{\Gamma \vdash [\pi \mapsto M \pipe \pi' \mapsto M'] : \u B \wedge \u B'}
\inferrule
{\Gamma \vdash V : A \times A'\and
\Gamma, x : A, x': A' \vdash M : \u B}
{\Gamma \vdash \lett (x,x') = V; M : \u B}
\inferrule
{\Gamma \vdash V : A + A'\and
\Gamma , x:A \vdash M : \u B\and
\Gamma , x:A' \vdash M' : \u B}
{\Gamma \vdash \case V \{ \sigma x \mapsto M \pipe \sigma' x' \mapsto M' \} : \u B}
\inferrule
{\Gamma \vdash \hat M : \u B_2 \and \u B_1 \ltdyn \u B_2}
{\Gamma \vdash \dncast{\u B_1}{\u B_2} \hat M : \u B_1}
\end{mathpar}
\mbox{Spines $\Gamma \pipe [ \u B ] \vdash S : \u C$}
\begin{mathpar}
\inferrule
{\Gamma \pipe [ \u B_1] \vdash S : \u C \and \u B_1 \ltdyn \u B_2}
{\Gamma \pipe [\u B_2] \vdash \dncast{\u B_1}{\u B_2}; S : \u C}
\end{mathpar}
\mbox{Computation Destructors $\Gamma\pipe [ \u B ] \vdash \hat S : \u C$}
\begin{mathpar}
\inferrule
{}
{\Gamma \pipe [\u B ] \vdash \bullet : \u B}
\inferrule
{\Gamma\pipe [\u B] \vdash S : \u C \and
\Gamma \vdash V : A}
{\Gamma\pipe [ A \to \u B ] \vdash 'V; S : \u C}
\inferrule
{\Gamma \pipe [\u B]\vdash S : C}
{\Gamma \pipe [\u B \wedge \u B'] \vdash \pi; S : \u C}
\inferrule
{\Gamma \pipe [\u B']\vdash S : C}
{\Gamma \pipe [\u B \wedge \u B'] \vdash \pi'; S : \u C}
\inferrule
{\Gamma, x : A \vdash M : \u C}
{\Gamma \pipe [\u F A] \vdash \too x. M : \u C}
\end{mathpar}
\caption{Operational Gradual Call By Push Value (Sketchy)}
\end{figure}
\section{The Notes we Don't Play}
From a ``completionist'' perspective, call-by-push-value is missing
some interesting connectives that are easy to define.
%
When added to call-by-push-value, the language is called the enriched
effect calculus (EEC) and has been studied extensively (cite).
First, there are 3 missing multiplicative connectives: the pure
function space $A \Rightarrow A'$, linear function space $\u B
\multimap \u B'$ and tensor product of a value and computation type $A
\otimes \u B$.
%
Since they are problematic I will only describe their sorts and their
sequent calculus invertible rule:
\begin{mathpar}
\inferrule
{A \vtype \and A' \vtype}
{A \Rightarrow A' \vtype}
\inferrule
{\Gamma, A \vdash^V A'}
{\Gamma \vdash^V A \Rightarrow A'}
\inferrule
{\u B \ctype \and \u B' \ctype}
{\u B \multimap \u B' \vtype}
\inferrule
{\Gamma \pipe \u B \vdash \u B'}
{\Gamma \vdash \u B \multimap \u B'}
\inferrule
{A \vtype \and \u B \ctype}
{A \otimes \u B \ctype}
\inferrule
{\Gamma, A \pipe \u B \vdash \u C}
{\Gamma \pipe A \otimes \u B \vdash \u C}
\end{mathpar}
First, they are ``boundary-crossing'' connectives in that they each
have a \emph{covariant} argument whose sort is different from the sort
of the constructor or a \emph{contravariant} argument whose sort is
the same as the constructor.
%
The pure function space has a contravariant argument of the same sort,
the linear function space has a covariant computation type argument
while it is a value type and the value-computation tensor has a
covariant value type argument while it is a computation type.
Second, from the perspective of our focusing operational semantics,
each of them violates the rule of our focusing system that the only
negative value type is $U$ and the only positive computation type is
$\u F$.
%
Note that this is similar to but not the same as the boundary crossing
rule, and there are some \emph{additives} that we violate the focusing
restriction but not the boundary-crossing restriction: the negative
value product and the positive computation sum, which we show now.
\begin{mathpar}
\inferrule
{A \vtype \and A' \vtype}
{A \& A' \vtype}
\inferrule
{\Gamma \vdash A \and \Gamma \vdash A'}
{\Gamma \vdash A \& A'}
\inferrule
{\u B \ctype \and \u B' \ctype}
{\u B \oplus \u B' \ctype}
\inferrule
{{\Gamma \pipe \u B \vdash \u C} \and
{\Gamma \pipe \u B' \vdash \u C}}
{\Gamma \pipe \u B \oplus \u B' \vdash \u C}
\end{mathpar}
\end{document}
%% Local Variables:
%% compile-command: "pdflatex gcbpv.tex"
%% End: