add F, U types, prove that they "preserve" upcasts, downcasts resp.

gcbpv.tex

@@ -14,6 +14,8 @@
 \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}}
 
@@ -27,6 +29,9 @@
 \newcommand{\M}{\mathcal{M}}
 \newcommand{\sq}{\square}
 \newcommand{\lett}{\text{let}\,\,}
+\newcommand{\ret}{\text{ret}\,\,}
+\newcommand{\thunk}{\text{thunk}\,\,}
+\newcommand{\force}{\text{force}\,\,}
 
 \begin{document}
 \title{Gradual Call-By-Push-Value}
@@ -306,5 +311,206 @@ dynamism.
   \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}
+  \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}
+  \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}
+\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}
 \end{document}
+
+%% Local Variables:
+%% compile-command: "pdflatex gcbpv.tex"
+%% End: