From 1a8ea28606ee5c11b1e0d1ef25915122a2107838 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Tue, 24 Apr 2018 20:02:33 -0400
Subject: [PATCH] make upcasts uparrows, dncast down, add model stuff, start
function types
---
gcbpv.tex | 130 ++++++++++++++++++++++++++++++++++++++++++++++++++----
1 file changed, 122 insertions(+), 8 deletions(-)
diff --git a/gcbpv.tex b/gcbpv.tex
index 2d10118..bb8a398 100644
--- a/gcbpv.tex
+++ b/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:
--
GitLab