\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{\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{\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?).
%
Gradual Call-by-push-value adds an ordering form for each of these
judgments: value type dynamism, computation type dynamism, value
dynamism, term dynamism 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}\\
\inferrule
{\Gamma \ctx \and B \ctype}
{\Gamma \vdash M : \underline B}
\inferrule
{\Phi \vdash \Gamma_1 \ltdyn \Gamma_2 \ctx \and
\Gamma_1 \vdash M_1 : \u B_1\and
\Gamma_2 \vdash M_2 : \u B_2\and
\u B_1 \ltdyn \u B_2}
{\Phi \vdash M_1 \ltdyn M_2 : \u B_1 \ltdyn \u B_2}\\
\inferrule
{\Gamma\ctx \and \u B\ctype \and \u C \ctype}
{\Gamma\pipe \hole : \u B \vdash S : \u C}
\inferrule
{\Phi : \Gamma_1 \ltdyn \Gamma_2 \and
\u B_1 \ltdyn \u B_2 \and
{\Gamma_1\pipe \hole : \u B_1 \vdash S_1 : \u C_1}\and
{\Gamma_2\pipe \hole : \u B_2 \vdash S_2 : \u C_2}\and
\u C_1 \ltdyn \u C_2}
{\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}
\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
{}
{\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
{\gamma : \prod_{x' : A' \in \Gamma'} \Gamma \vdash \cdot : 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
{\gamma : \prod_{x' : A' \in \Gamma'} \Gamma \vdash \cdot : A'\and
\Gamma \vdash M : \u B
}
{\Gamma \vdash M[\gamma] : \u B}
\inferrule
{\Phi' \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 \vdash M_1[\gamma_1] \ltdyn M_2[\gamma_2] : \u B_1 \ltdyn \u B_2}\\
\inferrule
{\gamma : \prod_{x' : A' \in \Gamma'} \Gamma \vdash \cdot : A'\and
\Gamma\pipe \u B \vdash S : \u C
}
{\Gamma\pipe \u B \vdash S[\gamma] : \u C}
\inferrule
{\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\\
\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 \hole\ltdyn \hole : \u B_1 \ltdyn \u B_2 \vdash S_1[\gamma_1] \ltdyn S_2[\gamma_2] : \u C_1 \ltdyn \u C_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 \ltdyn \hole : \u B_1 \ltdyn \u B_2}
\inferrule
{\Gamma \vdash M : \u B \and \Gamma \pipe \hole : \u B \vdash S : \u C}
{\Gamma\pipe \hole : \u B \vdash S[M/\hole] : \u C}
\inferrule
{\Gamma \pipe \u B \vdash S : \u B' \and \Gamma \pipe \hole : \u B' \vdash S' : \u B''}
{\Gamma\pipe \hole : \u B \vdash S'[S/\hole] : \u B''}
\end{mathpar}
\caption{GCBPV Basic Judgmental Rules 1 (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 \hole : \u C \vdash S : \u B_2 \and \u B_1 \ltdyn \u B_2}
{\Gamma \pipe \hole : \u C \vdash \dncast{\u B_1}{\u B_2} S : \u B_1}
\inferrule
{\Gamma \vdash M : \u B_2 \and \u B_1 \ltdyn \u B_2}
{\Gamma \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}
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}
It seems like the easiest thing to do is have a most dynamic function
type and product type, but I'm not sure if it's really necessary.
%
Explore this in the models.
\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
\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}
\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} \{
\sigma x_2 \mapsto \dncast{\u F A_1}{\u F A_2}\ret x_2
\pipe \sigma' x_2' \mapsto \dncast{\u F A_1'}{\u F A_2'}\ret x_2'
\}
\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\\
\pair
{\force \upcast{U \u B_1}{U \u B_2}\thunk \pi\force x_{\wedge}}
{\force \upcast{U \u B_1'}{U \u B_2'}\thunk \pi'\force x_{\wedge}}
\end{mathpar}
\caption{Binary Sum and Binary Computation Product Contract Uniqueness Theorems}
\end{figure}
\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}
\end{mathpar}
\caption{Function Type}
\end{figure}
\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 {U({A_1 \to \u B_1})}{U({A_2 \to \u B_2})} (f : U(A_1 \to \u B_1)) \equidyn\\
\thunk \lambda x_2 : A_2.
\lett x_1 = \dncast{\u F A_1}{\u F A_2}\ret x_2;
(\force \upcast{U \u B_1}{U \u B_2}(\thunk ((\force f)(x_1))))
}
\end{mathpar}
\caption{Function Contract Theorem, Proof}
\end{figure}
\section{Models}
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.
\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.
\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 ] \]
\end{document}
%% Local Variables:
%% compile-command: "pdflatex gcbpv.tex"
%% End: