diff --git a/paper/gtt.tex b/paper/gtt.tex
index bda75ca872539357f926b769c44976210e0967ca..fc462a2412428940d97b8071ed45db0756fef516 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -860,47 +860,165 @@ of $\beta, \eta$ and graduality for all of these interpretations.
\section{Axiomatic Gradual Type Theory}
\begin{figure}
+ \begin{small}
\[
\begin{array}{l}
- \begin{array}{l l}
- A ::= \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 &
- \u B ::= \colorbox{lightgray}{$\dync$} \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 \\
- \colorbox{lightgray}{$\Phi ::= \cdot \mid \Phi, x \ltdyn x': A \ltdyn A'$} &
- \colorbox{lightgray}{$\Psi ::= \cdot \mid \bullet \ltdyn \bullet : \u B \ltdyn \u B'$} \\
- T ::= A \mid \u B &
- E ::= V \mid M \\
- \end{array}\\
- \begin{array}{lcl}
- V & ::= & \colorbox{lightgray}{$\upcast A {A'} V$} \mid x \mid \abort{V}
- \mid \inl{V} \mid \inr{V} \mid \caseofXthenYelseZ V {x_1. V_1}{x_2.V_2} \mid \\
- & & () \mid \pmpairWtoinZ V V' \mid (V_1,V_2) \mid \pmpairWtoXYinZ V x y V' \mid \thunk{M}
- \\
- M,S & ::= & \colorbox{lightgray}{$\dncast{\u B} {\u B'} M$} \mid \bullet \mid \err_{\u B} \mid \letXbeYinZ V x 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
+ %
+ \begin{array}{rl|rl}
+ A ::= & \colorbox{lightgray}{$\dynv$} \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 &
+ \u B ::= & \colorbox{lightgray}{$\dync$} \mid \u F A \mid \top \mid \u B_1 \with \u B_2 \mid A \to \u B\\
+
+ V ::= & \begin{array}{l}
+ \colorbox{lightgray}{$\upcast A {A'} V$} \mid x \mid \abort{V} \\
+ \mid \inl{V} \mid \inr{V} \mid \caseofXthenYelseZ V {x_1. V_1}{x_2.V_2} \\
+ \mid () \mid \pmpairWtoinZ V V' \\
+ \mid (V_1,V_2) \mid \pmpairWtoXYinZ V x y V' \mid \thunk{M}
+ \end{array} &
+
+ M,S ::= & \begin{array}{l}
+ \colorbox{lightgray}{$\dncast{\u B} {\u B'} M$} \mid \bullet \mid \err_{\u B} \\
+ \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
+ \end{array}\\
+
+ \Gamma ::= & \cdot \mid \Gamma, x : A &
+ \Delta ::= & \cdot \mid \bullet : \u B \\
+ \colorbox{lightgray}{$\Phi$} ::= & \colorbox{lightgray}{$\cdot \mid \Phi, x \ltdyn x': A \ltdyn A'$} &
+ \colorbox{lightgray}{$\Psi$} ::= & \colorbox{lightgray}{$\cdot \mid \bullet \ltdyn \bullet : \u B \ltdyn \u B'$} \\
+ \end{array}\\\\
+ \begin{array}{c}
+ \hspace{2.5in} T ::= A \mid \u B \\
+ \hspace{2.5in} E ::= V \mid M \\
+ \end{array}\\\\
+ %
+ \begin{array}{c}
+ \framebox{$\Gamma \vdash V : A$ and $\Gamma \mid \Delta \vdash M : \u B$} \qquad
+ \colorbox{lightgray}{
+ \inferrule
+ {\Gamma \vdash V : A \and A \ltdyn A'}
+ {\Gamma \vdash \upcast A {A'} V : A'}
+ \qquad
+ \inferrule
+ {\Gamma\pipe \Delta \vdash M : \u B' \and \u B \ltdyn \u B'}
+ {\Gamma\pipe \Delta \vdash \dncast{\u B}{\u B'} M : \u B}
+ }
+ \\\\
+ \inferrule
+ { }
+ {\Gamma,x : A,\Gamma' \vdash x : A}
+ \qquad
+ \inferrule
+ { }
+ {\Gamma\pipe \bullet : \u B \vdash \bullet : \u B}
+ \qquad
+ \inferrule
+ { }
+ {\Gamma \mid \cdot \vdash \err_{\u B} : \u B}
+ \\\\
+ \inferrule
+ {\Gamma \vdash V : 0}
+ {\Gamma \mid \Delta \vdash \abort V : T}
+ \qquad
+ \inferrule
+ {\Gamma \vdash V : A_1}
+ {\Gamma \vdash \inl V : A_1 + A_2}
+ \qquad
+ \inferrule
+ {\Gamma \vdash V : A_2}
+ {\Gamma \vdash \inr V : A_1 + A_2}
+ \qquad
+ \inferrule
+ {
+ \Gamma \vdash V : A_1 + A_2 \\\\
+ \Gamma, x_1 : A_1 \mid \Delta \vdash E_1 : T \\\\
+ \Gamma, x_2 : A_2 \mid \Delta \vdash E_2 : T
+ }
+ {\Gamma \mid \Delta \vdash \caseofXthenYelseZ V {x_1. E_1}{x_2.E_2} : T}
+ \\\\
+ \inferrule
+ { }
+ {\Gamma \vdash (): 1}
+ \qquad
+ \inferrule
+ {\Gamma \vdash V : 1 \and
+ \Gamma \mid \Delta \vdash E : T
+ }
+ {\Gamma \mid \Delta \vdash \pmpairWtoinZ V E : T}
+ \qquad
+ \inferrule
+ {\Gamma \vdash V_1 : A_1\and
+ \Gamma\vdash V_2 : A_2}
+ {\Gamma \vdash (V_1,V_2) : A_1 \times A_2}
+ \qquad
+ \inferrule
+ {\Gamma \vdash V : A_1 \times A_2 \\\\
+ \Gamma, x : A_1,y : A_2 \mid \Delta \vdash E : T
+ }
+ {\Gamma \mid \Delta \vdash \pmpairWtoXYinZ V x y E : T}
+ \\\\
+ \inferrule
+ {\Gamma \mid \cdot \vdash M : \u B}
+ {\Gamma \vdash \thunk M : U \u B}
+ \qquad
+ \inferrule
+ {\Gamma \vdash V : U \u B}
+ {\Gamma \pipe \cdot \vdash \force V : \u B}
+ \qquad
+ \inferrule
+ {\Gamma \vdash V : A}
+ {\Gamma \pipe \cdot \vdash \ret V : \u F A}
+ \qquad
+ \inferrule
+ {\Gamma \pipe \Delta \vdash M : \u F A \\\\
+ \Gamma, x: A \pipe \cdot \vdash N : \u B}
+ {\Gamma \pipe \Delta \vdash \bindXtoYinZ M x N : \u B}
+ \\\\
+ \inferrule
+ {\Gamma, x: A \pipe \Delta \vdash M : \u B}
+ {\Gamma \pipe \Delta \vdash \lambda x : A . M : A \to \u B}
+ \qquad
+ \inferrule
+ {\Gamma \pipe \Delta \vdash M : A \to \u B\and
+ \Gamma \vdash V : A}
+ {\Gamma \pipe \Delta \vdash M\,V : \u B }
+ \\\\
+ \inferrule{ }{\Gamma \mid \Delta \vdash \emptypair : \top}
+ \qquad
+ \inferrule
+ {\Gamma \mid \Delta \vdash M_1 : \u B_1\and
+ \Gamma \mid \Delta \vdash M_2 : \u B_2}
+ {\Gamma \mid \Delta \vdash \pair {M_1} {M_2} : \u B_1 \with \u B_2}
+ \qquad
+ \inferrule
+ {\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
+ {\Gamma \mid \Delta \vdash \pi M : \u B_1}
+ \qquad
+ \inferrule
+ {\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
+ {\Gamma \mid \Delta \vdash \pi' M : \u B_2}
\end{array}
\end{array}
\]
- \vspace{-0.2in}
- \caption{GTT Syntax}
- \label{fig:gtt-syntax}
+\end{small}
+ \vspace{-0.1in}
+ \caption{GTT Syntax and Term Typing}
+ \label{fig:gtt-syntax-and-terms}
\end{figure}
-\subsection{Call-by-Push-Value}
+\subsection{Background: Call-by-Push-Value}
Because the extensionality principles for types play a key role in our
analysis of gradual typing, it is necessary to work in a setting where
we can have extensionality principles for both data (e.g. sum types) and
computations (e.g. functions). One such setting is Levy's
-Call-by-Push-Value~\citep{levyXXcbv-book} (CBPV). The syntax of CBPV is
-the unshaded rules in Figure~\ref{fig:gtt-syntax}, and the term typing
-rules for CBPV are the rules for these constructs in
-Figure~\ref{fig:gtt-type-dynamism-and-terms}. We briefly review the
-basic concepts of CBPV; see ~\cite{levybook,eff,frank?,...} for more
-details. CBPV makes a distinction between \emph{value types} $A$ and
+Call-by-Push-Value~\citep{levyXXcbv-book} (CBPV). The syntax and term
+typing of CBPV is the unshaded rules in
+Figure~\ref{fig:gtt-syntax-and-terms}. We briefly review the basic
+concepts of CBPV; see ~\cite{levybook,eff,frank?,...} for more details.
+CBPV makes a distinction between \emph{value types} $A$ and
\emph{computation types} $\u B$, where value types classify
\emph{values} $\Gamma \vdash V : A$ and computation types classify
\emph{computations} $\Gamma \vdash M : \u B$. Effects are computations:
@@ -934,7 +1052,7 @@ elimination rule whose branches are values
(e.g. $\caseofXthenYelseZ{s}{x_1.V_1}{x_2.V_2}$) and one whose branches
are computations (e.g. $\caseofXthenYelseZ{s}{x_1.M_1}{x_2.M_2}$). To
abbreviate the typing rules for both in
-Figure~\ref{fig:gtt-type-dynamism-and-terms}, we use the following
+Figure~\ref{fig:gtt-syntax-and-terms}, we use the following
convention: we write $E$ for either a complex value or a computation,
and $T$ for either a value type $A$ or a computation type $\u B$, and a
judgement $\Gamma \mid \Delta \vdash E : T$ for either $\Gamma \vdash V
@@ -1015,39 +1133,40 @@ focus rules. In the equational theory of CBPV, $\u F$ and $U$ are
B$ are bijective with values $x : A \vdash V : U \u B$, as both are
bijective with computations $x : A \vdash M : \u B$.
-To compress the presentation in
-Figure~\ref{fig:gtt-type-dynamism-and-terms}, we use a typing judgement
-$\Gamma \mid \Delta \vdash M : \u B$ with a ``stoup''~\citep{girard?},
-i.e. a typing context $\Delta$ that is either empty or contains exactly
-one assumption $\bullet : \u B$, so $\Gamma \mid \cdot \vdash M : \u B$
-is a computation, while $\Gamma \mid \bullet : \u B \vdash M : \u B'$ is
-a stack. The typing rules for $\top$ and $\with$ treat the stack input
-variable additively; for a function application to be a stack, the stack
-input must occur in the function position of a function application. The
-elimination form for $U \u B$, $\force{V}$, is the prototypical
-non-stack computation ($\Delta$ is required to be empty), because
-forcing a thunk does not use the stack input.
+To compress the presentation in Figure~\ref{fig:gtt-syntax-and-terms},
+we use a typing judgement $\Gamma \mid \Delta \vdash M : \u B$ with a
+``stoup''~\citep{girard?}, i.e. a typing context $\Delta$ that is either
+empty or contains exactly one assumption $\bullet : \u B$, so $\Gamma
+\mid \cdot \vdash M : \u B$ is a computation, while $\Gamma \mid \bullet
+: \u B \vdash M : \u B'$ is a stack. The typing rules for $\top$ and
+$\with$ treat the stack input variable additively; for a function
+application to be a stack, the stack input must occur in the function
+position of a function application. The elimination form for $U \u B$,
+$\force{V}$, is the prototypical non-stack computation ($\Delta$ is
+required to be empty), because forcing a thunk does not use the stack
+input.
\paragraph{Embedding call-by-value and call-by-name}
-To translate call-by-value into CBPV, a judgement $x_1 : A_1, \ldots,
-x_n : A_n \vdash e : A$ is interpreted as a computation $x_1 : A_1,
-\ldots, x_n : A_n \vdash e^* : \u F A$, where call-by-value products and
-sums are interpreted as $\times$ and $+$, and the call-by-value function
-type $A \to A'$ as $U(A \to \u F A')$. Thus, a call-by-value term $e :
-A \to A'$, which should mean an effectful computation of a function
-value, is translated to a computation of type $e^* : \u F U (A \to \u F
-A')$. Here, the comonad $\u F U$ offers an opportunity to perform
-effects \emph{before} returning a function value, in addition to effects
-that are performed when the function is applied---so under transalation
-the CBV terms $\print c; \lambda x. e$ and $\lambda x.\print c; e$ will
-not be contextually equivalent. To translate call-by-name to CBPV, a
-judgement $x_1 : \u B_1, \ldots, x_n : \u B_n \vdash e : \u B$ is
-translated to $x_1 : U \u B_1, \ldots, x_n : U \u B_n \vdash e_* : \u
-B$, representing the fact that call-by-name terms are passed thunked
-arguments. Product types are translated to $\top$ and $\times$, while a
-CBN function $B \to B'$ is translated to $U \u B \to \u B'$ with a
-thunked argument. Sums $B_1 + B_2$ are translated to $\u F (U \u B_1 +
-U \u B_2)$, making the ``lifting'' in lazy sums explicit.
+To translate call-by-value (CBV) into CBPV, a judgement $x_1 : A_1,
+\ldots, x_n : A_n \vdash e : A$ is interpreted as a computation $x_1 :
+A_1, \ldots, x_n : A_n \vdash e^* : \u F A$, where call-by-value
+products and sums are interpreted as $\times$ and $+$, and the
+call-by-value function type $A \to A'$ as $U(A \to \u F A')$. Thus, a
+call-by-value term $e : A \to A'$, which should mean an effectful
+computation of a function value, is translated to a computation of type
+$e^* : \u F U (A \to \u F A')$. Here, the comonad $\u F U$ offers an
+opportunity to perform effects \emph{before} returning a function value,
+in addition to effects that are performed when the function is
+applied---so under transalation the CBV terms $\print c; \lambda x. e$
+and $\lambda x.\print c; e$ will not be contextually equivalent. To
+translate call-by-name (CBN) to CBPV, a judgement $x_1 : \u B_1, \ldots,
+x_n : \u B_n \vdash e : \u B$ is translated to $x_1 : U \u B_1, \ldots,
+x_n : U \u B_n \vdash e_* : \u B$, representing the fact that
+call-by-name terms are passed thunked arguments. Product types are
+translated to $\top$ and $\times$, while a CBN function $B \to B'$ is
+translated to $U \u B \to \u B'$ with a thunked argument. Sums $B_1 +
+B_2$ are translated to $\u F (U \u B_1 + U \u B_2)$, making the
+``lifting'' in lazy sums explicit.
%% While these rules are very intuitive when the input and output types
%% of the stack are $\u F A$ for some value type (which is always the
@@ -1098,7 +1217,8 @@ $\eta$ principle for functions in CBPV is that any computation $M : A
translated to a CBPV computation of type $U \u B \to \u B'$, to which
CBPV function extensionality applies, while a CBV term $e : A \to A'$ is
translated to a computation of type $\u F U(A \to \u F A')$, which does
-not satisfy the $\eta$ rule for functions.
+not satisfy the $\eta$ rule for functions. We discuss a formal
+statement of these extensionality principles with term dynamism below.
%% \begin{mathpar}
%% \inferrule
@@ -1109,114 +1229,81 @@ not satisfy the $\eta$ rule for functions.
%% {\Gamma \vdash S[\print V; M] \equidyn \print V; S[M] : \u C}
%% \end{mathpar}
-\subsection{Call-by-Push-Value, Gradualized}
-
-In figure \ref{judge} we present the syntax of Gradual Type Theory.
-%
-For the types inherited from CBPV, we follow the dogma of
-gradualization: everything is monotone with respect to the ordering,
-and to axiomatize strong type soundness we include the $\beta$ and
-$\eta$ principles of CBPV as order equivalences, but otherwise
-unmodified.
-
-
-\subsection{Casts}
-
-It is not immediately obvious how to add type casts to
-call-by-push-value, but we can use previous work on call-by-value and
-call-by-name gradual typing, combined with the embeddings of CBV and
-CBN into CBPV for guidance.
-%
-In both CBV and CBN, we add a type dynamism judgment $A \ltdyn B$ and
-for every such pair, we add an upcast from $A$ to $B$: $\upcast A B M$
-and a downcast from $B$ to $A$: $\dncast A B M$.
-%
-Then because CBV types are associated to CBPV value types and CBN
-types are associated to CBPV computation types, it seems reasonable to
-simply have a value type dynamism $A \ltdyn A'$ and computation type
-dynamism $\u B \ltdyn \u B'$ and an upcast and downcast form for each
-corresponding to the CBV and CBN casts.
-%
-A CBV terms $x : A \vdash M : A'$ is in CBPV a term $x : A \vdash M :
-\u F A'$, because in call by value values are passed as arguments,
-then effects are performed and possibly a value is returned.
-%
-A CBN term $x : \u B \vdash M : \u B'$ is in CBPV a term $x : U \u
-B\vdash M : \u B'$, because in CBN unevaluated thunks are passed as
-arguments and terms satisfy the $\eta$ laws of the computation type.
+\subsection{The Dynamic Type(s)}
+
+Next, we discuss the additions that make CBPV into our gradual type
+theory GTT. In many accounts of gradual typing, dynamic typing is
+integrated into a statically typed language by way of a \emph{dynamic
+ type} $\dynv$, which in some sense includes all of the static types of
+the language. For example, one implementation of a dynamic type is as a
+recursive type such that $\dynv \cong (\dynv + \dynv) + (\dynv \times
+\dynv) + (\dynv \to \dynv)$ etc. for each type constructor of the static
+language. Then dynamically typed code is represented by statically
+typed code that works with the dynamic type $\dynv$.
+
+Since GTT has two different kinds of types, we have a new question of
+whether the dynamic type should be a value type, or a computation type,
+or whether we should have \emph{two} dynamic types: a dynamic value type
+and a dynamic computation type.
+%
+Our modular, type-theoretic presentation of gradual typing allows us to
+easily explore all of these options, by including or not including each,
+though we find that (surprisingly) having both a dynamic value $\dynv$
+and a dynamic computation type $\dync$ gives the most natural
+implementation (see Section~\ref{sec:dynamic-type-interp}). Thus, we
+add both $\dynv$ and $\dync$ to the grammar of types in
+Figure~\ref{fig:gtt-syntax-and-terms}. We do \emph{not} give
+introduction and elimination rules for the dynamic types, because we
+would like constructions in GTT to imply results for many different
+possible implementations of the dynamic types. Instead, the terms for
+the dynamic types will arise from type dynamism and casts.
+
+\subsection{Type Dynamism}
+
+The \emph{type dynamism} relation of gradual type
+theory~\cite{nl18cbngtt} corresponds to the type precision relation of
+\cite{siek} and the na\"ive subtyping of \cite{wadler-findler}. We
+write type dynamism as $A \ltdyn A'$, which is read as ``$A'$ is more
+dynamic than $A$''; intuitively, this means that $A'$ supports more
+behaviors than $A$. \cite{nl18cbngtt,icfp} analyze this as the
+existence of an \emph{upcast} from $A$ to $A'$ and a downcast from $A'$
+to $A$ which form an embedding-projection pair (\emph{ep pair}) for an
+ordering on terms where runtime type errors are minimal: the upcast
+followed by the downcast is a no-op, while the downcast followed by the
+upcast might error more than the original term, because it imposes a
+run-time type check. Syntactically, type dynamism is defined (1) to be
+reflexive and transitive (a preorder), (2) where every type constructor
+is monotone is all positions, and (3) where the dynamic type is greatest
+in the type dynamism ordering. In \cite{fscd}, this last condition,
+\emph{the dynamic type is the most dynamic type}, then implies the
+existence of an upcast $\upcast{A}{\dynv}$ and a downcast
+$\dncast{A}{\dynv}$ which give a kind of intro and elim for the dynamic
+type: any type can be embedded into it and projected from it. While
+this gives some information about the dynamic type, it by design does
+not characterize $\dynv$ uniquely up to isomorphism (e.g. as a recursive
+sum)---instead, it is left open-ended exactly which types exist, and
+therefore which injections/projections $\dynv$ has, to allow theorems in
+gradual type theory that are open-ended with respect to the addition of
+new types.
+
+We extend this in a straightforward way to CBPV's distinction between
+value and computation types in Figure~\ref{fig:gtt-type-dynamism}: there
+is a type dynamism relation for value types $A \ltdyn A'$ and for
+computation types $\u B \ltdyn \u B'$, which (1) each are preorders, (2)
+every type constructor is monotone, where the shifts $\u F$ and $U$
+switch which relation is being considered, and (3) the dynamic value
+type $\dynv$ is the most dynamic value type, and the dynamic computation
+type $\dync$ is the most dynamic computation type. For example, we have
+$U(A \to \u F A') \ltdyn U(\dynv \to \u F \dynv)$, which is the analogue
+of $A \to A' \ltdyn \dynv \to \dynv$ in call-by-value---because $\to$
+preserves embedding-retraction pairs, it is monotone, not contravariant,
+in the domain~\cite{fscd,icfp}.
\begin{figure}
- \begin{mathpar}
- \inferrule
- {\Gamma \vdash V : A \and A \ltdyn A'}
- {\Gamma \vdash \upcast {A}{A'} V : \u F A'}
-
- \inferrule
- {\Gamma \vdash V' : A' \and A \ltdyn A'}
- {\Gamma \vdash \dncast {A}{A'} V' : \u F A}
-
- \inferrule
- {\Gamma \vdash V : U \u B \and \u B \ltdyn \u B'}
- {\Gamma \vdash \upcast {\u B}{\u B'} V : \u B'}
-
- \inferrule
- {\Gamma \vdash V' : U \u B' \and \u B \ltdyn \u B'}
- {\Gamma \vdash \dncast {\u B}{\u B'} V' : \u B'}
- \end{mathpar}
- \caption{Na\"ive Interpretation of Casts}
- \label{Bad Casts}
-\end{figure}
-
-So to reproduce this in GTT, we could add casts to the language as in
-figure \ref{bad-casts}, which we call the ``na\"ive'' interpretation
-of casts.
-%
-We call it na\"ive because it is problematic for multiple reasons:
-some syntactic and some semantic.
-
-First, semantically, it is \emph{insufficient} to recover all of the
-known properties of casts in CBV: specifically that in CBV, upcasts
-always terminate without performing any effects, and in some systems
-upcasts are defined to be values.
-%
-In previous work on a logical relation for call-by-value gradual
-typing, it was possible to prove from the properties we axiomatized
-that all upcasts had this property, but this was only because we were
-working in a language whose only effects were divergence and error.
-%
-In a language with effects,
-
-The na\"ive casts are also problemantic syntactically.
-%
-The first issue is that they violate a type theoretic principle of
-\emph{modularity}: every construction of the language should be
-independent of the presence of any other.
-%
-In this case, the na\"ive casts all violate this principle because the
-casts for value types use $\u F$ and the casts for computation types
-use $U$.
-%
-TODO: do we actually know what would go wrong in that case?
-
-%% Counterexample
-
-%% consider a language whose only effects are error and incrementing
-%% and decrementing an integer counter.
-%%
-
-%% Then for closed programs with unit output, P <= P' when P ->* err
-%% or P ->* (n, ()) and P' ->* (n', ()) and n = n', where n,n' are the
-%% final counts
-
-%% Then for every type A, there are CBV coreflections (e(x) = inc; ret x | p(y) = dec; ret y)
-
-\newpage
-
-\begin{figure}[t]
\begin{small}
\begin{mathpar}
- \framebox{$A \ltdyn A'$ and $\u B \ltdyn \u B'$}
+ \framebox{$A \ltdyn A'$ and $\u B \ltdyn \u B'$}
\inferrule{ }{A \ltdyn A}
@@ -1262,118 +1349,313 @@ TODO: do we actually know what would go wrong in that case?
\inferrule{\u B \ltdyn \u B'}
{(\bullet \ltdyn \bullet : \u B \ltdyn \u B') \, \dyncctx}
\end{mathpar}
+\caption{GTT Type Dynamism and Dynamism Contexts}
+\label{fig:gtt-type-dynamism}
+\end{small}
+\end{figure}
-\begin{mathpar}
-\framebox{$\Gamma \vdash V : A$ and $\Gamma \mid \Delta \vdash M : \u B$}
+\subsection{Casts}
+
+Even given previous work on call-by-value~\cite{icfp} and
+call-by-name~\cite{fscd} gradual typing, it is not immediately obvious
+how to add type casts to CPBV, because CBPV exposes finer judgemental
+distinctions than were considered in previous work. However, we can use
+this previous work, with the embeddings of CBV and CBN into CBPV, for
+guidance.
+%
+In the previous work on both CBV and CBN, every type dynamism judgement
+$A \ltdyn A'$ induces both an upcast from $A$ to $A'$ and a downcast
+from $A'$ to $A$.
+%
+Because CBV types are associated to CBPV value types and CBN types are
+associated to CBPV computation types, this suggests that each value type
+dynamism $A \ltdyn A'$ should induce an upcast and a downcast, and each
+computation type dynamism $\u B \ltdyn \u B'$ should also induce an
+upcast and a downcast.
+%
+In CBV, a cast from $A$ to $A'$ typically can be represented by a CBV
+function $A \to A'$, whose analogue in CBPV is $U(A \to \u F A')$, and
+values of this type are bijective with computations $x : A \vdash M : \u
+F A'$. Since computations $x : A \vdash M : \u F A'$ are bijective with
+stacks $\bullet : \u F A \vdash \bindXtoYinZ{\bullet}{x}{M} : \u F A'$,
+this suggests that a \emph{value} type dynamism $A \ltdyn A'$ should
+induce an embedding-projection pair of \emph{stacks} $\bullet : \u F A
+\vdash S_u : \u F A'$ and $\bullet : \u F A' \vdash S_d : \u F A$.
+%
+Dually, a CBN cast typically can be represented by a CBN function of
+type $B \to B'$, whose CBPV analogue is a computation of type $U \u B
+\to \u B'$, or equivalently a computation $x : U \u B \vdash M : \u B'$,
+Since computations $x : U \u B \vdash M : \u B'$ are bijective with
+values $x : U \u B \vdash \thunk{M} : U \u B'$, this suggests that a
+\emph{computation} type dynamism $\u B \ltdyn \u B'$ should induce an
+embedding-projection pair of \emph{values} $x : U \u B \vdash V_u : U \u
+B'$ and $x : U \u B' \vdash V_d : U \u B$.
+
+However, this analysis ignores an important property of CBV casts:
+upcasts always terminate without performing any effects, and in some
+systems upcasts are even defined to be values. For example, an upcast
+from $A$ to $\dynv$ is often implemented as a sum/recursive type
+injection, which are value constructors. In previous work on a logical
+relation for call-by-value gradual typing~\cite{icfp}, it was possible
+to prove that all upcasts had this property (but this depended on the
+only effects being divergence and type error). In GTT, we can make this
+property explicit in the syntax of the casts, by making the upcast
+$\upcast{A}{A'}$ induced by a value type precision $A \ltdyn A'$ itself
+a complex value, rather than computation. On the other hand, a downcast
+between value types is typically implemented as a case-analysis looking
+for a specific tag, and therefore can error, and so should be a
+computation, not a complex value.
+
+In the present work, we make a dual observation about CBN casts. The
+\emph{downcast} arising from $\u B \ltdyn \u B'$ has a stronger property
+than being a computation $x : U \u B' \vdash M : \u B$ as suggested
+above: it can be taken to be a stack $\bullet : \u B' \vdash \dncast{\u
+ B}{\u B'}{\bullet} : \u B$. This formalizes the intuitive idea that a
+downcast evaluates the computation it is ``wrapping'' exactly once.
+Intuitively, this point of view is justified by thinking of the dynamic
+computation type $\dync$ as a recursive \emph{product} of all possible
+behaviors that a computation might have, and the downcast as a recursive
+type unrolling and product projection, which is a stack. From this
+point of view, an \emph{upcast} can introduce errors, because the upcast
+of an object supporting some ``methods'' to one with all possible
+methods will error dynamically on the unimplemented ones.
+
+These observations are expressed in the (shaded) rules for casts in
+Figure~\ref{fig:gtt-syntax-and-terms}: the upcast for a value type
+precsion is a complex value, while the downcast for a computation type
+precsion is a stack (if its argument is). Indeed, the description of
+the casts is simpler than the intuition we began the section with: from
+these two rules and monotonicity of type precsion for $U$/$\u F$ types,
+we automatically obtain the \emph{downcast} for a \emph{value} type
+precision $A \ltdyn A'$ as a stack $\bullet : \u F A' \vdash \dncast{\u
+ F A}{\u F A'}{\bullet} : \u F A$ as described above, representing the
+fact that the downcast might fail. We also automatically obtain the
+upcast for a computation type precsion $\u B \ltdyn \u B'$ as a value $x
+: U \u B \vdash \upcast{U \u B}{U \u B'}{x} : U \u B'$ as suggested
+above. Moreover, we will show below that the value upcast
+$\upcast{A}{A'}$ induces a stack $\bullet : \u F A \vdash \ldots : \u F
+A'$ that behaves like an upcast, and dually for the downcast, so this
+formulation is stronger than the one suggested above.
+
+We justify the stronger assertion that value type upcasts are complex
+values and computation type downcasts are complex stacks in two ways in
+the remainder of the paper. In Section~\ref{sec:contract}, we show how
+to implement casts by a contract translation to CBPV in such a way that
+it is true, so there is at least one model where casts have these
+properties. However, one goal of GTT is to be able to prove things
+about many gradually typed languages at once, by giving different
+interpretations of the syntax, so one might wonder whether this design
+rules out potential models where casts are only computations. In
+Theorem~\ref{sec:thm:upcasts-values-downcasts-stacks}, we show instead
+that this design is forced for all casts, as long as the casts between
+ground types and the dynamic types have this property, which is true in
+all implementations we are aware of.
+
+%% Counterexample
+
+%% consider a language whose only effects are error and incrementing
+%% and decrementing an integer counter.
+%%
+
+%% Then for closed programs with unit output, P <= P' when P ->* err
+%% or P ->* (n, ()) and P' ->* (n', ()) and n = n', where n,n' are the
+%% final counts
+
+%% Then for every type A, there are CBV coreflections (e(x) = inc; ret x | p(y) = dec; ret y)
+
+\subsection{Term Dynamism Judgements and Structural Rules}
+
+The final piece of GTT is the \emph{term dynamism} relation, a syntactic
+judgement that is used for reasoning about the behavorial properties of
+terms in GTT. To a first approximation, term dynamism can be thought of
+as syntactic rules for reasoning about \emph{contextual approximation},
+where $E \ltdyn E'$ means that either $E$ errors or $E$ and $E'$ have
+the same result. However, a key idea in GTT is to consider a
+\emph{heterogeneous} term dynamism judgement $E \ltdyn E' : T \ltdyn T'$
+between terms $E : T$ and $E' : T'$ where $T \ltdyn T'$---i.e. relating
+two terms at two different types, where the type on the right is more
+dynamic than the type on the right. This judgement structure allows
+simple axioms characterizing the behavior of casts~\cite{fscd}. Here,
+we break this judgement up into value dynamism $V \ltdyn V' : A \ltdyn
+A'$ and computation dynamism $M \ltdyn M' : \u B \ltdyn \u B'$. To
+support reasoning about open terms, the full form of the judgements are
+\begin{itemize}
+\item $\Gamma \ltdyn \Gamma' \vdash V \ltdyn V' : A \ltdyn A'$ where
+ $\Gamma \vdash V : A$ and $\Gamma' \vdash V' : A'$ and $\Gamma \ltdyn
+ \Gamma'$ and $A \ltdyn A'$.
+\item
+$\Gamma \ltdyn \Gamma' \mid \Delta \ltdyn \Delta' \vdash M \ltdyn M' :
+ \u B \ltdyn \u B'$ where $\Gamma \mid \Delta \vdash M : \u B$ and
+ $\Gamma' \mid \Delta' \vdash M' : \u B'$.
+\end{itemize}
+where $\Gamma \ltdyn \Gamma'$ is the pointwise lifting of value type
+dynamism, and $\Delta \ltdyn \Delta'$ is the optional lifting of
+computation type dynamism. In Figure~\ref{fig:gtt-type-dynamism} we
+define $\Phi$ and $\Psi$ as syntax for ``zipped'' pairs of contexts that
+are pointwise related by type dynamism, because the notation $x \ltdyn
+x' : A \ltdyn A'$ correctly suggests that one can substitute related
+terms for related variables. We will implicitly zip/unzip pairs of
+contexts, and sometimes write e.g. $\Gamma \ltdyn \Gamma$ to mean $x
+\ltdyn x : A \ltdyn A$ for all $x : A$ in $\Gamma$.
+
+The basic structural rules of term dynamism in
+Figure~\ref{fig:gtt-term-dynamism-structural} say that it is reflexive
+and transitive, that assumptions can be used and substituted for, and
+that every term constructor is monotone. This much of the definition
+can be derived in a generic way from the typing rules.
+
+Type dynamism is reflexive, and we will often abbreviate a homogeneous
+term dynamism by writing e.g. $\Gamma \vdash V \ltdyn V' : A \ltdyn A'$
+for $\Gamma \ltdyn \Gamma \vdash V \ltdyn V' : A \ltdyn A'$, or $\Phi
+\vdash V \ltdyn V' : A$ for $\Phi \vdash V \ltdyn V' : A \ltdyn A$, and
+similarly for computations. The entirely homogeneous judgements $\Gamma
+\vdash V \ltdyn V' : A$ and $\Gamma \mid \Delta \vdash M \ltdyn M' : \u
+B$ can be thought of straightforwardly as a syntax for contextual
+approximation; the structural rules of term precsion then say that this
+is a preorder, has identity and substitution principles, and is a
+congruence for all term constructors. We often write $V \equidyn V'$ to
+mean term dynamism relations in both directions (which requires that the
+types are also equidynamic, typically because they are identical), which
+can be thought of as a syntactic judgement for contextual equivalence.
+
+\begin{figure}
+\begin{small}
+ \begin{mathpar}
+ \framebox{$\Phi \vdash V \ltdyn V' : A \ltdyn A'$ and $\Phi \mid \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'$}
+ \\
+
+ \inferrule{ }{\Gamma \ltdyn \Gamma \mid \Delta \ltdyn \Delta \vdash E \ltdyn E : T \ltdyn T}
+
+ \inferrule{\Gamma \ltdyn \Gamma' \mid \Delta \ltdyn \Delta' \vdash E \ltdyn E' : T \ltdyn T' \\\\
+ \Gamma' \ltdyn \Gamma'' \mid \Delta' \ltdyn \Delta'' \vdash E' \ltdyn E'' : T' \ltdyn T''
+ }
+ {\Gamma \ltdyn \Gamma'' \mid \Delta \ltdyn \Delta'' \vdash E \ltdyn E'' : T \ltdyn T''}
+ \\
\inferrule
{ }
- {\Gamma,x : A,\Gamma' \vdash x : A}
+ {\Phi,x \ltdyn x' : A \ltdyn A',\Phi' \vdash x \ltdyn x' : A \ltdyn A'}
\inferrule
- { }
- {\Gamma\pipe \bullet : \u B \vdash \bullet : \u B}
+ {\Phi \vdash V \ltdyn V' : A \ltdyn A' \\\\
+ \Phi, x \ltdyn x' : A \ltdyn A',\Phi' \pipe \Psi \vdash E \ltdyn E' : T \ltdyn T'
+ }
+ {\Phi \mid \Psi \vdash E[V/x] \ltdyn E'[V'/x'] : T \ltdyn T'}
\inferrule
{ }
- {\Gamma \mid \cdot \vdash \err_{\u B} : \u B}
+ {\Phi \pipe \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \bullet : \u B \ltdyn \u B'}
- \\
- \inferrule
- {\Gamma \vdash V : A \and A \ltdyn A'}
- {\Gamma \vdash \upcast A {A'} V : A'}
- \qquad
\inferrule
- {\Gamma\pipe \Delta \vdash M : \u B' \and \u B \ltdyn \u B'}
- {\Gamma\pipe \Delta \vdash \dncast{\u B}{\u B'} M : \u B}
-\\
- \inferrule
- {\Gamma \vdash V : 0}
- {\Gamma \mid \Delta \vdash \abort V : T}
-
+ {\Phi \pipe \Psi \vdash M_1 \ltdyn M_1' : \u B_1 \ltdyn \u B_1' \\\\
+ \Phi \pipe \bullet \ltdyn \bullet : \u B_1 \ltdyn \u B_1' \vdash M_2 \ltdyn M_2' : \u B_2 \ltdyn \u B_2'
+ }
+ {\Phi \mid \Psi \vdash M_2[M_1/\bullet] \ltdyn M_2'[M_1'/\bullet] : \u B_2 \ltdyn \u B_2'}
+ \\
+ %% congruence for casts is derivable, right?
+ \\
\inferrule
- {\Gamma \vdash V : A_1}
- {\Gamma \vdash \inl V : A_1 + A_2}
+ {\Phi \vdash V \ltdyn V' : A_1 \ltdyn A_1'}
+ {\Phi \vdash \inl V \ltdyn \inl V' : A_1 + A_2 \ltdyn A_1' + A_2'}
\inferrule
- {\Gamma \vdash V : A_2}
- {\Gamma \vdash \inr V : A_1 + A_2}
-
+ {\Phi \vdash V \ltdyn V' : A_2 \ltdyn A_2'}
+ {\Phi \vdash \inr V \ltdyn \inr V' : A_1 + A_2 \ltdyn A_1' + A_2'}
+ \\
\inferrule
{
- \Gamma \vdash V : A_1 + A_2 \\\\
- \Gamma, x_1 : A_1 \mid \Delta \vdash E_1 : T \\\\
- \Gamma, x_2 : A_2 \mid \Delta \vdash E_2 : T
+ \Phi \vdash V \ltdyn V' : A_1 + A_2 \ltdyn A_1' + A_2' \\\\
+ \Phi, x_1 \ltdyn x_1' : A_1 \ltdyn A_1' \mid \Psi \vdash E_1 \ltdyn E_1' : T \ltdyn T' \\\\
+ \Phi, x_2 \ltdyn x_2' : A_2 \ltdyn A_2' \mid \Psi \vdash E_2 \ltdyn E_2' : T \ltdyn T'
}
- {\Gamma \mid \Delta \vdash \caseofXthenYelseZ V {x_1. E_1}{x_2.E_2} : T}
- \\
+ {\Phi \mid \Psi \vdash \caseofXthenYelseZ V {x_1. E_1}{x_2.E_2} \ltdyn \caseofXthenYelseZ V {x_1'. E_1'}{x_2'.E_2'} : T'}
+
\inferrule
- { }
- {\Gamma \vdash (): 1}
- \qquad
+ {\Phi \vdash V \ltdyn V' : 0 \ltdyn 0}
+ {\Phi \mid \Psi \vdash \abort V \ltdyn \abort V' : T \ltdyn T'}
+ \\
\inferrule
- {\Gamma \vdash V : 1 \and
- \Gamma \mid \Delta \vdash E : T
+ {\Phi \vdash V \ltdyn V' : 1 \ltdyn 1 \\\\
+ \Phi \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
}
- {\Gamma \mid \Delta \vdash \pmpairWtoinZ V E : T}
- \qquad
+ {\Phi \mid \Psi \vdash \pmpairWtoinZ V E \ltdyn \pmpairWtoinZ V' E' : T \ltdyn T'}
+ \and
\inferrule
- {\Gamma \vdash V_1 : A_1\and
- \Gamma\vdash V_2 : A_2}
- {\Gamma \vdash (V_1,V_2) : A_1 \times A_2}
- \qquad
+ {\Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'\\\\
+ \Phi\vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'}
+ {\Phi \vdash (V_1,V_2) \ltdyn (V_1',V_2') : A_1 \times A_2 \ltdyn A_1' \times A_2'}
+ \\
\inferrule
- {\Gamma \vdash V : A_1 \times A_2 \\\\
- \Gamma, x : A_1,y : A_2 \mid \Delta \vdash E : T
+ {\Phi \vdash V \ltdyn V' : A_1 \times A_2 \ltdyn A_1' \times A_2' \\\\
+ \Phi, x \ltdyn x' : A_1 \ltdyn A_1', y \ltdyn y' : A_2 \ltdyn A_2' \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
}
- {\Gamma \mid \Delta \vdash \pmpairWtoXYinZ V x y E : T}
+ {\Phi \mid \Psi \vdash \pmpairWtoXYinZ V x y E \ltdyn \pmpairWtoXYinZ {V'} {x'} {y'} {E'} : T \ltdyn T'}
\\
+
\inferrule
- {\Gamma \mid \cdot \vdash M : \u B}
- {\Gamma \vdash \thunk M : U \u B}
+ {\Phi \mid \cdot \vdash M \ltdyn M' : \u B \ltdyn \u B'}
+ {\Phi \vdash \thunk M \ltdyn \thunk M' : U \u B \ltdyn U \u B'}
\inferrule
- {\Gamma \vdash V : U \u B}
- {\Gamma \pipe \cdot \vdash \force V : \u B}
-
+ {\Phi \vdash V \ltdyn V' : U \u B \ltdyn U \u B'}
+ {\Phi \pipe \cdot \vdash \force V \ltdyn \force V' : \u B \ltdyn \u B'}
+ \\
+
\inferrule
- {\Gamma \vdash V : A}
- {\Gamma \pipe \cdot \vdash \ret V : \u F A}
+ {\Phi \vdash V \ltdyn V' : A \ltdyn A'}
+ {\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
\inferrule
- {\Gamma \pipe \Delta \vdash M : \u F A \\\\
- \Gamma, x: A \pipe \cdot \vdash N : \u B}
- {\Gamma \pipe \Delta \vdash \bindXtoYinZ M x N : \u B}
+ {\Phi \pipe \Psi \vdash M \ltdyn M' : \u F A \ltdyn \u F A' \\\\
+ \Phi, x \ltdyn x' : A \ltdyn A' \pipe \cdot \vdash N \ltdyn N' : \u B \ltdyn \u B'}
+ {\Phi \pipe \Psi \vdash \bindXtoYinZ M x N \ltdyn \bindXtoYinZ {M'} {x'} {N'} : \u B \ltdyn \u B'}
\inferrule
- {\Gamma, x: A \pipe \Delta \vdash M : \u B}
- {\Gamma \pipe \Delta \vdash \lambda x : A . M : A \to \u B}
+ {\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
+ {\Phi \pipe \Psi \vdash \lambda x : A . M \ltdyn \lambda x' : A' . M' : A \to \u B \ltdyn A' \to \u B'}
\inferrule
- {\Gamma \pipe \Delta \vdash M : A \to \u B\and
- \Gamma \vdash V : A}
- {\Gamma \pipe \Delta \vdash M\,V : \u B }
+ {\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \\\\
+ \Phi \vdash V \ltdyn V' : A \ltdyn A'}
+ {\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
\\
- \inferrule{ }{\Gamma \mid \Delta \vdash \emptypair : \top}
-
\inferrule
- {\Gamma \mid \Delta \vdash M_1 : \u B_1\and
- \Gamma \mid \Delta \vdash M_2 : \u B_2}
- {\Gamma \mid \Delta \vdash \pair {M_1} {M_2} : \u B_1 \with \u B_2}
-
+ {\Phi \mid \Psi \vdash M_1 \ltdyn M_1' : \u B_1 \ltdyn \u B_1'\and
+ \Phi \mid \Psi \vdash M_2 \ltdyn M_2' : \u B_2 \ltdyn \u B_2'}
+ {\Phi \mid \Psi \vdash \pair {M_1} {M_2} \ltdyn \pair {M_1'} {M_2'} : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
+ \\
\inferrule
- {\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
- {\Gamma \mid \Delta \vdash \pi M : \u B_1}
+ {\Phi \mid \Psi \vdash M \ltdyn M' : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
+ {\Phi \mid \Psi \vdash \pi M \ltdyn \pi M' : \u B_1 \ltdyn \u B_1'}
\inferrule
- {\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
- {\Gamma \mid \Delta \vdash \pi' M : \u B_2}
+ {\Phi \mid \Psi \vdash M \ltdyn M' : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
+ {\Phi \mid \Psi \vdash \pi' M \ltdyn \pi' M' : \u B_2 \ltdyn \u B_2'}
\end{mathpar}
-\caption{GTT Type Dynamism, Dynamism Contexts, and Terms}
-\label{fig:gtt-type-dynamism-and-terms}
+ \vspace{-0.1in}
+ \caption{GTT Term Dynamism (Structural and Congruence Rules)}
+ \label{fig:gtt-term-dynamism-structural}
\end{small}
\end{figure}
+\subsection{Term Dynamism Axioms}
+
+Finally, we assert some term dynamism axioms that are specific to the
+programs involved. Only a few of these axioms are specific to GTT as
+opposed to being inherited from CBPV, those in the top of
+Figure~\ref{fig:gtt-term-dynamism-axioms} that pertain to casts.
+FIXME: explain
+
+The axioms in the middle of the figure assert the $\beta\eta$
+rules for each type as (homogeneous) term equidynamisms (these should be
+understood as applying under the typing conditions that make both sides
+type check, in any context).
+
+The final axioms assert properties of the error term $\err$: it is the
+least dynamic term (has the fewest behaviors), and all complex stacks
+are strict in errors. We state these axioms in a heterogeneous way,
+which
+
\begin{figure}
\begin{small}
@@ -1492,7 +1774,9 @@ TODO: do we actually know what would go wrong in that case?
\bigskip
\begin{mathpar}
- \framebox{Error Universal Properties}
+ \framebox{Error Properties}
+ \inferrule{ \Gamma \mid \cdot \vdash M : \u B }
+ { \Gamma \mid \cdot \vdash \err \ltdyn M : \u B}
\qquad
\inferrule{ \Gamma' \mid \cdot \vdash M' : \u B' }
{ \Gamma \ltdyn \Gamma' \mid \cdot \vdash \err \ltdyn M : \u B \ltdyn \u B'}
@@ -1508,144 +1792,9 @@ TODO: do we actually know what would go wrong in that case?
\label{fig:gtt-term-dyn-axioms}
\end{figure}
-\begin{figure}
-\begin{small}
- \begin{mathpar}
- \framebox{$\Phi \vdash V \ltdyn V' : A \ltdyn A'$ and $\Phi \mid \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'$}
- \\
-
- \inferrule{ }{\Gamma \ltdyn \Gamma \mid \Delta \ltdyn \Delta \vdash E \ltdyn E : T \ltdyn T}
-
- \inferrule{\Gamma \ltdyn \Gamma' \mid \Delta \ltdyn \Delta' \vdash E \ltdyn E' : T \ltdyn T' \\\\
- \Gamma' \ltdyn \Gamma'' \mid \Delta' \ltdyn \Delta'' \vdash E' \ltdyn E'' : T' \ltdyn T''
- }
- {\Gamma \ltdyn \Gamma'' \mid \Delta \ltdyn \Delta'' \vdash E \ltdyn E'' : T \ltdyn T''}
- \\
-
- \inferrule
- { }
- {\Phi,x \ltdyn x' : A \ltdyn A',\Phi' \vdash x \ltdyn x' : A \ltdyn A'}
-
- \inferrule
- {\Phi \vdash V \ltdyn V' : A \ltdyn A' \\\\
- \Phi, x \ltdyn x' : A \ltdyn A',\Phi' \pipe \Psi \vdash E \ltdyn E' : T \ltdyn T'
- }
- {\Phi \mid \Psi \vdash E[V/x] \ltdyn E'[V'/x'] : T \ltdyn T'}
-
- \inferrule
- { }
- {\Phi \pipe \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \bullet : \u B \ltdyn \u B'}
-
- \inferrule
- {\Phi \pipe \Psi \vdash M_1 \ltdyn M_1' : \u B_1 \ltdyn \u B_1' \\\\
- \Phi \pipe \bullet \ltdyn \bullet : \u B_1 \ltdyn \u B_1' \vdash M_2 \ltdyn M_2' : \u B_2 \ltdyn \u B_2'
- }
- {\Phi \mid \Psi \vdash M_2[M_1/\bullet] \ltdyn M_2'[M_1'/\bullet] : \u B_2 \ltdyn \u B_2'}
- \\
- %% congruence for casts is derivable, right?
- \\
- \inferrule
- {\Phi \vdash V \ltdyn V' : A_1 \ltdyn A_1'}
- {\Phi \vdash \inl V \ltdyn \inl V' : A_1 + A_2 \ltdyn A_1' + A_2'}
-
- \inferrule
- {\Phi \vdash V \ltdyn V' : A_2 \ltdyn A_2'}
- {\Phi \vdash \inr V \ltdyn \inr V' : A_1 + A_2 \ltdyn A_1' + A_2'}
- \\
- \inferrule
- {
- \Phi \vdash V \ltdyn V' : A_1 + A_2 \ltdyn A_1' + A_2' \\\\
- \Phi, x_1 \ltdyn x_1' : A_1 \ltdyn A_1' \mid \Psi \vdash E_1 \ltdyn E_1' : T \ltdyn T' \\\\
- \Phi, x_2 \ltdyn x_2' : A_2 \ltdyn A_2' \mid \Psi \vdash E_2 \ltdyn E_2' : T \ltdyn T'
- }
- {\Phi \mid \Psi \vdash \caseofXthenYelseZ V {x_1. E_1}{x_2.E_2} \ltdyn \caseofXthenYelseZ V {x_1'. E_1'}{x_2'.E_2'} : T'}
-
- \inferrule
- {\Phi \vdash V \ltdyn V' : 0 \ltdyn 0}
- {\Phi \mid \Psi \vdash \abort V \ltdyn \abort V' : T \ltdyn T'}
- \\
- \inferrule
- {\Phi \vdash V \ltdyn V' : 1 \ltdyn 1 \\\\
- \Phi \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
- }
- {\Phi \mid \Psi \vdash \pmpairWtoinZ V E \ltdyn \pmpairWtoinZ V' E' : T \ltdyn T'}
- \and
- \inferrule
- {\Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'\\\\
- \Phi\vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'}
- {\Phi \vdash (V_1,V_2) \ltdyn (V_1',V_2') : A_1 \times A_2 \ltdyn A_1' \times A_2'}
- \\
- \inferrule
- {\Phi \vdash V \ltdyn V' : A_1 \times A_2 \ltdyn A_1' \times A_2' \\\\
- \Phi, x \ltdyn x' : A_1 \ltdyn A_1', y \ltdyn y' : A_2 \ltdyn A_2' \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
- }
- {\Phi \mid \Psi \vdash \pmpairWtoXYinZ V x y E \ltdyn \pmpairWtoXYinZ {V'} {x'} {y'} {E'} : T \ltdyn T'}
- \\
-
- \inferrule
- {\Phi \mid \cdot \vdash M \ltdyn M' : \u B \ltdyn \u B'}
- {\Phi \vdash \thunk M \ltdyn \thunk M' : U \u B \ltdyn U \u B'}
-
- \inferrule
- {\Phi \vdash V \ltdyn V' : U \u B \ltdyn U \u B'}
- {\Phi \pipe \cdot \vdash \force V \ltdyn \force V' : \u B \ltdyn \u B'}
- \\
-
- \inferrule
- {\Phi \vdash V \ltdyn V' : A \ltdyn A'}
- {\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
-
- \inferrule
- {\Phi \pipe \Psi \vdash M \ltdyn M' : \u F A \ltdyn \u F A' \\\\
- \Phi, x \ltdyn x' : A \ltdyn A' \pipe \cdot \vdash N \ltdyn N' : \u B \ltdyn \u B'}
- {\Phi \pipe \Psi \vdash \bindXtoYinZ M x N \ltdyn \bindXtoYinZ {M'} {x'} {N'} : \u B \ltdyn \u B'}
-
- \inferrule
- {\Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'}
- {\Phi \pipe \Psi \vdash \lambda x : A . M \ltdyn \lambda x' : A' . M' : A \to \u B \ltdyn A' \to \u B'}
-
- \inferrule
- {\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \\\\
- \Phi \vdash V \ltdyn V' : A \ltdyn A'}
- {\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
- \\
- \inferrule
- {\Phi \mid \Psi \vdash M_1 \ltdyn M_1' : \u B_1 \ltdyn \u B_1'\and
- \Phi \mid \Psi \vdash M_2 \ltdyn M_2' : \u B_2 \ltdyn \u B_2'}
- {\Phi \mid \Psi \vdash \pair {M_1} {M_2} \ltdyn \pair {M_1'} {M_2'} : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
- \\
- \inferrule
- {\Phi \mid \Psi \vdash M \ltdyn M' : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
- {\Phi \mid \Psi \vdash \pi M \ltdyn \pi M' : \u B_1 \ltdyn \u B_1'}
-
- \inferrule
- {\Phi \mid \Psi \vdash M \ltdyn M' : \u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
- {\Phi \mid \Psi \vdash \pi' M \ltdyn \pi' M' : \u B_2 \ltdyn \u B_2'}
- \end{mathpar}
- \caption{GTT Term Dynamism (Structural and Congruence Rules)}
-\end{small}
-\end{figure}
\subsection{Dynamic Types and Errors}
-Since our language has two different kinds of types, we have several
-choices in deciding what our dynamic type should be: either the
-dynamic type should be a value type, or a computation type, or we
-should have \emph{two} dynamic types: a dynamic value type and a
-dynamic computation type.
-%
-Fortunately our modular type-theoretic presentation of gradual typing
-allows us to easily explore all of these options, though we find that
-(surprisingly) having both dynamic value and computation types gives
-the most natural implementation (TODO: forward reference).
-
-Regardless, the dynamic types each have a simple definition: the
-dynamic value type $\dynv$ is the most dynamic value type and the
-dynamic computation type is the most dynamic computation type!
-%
-The reason for this simplicity is that we are leaving abstract what
-the actual implementation of the dynamic type so that we can prove
-quite general theorems.
%
Because of this, we have ``stuck'' terms in some sense: for example we
cannot prove in the theory that $\dncast{\u F 1+1}{\u
@@ -3517,6 +3666,7 @@ the dynamic types are such (which they are in the model constructed
below): \emph{any} monadic upcast/comonadic downcast is pure, in the
sense that it is the (co)monadic lift of a value upcast/stack downcast.
\begin{theorem}[Upcasts are Necessarily Values, Downcasts are Necessarily Stacks]
+ \label{thm:upcasts-values-downcasts-stacks}
Suppose we postulate the casts between ground types and the dynamic
type (and the shifts thereof) as complex values/stacks as in
Lemma~\ref{lem:casts-admissible}: $x : G \vdash \upcast{G}{\dynv}{x} :
@@ -3611,6 +3761,7 @@ universal property already existing).
\newpage
\section{Contract Models of GTT}
+\label{sec:contract}
To show the soundness of our theory, and demonstrate its relationship
to operational definitions of observational equivalence and the
@@ -3790,6 +3941,7 @@ The inequational theory of CBPV includes the $\beta, \eta$ rules for
% the one without complex values maybe instead.
\subsection{Interpreting the Dynamic Types}
+\label{sec:dynamic-type-interp}
As shown in \ref{TODO:sec:uniqeness-theorems}, almost all of the
contract translation is uniquely determined already: casts between