From d50d6834aeec700548bd25184cac45fe684e6840 Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Mon, 9 Jul 2018 19:55:09 -0400
Subject: [PATCH] cut more
---
paper/gtt.tex | 130 ++++++++++++++++++++++++++++----------------------
1 file changed, 73 insertions(+), 57 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 2cf8c56..93ce54b 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -2116,9 +2116,9 @@ isomorphism $\u F A \cong \u F A'$, and dually~\cite{levy16popl}.
\end{proof}
\end{longonly}
+\begin{longonly}
\subsection{Derived Cast Rules}
-\begin{longonly}
As noted above, montonicity of type dynamism for $U$ and $\u F$ means
that we have the following as instances of the general cast rules:
\begin{lemma}[Shifted Casts]
@@ -2141,7 +2141,6 @@ that we have the following as instances of the general cast rules:
first rule $\u F A \ltdyn \u F A'$, and in the second, $U \u B \ltdyn
U \u B'$.
\end{longproof}
-\end{longonly}
The cast universal properties in Figure~\ref{fig:gtt-term-dyn-axioms}
imply the following seemingly more general rules for reasoning about
@@ -2168,7 +2167,6 @@ casts:
\end{mathpar}
\end{small}
\end{lemma}
-\begin{longonly}
In sequent calculus terminology, an upcast is left-invertible, while a
downcast is right-invertible, in the sense that any time we have a
conclusion with a upcast on the left/downcast on the right, we can
@@ -2177,7 +2175,6 @@ and downcasts forming a Galois connection). We write the $A \ltdyn A'$
and $\u B' \ltdyn \u B''$ premises on the non-invertible rules to
emphasize that the premise is not necessarily well-formed given that the
conclusion is.
-\end{longonly}
\begin{longproof}
For upcast left, substitute $V'$ into the axiom $x \ltdyn
@@ -2251,13 +2248,14 @@ For the fourth, by downcast right, it suffices show
$\dncast{\u B}{\u B''}{\bullet''}\ltdyn {\bullet''} : \u B \ltdyn \u B''$,
which is true by downcast left.
\end{longproof}
+\end{longonly}
\subsection{Type-generic Properties of Casts}
The universal property axioms for upcasts and downcasts in
Figure~\ref{fig:gtt-term-dyn-axioms} define them \emph{uniquely} up to
-equi-dynamism ($\equidyn$): anything with the same property like a cast
-is behaviorallty equivalent to a cast.
+equi-dynamism ($\equidyn$): anything with the same property
+is behaviorally equivalent to a cast.
\begin{theorem}[Specification for Casts is a Universal Property]
~ \label{thm:casts-unique}
@@ -2736,10 +2734,12 @@ The casts' behavior is uniquely determined as follows: \ifshort (See the extende
\bindXtoYinZ{\bullet}{p'} {\pmpairWtoXYinZ{p'}{x_1'}{x_2'}{}}\\
& & \bindXtoYinZ{\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}{x_1}\\
& & \bindXtoYinZ{\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}{x_2} {\ret (x_1,x_2) }\\
+\iflong
& \equidyn &
\bindXtoYinZ{\bullet}{p'} \pmpairWtoXYinZ{p'}{x_1'}{x_2'}{} \\
& & \bindXtoYinZ{\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}{x_2} \\
& & \bindXtoYinZ{\dncast{\u F A_1}{\u F A_1'}{\ret x_1'}}{x_1} {\ret (x_1,x_2) }
+\fi
\end{array}\\\\
%% if losing space due to not pagebreaking in the middle of this
%% \\\\
@@ -2770,12 +2770,13 @@ The casts' behavior is uniquely determined as follows: \ifshort (See the extende
\]
\end{small}
\end{theorem}
-The most interesting case is the downcast for an eager product, where
-there are two reasonable implementations, because there is a choice of
-sequencing between downcasting each component. The axioms of GTT imply
-that the two are equivalent; intuively, this is sensible because if the
-only effect a downcast introduces is a run-time error, then if either
-downcast errors, both possible implementations will.
+In the case for an eager product $\times$, we can actually also show
+that running ${\dncast{\u F A_2}{\u F A_2'}{\ret x_2'}}$ and then
+${\dncast{\u F A_1}{\u F A_1'}{\ret x_2'}}$ is also an implementation of
+this cast, and therefore equal to the above. Intuively, this is
+sensible because the only effect a downcast introduces is a run-time
+error, and if either downcast errors, both possible implementations
+will.
%% For the function downcast, the structure of CBPV nicely requires
%% let-binding the result of the downcast, rather than running the
%% downcast each time the variable occurs, which is a plausible
@@ -3761,12 +3762,14 @@ Let GTT$_G$ be the fragment of GTT where the only primitive casts are
those between ground types and the dynamic types, i.e. the cast terms
are restricted to the substitution closures of
\[
-\begin{array}{l|l}
+\begin{small}
+\begin{array}{llll}
x : G \vdash \upcast{G}{\dynv}{x} : \dynv &
-\bullet : \u F \dynv \vdash \dncast{\u F G}{\u F \dynv}{x} : \u F \dynv\\
+\bullet : \u F \dynv \vdash \dncast{\u F G}{\u F \dynv}{x} : \u F \dynv &
\bullet : \dync \vdash \dncast{\u G}{\dync}{\bullet} : \dync &
-x : U \u G \vdash \upcast{U \u G}{U \dync}{x} : U \dync \\
+x : U \u G \vdash \upcast{U \u G}{U \dync}{x} : U \dync
\end{array}
+\end{small}
\]
\begin{lemma}[Casts are Admissible] \label{lem:casts-admissible}
@@ -4552,6 +4555,7 @@ the case) and a payload with the actual value.
We can model this by using the canonical isomorphisms
\[ \dynv + \dynv \cong ((1+1) \times \dynv) \qquad \dync \with \dync \cong (1+1) \to \dync \]
and representing sums as pairs, and lazy products as functions.
+\begin{longonly}
The fact that isomorphisms are ep pairs is useful for constructing the
ep pairs needed in the dynamic type interpretation.
\begin{lemma}[Isomorphisms are EP Pairs]
@@ -4563,6 +4567,7 @@ ep pairs needed in the dynamic type interpretation.
\bullet$ and $S'[S] \equiv \bullet$ then $(z. S'[\force z], S)$ is an
ep pair from $\u B$ to $\u B'$.
\end{lemma}
+\end{longonly}
With this in mind, we remove the cases for sums and lazy pairs from the
natural dynamic types, and include some atomic type as a case of
@@ -4617,6 +4622,7 @@ This leads to the following definition:
be the ep pair to $1+1$ defined by the left case and
Lemma~\ref{lem:injections-are-embeddings}, composed with this. The ep
pair for $\dynv + \dynv$ is defined by composing the isomorphism
+ (which is always an ep pair)
$(\dynv + \dynv) \cong ((1+1) \times \dynv)$ with the ep pair for
$1+1$ using the action of product types on ep pairs (proven as part of
Theorem \ref{thm:axiomatic-graduality}): $(\dynv + \dynv) \cong
@@ -4733,9 +4739,10 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
\begin{mathpar}
1 \ltdyn \bool\and
A + A \equidyn \bool \times A\and
- \u B \with \u B \equidyn \bool \to \u B\\
+ \u B \with \u B \equidyn \bool \to \u B
\begin{longonly}
+ \\
\inferrule
{}
{\Gamma \vdash \tru, \fls : \bool}
@@ -4758,6 +4765,22 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
\pi'\dncast{\u B\with\u B}{\bool \to \u B}M \equidyn M\,\fls\\
\end{longonly}
+ \inferrule
+ {\Gamma \pipe \Delta \vdash M_{\to} : \dynv \to \dync\\
+ \Gamma \pipe \Delta \vdash M_{\u F} : \u F \dynv}
+ {\Gamma \pipe \Delta \vdash \dyncocaseFunF{M_{\to}}{M_{\u F}} : \dync}\\
+
+ \begin{longonly}
+ \dncast{\u G}{\dync}\dyncocaseFunF{M_{\to}}{M_{\u F}} \equidyn M_{\u G}\quad(\dync\beta)
+
+ {\bullet : \dync \vdash \bullet
+ \equidyn
+ \dyncocaseFunF
+ {\dncast{\dynv\to\dync}{\dync}\bullet}
+ {\dncast{\u F\dynv}{\dync}\bullet}}\quad(\dync\eta)\\
+
+ \end{longonly}
+
\inferrule
{\Gamma\pipe \Delta \vdash V : \dynv \and
\Gamma, x_{\bool}:\bool\pipe \Delta \vdash E_\bool : T\and
@@ -4777,23 +4800,8 @@ in the ep pairs used in Definition~\ref{def:scheme-like-type-interp}.
{x_\bool. E[\upcast{\bool}{\dynv}/x_\bool]}
{x_{\times}. E[\upcast{{\times}}{\dynv}/x_{\times}]}
{x_U. E[\upcast{U}{\dynv}/x_U]}}\quad(\dynv\eta)\\
-
\end{longonly}
- \inferrule
- {\Gamma \pipe \Delta \vdash M_{\to} : \dynv \to \dync\\
- \Gamma \pipe \Delta \vdash M_{\u F} : \u F \dynv}
- {\Gamma \pipe \Delta \vdash \dyncocaseFunF{M_{\to}}{M_{\u F}} : \dync}\\
- \begin{longonly}
- \dncast{\u G}{\dync}\dyncocaseFunF{M_{\to}}{M_{\u F}} \equidyn M_{\u G}\quad(\dync\beta)
-
- {\bullet : \dync \vdash \bullet
- \equidyn
- \dyncocaseFunF
- {\dncast{\dynv\to\dync}{\dync}\bullet}
- {\dncast{\u F\dynv}{\dync}\bullet}}\quad(\dync\eta)\\
-
- \end{longonly}
\end{mathpar}
\end{small}
\vspace{-0.4in}
@@ -6593,9 +6601,13 @@ to
%
In \cbpv, values include only introduction forms, as usual for values in
operational semantics, and \cbpv\/ stacks consist only of elimination
-forms for computation types (the syntax of \cbpv\/ enforces an A-normal
+forms for computation types
+\begin{longonly}
+(the syntax of \cbpv\/ enforces an A-normal
form, where only values can be pattern-matched on, so $\kw{case}$ and
-$\kw{split}$ are not evaluation contexts in the operational semantics).
+$\kw{split}$ are not evaluation contexts in the operational semantics)
+\end{longonly}
+.
\begin{longfigure}
\begin{small}
@@ -6898,9 +6910,8 @@ the same type.
The full translation is in the extended version, and is defined by a
simple structural induction that sequences the evaluation of the
translation of each complex value, e.g.
-\[\simpp{\caseofXthenYelseZ V {x_1. E_1}{x_2. E_2}} =
- \bindXtoYinZ {\simp V} x \caseofXthenYelseZ x {x_1. \simp {E_1}}{x_2. \simp {E_2}}
-\]
+$\simpp{\caseofXthenYelseZ V {x_1. E_1}{x_2. E_2}} =
+ \bindXtoYinZ {\simp V} x \caseofXthenYelseZ x {x_1. \simp {E_1}}{x_2. \simp {E_2}}$.
We could replace this translation with one as in \cite{levybook} that
introduces fewer administrative redices, but this translation is simpler
and suffices for reasoning up to observational equivalence.
@@ -6947,7 +6958,7 @@ some of the proofs simpler.
\end{small}
\end{definition}
\end{longonly}
-The translation is type-preserving
+The translation is type-preserving and the identity from \cbpvstar's point of view
\begin{lemma}[De-complexification De-complexifies]
For any \cbpvstar\/ term $\Gamma \pipe \Delta \vdash E : T$, $\simp E$
is a term of \cbpv\/ satisfying $\Gamma, \simp\Delta \vdash \simp E :
@@ -6955,7 +6966,7 @@ The translation is type-preserving
$\simp{\cdot} = \cdot$ $\simpp{\bullet:\u B} = z:U\u B$,
$\simp{\u B} = \u B$, $\simp A = \u F A$.
\end{lemma}
-\noindent and is the identity from \cbpvstar's point of view
+
\begin{lemma}[De-complexification is Identity in \cbpvstar]
Considering CBPV as a subset of \cbpvstar\, we have
\begin{enumerate}
@@ -6987,11 +6998,8 @@ In the inequational theory of \cbpv\/, this is defined by saying that
running $M$ to a value and then duplicating its value is the same as
runing $M$ every time we need its value.
\begin{definition}[Thunkable Computation]
- A computation $\Gamma \vdash M : \u FA$ is \emph{thunkable} if the
- following is provable:
- \[
- \Gamma \vdash \ret \thunk M \equidyn \bindXtoYinZ M x \ret\thunk\ret x : \u FU\u F A
- \]
+ A computation $\Gamma \vdash M : \u FA$ is \emph{thunkable} if \\
+ $\Gamma \vdash \ret \thunk M \equidyn \bindXtoYinZ M x \ret\thunk\ret x : \u FU\u F A$
\end{definition}
Dually, we show that complex stacks are translated to computations that
satisfy (semantic) \emph{linearity}, where intuitively a computation $M$
@@ -7004,22 +7012,36 @@ thunk that will force $z$ each time $M$ is forced---but if $M$ forces
$x$ exactly once, first, these two are the same.
\begin{definition}[Linear Term]
A term $\Gamma, x : U\u B \vdash M : \u C$ is \emph{linear in $x$}
- if the following is provable:
- \[
- \Gamma, z : U\u FU\u B \vdash
+ if\\
+ $\Gamma, z : U\u FU\u B \vdash
\bindXtoYinZ {\force z} x M
\equidyn
- M[\thunk{(\bindXtoYinZ {\force z} x \force x)}]
- \]
+ M[\thunk{(\bindXtoYinZ {\force z} x \force x)}]$
\end{definition}
Thunkability/linearity of the translations of complex values/stacks are
used to prove the preservation of the $\eta$ principles for positive
types and the strictness of complex stacks with respect to errors under
decomplexification.
+\begin{shortonly}
+ We have
+ \begin{theorem}[Soundness and Conservativity of De-Complexification] ~~
+ \begin{enumerate}
+ \item
+ If $\Gamma \vdash V : A$ is a (possibly) complex value, then $\Gamma
+ \vdash \simp V : \u F A$ is thunkable.
+\item If $\Gamma\pipe \bullet : \u B \vdash S : \u C$ is a (possibly)
+ complex stack, then $\Gamma, z : U\u B \vdash \simpp{S} : \u C$ is linear in $z$.
+\item If $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ then ${\Gamma, \simp
+ \Delta \vdash \simp E \ltdyn \simp{E'} : \simp T}$.
+\item If $M, M'$ are terms in CBPV and $M \ltdyn M'$ in \cbpvstar\
+ then $M \ltdyn M'$ in CBPV.
+ \end{enumerate}
+ \end{theorem}
+\end{shortonly}
\begin{longonly}
-We need a few lemmas about thunkables and linears to prove that
-complex values become thunkable and complex stacks become linear.
+We need a few lemmas about thunkables and linears to prove that complex
+values become thunkable and complex stacks become linear.
First, the following lemma is useful for optimizing programs with
thunkable subterms.
@@ -7078,7 +7100,6 @@ bigger thunkables from smaller ones.
By $\u F\beta$:
\[ \bindXtoYinZ {\ret V} x \ret\thunk\ret x \equidyn \ret\thunk\ret V \]
\end{proof}
-\end{longonly}
\begin{lemma}[Complex Values Simplify to Thunkable Terms]
If $\Gamma \vdash V : A$ is a (possibly) complex value, then $\Gamma
@@ -7137,7 +7158,6 @@ bigger thunkables from smaller ones.
\end{enumerate}
\end{longproof}
-\begin{longonly}
Dually, we have that a stack out of a force is linear and that linears
are closed under composition, so we can easily build up bigger linear
morphisms from smaller ones.
@@ -7177,7 +7197,6 @@ morphisms from smaller ones.
&\equidyn \bindXtoYinZ {\force z} x N[\thunk M/y]
\end{align*}
\end{proof}
-\end{longonly}
\begin{lemma}[Complex Stacks Simplify to Linear Terms]
If $\Gamma\pipe \bullet : \u B \vdash S : \u C$ is a (possibly)
@@ -7301,8 +7320,6 @@ Composing this with the previous translation from GTT to \cbpvstar\/
shows that \emph{GTT value type upcasts are thunkable and computation
type downcasts are linear}.
-\begin{longonly}
-
Since the translation takes values and stacks to terms, it cannot
preserve substitution up to equality.
%
@@ -7367,8 +7384,6 @@ composition.
\]
\end{enumerate}
\end{longproof}
-\end{longonly}
-
\begin{theorem}[De-complexification preserves Dynamism]
If $\Gamma \pipe \Delta \vdash E \ltdyn E' : T$ then ${\Gamma, \simp
@@ -7538,6 +7553,7 @@ composition.
de-complexification is equivalent to identity (in CBPV):
\[ M \equidyn \simp M \ltdyn \simp {M'} \equidyn M' \]
\end{longproof}
+\end{longonly}
\section{Operational Model of GTT}
\label{sec:operational}
--
GitLab