judgmental structure and casts for gradual call by push value

gcbpv.tex

+\documentclass{article}
+
+\usepackage{amsmath,amssymb}
+\usepackage{tikz-cd}
+\usepackage{mathpartir}
+
+\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{\ltdynv}{\mathrel{\sqsubseteq_V}}
+\newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
+
+\newcommand{\dyn}{{?}}
+\newcommand{\upcast}[2]{\langle{#2}\leftarrowtail{#1}\rangle}
+\newcommand{\dncast}[2]{\langle{#1}\twoheadleftarrow{#2}\rangle}
+
+
+\newcommand{\Set}{\text{Set}}
+\newcommand{\relto}{\to}
+\newcommand{\M}{\mathcal{M}}
+\newcommand{\sq}{\square}
+\newcommand{\lett}{\text{let}\,\,}
+
+\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}
+  \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}
+  \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\and
+      \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\and
+      \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\and
+      \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}
+  \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}
+
+Errors are least terms at every computation type (not stacks).
+%
+The dynamic type is probably a greatest \emph{value type}.
+%
+Casts are, naturally, the most interesting case.
+%
+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}
+  \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}
+
+
+\end{document}