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}