make upcasts uparrows, dncast down, add model stuff, start function types

gcbpv.tex

@@ -3,10 +3,12 @@
 \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}}
@@ -20,8 +22,15 @@
 \newcommand{\ltdynt}{\mathrel{\sqsubseteq_T}}
 
 \newcommand{\dyn}{{?}}
-\newcommand{\upcast}[2]{\langle{#2}\leftarrowtail{#1}\rangle}
-\newcommand{\dncast}[2]{\langle{#1}\twoheadleftarrow{#2}\rangle}
+\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}}
@@ -29,6 +38,7 @@
 \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}\,\,}
@@ -236,12 +246,6 @@ for each.
   \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
@@ -509,6 +513,116 @@ from a preordering.
   \caption{Functoriality Preserves Representability (Proofs)}
   
 \end{figure}
+
+
+\begin{figure}
+  \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{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 ] \]
+
+\begin{figure}
+  \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}
+  \caption{Function Type}
+\end{figure}
+
+\begin{figure}
+  \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}))}
+
+  \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. \force \upcast{U \u B_1}{U \u B_2}(\thunk ((\force f)))
+  }
+
+  
+  
+  \caption{Function Contract Theorem, Proof}
+\end{figure}
+
 \end{document}
 
 %% Local Variables: