From 10deb9d3d13e635852174e8887304ebb9c5f7a28 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Fri, 20 Apr 2018 12:28:13 -0400
Subject: [PATCH] add F, U types, prove that they "preserve" upcasts, downcasts
resp.
---
gcbpv.tex | 206 ++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 206 insertions(+)
diff --git a/gcbpv.tex b/gcbpv.tex
index 6dbcf46..2d10118 100644
--- a/gcbpv.tex
+++ b/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:
--
GitLab