some notes on doing threesomes with cbpv

notes/impl.tex

+\documentclass{article}
+
+\usepackage{float}
+\usepackage{amsmath,amssymb, amsthm}
+\usepackage{tikz-cd}
+\usepackage{mathpartir}
+\usepackage{rotating}
+\usepackage{stmaryrd}
+
+\newtheorem{lemma}{Lemma}
+
+\renewcommand{\u}{\underline}
+\newcommand{\kw}[1]{\texttt{#1}\,\,}
+
+\newcommand{\sem}[1]{\llbracket#1\rrbracket}
+\newcommand{\dynv}{{?}}
+\newcommand{\dync}{\u {\text{?`}}}
+\newcommand{\ltdyn}{\sqsubseteq}
+\newcommand{\gtdyn}{\sqsupseteq}
+\newcommand{\equidyn}{\mathrel{\gtdyn\ltdyn}}
+\newcommand{\dynmeet}{\sqcap}
+\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{\case}{\kw{case}}
+\newcommand{\pipe}{\,|\,}
+\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
+\newcommand{\bindXtoYinZ}[2]{\kw{bind} #2 \leftarrow #1;}
+\newcommand{\ret}{\kw{ret}}
+\newcommand{\err}{\mho}
+\newcommand{\thunk}[1]{\{#1\}}
+\newcommand{\force}{!}
+
+\begin{document}
+
+\title{Zig-zag Casts in Gradual Type Theory}
+\author{Max S. New}
+
+\section{Reflecting on Type Dynamism}
+
+We translate GTT into a CBPV language extended with a pair of
+connectives that model.
+%
+These come in two forms: the delayed upcast of a thunk $(U)$, and the
+delayed downcast of a returner $(\u F)$.
+%
+In the contract translation, these cases are ``problematic''.
+%
+The upcast of a $U$ type introduces a proxy, for instance the cast
+$\upcast{U(2 \to \u B)}{U(\dynv \to \u B)}$ is implemented as:
+\[
+\sem{\upcast{U(2 \to \u B)}{U(\dynv \to \u B)}V}
+\cong
+\thunk{(\lambda (x:\dynv). \bindXtoYinZ {\dncast{\u F 2}{\u F \dynv}x} {(x':2)} \force V\, x')}
+\]
+%
+which adds an indirection to the actual implementation.
+%
+In general, one indirection seems unavoidable, but worse is that a
+sequence of upcasts of the same thunk will result in a linear number
+of indirections.
+%
+Dually, the downcast of a $\u F$ type is a \emph{non-tail} call, for
+instance the cast $\dncast{\u F 2}{\u F \dynv}$ is, in the natural and
+Scheme-like interpretations, implemented as a case-analysis:
+\[ \sem{\dncast{\u F 2}{\u F \dynv}M} \cong
+\bindXtoYinZ M x
+\caseofXthenYelseZ x {\texttt{in}_2 x_2. \ret x_2}{\texttt{else}. \err}
+\]
+if $M$ is a tail call, then this downcast breaks the tail call,
+because we need $M$ to return to the cast, which then performs the
+case-analysis and returns.
+%
+Adding one return indirection like this seems unavoidable, but worse
+is that a sequence of downcasts of $\u F$ types results in a linear
+number of indirections.
+
+Essentially these are the same/dual problems, and we solve them with
+the same/dual solution.
+%
+The basic idea is to consider the $U$ type of GTT \emph{not} to be a
+type of thunks, but \emph{delayed casts of thunks}.
+%
+That is, a value of type $U \u B$ in GTT is not necessarily
+represented by a $U \u B$ at runtime, but rather some original type
+$\u B_i$ (i for implementation) that has been casted to $U\u B$,
+\emph{via} some type $\u B_m$ (m for middle).
+%
+This is a ``threesome cast'' (which I will refer to as a zig-zag cast
+because it is more descriptive: we cast down and then up), the use of
+a middle type allows us to ``summarize'' a sequence of casts into a
+single pair of casts.
+%
+Thus in general the cast through the middle type will be
+\emph{stronger} than the direct cast: otherwise we wouldn't need the
+middle type at all.
+%
+We can represent this as a \emph{dependent pair}:
+\[ \sem{U \u B} = \sum_{\u Y \ltdyn \u B} \sum_{\u Y' \gtdyn \u Y} U\u Y' \]
+%
+Then a thunk is implemented by instantiating $\u Y$ with $\u B$ (using
+reflexivity):
+\[
+\sem{{\thunk M}_{\u B}} = (\u B \ltdyn \u B, \u B\gtdyn \u B, \thunk M)
+\]
+Forcing a proxied thunk is implemented by running the implementation
+of the zig zag of casts (which can be interpreted on the fly or a jump
+to a predetermined implementation):
+\[
+\sem{\force} (\u Y \ltdyn \u B, \u Y' \gtdyn \u Y, V : U\u Y') = \force \sem{\upcast{U\u Y}{U\u B}}\thunk {\sem{\dncast{\u Y}{\u Y'}}\force V}
+\]
+Finally, we compose with casts.
+%
+An upcast of a thunk is trivial: just replace $B$ with $B'$.
+%
+\[ \sem{\upcast{U B}{U B'}}(Y \ltdyn B, Y' \gtdyn Y, V) =
+(Y \ltdyn B', Y' \gtdyn Y, V)
+\]
+A downcast of a thunk does the real computation: we replace the middle
+type $Y$ with the \emph{meet} of $Y$:
+\[ \sem{\dncast{U B}{U B'}(Y \ltdyn B', Y' \gtdyn Y, V)}
+= (Y \dynmeet B \ltdyn B, Y' \gtdyn Y \dynmeet B, V) \]
+
+Dually, for $\u F$ types, we want the \emph{stacks} out of a $\u F$
+type to be delayed casts.
+%
+We translate a $\u F A$ term to a term that will perform a zig-zag
+cast when told which one to do, or in other words it expects the
+\emph{stack} to provide it a zig-zag.
+%
+We can represent this as a \emph{dependent function}:
+\[ \sem{\u F A} = \prod_{X \ltdyn A}\prod_{X' \gtdyn X} \u F X' \]
+A bind out of $\u F A$ is implemented by instantiating $X$ with $A$
+itself, using reflexivity of dynamism:
+\[ \sem{\bindXtoYinZ {M : \u F A} {x} {N}} = \bindXtoYinZ {M\,(A \ltdyn A)\,(A\ltdyn A)} x N \]
+Return is implemented by running the zigzag cast on the stack:
+\[ \sem{\ret{}} (V : A) = \lambda (X \ltdyn A) \lambda (X' \gtdyn X).
+\bindXtoYinZ {\sem{\dncast{\u F X}{\u F A}} \ret V} x \upcast{X}{X'} x \]
+
+The downcast is trivial, using transitivity of dynamism.
+\[
+\sem{\dncast{\u F A}{\u F A'}}[M]\,(X\ltdyn A)\,(X'\gtdyn X)
+=
+M\,(X \ltdyn A \ltdyn A')\,(X' \gtdyn X)
+\]
+The upcast does the work, computing the meet:
+\[
+\sem{\upcast{\u F A}{\u F A'}}[M]\,(X \ltdyn A')\,(X'\gtdyn X)
+=
+M\,(X \dynmeet A \ltdyn A)\,(X' \gtdyn X \gtdyn X \dynmeet A)
+\]
+
+We can model cast \emph{failure} by adding rules that $0, \top$ are
+least value and computation types respectively.
+
+%% \begin{figure}
+%%   \begin{mathpar}
+%%   \begin{array}{lcl}
+%%     A & \bnfdef & X \mid \mu X.A \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 \\
+%%     \u B  & ::= & \u Y\mid \nu \u Y. \u B \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B\\
+%%     \Gamma & ::= & \cdot \mid \Gamma, x : A \\
+%%     \Delta  & ::= & \cdot \mid \bullet : \u B \\
+%%     V  & ::= & x \mid \rollty{\mu X.A}V \mid \inl{V} \mid \inr{V} \mid \\
+%%        & & () \mid (V_1,V_2)\mid \thunk{M}
+%%     \\
+%%     M & ::= & \err_{\u B} \mid \letXbeYinZ V x M \mid \pmmuXtoYinZ V x M \mid \rollty{\nu \u Y.\u B} M \mid \unroll M \mid \abort{V} \mid \\
+%%     & & \caseofXthenYelseZ V {x_1. M_1}{x_2.M_2} \mid \pmpairWtoinZ V M \mid \pmpairWtoXYinZ V x y M
+%%     \mid \force{V} \mid \\
+%%     & & \ret{V} \mid \bindXtoYinZ{M}{x}{N} \mid \lambda x:A.M \mid M\,V \mid \emptypair \mid \pair{M_1}{M_2} \mid \pi M \mid \pi' M
+%%     \\
+%%     S & ::= & \bullet \mid \bindXtoYinZ S x M \mid S\, V \mid \pi S \mid \pi' S
+%%   \end{array}
+%%   \end{mathpar}
+%%   \caption{Operational GTT Syntax}
+%% \end{figure}
+
+\section{Correctness}
+
+We can show the correctness of this translation by showing that it
+\emph{simulates} the inefficient semantics.
+
+That is for any GTT type $T$ we can implement total ``wrapper''
+functions $T \Rightarrow \sem T$ and $\sem T \Rightarrow T$ with the
+property that for every term $\Gamma\pipe\Delta \vdash E : T$
+implemented in GTT, $E$ is equivalent to composing
+$\sem\Gamma\pipe\sem\Delta \vdash \sem E : \sem T$ with the wrappers.
+
+To prove this, the main lemma would be to prove
+\begin{lemma}[Correctness of Zigging through Meets]
+  {~}
+  \begin{enumerate}
+  \item For every zig-zag-zig $A_2' \gtdyn A_2 \ltdyn A_1' \gtdyn A_1$
+    the cast sequence
+    \[ \upcast{\u F A_2}{\u F A_2'}\dncast{\u F A_2}{\u F A_1'}\upcast{\u F A_1}{\u F A_1'} \]
+    is equivalent ($\equidyn$) to the single zig-zag:
+    \[ \upcast{\u F (A_2 \dynmeet A_1)}{\u F A_2'}\dncast{\u F (A_2 \dynmeet A_1)}{\u F A_1} \]
+  \item For every $B_1 \ltdyn B_1' \gtdyn B_2 \ltdyn B_2'$
+    the cast sequence
+    \[ \dncast{UB_1}{UB_1'}\upcast{UB_2}{UB_1'}\dncast{UB_2}{UB_2'} \]
+    is equivalent to the single zig-zag:
+    \[ \upcast{U(B_1 \dynmeet B_2)}{UB_1}\dncast{U(B_1 \dynmeet B_2)}{UB_2'} \]
+  \end{enumerate}
+\end{lemma}
+
+Which seems to want the following universal property of meets:
+\begin{lemma}[Meets turn a Zag-zig into a Zig-zag]
+  {~}
+  \begin{enumerate}
+  \item For any $A_1, A_2$, the cast through $\dynv$:
+    \[ \dncast{\u F A_1}{\u F \dynv}\upcast{\u F A_2}{\u F \dynv} \]
+    is equivalent to the cast through $\u F(A_1 \dynmeet A_2)$:
+    \[ \upcast{\u F (A_1 \dynmeet A_2)}{\u F A_1}\dncast{\u F (A_1 \dynmeet A_2)}{\u F A_2} \]
+  \item For any $B_1, B_2$, the cast through $\dync$:
+    \[ \dncast{U B_1}{U\dync}\upcast{UB_2}{U\dync} \]
+    is equivalent to the cast through $B_1 \dynmeet B_2$:
+    \[ \upcast{U(B_1\dynmeet B_2)}{UB_1}\dncast{U(B_1\dynmeet B_2)}{UB_2} \]
+  \end{enumerate}
+\end{lemma}
+
+\end{document}