diff --git a/paper/gtt.tex b/paper/gtt.tex
index b82df0b21769f1a131d96a37bb8c00fa2eb62cd1..c383f59b602f90029dbda83ed073db1cb0ac8bee 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -253,7 +253,7 @@
\newcommand{\dyncaseofXthenOnePairSumU}[5]{\kw{tycase} #1\,\{ #2 \pipe #3 \pipe #4 \pipe #5 \}}
\newcommand{\dyncaseofXthenYelseZ}[3]{\kw{tycase} #1\,\{ #2 \pipe #3 \}}
\newcommand{\dyncocaseWithFunF}[3]{\{\with \mapsto #1 \pipe (\to) \mapsto #2 \pipe \u F \mapsto #3 \}}
-\newcommand{\dyncaseofXthenBoolUPair}[5]{\kw{tycase} #1\,\{ #2 \pipe #3 \pipe #4 \pipe #5 \}}
+\newcommand{\dyncaseofXthenBoolUPair}[4]{\kw{tycase} #1\,\{ #2 \pipe #3 \pipe #4 \}}
\newcommand{\dyncocaseFunF}[2]{\{(\to) \mapsto #1 \pipe \u F \mapsto #2 \}}
\newcommand{\bnfalt}{\mathrel{\bf \,\mid\,}}
@@ -407,6 +407,7 @@ Saying that a resulting value satisfies type $A$ might be a strong
statement, but in transient semantics it only means that the head
connective satisfies the type.
%
+% AA: need to explain why blame is an element of system as defined.
The blame soundness theorem might also be quite strong, but depends on
the definition of blame, which is an element of the system as defined.
%
@@ -415,6 +416,13 @@ getting at the actual desired properties of the gradual language,
which are program equivalences in the typed portion of the code that
are not valid in the dynamically typed portion.
+% AA: To directly get at the desired properties of a gradual language, we will
+% first axiomatize all the properties we want, and then show what operational
+% semantics (models) satisfy the desired properties. This gives us a way of
+% exploring the design space: what are all the implementations that satisfy our
+% design criteria.
+% AA: (But we need to be clear about why $\eta$ is desired.)
+
In this paper, we systematically study questions of program equivalence
for a broad class of gradually typed languages by working in an
\emph{axiomatic theory} of gradual program equivalence, a language and
@@ -445,7 +453,8 @@ common.
The second property we take for granted is that the language satisfy
Siek-Vitousek-Cimini-Boyland's \emph{dynamic gradual guarantee}, a now
standard correctness theorem of gradual typing that most newly
-proposed gradual languages seek to satisfy.
+proposed gradual languages seek to satisfy.
+% AA: Following New-Ahmed, we call it graduality, which says that...
We then study what program equivalences are provable in GTT under
various assumptions.
@@ -461,7 +470,8 @@ We approach this problem by a surprising tack: rather than defining
the behavior of dynamic type casts and then verifying the $\beta$ and
$\eta$ equalities, we \emph{assume} the language satisfies $\beta$ and
$\eta$ equality and then show that certain reductions of casts are in
-fact \emph{theorems} in GTT.
+fact \emph{theorems} in GTT.
+% AA: should explain what it means for cast reductions to be "theorems"
%
This shows that gradually typed languages in which these reductions
are not program equivalences are \emph{not} models of the axioms we
@@ -490,7 +500,7 @@ overly eager: in its effort to find bugs faster than ``lazy''
semantics it disables the very program equivalences that gradual
typing is intended to provide.
-\subparagraph*{From $\eta$ Equality to Program Transformation}
+\paragraph*{From $\eta$ Equality to Program Transformation}
The reader unfamiliar with proof theory may find the centrality of
$\eta$ equalities in our development unusual.
@@ -596,6 +606,9 @@ In combination these proofs give an implementation of the term
language of GTT in which $\beta, \eta$ are observational equivalences
and the dynamic gradual guarantee is satisfied.
+% AA: first mention of uniqueness theorems below (since abstract)?
+% Need to give intuition about why they're good/important.
+
Due to the uniqueness theorems of GTT, there is very little of the
translation that cannot be directly ``calculated'' from the uniqueness
theorems.
@@ -2467,13 +2480,12 @@ establish the following theorems:
As a consequence we will also get the consistency of the type theory:
\begin{corollary}{Consistency of GTT}
- There exists a judgment $\Gamma_1 \ltdyn \Gamma_2 \vdash M_1 \ltdyn
- M_2 : B_1 \ltdyn B_2$ that is not provable.
+ The judgment $\vdash \ret \inl() \ltdyn \ret \inr() : \u F(1+1)$ is not
+ provable in GTT.
\end{corollary}
-\begin{proof}
- $\ret \tru \ltdyn \ret \fls$ is not provable since they are
- distinguished by the empty context.
-\end{proof}
+\begin{longproof}
+ They are distinguished by the identity context.
+\end{longproof}
We break down this proof into 3 major steps.
\begin{enumerate}
@@ -3082,16 +3094,11 @@ typed version of scheme's \emph{case-lambda} construct.
x : \bool \vdash E \equidyn \ifXthenYelseZ x {E[\tru/x]} {E[\fls/x]}\\
\upcast{1}{\bool}V \equidyn \tru\and
- \dncast{\u F 1}{\u F\bool}\ret V \equidyn \ifXthenYelseZ V {\ret ()} {\err}\\
\upcast{A+A}{\bool \times A}\inl V \equidyn (\tru, V)\and
\upcast{A+A}{\bool \times A}\inr V \equidyn (\fls, V)\\
- \upcast{\bool \times A}{A+A}(\tru, V) \equidyn \inl V\and
- \upcast{\bool \times A}{A+A}(\fls, V) \equidyn \inr V\\
\pi\dncast{\u B\with\u B}{\bool \to \u B}M \equidyn M\,\tru\and
\pi'\dncast{\u B\with\u B}{\bool \to \u B}M \equidyn M\,\fls\\
- (\dncast{\bool \to \u B}{\u B\with\u B}M)\,\tru\equidyn \pi M\and
- (\dncast{\bool \to \u B}{\u B\with\u B}M)\,\fls\equidyn \pi' M\\
\end{longonly}
\inferrule
@@ -3114,17 +3121,14 @@ typed version of scheme's \emph{case-lambda} construct.
{x_{\times}. E[\upcast{{\times}}{\dynv}/x_{\times}]}
{x_U. E[\upcast{U}{\dynv}/x_U]}}\quad(\dynv\eta)\\
- {\dncast{\u F \bool}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_\bool. \ret x_\bool}{\els \err}}\\
- {\dncast{\u F(\dynv\times\dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_\times. \ret x_\times}{\els \err}}\\
- {\dncast{\u F U\dync}{\u F\dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_U. \ret x_U}{\els \err}}\\
\end{longonly}
\inferrule
{\Gamma \pipe \Delta \vdash M_{\to} : \dynv \to \dync\\
- \Gamma \pipe \Delta \vdash M_{\u F} : \u F \dync}
- {\Gamma \pipe \Delta \vdash \dyncocaseFunF{M_{\to}}{M_{\u F}} : \u B}
+ \Gamma \pipe \Delta \vdash M_{\u F} : \u F \dynv}
+ {\Gamma \pipe \Delta \vdash \dyncocaseFunF{M_{\to}}{M_{\u F}} : \u B}\\
\begin{longonly}
- \dncast{\u G}{\dync}\dyncocaseFunF{M_{\to}}{M_{\u F}} \equidyn M_{\u G}\quad(\dync\beta)\\
+ \dncast{\u G}{\dync}\dyncocaseFunF{M_{\to}}{M_{\u F}} \equidyn M_{\u G}\quad(\dync\beta)
{\bullet : \dync \vdash \bullet
\equidyn
@@ -3132,13 +3136,95 @@ typed version of scheme's \emph{case-lambda} construct.
{\dncast{\dynv\to\dync}{\dync}\bullet}
{\dncast{\u F\dynv}{\dync}\bullet}}\quad(\dync\eta)\\
- \force\upcast{U(\dynv \to \dync)}{U\dync}V \equidyn \dyncocaseFunF{\force V}{\err}\\
- \force\upcast{U\u F\dynv}{U\dync}V \equidyn \dyncocaseFunF{\err}{\force V}\\
\end{longonly}
\end{mathpar}
\caption{Scheme-like Extension to GTT}
\end{figure}
+\begin{longonly}
+ The reader may be surprised by how \emph{few} axioms we need to add
+ to GTT for this extension: for instance we only define the upcast
+ from $1$ to $\bool$ and not vice-versa, and similarly the sum/lazy
+ pair type isomorphisms only have one cast defined when a priori
+ there are $4$ to be defined.
+ %
+ Finally for the dynamic types we define $\beta$ and $\eta$ laws
+ that use the ground casts as injections and projections
+ respectively, but we don't define the corresponding dual casts (the
+ ones that possibly error).
+
+ In fact all of these expected axioms can be \emph{proven} from those
+ we have shown.
+ %
+ Again we see the surprising rigidity of GTT: because an $\u F$
+ downcast is determined by its dual value upcast (and vice-versa for
+ $U$ upcasts), we only need to define the upcast as long as the
+ downcast \emph{could} be implemented already.
+ %
+ Because we give the dynamic types the universal property of a
+ sum/lazy product type respectively, we can derive the
+ implementations of the ``checking'' casts.
+ %
+ All of the proofs are direct from the uniqueness of adjoints
+ lemma.
+
+ \begin{theorem}[Boolean to Unit Downcast]
+ In Scheme-like GTT, we can prove
+ \[
+ \dncast{\u F1}{\u F\bool}\bullet
+ \equidyn
+ \bindXtoYinZ \bullet x \ifXthenYelseZ x {\ret()}{\err}
+ \]
+ \end{theorem}
+
+ \begin{theorem}[Tagged Value to Sum]
+ In Scheme-like GTT, we can prove
+ \[
+ \upcast{\bool \times A}{A+A}V \equidyn \pmpairWtoXYinZ V {x}{y} \ifXthenYelseZ x {\inl y}{\inr y}
+ \]
+ and the downcasts are given by lemma (TODO: some lemma about equidynamism isos)
+ \end{theorem}
+ \begin{theorem}[Lazy Product to Tag Checking Function]
+ In Scheme-like GTT, we can prove
+ \[
+ \dncast{\bool\to \u B}{\u B\with\u B}\bullet
+ \equidyn
+ \lambda x:\bool. \ifXthenYelseZ x {\pi \bullet}{\pi' \bullet}
+ \]
+ and the upcasts are given by lemma (TODO)
+ \end{theorem}
+
+ \begin{theorem}[Ground Mismatches are Errors]
+ In Schemish GTT we can prove
+ \begin{mathpar}
+ {\dncast{\u F \bool}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_\bool. \ret x_\bool}{\els \err}}\\
+ {\dncast{\u F(\dynv\times\dynv)}{\u F \dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_\times. \ret x_\times}{\els \err}}\\
+ {\dncast{\u F U\dync}{\u F\dynv}\ret V \equidyn \dyncaseofXthenYelseZ V {x_U. \ret x_U}{\els \err}}\\
+
+ \force\upcast{U(\dynv \to \dync)}{U\dync}V \equidyn \dyncocaseFunF{\force V}{\err}\\
+ \force\upcast{U\u F\dynv}{U\dync}V \equidyn \dyncocaseFunF{\err}{\force V}\\
+ \end{mathpar}
+ \end{theorem}
+
+ Finally, we note now that all of these axioms are satisfied when
+ using the Scheme-like dynamic type interpretation and extending the
+ translation of GTT into CBPV* with the following, tediously
+ explicit definition:
+ \begin{align*}
+ &\sem{\bool} = 1+1\\
+ &\sem{\tru} =\inl()\\
+ &\sem{\fls} =\inr()\\
+ &\sem{\ifXthenYelseZ V {E_t} {E_f}} = \caseofXthenYelseZ {\sem V}{x. E_t}{x.E_f}\\
+ &\sem{\dyncaseofXthenBoolUPair x {x_\bool. E_\bool}{x_U. E_U}{x_\times. E_\times}}
+ =\\
+ &\quad\pmmuXtoYinZ {(x:\dynv)} {x'} \pmmuXtoYinZ {x' : \texttt{Tree}[(1+1)+U\dync]}t \caseofX t\\
+ &\qquad\thenY{l. \caseofXthenYelseZ l {x_\bool. \sem{E_\bool}}{x_U. \sem{E_U}}}\\
+ &\qquad\elseZ{x_\times. \sem{E_\times}}\\
+ &\sem{\dyncocaseFunF{M_\to}{M_{\u F}}}
+ = \rollty{\nu \u Y. (\dynv \to \u Y)\with \u F\dynv}\pair{\sem{M_\to}}{\sem{M_{\u F}}}
+ \end{align*}
+\end{longonly}
+
Next, we easily see that if we want to limit to just the CBV types
(i.e. the only computation types are $A \to \u F A'$), then we can
restrict either of the previous interpretations as follows:
@@ -3175,8 +3261,15 @@ First, we define in figure \ref{fig:cast-to-contract} the extension of
the dynamic type interpretation to an interpretation of \emph{all}
casts in GTT.
%
-We extend this to a full translation from GTT to CBPV* by intepreting
-all other value and term constructors as themselves.
+The definition should be interpreted as ordered, since multiple cases
+could apply (though we will ultimately show they are equivalent).
+%
+The definition is also not obviously total: we need to verify that it
+covers every possible case where $A \ltdyn A'$ and $\u B \ltdyn \u
+B'$.
+%
+As in previous work, this is proven correct by an analysis of the type
+dynamism relation.
\begin{figure}
\begin{mathpar}
@@ -3237,23 +3330,168 @@ all other value and term constructors as themselves.
\label{fig:cast-to-contract}
\end{figure}
-\begin{lemma}[Type Preservation of Contract Translation]
+We present a normalized set of rules for type dynamism in figure
+\ref{fig:normalized}.
+%
+We can see that the definition of casts is defined by recursion on
+these derivations, so to prove that our definition is defined for all
+possible upcasts and downcasts it is sufficient to show that every
+rule of the original system is admissible in the normalized system.
+%
+Furthermore, it is clear that the normalized system is a subset of the
+original: every rule corresponds directly to a rule of the original
+system except the $A \ltdyn \dynv$ and similar $\u B \ltdyn \dync$
+rules use the $\dynv, \dync$ are top rules and transitivity.
+
+\begin{figure}
+ \begin{mathpar}
+ \inferrule
+ {A \in \{\dynv, 1\}}
+ {A \ltdyn A}
+
+ \inferrule
+ {A \in \{\dynv, 0\}}
+ {0 \ltdyn A}
+
+ \inferrule
+ {A \ltdyn \floor A\and
+ A \not\in\{0,\dynv \}}
+ {A \ltdyn \dynv}\\
+
+ \inferrule
+ {\u B \ltdyn \u B'}
+ {U B \ltdyn U B'}
+
+ \inferrule
+ {A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+ {A_1 + A_2 \ltdyn A_1' + A_2'}
+
+ \inferrule
+ {A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+ {A_1 \times A_2 \ltdyn A_1' \times A_2'}\\
+
+ \inferrule
+ {}
+ {\dync \ltdyn \dync}
+
+ \inferrule
+ {\u B \in \{ \dync, \top \}}
+ {\top \ltdyn \u B}
+
+ \inferrule
+ {\u B \ltdyn \floor {\u B} \and \u B \not\in \{ \top, \dync \}}
+ {\u B \ltdyn \dync}\\
+
+ \inferrule
+ {A \ltdyn A'}
+ {\u F A \ltdyn \u F A'}
+
+ \inferrule
+ {\u B_1 \ltdyn \u B_1' \and \u B_2 \ltdyn \u B_2'}
+ {\u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
+
+ \inferrule
+ {A \ltdyn A' \and \u B \ltdyn \u B'}
+ {A \to \u B \ltdyn A' \to \u B'}
+ \end{mathpar}
+ \caption{Normalized Type Dynamism Relation}
+\end{figure}
+
+\begin{lemma}[Normalized Type Dynamism is Equivalent to Original]
+ $T \ltdyn T'$ is provable in the normalized typed dynamism
+ definition if and only if it is provable in the original typed
+ dynamism definition.
+\end{lemma}
+\begin{longproof}
+ The forward direction is clear by an argument above. First we show
+ by induction that reflexivity is admissible:
\begin{enumerate}
- \item If $\Gamma \vdash M : \u B$ in GTT, then $\sem{\Gamma} \vdash
- \sem M : \sem {\u B}$ in \cbpvtxt.
- \item If $\Gamma \vdash V : A$ in GTT, then
- $\sem\Gamma \vdash \sem V : \sem{\u B}$ in \cbpvtxt.
- \item If $\Gamma \pipe \u B \vdash S : \u B'$in GTT, then
- $\sem{\Gamma} \pipe \sem{\u B} \vdash \sem S : \sem {\u B'}$ in \cbpvtxt.
+ \item If $A \in \{\dynv, 1, 0\}$, we use a normalized rule.
+ \item If $A \not\in\{\dynv, 1, 0\}$, we use the inductive hypothesis
+ and the monotonicity rule.
+ \item If $\u B\in \{\dync, \top\}$ use the normalized rule.
+ \item If $\u B \not\in\{\dync, \top\}$ use the inductive hypothesis
+ and monotonicity rule.
\end{enumerate}
+ Next we show that transitivity is admissible:
+ \begin{enumerate}
+ \item Assume we have $A \ltdyn A' \ltdyn A''$
+ \begin{enumerate}
+ \item If the left rule is $0 \ltdyn A'$, then either $A' = \dynv$
+ or $A' = 0$. If $A' = 0$ the right rule is $0 \ltdyn A''$ and we
+ can use that proof. Otherwise, $A' = \dynv$ then the right rule
+ is $\dynv \ltdyn \dynv$ and we can use $0 \ltdyn \dynv$.
+ \item If the left rule is $A \ltdyn A$ where $A \in \{ \dynv, 1\}$
+ then either $A = \dynv$, in which case $A'' = \dynv$ and we're
+ done. Otherwise the right rule is either $1 \ltdyn 1$ (done) or
+ $1 \ltdyn \dynv$ (also done).
+ \item If the left rule is $A \ltdyn \dynv$ with
+ $A\not\in\{0,\dynv\}$ then the right rule must be $\dynv \ltdyn
+ \dynv$ and we're done.
+ \item Otherwise the left rule is a monotonicity rule for one of
+ $U, +, \times$ and the right rule is either monotonicity (use
+ the inductive hypothesis) or the right rule is $A' \ltdyn \dynv$
+ with a sub-proof of $A' \ltdyn \floor{A'}$. Since the left rule
+ is monotonicity, $\floor{A} = \floor{A'}$, so we inductively use
+ transitivity of the proof of $A \ltdyn A'$ with the proof of $A'
+ \ltdyn \floor{A'}$ to get a proof $A \ltdyn \floor{A}$ and thus
+ $A \ltdyn \dynv$.
+ \end{enumerate}
+ \item Assume we have $\u B \ltdyn \u B' \ltdyn \u B''$.
+ \begin{enumerate}
+ \item If the left rule is $\top \ltdyn \u B'$ then $\u B'' \in
+ \{\dync, \top\}$ so we apply that rule.
+ \item If the left rule is $\dync\ltdyn \dync$, the right rule must
+ be as well.
+ \item If the left rule is $\u B \ltdyn \dync$ the right rule must
+ be reflexivity.
+ \item If the left rule is a monotonicity rule for $\with, \to, \u
+ F$ then the right rule is either also monotonicity (use the
+ inductive hypothesis) or it's a $\u B \ltdyn \dync$ rule and we
+ proceed with $\dynv$ above
+ \end{enumerate}
+ \end{enumerate}
+ Finally we show $A \ltdyn \dynv$, $\u B \ltdyn \dync$ are admissible
+ \begin{enumerate}
+ \item If $A \in \{ \dynv, 0\}$ we use the primitive rule.
+ \item If $A \not\in \{ \dynv, 0 \}$ we use the $A \ltdyn \dynv$ rule
+ and we need to show $A \ltdyn \floor A$. If $A = 1$, we use the
+ $1\ltdyn 1$ rule, otherwise we use the inductive hypothesis and
+ monotonicity.
+ \item If $\u B \in \{ \dync, \top\}$ we use the primitive rule.
+ \item If $\u B \not\in \{ \dync, \top \}$ we use the $\u B \ltdyn
+ \dync$ rule and we need to show $\u B \ltdyn \floor {\u B}$, which
+ follows by inductive hypothesis and monotonicity.
+ \end{enumerate}
+\end{longproof}
+
+Next, we extend the translation of casts to a translation of all terms.
+%
+Since all term constructions in GTT besides casts are constructions in
+CBPV*, we simply extend it by congruence.
+%
+We note that the translation is clearly type preserving in the
+following sense:
+\begin{lemma}[Type Preservation of Contract Translation]
+ If $\Gamma\pipe\Delta \vdash E : T$ in GTT, then $\sem{\Gamma}
+ \pipe\sem\Delta\vdash \sem E : \sem T$ in CBPV*.
\end{lemma}
+In effect we have now given a model of the types, terms and type
+dynamism proofs of GTT in CBPV*, and we now need to interpret the
+\emph{term dynamism} proofs.
+%
Our goal in the remainder of this section is to establish the
-following ``axiomatic graduality'' theorem, which interprets a term
-dynamism judgment of GTT as an ordering ``up to cast'' in CBPV. In the
-next section, we provide an operational \emph{model} of CBPV and thus
-obtain by composition an operational gradulity theorem (the dynamic
-gradual guarantee).
+following ``axiomatic graduality'' theorem, that defines such an
+interpretation.
+%
+The basic idea is that GTT has \emph{heterogeneous} term dynamism
+rules indexed by type dynamism, but CBPV* has only \emph{homogeneous}
+inequalities between terms with the same types.
+%
+Since every type dynamism judgment has an associated cast, we can
+translate a heterogeneous inequality to a homogeneous inequality
+\emph{up to cast}.
\begin{theorem}[Axiomatic Graduality]
For any dynamic type interpretation, the following are true:
\begin{mathpar}
@@ -3268,152 +3506,96 @@ gradual guarantee).
\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\sem{\Gamma} \vdash \supcast{A}{A'}[\sem{V}] \ltdyn\sem{V'}[\sem\Phi] : \sem {A'}}
\end{mathpar}
+ where we define $\sem{\Phi}, \sem{\Delta}$%
+ \begin{shortonly}
+ in the obvious way, where if $\Delta = \cdot$, then
+ $M[\sem{\Delta}] = M$.
+ \end{shortonly}
+ \begin{longonly}
+ as follows.
+ \begin{enumerate}
+ \item If $\Phi : \Gamma \ltdyn \Gamma'$, then there exists $n$
+ such that $\Gamma = x_1:A_1,\ldots,x_n:A_n$ and $\Gamma' =
+ x_1':A_1',\ldots,x_n':A_n'$ where $A_i \ltdyn A_i'$ for each
+ $i\leq n$.
+ Then $\sem{\Phi}$ is a substitution from $\sem{\Gamma}$ to $\sem{\Gamma'}$
+ defined as
+ \[ \sem{\Phi} = \supcast{A_1}{A_1'}x_1/x_1',\ldots\supcast{A_n}{A_n'}x_n/x_n' \]
+ \item If $\Psi : \Delta \ltdyn \Delta'$, then we similarly define
+ $\sem{\Psi}$ as a ``linear substitution''. That is, if $\Delta =
+ \Delta' = \cdot$, then $\sem{\Psi}$ is an empty substitution and
+ $M[\sem{\Psi}] = M$, otherwise $\sem{\Psi}$ is a linear
+ substitution from $\Delta' = \bullet : \u B'$ to $\Delta =
+ \bullet : \u B$ where $\u B \ltdyn \u B'$ defined as
+ \[ \sem\Psi = \sdncast{\u B}{\u B'}\bullet/\bullet \]
+ \end{enumerate}
+ \end{longonly}
\end{theorem}
+We note that in previous work on graduality (\cite{new-ahmed2018}),
+where to insert the casts was seen as an arbitrary choice because all
+casts there were syntactic evaluation contexts.
+%
+Here on the other hand, by using complex values and complex stacks for
+casts, using upcasts between value types and downcasts between
+computation types than the alternatives, which would require many uses
+of bind and thunk.
-Quite frequently we need the following commuting conversions, which
-are derivable from the $\eta$ rules for positive connectives.
-
-We need two versions of each rule for the positive value type
-connectives because of complex values: one when the continuation is a
-value and one when the continuation is a term.
-\begin{lemma}[Commuting Conversions]
- All of the following are provable when both sides are well-typed/scoped:
- % TODO: 1, 0?
- \begin{mathpar}
- E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]
- \equidyn
- \caseofXthenYelseZ V {x_1.E[V_1/y]}{x_2.E[V_2/y]}
-
- S[\caseofXthenYelseZ V {x_1.M_1}{x_2.M_2}]
- \equidyn
- \caseofXthenYelseZ V {x_1.S[M_1]}{x_2.S[M_2]}
-
- E[\pmpairWtoXYinZ V {x}{y} V'/z]
- \equidyn
- \pmpairWtoXYinZ V {x}{y} E[V'/z]
-
- S[\pmpairWtoXYinZ V {x}{y} M']
- \equidyn
- \pmpairWtoXYinZ V {x}{y} S[M']
-
- S[\bindXtoYinZ M x N]
- \equidyn
- \bindXtoYinZ M x S[N]
- \end{mathpar}
-\end{lemma}
-\begin{proof}
- \begin{enumerate}
- \item For $+$, we just show one case since the other is exactly the same:
- \begin{align*}
- &E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]\\
- &\equidyn
- \caseofXthenYelseZ V {x_1'. E[\caseofXthenYelseZ {\inl x_1'} {x_1.V_1}{x_2.V_2}/y]}{x_2'. E[\caseofXthenYelseZ {\inr x_2'} {x_1.V_1}{x_2.V_2}/y]}\tag{$+\eta$}\\
- &\equidyn \caseofXthenYelseZ V {x_1'. E[V_1[x_1'/x_1]]} {x_2'. E[V_2[x_2'/x_2]]}\tag{$+\beta$ twice}\\
- &\equidyn \caseofXthenYelseZ V {x_1. E[V_1]} {x_2. E[V_2]} \tag{$\alpha$}
- \end{align*}
- \item For $\times$
- \begin{align*}
- &E[\pmpairWtoXYinZ V x y V']\\
- &\pmpairWtoXYinZ V {x'}{y'} E[\pmpairWtoXYinZ {(x',y')} x y V']\tag{$\times\eta$}\\
- &\pmpairWtoXYinZ V {x'}{y'} E[V'[x'/x][y'/y]] \tag{$\times\beta$}\\
- &\pmpairWtoXYinZ V {x}{y} E[V'] \tag{$\alpha$}
- \end{align*}
- \item For $\u F$
- \begin{align*}
- &S[\bindXtoYinZ M x N]\\
- &\bindXtoYinZ M y S[\bindXtoYinZ {\ret y} x N]\tag{$\u F\eta$}\\
- &\bindXtoYinZ M y S[N[y/x]]\tag{$\u F\beta$}\\
- &\bindXtoYinZ M y S[N] \tag{$\alpha$}
- \end{align*}
- \end{enumerate}
-\end{proof}
+\begin{shortonly}
+ We present the key lemmas of the proof, and a few demonstrative cases.
+ %
+ The full proofs can be found in the supplementary material.
+\end{shortonly}
+\begin{longonly}
+ First, to keep proofs high-level, we establish the following cast
+ reductions that follow easily from $\beta,\eta$ principles.
\begin{lemma}{Cast Reductions}
The following are all provable
- \begin{mathpar}
- \sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inl V] \equidyn
+ \begin{align*}
+ &\sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inl V] \equidyn \inl \sem{\upcast{A_1}{A_1'}}[V]\\
+ &\sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inr V] \equidyn \inr \sem{\upcast{A_2}{A_2'}}[V]\\
+ &\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inl V] \equidyn
\bindXtoYinZ {\sem{\dncast{A_1}{A_1'}}[\ret V]} {x_1} \ret \inl x_1\\
-
- \sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inr V] \equidyn
+ &\sem{\dncast{\u F(A_1+A_2)}{\u F(A_1'+A_2')}}[\ret \inr V] \equidyn
\bindXtoYinZ {\sem{\dncast{A_2}{A_2'}}[\ret V]} {x_2} \ret \inr x_2\\
-
- \sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inl V] \equidyn \inl \sem{\upcast{A_1}{A_1'}}[V]\\
-
- \sem{\upcast{A_1+A_2}{A_1'+A_2'}}[\inr V] \equidyn \inr \sem{\upcast{A_2}{A_2'}}[V]\\
-
- \sem{\dncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}}[\ret (V_1,V_2)] \equidyn
+ &\sem{\dncast{\u F(A_1\times A_2)}{\u F(A_1'\times A_2')}}[\ret (V_1,V_2)]\\
+ &\quad\equidyn
\bindXtoYinZ {\sdncast{\u FA_1}{\u F A_1'}[\ret V_1]} {x_1} \bindXtoYinZ {\sdncast{\u FA_2}{\u F A_2'}[\ret V_2]} {x_2} \ret (x_1,x_2)\\
-
- \supcast{A_1\times A_2}{A_1'\times A_2'}[(V_1,V_2)] \equidyn (\supcast{A_1}{A_1'}[V_1], \supcast{A_2}{A_2'}[V_2])\\
-
- (\sdncast{A \to \u B}{A' \to \u B'} M)\, V \equidyn
+ &\supcast{A_1\times A_2}{A_1'\times A_2'}[(V_1,V_2)] \equidyn (\supcast{A_1}{A_1'}[V_1], \supcast{A_2}{A_2'}[V_2])\\
+ &(\sdncast{A \to \u B}{A' \to \u B'} M)\, V \equidyn
(\sdncast{\u B}{\u B'} M)\, (\supcast{A}{A'}{V})\\
-
- (\force (\supcast{U(A\to\u B)}{U(A'\to\u B')} V))\,V' \equidyn
+ &(\force (\supcast{U(A\to\u B)}{U(A'\to\u B')} V))\,V'\\
+ &\quad\equidyn
\bindXtoYinZ {\dncast{\u FA}{\u FA'}[\ret V']} x {\force (\supcast{U\u B}{U\u B'}{(\thunk (\force V\, x))})}\\
-
- \pi \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
+ &\pi \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
\sdncast{\u B_1}{\u B_1'} \pi M\\
-
- \pi' \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
+ &\pi' \sdncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} M \equidyn
\sdncast{\u B_2}{\u B_2'} \pi' M\\
-
- \pi \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
+ &\pi \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
\equidyn
\force \supcast{U\u B_1}{U\u B_1'}{\thunk (\pi \force V)}\\
-
- \pi' \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
+ &\pi' \force (\supcast{U(\u B_1 \with \u B_2)}{U(\u B_1' \with \u B_2')} V)
\equidyn
\force \supcast{U\u B_2}{U\u B_2'}{\thunk (\pi' \force V)}\\
-
- \sdncast{\u F U \u B}{\u F U \u B'}[\ret V] \equidyn \ret\thunk \sdncast{\u B}{\u B'}\force V\\
-
- \force \supcast{U\u FA}{U \u F A'}[V]
+ &\sdncast{\u F U \u B}{\u F U \u B'}[\ret V] \equidyn \ret\thunk \sdncast{\u B}{\u B'}\force V\\
+ &\force \supcast{U\u FA}{U \u F A'}[V]
\equidyn
\bindXtoYinZ {\force V} x \thunk\ret\upcast{A}{A'} x
- \end{mathpar}
+ \end{align*}
\end{lemma}
+\end{longonly}
-\begin{lemma}[EP Pairs Compose]
- \begin{enumerate}
- \item If $(V_1, S_1)$ is a value ep pair from $A_1$ to $A_2$ and
- $(V_2,S_2)$ is a value ep pair from $A_2$ to $A_3$, then
- $(V_2[V_1], S_1[S_2])$ is a value ep pair from $A_1$ to $A_3$.
- \item If $(V_1, S_1)$ is a computation ep pair from $\u B_1$ to $\u B_2$ and
- $(V_2,S_2)$ is a computation ep pair from $\u B_2$ to $\u B_3$, then
- $(V_2[V_1], S_1[S_2])$ is a computation ep pair from $\u B_1$ to $\u B_3$.
- \end{enumerate}
-\end{lemma}
-\begin{proof}
- \begin{enumerate}
- \item First, retraction follows from retraction twice:
- \[ S_1[S_2[\ret V_2[V_1[x]]]] \equidyn S_1[\ret [V_1[x]]] \equidyn x \]
- and projection follows from projection twice:
- \begin{align*}
- \bindXtoYinZ {S_1[S_2[\bullet]]} x \ret V_2[V_1[x]]
- &\equidyn
- {\bindXtoYinZ {S_1[S_2[\bullet]]} x \bindXtoYinZ {\ret [V_1[x]]} y \ret V_2[y]}\tag{$\u F\beta$}\\
- &\equidyn
- \bindXtoYinZ {(\bindXtoYinZ {S_1[S_2[\bullet]]} x {\ret [V_1[x]]})} y \ret V_2[y]\tag{Commuting conversion}\\
- &\ltdyn
- \bindXtoYinZ {S_2[\bullet]} y \ret V_2[y]\tag{Projection}\\
- &\ltdyn \bullet \tag{Projection}
- \end{align*}
- \item Again retraction follows from retraction twice:
- \[ S_1[S_2[\force V_2[V_1[z]]]] \equidyn S_1[\force V_1[z]] \equidyn \force z \]
- and projection from projection twice:
- \begin{align*}
- V_2[V_1[\thunk S_1[S_2[\force w]]]]
- &\equidyn V_2[V_1[\thunk S_1[\force \thunk S_2[\force w]]]]\tag{$U\beta$}\\
- &\ltdyn V_2[\thunk S_2[\force w]] \tag{Projection}\\
- &\ltdyn w \tag{Projection}
- \end{align*}
- \end{enumerate}
-\end{proof}
+The first main lemma is the following ``fundamental theorem'' for
+that says that from the basic casts being ep pairs, we can prove that
+all casts are ep pairs.
+%
+\begin{shortonly}
+ This follows mostly from straightforward calculation, but also from
+ some lemmas that say ep pairs compose.
+\end{shortonly}
\begin{lemma}[Casts are EP Pairs]
- For any dynamic type interpretation,
\begin{enumerate}
\item For any $A \ltdyn A'$, the casts $(x.\sem{\upcast{A}{A'}x},
\sem{\dncast{\u F A}{\u F A'}})$ are a value ep pair from
@@ -3423,7 +3605,7 @@ value and one when the continuation is a term.
pair from $\sem{\u B}$ to $\sem{\u B'}$.
\end{enumerate}
\end{lemma}
-\begin{proof}
+\begin{longproof}
By mutual induction on $A, \u B$
\begin{enumerate}
\item TODO: There's a few base cases about the dynamic type
@@ -3782,6 +3964,104 @@ value and one when the continuation is a term.
\end{align*}
\end{enumerate}
\end{enumerate}
+\end{longproof}
+
+\begin{longonly}
+Quite frequently we need the following commuting conversions, which
+are derivable from the $\eta$ rules for positive connectives.
+
+We need two versions of each rule for the positive value type
+connectives because of complex values: one when the continuation is a
+value and one when the continuation is a term.
+\begin{lemma}[Commuting Conversions]
+ All of the following are provable when both sides are well-typed/scoped:
+ % TODO: 1, 0?
+ \begin{mathpar}
+ E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]
+ \equidyn
+ \caseofXthenYelseZ V {x_1.E[V_1/y]}{x_2.E[V_2/y]}
+
+ S[\caseofXthenYelseZ V {x_1.M_1}{x_2.M_2}]
+ \equidyn
+ \caseofXthenYelseZ V {x_1.S[M_1]}{x_2.S[M_2]}
+
+ E[\pmpairWtoXYinZ V {x}{y} V'/z]
+ \equidyn
+ \pmpairWtoXYinZ V {x}{y} E[V'/z]
+
+ S[\pmpairWtoXYinZ V {x}{y} M']
+ \equidyn
+ \pmpairWtoXYinZ V {x}{y} S[M']
+
+ S[\bindXtoYinZ M x N]
+ \equidyn
+ \bindXtoYinZ M x S[N]
+ \end{mathpar}
+\end{lemma}
+\begin{proof}
+ \begin{enumerate}
+ \item For $+$, we just show one case since the other is exactly the same:
+ \begin{align*}
+ &E[\caseofXthenYelseZ V {x_1.V_1}{x_2.V_2}/y]\\
+ &\equidyn
+ \caseofXthenYelseZ V {x_1'. E[\caseofXthenYelseZ {\inl x_1'} {x_1.V_1}{x_2.V_2}/y]}{x_2'. E[\caseofXthenYelseZ {\inr x_2'} {x_1.V_1}{x_2.V_2}/y]}\tag{$+\eta$}\\
+ &\equidyn \caseofXthenYelseZ V {x_1'. E[V_1[x_1'/x_1]]} {x_2'. E[V_2[x_2'/x_2]]}\tag{$+\beta$ twice}\\
+ &\equidyn \caseofXthenYelseZ V {x_1. E[V_1]} {x_2. E[V_2]} \tag{$\alpha$}
+ \end{align*}
+ \item For $\times$
+ \begin{align*}
+ &E[\pmpairWtoXYinZ V x y V']\\
+ &\pmpairWtoXYinZ V {x'}{y'} E[\pmpairWtoXYinZ {(x',y')} x y V']\tag{$\times\eta$}\\
+ &\pmpairWtoXYinZ V {x'}{y'} E[V'[x'/x][y'/y]] \tag{$\times\beta$}\\
+ &\pmpairWtoXYinZ V {x}{y} E[V'] \tag{$\alpha$}
+ \end{align*}
+ \item For $\u F$
+ \begin{align*}
+ &S[\bindXtoYinZ M x N]\\
+ &\bindXtoYinZ M y S[\bindXtoYinZ {\ret y} x N]\tag{$\u F\eta$}\\
+ &\bindXtoYinZ M y S[N[y/x]]\tag{$\u F\beta$}\\
+ &\bindXtoYinZ M y S[N] \tag{$\alpha$}
+ \end{align*}
+ \end{enumerate}
+\end{proof}
+
+\end{longonly}
+
+\begin{lemma}[EP Pairs Compose]
+ \begin{enumerate}
+ \item If $(V_1, S_1)$ is a value ep pair from $A_1$ to $A_2$ and
+ $(V_2,S_2)$ is a value ep pair from $A_2$ to $A_3$, then
+ $(V_2[V_1], S_1[S_2])$ is a value ep pair from $A_1$ to $A_3$.
+ \item If $(V_1, S_1)$ is a computation ep pair from $\u B_1$ to $\u B_2$ and
+ $(V_2,S_2)$ is a computation ep pair from $\u B_2$ to $\u B_3$, then
+ $(V_2[V_1], S_1[S_2])$ is a computation ep pair from $\u B_1$ to $\u B_3$.
+ \end{enumerate}
+\end{lemma}
+\begin{proof}
+ \begin{enumerate}
+ \item First, retraction follows from retraction twice:
+ \[ S_1[S_2[\ret V_2[V_1[x]]]] \equidyn S_1[\ret [V_1[x]]] \equidyn x \]
+ and projection follows from projection twice:
+ \begin{align*}
+ \bindXtoYinZ {S_1[S_2[\bullet]]} x \ret V_2[V_1[x]]
+ &\equidyn
+ {\bindXtoYinZ {S_1[S_2[\bullet]]} x \bindXtoYinZ {\ret [V_1[x]]} y \ret V_2[y]}\tag{$\u F\beta$}\\
+ &\equidyn
+ \bindXtoYinZ {(\bindXtoYinZ {S_1[S_2[\bullet]]} x {\ret [V_1[x]]})} y \ret V_2[y]\tag{Commuting conversion}\\
+ &\ltdyn
+ \bindXtoYinZ {S_2[\bullet]} y \ret V_2[y]\tag{Projection}\\
+ &\ltdyn \bullet \tag{Projection}
+ \end{align*}
+ \item Again retraction follows from retraction twice:
+ \[ S_1[S_2[\force V_2[V_1[z]]]] \equidyn S_1[\force V_1[z]] \equidyn \force z \]
+ and projection from projection twice:
+ \begin{align*}
+ V_2[V_1[\thunk S_1[S_2[\force w]]]]
+ &\equidyn V_2[V_1[\thunk S_1[\force \thunk S_2[\force w]]]]\tag{$U\beta$}\\
+ &\ltdyn V_2[\thunk S_2[\force w]] \tag{Projection}\\
+ &\ltdyn w \tag{Projection}
+ \end{align*}
+ \end{enumerate}
\end{proof}
\begin{corollary}[Hom-set formulation of Adjunction]