gcbpv.tex

\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;\\&&