some comments on the general picture

gcbpv.tex

 \documentclass{article}
 
 \usepackage{float}
-\usepackage{amsmath,amssymb}
+\usepackage{amsmath,amssymb, amsthm}
 \usepackage{tikz-cd}
 \usepackage{mathpartir}
 \usepackage{rotating}
@@ -532,10 +532,138 @@ from a preordering.
 
 \section{Connectives and Contract Uniqueness Theorems}
 
-Next we consider the multiplicative and additive connectives of
-gradual call-by-push value, and their corresponding contracts.
+Next we consider the contract uniqueness theorems for the connectives
+of call-by-push-value.
 %
-We start with the additives because they are comparatively easier.
+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}