diff --git a/jfp-paper/defs.tex b/jfp-paper/defs.tex
index 781407cd92a953852e3dcc36cb4b4820e9250f7a..21ab4260929750b8f99ebcba7a9bbbe5d48dd4d6 100644
--- a/jfp-paper/defs.tex
+++ b/jfp-paper/defs.tex
@@ -165,6 +165,25 @@
\newcommand\cbvtocbpvty[1]{#1^{ty}}
\newcommand\purely{\downarrow}
+% Stack formatting
+\newenvironment{stackAux}[2]{%
+\setlength{\arraycolsep}{0pt}
+\begin{array}[#1]{#2}}{
+\end{array}\ignorespacesafterend}
+\newenvironment{stackCC}{
+\begin{stackAux}{c}{c}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackCL}{
+\begin{stackAux}{c}{l}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackTL}{
+\begin{stackAux}{t}{l}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackTR}{
+\begin{stackAux}{t}{r}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackBC}{
+\begin{stackAux}{b}{c}}{\end{stackAux}\ignorespacesafterend}
+\newenvironment{stackBL}{
+\begin{stackAux}{b}{l}}{\end{stackAux}\ignorespacesafterend}
+
%% Local Variables:
%% compile-command: "./latexrun jfp-gtt.tex"
%% End:
+
diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index 7211e5bc1bc0844bb669e2dd2e345a6f2bec1c53..dbf0c01d728ae72e3dc53348c16cb225bad51320 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -633,6 +633,7 @@ The main contributions of the paper are as follows.
\end{enumerate}
\begin{shortonly}
+ TODO: update this
\textbf{Extended version:} An extended version of the paper, which
includes the omitted cases of definitions, lemmas, and proofs is
available in \citet{newlicataahmed19:extended}.
@@ -816,49 +817,45 @@ orderings on types and terms.
\begin{figure}
\begin{small}
\[
- \begin{array}{l}
- \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 &
+ \begin{array}{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\\
-
+ T ::= & A \mid \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} &
+ \colorbox{lightgray}{$\upcast A {A'} V$} \mid x \mid \thunk{M} \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' \\
+ \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}\\
+ \colorbox{lightgray}{$\dncast{\u B} {\u B'} M$} \mid \bullet \mid \err_{\u B} \mid \force{V} \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 \ret{V} \mid \bindXtoYinZ{M}{x}{N}
+ \mid \emptypair \mid \pair{M_1}{M_2}
\mid \pi M \mid \pi' M
- \end{array}\\
-
- \Gamma ::= & \cdot \mid \Gamma, x : A &
+ \mid \lambda x:A.M \mid M\,V\\
+ \end{array}\\\\
+ E ::= & V \mid M \\\\
+
+ \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}{$\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}\\\\
-\iflong
- \begin{array}{c}
- \hspace{2.5in} T ::= A \mid \u B \\
- \hspace{2.5in} E ::= V \mid M \\
- \end{array}\\\\
-\fi
- %
- \begin{array}{c}
- \framebox{$\Gamma \vdash V : A$ and $\Gamma \mid \Delta \vdash M : \u B$} \qquad
+ \end{array}
+ \]
+\end{small}
+ \caption{GTT Type and Term Syntax}
+ \label{fig:gtt-syntax}
+\end{figure}
+
+\begin{figure}
+ \begin{small}
+ \begin{mathpar}
+ \framebox{$\Gamma \vdash V : A$ and $\Gamma \mid \Delta \vdash M : \u B$} \and
\colorbox{lightgray}{
$\inferrule*[lab=UpCast]
{\Gamma \vdash V : A \and A \ltdyn A'}
{\Gamma \vdash \upcast A {A'} V : A'}$
- \qquad
+ \and
$\inferrule*[lab=DnCast]
{\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}$
@@ -867,29 +864,45 @@ orderings on types and terms.
\inferrule*[lab=Var]
{ }
{\Gamma,x : A,\Gamma' \vdash x : A}
- \qquad
+ \and
\inferrule*[lab=Hole]
{ }
{\Gamma\pipe \bullet : \u B \vdash \bullet : \u B}
- \qquad
+ \and
\inferrule*[lab=Err]
{ }
{\Gamma \mid \cdot \vdash \err_{\u B} : \u B}
- \\
-\iflong
+ \and
+ \inferrule*[lab=$U$I]
+ {\Gamma \mid \cdot \vdash M : \u B}
+ {\Gamma \vdash \thunk M : U \u B}
+ \and
+ \inferrule*[lab=$U$E]
+ {\Gamma \vdash V : U \u B}
+ {\Gamma \pipe \cdot \vdash \force V : \u B}
+ \and
+ \inferrule*[lab=$F$I]
+ {\Gamma \vdash V : A}
+ {\Gamma \pipe \cdot \vdash \ret V : \u F A}
+ \and
+ \inferrule*[lab=$F$E]
+ {\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*[lab=$0$E]
{\Gamma \vdash V : 0}
{\Gamma \mid \Delta \vdash \abort V : T}
- \qquad
+ \and
\inferrule*[lab=$+$Il]
{\Gamma \vdash V : A_1}
{\Gamma \vdash \inl V : A_1 + A_2}
- \qquad
+ \and
\inferrule*[lab=$+$Ir]
{\Gamma \vdash V : A_2}
{\Gamma \vdash \inr V : A_1 + A_2}
- \qquad
+ \and
\inferrule*[lab=$+$E]
{
\Gamma \vdash V : A_1 + A_2 \\\\
@@ -897,78 +910,55 @@ orderings on types and terms.
\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}
- \\\\
- \fi
+ \and
\inferrule*[lab=$1$I]
{ }
{\Gamma \vdash (): 1}
- \,\,\,
+ \and
\inferrule*[lab=$1$E]
{\Gamma \vdash V : 1 \and
\Gamma \mid \Delta \vdash E : T
}
{\Gamma \mid \Delta \vdash \pmpairWtoinZ V E : T}
- \,\,\,
+ \and
\inferrule*[lab=$\times$I]
{\Gamma \vdash V_1 : A_1\and
\Gamma\vdash V_2 : A_2}
{\Gamma \vdash (V_1,V_2) : A_1 \times A_2}
- \,\,\,
+ \and
\inferrule*[lab=$\times$E]
{\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*[lab=$U$I]
- {\Gamma \mid \cdot \vdash M : \u B}
- {\Gamma \vdash \thunk M : U \u B}
- \,\,\,
- \inferrule*[lab=$U$E]
- {\Gamma \vdash V : U \u B}
- {\Gamma \pipe \cdot \vdash \force V : \u B}
- \,\,\,
- \inferrule*[lab=$F$I]
- {\Gamma \vdash V : A}
- {\Gamma \pipe \cdot \vdash \ret V : \u F A}
- \,\,\,
- \inferrule*[lab=$F$E]
- {\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}
- \\\\
+ \and
\inferrule*[lab=$\to$I]
{\Gamma, x: A \pipe \Delta \vdash M : \u B}
{\Gamma \pipe \Delta \vdash \lambda x : A . M : A \to \u B}
- \quad
+ \and
\inferrule*[lab=$\to$E]
{\Gamma \pipe \Delta \vdash M : A \to \u B\and
\Gamma \vdash V : A}
{\Gamma \pipe \Delta \vdash M\,V : \u B }
-\iflong
- \\\\
+ \and
\inferrule*[lab=$\top$I]{ }{\Gamma \mid \Delta \vdash \emptypair : \top}
- \quad
+ \and
\inferrule*[lab=$\with$I]
{\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}
- \quad
+ \and
\inferrule*[lab=$\with$E]
{\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
{\Gamma \mid \Delta \vdash \pi M : \u B_1}
- \quad
+ \and
\inferrule*[lab=$\with$E']
{\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
{\Gamma \mid \Delta \vdash \pi' M : \u B_2}
-\fi
- \end{array}
- \end{array}
- \]
-\end{small}
- \vspace{-0.1in}
- \caption{GTT Syntax and Term Typing \ifshort{($+$ and $\with$ typing rules in extended version)}\fi}
- \label{fig:gtt-syntax-and-terms}
+ \end{mathpar}
+ \end{small}
+ \caption{GTT Typing}
+ \label{fig:gtt-typing}
\end{figure}
\subsection{Background: Call-by-Push-Value}
@@ -983,7 +973,7 @@ computations: for example, we might have an error computation $\err_{\u
if $V : \kw{string}$ and $M : \u B$, which prints $V$ and then behaves as
$M$.
-\emph{Value types and complex values.}
+\paragraph{Value types and complex values}
The value types include \emph{eager} products $1$ and $A_1 \times A_2$
and sums $0$ and $A_1 + A_2$, which behave as in a call-by-value/eager
language (e.g. a pair is only a value when its components are). The
@@ -999,10 +989,8 @@ class of ``pure functions'' from $A$ to $A'$ (though there is no pure
function \emph{type} internalizing this judgement), which can be treated
like values by a compiler because they have no effects (e.g. they can be
dead-code-eliminated, common-subexpression-eliminated, and so on).
-\begin{longonly}
In focusing~\cite{andreoli92focus} terminology, complex
values consist of left inversion and right focus rules.
-\end{longonly}
For each pattern-matching construct (e.g. case analysis on a sum,
splitting a pair), we have both an elimination rule whose branches are
values (e.g. $\pmpairWtoXYinZ{p}{x_1}{x_2}{V}$) and one whose branches
@@ -1023,7 +1011,7 @@ $\letXbeYinZ{V}{x}{\letXbeYinZ{V'}{x'}{M}} \equiv
\letXbeYinZ{V'}{x'}{\letXbeYinZ{V}{x}{M}}$ --- complex values can be
reordered, while arbitrary computations cannot).
-\emph{Shifts.}
+\paragraph{Shifts}
A key notion in CBPV is the \emph{shift} types $\u F A$ and $U \u B$,
which mediate between value and computation types: $\u F A$ is the
computation type of potentially effectful programs that return a value
@@ -1039,26 +1027,21 @@ The introduction and elimination rules for $U$ are written $\thunk{M}$
and $\force{V}$, and say that computations of type $\u B$ are bijective
with values of type $U \u B$. As an example of the action of the
shifts,
-\begin{longonly}
$0$ is the empty value type, so $\u F 0$ classifies effectful
computations that never return, but may perform effects (and then, must
e.g. non-terminate or error), while $U \u F 0$ is the value type where
such computations are thunked/delayed and considered as values.
-\end{longonly}
$1$ is the trivial value type, so $\u F 1$ is the type of computations
that can perform effects with the possibility of terminating
successfully by returning $()$, and $U \u F 1$ is the value type where
such computations are delayed values.
-\begin{longonly}
$U \u F$ is a monad on value
types~\citep{moggi91}, while $\u F U$ is a comonad on computation types.
-\end{longonly}
-\emph{Computation types.}
-The computation type constructors in CBPV include lazy unit/products
-$\top$ and $\u B_1 \with \u B_2$, which behave as in a call-by-name/lazy
-language (e.g. a component of a lazy pair is evaluated only when it is
-projected). Functions $A \to \u B$ have a value type as input and a
+\paragraph{Computation types}
+The computation type constructors in CBPV include first the lazy unit
+$\top$ and lazy product $\u B_1 \with \u B_2$, which behave as in a call-by-name language (e.g. a component of a lazy pair is evaluated only when it is
+projected). Functions $A \to \u B$ have a value type as input and a
computation type as a result. The equational theory of effects in CBPV
computations may be surprising to those familiar only with
call-by-value, because at higher computation types effects have a
@@ -1072,16 +1055,13 @@ computation means supplying it with an argument, and applying both of
the above to an argument $V$ is defined to result in $\print c;M[V/x]$.
This does \emph{not} imply that the corresponding equations holds for
the call-by-value function type, which we discuss below.
-\begin{longonly}
As another
example, \emph{all} computations are considered equal at type $\top$,
even computations that perform different effects ($\print c$ vs. $\{\}$
-vs. $\err$), because there is by definition \emph{no} way to extract an
-observable of type $\u F A$ from a computation of type $\top$.
+vs. $\err$), because there is by definition \emph{no} way to extract an observable type $\u F A$ from a computation of type $\top$.
Consequently, $U \top$ is isomorphic to $1$.
-\end{longonly}
-\emph{Complex stacks.} Just as the complex values $V$ are a syntactic
+\paragraph{Complex stacks} Just as the complex values $V$ are a syntactic
class terms that have no effects, CBPV includes a judgement for
``stacks'' $S$, a syntactic class of terms that reflect \emph{all}
effects of their input. A \emph{stack} $\Gamma \mid \bullet : \u B
@@ -1099,11 +1079,9 @@ introduction forms for the stack's output type. For example, $\bullet :
than once, because running it requires choosing a projection to get to
an observable of type $\u F A$, so \emph{each time it is run} it uses
$\bullet$ exactly once.
-\begin{longonly}
In
focusing terms, complex stacks include both left and right inversion,
and left focus rules.
-\end{longonly}
In the equational theory of CBPV, $\u F$ and $U$
are \emph{adjoint}, in the sense that stacks $\bullet : \u F A \vdash S
: \u B$ are bijective with values $x : A \vdash V : U \u B$, as both are
@@ -1114,7 +1092,7 @@ we use a typing judgement $\Gamma \mid \Delta \vdash M : \u B$ with a
``stoup'', 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 \ifshort{(omitted) }\fi typing
+: \u B \vdash M : \u B'$ is a stack. The typing
rules for $\top$ and $\with$ treat the stoup additively
(it is arbitrary in the conclusion and the same in all premises); for a
function application to be a stack, the stack input must occur in the
@@ -1122,29 +1100,31 @@ function position. 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's input.
-\emph{Embedding call-by-value and call-by-name.} 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^v, \ldots, x_n
-: A_n^v \vdash e^v : \u F A^v$, 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^v \to \u F A'^v)$. 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 $e^v : \u F U (A^v \to \u F A'^v)$. Here,
-the comonad $\u F U$ offers an opportunity to perform effects
-\emph{before} returning a function value---so under translation 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_m : \u B_m \vdash e : \u B$ is
-translated to $x_1 : U \u {B_1}^n, \ldots, x_m : U \u {B_m}^n \vdash e^n
-: \u B^n$, 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^n \to \u B'^n$
-with a thunked argument. Sums $B_1 + B_2$ are translated to $\u F (U \u
-{B_1}^n + U \u {B_2}^n)$, making the ``lifting'' in lazy sums explicit.
-Call-by-push-value \emph{subsumes} call-by-value and call-by-name in
-that these embeddings are \emph{full and faithful}: two CBV or CBN programs are
-equivalent if and only if their embeddings into CBPV are equivalent, and
-every CBPV program with a CBV or CBN type can be back-translated.
+\paragraph{Embedding Call-by-value and Call-by-name} To translate
+from call-by-value (CBV) to CBPV, a CBV expression $x_1 : A_1, \ldots,
+x_n : A_n \vdash e : A$ is interpreted as a computation $x_1 : A_1^v,
+\ldots, x_n : A_n^v \vdash e^v : \u F A^v$, 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^v \to \u F A'^v)$.
+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 $e^v : \u F U (A^v \to \u F A'^v)$. Here, the comonad $\u
+F U$ offers an opportunity to perform effects \emph{before} returning
+a function value---so under translation 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_m : \u B_m \vdash e : \u B$ is translated to $x_1
+: U \u {B_1}^n, \ldots, x_m : U \u {B_m}^n \vdash e^n : \u B^n$,
+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^n \to \u B'^n$ with
+a thunked argument. Sums $B_1 + B_2$ are translated to $\u F (U \u
+{B_1}^n + U \u {B_2}^n)$, making the ``lifting'' in lazy sums
+explicit. Call-by-push-value \emph{subsumes} call-by-value and
+call-by-name in that these embeddings are \emph{full and faithful}:
+two CBV or CBN programs are equivalent if and only if their embeddings
+into CBPV are equivalent, and every CBPV program with a CBV or CBN
+type can be back-translated.
%% 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
@@ -1172,7 +1152,7 @@ every CBPV program with a CBV or CBN type can be back-translated.
%% %% \to A_2 \to \u B$ \emph{supplies all of the arguments}
%% %% if the conclusion of the stack is an F?
-\emph{Extensionality/$\eta$ Principles.} The main advantage of CBPV for
+\paragraph{Extensionality/$\eta$ Principles} The main advantage of CBPV for
our purposes is that it accounts for the $\eta$/extensionality
principles of both eager/value and lazy/computation types, because
value types have $\eta$ principles relating them to the value
@@ -1207,7 +1187,6 @@ dynamism below.
%% {\Gamma \vdash S[\print V; M] \equidyn \print V; S[M] : \u C}
%% \end{mathpar}
-\ifshort \vspace{-0.1in} \fi
\subsection{The Dynamic Type(s)}
Next, we discuss the additions that make CBPV into our gradual type
@@ -1229,7 +1208,6 @@ would like constructions in GTT to imply results for many different
possible implementations of them. Instead, the terms for the dynamic
types will arise from type dynamism and casts.
-\ifshort \vspace{-0.12in} \fi
\subsection{Type Dynamism}
The \emph{type dynamism} relation of gradual type theory is written $A
@@ -1306,24 +1284,21 @@ in the domain~\citep{newahmed18,newlicata2018-fscd}.
\inferrule*[lab=$\to$Mon]{A \ltdyn A' \and \u B \ltdyn \u B'}
{A \to \u B \ltdyn A' \to \u B'}
-\begin{longonly}
\\
\framebox{Dynamism contexts}
-\quad
+\and
\inferrule{ }{\cdot \, \dynvctx}
-\quad
+\and
\inferrule{\Phi \, \dynvctx \and
A \ltdyn A'}
{\Phi, x \ltdyn x' : A \ltdyn A' \, \dynvctx}
-\quad
+\\
\inferrule{ }{\cdot \, \dyncctx}
-\quad
+\and
\inferrule{\u B \ltdyn \u B'}
{(\bullet \ltdyn \bullet : \u B \ltdyn \u B') \, \dyncctx}
-\end{longonly}
\end{mathpar}
- \vspace{-0.2in}
-\caption{GTT Type Dynamism \iflong and Dynamism Contexts \fi}
+\caption{GTT Type Dynamism and Dynamism Contexts}
\label{fig:gtt-type-dynamism}
\end{small}
\end{figure}
@@ -1478,62 +1453,24 @@ our design choice is forced for all casts, as long as the casts between ground t
\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'}
- \\\\
- \ifshort
- \inferrule*[lab=$\times$ICong]
- {\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'}
- \quad
- \inferrule*[lab=$\to$ICong]
- {\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*[lab=$\times$ECong]
- {\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*[lab=$\to$ECong]
- {\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*[lab=$F$ICong]
- {\Phi \vdash V \ltdyn V' : A \ltdyn A'}
- {\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
- \qquad
- \inferrule*[lab=$F$ECong]
- {\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'}
- \\\\
- \fi
\end{array}
\]
- \vspace{-0.25in}
- \caption{GTT Term Dynamism (Structural \ifshort and Congruence\fi Rules) \ifshort
- (Rules for $U,1,+,0,\with,\top$ in extended version)
- \fi}
+ \caption{GTT Term Dynamism (Structural and Congruence Rules)}
\label{fig:gtt-term-dynamism-structural}
-\end{small}
+ \end{small}
\end{figure}
-\iflong
\begin{figure}
- \begin{small}
- \[
- \begin{array}{c}
+ \begin{footnotesize}
+ \begin{mathpar}
\inferrule*[lab=$+$IlCong]
{\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'}
- \qquad
+ \and
\inferrule*[lab=$+$IrCong]
{\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'}
- \\\\
+ \and
\inferrule*[lab=$+$ECong]
{
\Phi \vdash V \ltdyn V' : A_1 + A_2 \ltdyn A_1' + A_2' \\\\
@@ -1541,19 +1478,19 @@ our design choice is forced for all casts, as long as the casts between ground 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'}
- \qquad
+ \and
\inferrule*[lab=$0$ECong]
{\Phi \vdash V \ltdyn V' : 0 \ltdyn 0}
{\Phi \mid \Psi \vdash \abort V \ltdyn \abort V' : T \ltdyn T'}
- \\\\
+ \and
\inferrule*[lab=$1$ICong]{ }{\Phi \vdash () \ltdyn () : 1 \ltdyn 1}
- \qquad
+ \and
\inferrule*[lab=$1$ECong]
{\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*[lab=$\times$ICong]
{\Phi \vdash V_1 \ltdyn V_1' : A_1 \ltdyn A_1'\\\\
\Phi\vdash V_2 \ltdyn V_2' : A_2 \ltdyn A_2'}
@@ -1563,56 +1500,54 @@ our design choice is forced for all casts, as long as the casts between ground t
{\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'}
- \\\\
+ \and
\inferrule*[lab=$\times$ECong]
{\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'}
- \,\,
+ \and
\inferrule*[lab=$\to$ECong]
- {\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \\\\
+ {\Phi \pipe \Psi \vdash M \ltdyn M' : A \to \u B \ltdyn A' \to \u B' \and
\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \Psi \vdash M\,V \ltdyn M'\,V' : \u B \ltdyn \u B' }
- \\\\
+ \and
\inferrule*[lab=$U$ICong]
{\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'}
- \qquad
+ \and
\inferrule*[lab=$U$ECong]
{\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'}
- \\\\
+ \and
\inferrule*[lab=$F$ICong]
{\Phi \vdash V \ltdyn V' : A \ltdyn A'}
{\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
- \qquad
+ \and
\inferrule*[lab=$F$ECong]
{\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'}
- \\\\
+ \and
\inferrule*[lab=$\top$ICong]{ }{\Phi \mid \Psi \vdash \{\} \ltdyn \{\} : \top \ltdyn \top}
- \qquad
+ \and
\inferrule*[lab=$\with$ICong]
{\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'}
- \\\\
+ \and
\inferrule*[lab=$\with$ECong]
{\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'}
- \qquad
+ \and
\inferrule*[lab=$\with$E'Cong]
{\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{array}
- \]
- \caption{GTT Term Dynamism (Congruence Rules)}
- \label{fig:gtt-term-dynamism-ext-congruence}
-\end{small}
+ \end{mathpar}
+ \caption{GTT Term Dynamism (Congruence Rules)}
+ \label{fig:gtt-term-dynamism-ext-congruence}
+ \end{footnotesize}
\end{figure}
-\fi
The final piece of GTT is the \emph{term dynamism} relation, a syntactic
judgement that is used for reasoning about the behavioral properties of
@@ -2110,14 +2045,15 @@ casts:
\end{mathpar}
\end{small}
\end{lemma}
- 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
-without loss of generality apply these rules (this comes from upcasts
-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.
+
+In sequent calculus terminology, in the term dynamism judgement 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 without loss of generality apply
+these rules (this comes from upcasts 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.
\begin{longproof}
For upcast left, substitute $V'$ into the axiom $x \ltdyn
@@ -2298,22 +2234,27 @@ out of the dynamic type are coherent, for example if $A \ltdyn A'$
then
$\upcast{A}{\dynv}{x} \equidyn \upcast{A'}{\dynv}{\upcast{A}{A'}{x}}$.
- The following theorem says essentially that $x \ltdyn
- \dncast{T}{T'}{\upcast{T}{T'}{x}}$ (upcast then downcast might error
- less but but otherwise does not change the behavior) and
- $\upcast{T}{T'}{\dncast{T}{T'}{x}} \ltdyn x$ (downcast then upcast
- might error more but otherwise does not change the behavior). However,
- since a value type dynamism $A \ltdyn A'$ induces a value upcast $x :
- A \vdash \upcast{A}{A'}{x} : A'$ but a stack downcast $\bullet : \u F
- A' \vdash \dncast{\u F A}{\u F A'}{\bullet} : \u F A$ (and dually for
- computations), the statement of the theorem wraps one cast with
- the constructors for $U$ and $\u F$ types (functoriality of $\u F/U$).
-\begin{theorem}[Casts are a Galois Connection] \label{thm:cast-adjunction} ~~~
+TODO: rewrite this section using defined casts.
+ %% The following theorem says essentially that $x \ltdyn
+ %% \dncast{T}{T'}{\upcast{T}{T'}{x}}$ (upcast then downcast might error
+ %% less but but otherwise does not change the behavior) and
+ %% $\upcast{T}{T'}{\dncast{T}{T'}{x}} \ltdyn x$ (downcast then upcast
+ %% might error more but otherwise does not change the behavior). However,
+ %% since a value type dynamism $A \ltdyn A'$ induces a value upcast $x :
+ %% A \vdash \upcast{A}{A'}{x} : A'$ but a stack downcast $\bullet : \u F
+ %% A' \vdash \dncast{\u F A}{\u F A'}{\bullet} : \u F A$ (and dually for
+ %% computations), the statement of the theorem wraps one cast with
+ %% the constructors for $U$ and $\u F$ types (functoriality of $\u F/U$).
+\begin{theorem}[Casts form Galois Connections] \label{thm:cast-adjunction}
+ If $A \ltdyn A'$, then the following hold
\begin{enumerate}
- \item $\bullet' : \u F A' \vdash \bindXtoYinZ{\dncast{\u F A}{\u F A'}{\bullet'}}{x}{\ret{(\upcast{A}{A'}{x})}} \ltdyn \bullet' : \u F A'$
- \item $\bullet : \u F A \vdash \bullet \ltdyn \bindXtoYinZ{\bullet}{x}{\dncast{\u F A}{\u F A'}{(\ret{(\upcast{A}{A'}{x})})}} : \u F A$
- \item $x : U \u B' \vdash {\upcast{U \u B}{U \u B'}{(\thunk{({\dncast{\u B}{\u B'}{\force x}})})}} \ltdyn x : U \u B'$
- \item $x : U \u B \vdash x \ltdyn \thunk{(\dncast{B}{B'}{(\force{(\upcast{U \u B}{U \u B'}{x})})})} : U \u B$
+ \item $\bullet' : \u F A' \vdash \defupcast{\u F A}{\u F A'}\dncast{\u F A}{\u F A'}\bullet' \ltdyn \bullet' : \u F A'$
+ \item $\bullet : \u F A \vdash \bullet \ltdyn \dncast{\u F A}{\u F A'}\defupcast{\u F A}{\u F A'}\bullet : \u F A$
+ \end{enumerate}
+ If $\u B \ltdyn \u B'$, then the following hold
+ \begin{enumerate}
+ \item $x : U \u B' \vdash {\upcast{U \u B}{U \u B'}\defdncast{U \u B}{U \u B'}x} \ltdyn x : U \u B'$
+ \item $x : U \u B \vdash x \ltdyn \defdncast{U \u B}{U \u B'}\upcast{U \u B}{U \u B'}{x} : U \u B$
\end{enumerate}
\end{theorem}
\begin{longproof} ~
@@ -2396,11 +2337,12 @@ the retraction property for general casts:
%% \equidyn \dncast{T}{\dynv}{\upcast{T}{\dynv}{x}} \equidyn x
%% \]
\begin{theorem}[Retract Property for General Casts] ~~~ \label{thm:retract-general}
+ If $A \ltdyn A'$ and $\u B \ltdyn \u B'$, then
\begin{enumerate}
\item
- $\bullet : \u F A \vdash \bindXtoYinZ{\bullet}{x}{\dncast{\u F A}{\u F A'}{(\ret{(\upcast{A}{A'}{x})})}} \equidyn \bullet : \u F A$
+ $\bullet : \u F A \vdash \defupcast{\u F A}{\u F A'}\dncast{\u F A}{\u F A'}\bullet \equidyn \bullet : \u F A$
\item
- $x : U \u B \vdash \thunk{(\dncast{\u B}{\u B'}{(\force{(\upcast{U \u B}{U \u B'}{x})})})} \equidyn x : U \u B$
+ $x : U \u B \vdash \defdncast{U\u B}{U\u B'}\upcast{U \u B}{U \u B'}{x} \equidyn x : U \u B$
\end{enumerate}
\end{theorem}
\begin{longproof}
@@ -2669,63 +2611,78 @@ Dually, we have
Together, the universal property for casts and the $\eta$ principles for
each type imply that the casts must behave as in lazy cast semantics:
\begin{theorem}[Cast Unique Implementation Theorem for $+,\times,\to,\with$] \label{thm:functorial-casts}
-The casts' behavior is uniquely determined as follows: \ifshort (See the extended version for $+$, $\with$.) \fi
-\begin{small}
-\[
- \begin{array}{c}
-\iflong
- \upcast{A_1 + A_2}{A_1' + A_2'}{s} \equidyn \caseofXthenYelseZ{s}{x_1.\inl{(\upcast{A_1}{A_1'}{x_1})}}{x_2.\inr{(\upcast{A_2}{A_2'}{x_2})}}\\\\
- \begin{array}{rcl}
- \dncast{\u F (A_1' + A_2')}{\u F (A_1 + A_2)}{\bullet} & \equidyn
- & \bindXtoYinZ{\bullet}{(s : (A_1' + A_2'))}\caseofX{s}\\
- & & \{{x_1'.\bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}{\ret{(\inl {x_1})}}} \\
- & & \mid {x_2'.\bindXtoYinZ{(\dncast{\u F A_2}{\u F A_2'}{(\ret{x_2'})})}{x_2}{\ret{(\inr {x_2})}}} \}\\
- \end{array}
- \\\\
-\fi
- \upcast{A_1 \times A_2}{A_1' \times A_2'}{p} \equidyn \pmpairWtoXYinZ{p}{x_1}{x_2}{(\upcast{A_1}{A_1'}{x_1},\upcast{A_2}{A_2'}{x_2})} \\\\
- \begin{array}{rcl}
- \dncast{\u F (A_1' \times A_2')}{\u F (A_1 \times A_2)}{\bullet} &
- \equidyn &
- \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
-%% \\\\
-%% \end{array}
-%% \]
-%% \[
-%% \begin{array}{c}
-\iflong
- \dncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}{\bullet} \equidyn
- \pair{\dncast{\u B_1}{\u B_1'}{\pi \bullet}}{\dncast{\u B_2}{\u B_2'}{\pi' \bullet}}\\\\
- \begin{array}{rcll}
- \upcast{U (\u B_1 \with \u B_2)}{U (\u B_1' \with \u B_2')}{p} & \equidyn &
- \thunk{} & {\{\pi \mapsto {\force{(\upcast{U \u B_1}{U \u B_1'}{(\thunk{\pi (\force{p})})})}}}\\
- &&& \pi' \mapsto {\force{(\upcast{U \u B_2}{U \u B_2'}{(\thunk{\pi' (\force{p})})})}} \}
- \end{array}\\\\
-\fi
-
- \dncast{A \to \u B}{A' \to \u B'}{\bullet} \equidyn
- \lambda{x}.{\dncast{\u B}{\u B'}{(\bullet \, (\upcast{A}{A'}{x}))}} \\\\
+ All of the equivalences in Figure~\ref{fig:uniq-impl} are derivable.
- \begin{array}{rcll}
- \upcast{U (A \to \u B)}{U (A' \to \u B')}{f} & \equidyn &
- \thunk (\lambda x'. & \bindXtoYinZ{\dncast{\u F A}{\u F A'}{(\ret x')}}{x}{} \\
- & & & { \force{(\upcast{U \u B}{U \u B'}{(\thunk{(\force{(f)}\,x)})})}} )
- \end{array}
- \\
- \end{array}
- \]
- \end{small}
+ \begin{figure}
+ \begin{footnotesize}
+ \[
+ \begin{array}{c}
+
+ \upcast{A_1 + A_2}{A_1' + A_2'}{s} \equidyn \caseofXthenYelseZ{s}{x_1.\inl{(\upcast{A_1}{A_1'}{x_1})}}{x_2.\inr{(\upcast{A_2}{A_2'}{x_2})}}\\\\
+ \begin{array}{rcl}
+ \dncast{\u F (A_1' + A_2')}{\u F (A_1 + A_2)}{\bullet} & \equidyn
+ & \bindXtoYinZ{\bullet}{(s : (A_1' + A_2'))}\caseofX{s}\\
+ & & \{x_1'.
+ \begin{stackTL}
+ \bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}\\ {\ret{(\inl {x_1})}}
+ \end{stackTL}
+ \\
+ & & \mid {x_2'.
+ \begin{stackTL}
+ \bindXtoYinZ{(\dncast{\u F A_2}{\u F A_2'}{(\ret{x_2'})})}{x_2}\\{\ret{(\inr {x_2})}}
+ \end{stackTL}
+ } \}\\
+ \end{array}
+ \\\\
+ \upcast{A_1 \times A_2}{A_1' \times A_2'}{p} \equidyn \pmpairWtoXYinZ{p}{x_1}{x_2}{(\upcast{A_1}{A_1'}{x_1},\upcast{A_2}{A_2'}{x_2})} \\\\
+ \begin{array}{rcl}
+ \dncast{\u F (A_1' \times A_2')}{\u F (A_1 \times A_2)}{\bullet} &
+ \equidyn &
+ \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) }\\\\
+ & \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) }
+ \end{array}\\\\
+ %% if losing space due to not pagebreaking in the middle of this
+ %% \\\\
+ %% \end{array}
+ %% \]
+ %% \[
+ %% \begin{array}{c}
+
+ \dncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'}{\bullet} \equidyn
+ \pair{\dncast{\u B_1}{\u B_1'}{\pi \bullet}}{\dncast{\u B_2}{\u B_2'}{\pi' \bullet}}\\\\
+ \begin{stackTL}
+ \upcast{U (\u B_1 \with \u B_2)}{U (\u B_1' \with \u B_2')}{p}\\
+ \quad\equidyn \thunk{}
+ \begin{stackTL}
+ {\{\pi \mapsto {\force{(\upcast{U \u B_1}{U \u B_1'}{(\thunk{\pi (\force{p})})})}}}\\
+ \,\,|\,\,\pi' \mapsto {\force{(\upcast{U \u B_2}{U \u B_2'}{(\thunk{\pi' (\force{p})})})}}
+ \end{stackTL}
+ \}
+ \end{stackTL}
+
+ \\\\
+ \dncast{A \to \u B}{A' \to \u B'}{\bullet} \equidyn
+ \lambda{x}.{\dncast{\u B}{\u B'}{(\bullet \, (\upcast{A}{A'}{x}))}} \\\\
+
+ \upcast{U (A \to \u B)}{U (A' \to \u B')}{f} \equidyn
+ \thunk (\lambda x'.
+ \begin{stackTL}
+ \bindXtoYinZ{\dncast{\u F A}{\u F A'}{(\ret x')}}{x}{} \\
+ { \force{(\upcast{U \u B}{U \u B'}{(\thunk{(\force{(f)}\,x)})})}}
+ \end{stackTL}
+ \end{array}
+ \]
+ \end{footnotesize}
+ \caption{Derivable Cast Behavior for $+,\times,\with,\to$}
+ \label{fig:uniq-impl}
+ \end{figure}
\end{theorem}
+
In the case for an eager product $\times$, we can actually also show
that reversing the order and 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_1'}}$ is also
@@ -3330,42 +3287,33 @@ such:
${x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn \defdncast{A}{A'} x' : A}$.
\end{enumerate}
\end{definition}
-\begin{longonly}
Because the proofs of Lemma~\ref{lem:cast-left-right},
Lemma~\ref{lem:cast-congruence}, Theorem~\ref{thm:decomposition},
Theorem~\ref{thm:casts-unique} rely only on the axioms for
upcasts/downcasts, the analogues of these theorems hold for stack
upcasts and value downcasts as well.
-\end{longonly}
+
+TODO: move this stuff earlier to the defined upcast/downcast section
Some value downcasts and computation upcasts do exist, leading to a
characterization of the casts for the monad $U \u F A$ and comonad $\u F
U \u B$ of $F \dashv U$:
\begin{theorem}[Cast Unique Implementation Theorem for $U \u F, \u F U$] \label{thm:monadic-comonadic-casts}
Let $A \ltdyn A'$ and $\u B \ltdyn \u B'$.
\begin{enumerate}
- \item $\bullet : \u F A \vdash
- \bindXtoYinZ{\bullet}{x:A}{\ret{(\upcast{A}{A'}{x})}} : \u F A'$
- is a stack upcast.
+ %% \item $\bullet : \u F A \vdash
+ %% \bindXtoYinZ{\bullet}{x:A}{\ret{(\upcast{A}{A'}{x})}} : \u F A'$
+ %% is a stack upcast.
- \item If $\defupcast{\u B}{\u B'}$ is a stack upcast, then\\
- $x : \u U B \vdash \upcast{U \u B}{\u U B'}{x} \equidyn \thunk{(\defupcast{\u B}{\u B'}{(\force x)})} : U \u B'$
+ \item $x : U \u F A \vdash \upcast{U \u F A}{\u U B'}{x} \equidyn \thunk{(\defupcast{\u F A}{\u F A'}{(\force x)})} : U \u F A'$
- \item $x : \u U B' \vdash \thunk{(\dncast{\u B}{\u B'}{(\force x)})} : U
- \u B$ is a value downcast.
+ %% \item $x : \u U B' \vdash \thunk{(\dncast{\u B}{\u B'}{(\force x)})} : U
+ %% \u B$ is a value downcast.
- \item If $\defdncast{A}{A'}$ is a value downcast, then\\
- $\bullet : \u F A' \vdash \dncast{\u F A}{\u F A'}{\bullet} \equidyn \bindXtoYinZ{\bullet}{x':A'}{\ret{(\dncast{A}{A'}{x})}}$
-
- \item
- $\begin{array}{c}
- x : U \u F A \vdash \upcast{U \u F A}{U \u F A'}{x} \equidyn \thunk{ (\bindXtoYinZ{{\force x}}{x:A}{\ret{(\upcast{A}{A'}{x})}})}\\
- \bullet : \u F U \u B' \vdash \dncast{\u F U \u B}{\u F U \u B'}{\bullet} \equidyn
- \bindXtoYinZ{\bullet}{x':U \u B'}{\ret{(\thunk{(\dncast{\u B}{\u B'}{(\force x)})})}}
- \end{array}$
+ \item $\bullet : \u F U \u B' \vdash \dncast{\u F U \u B}{\u F U \u B'}{\bullet} \equidyn \bindXtoYinZ{\bullet}{x':U \u B'}{\ret{(\dncast{U \u B}{U \u B'}{x})}}$
\end{enumerate}
\end{theorem}
-
\begin{longproof}
+ TODO: update the proof
\begin{enumerate}
\item
To show
@@ -3475,6 +3423,7 @@ U \u B$ of $F \dashv U$:
\end{enumerate}
\end{longproof}
+TODO: make this whole thing a forward reference to the CBV section
\begin{longonly}
\subsubsection{Derived Rules for Call-by-value Function Types}
\end{longonly}
@@ -3534,10 +3483,16 @@ let-bind $(\upcast{A_1}{A_1'}{x})$ to avoid duplicating it, but because
it is a (complex) value, it can also be substituted directly, which
might expose reductions that can be optimized.
-\begin{longonly}
\subsection{Least Dynamic Types}
-\begin{longonly}
+Though it is common in gradually typed surface languages to have a
+\emph{most} dynamic type in the form of the dynamic type $\dyn$, it is
+less common to have a \emph{least} dynamic type. We consider here the
+\emph{semantic} impliciations of having a least dynamic value or
+computation type. Perhaps unsurprisingly, we find that a least dynamic
+type must be isomorphic to $0$ and a least dynamic computation type
+must be isomorphic to $\top$.
+
\begin{theorem}[Least Dynamic Value Type]
If $\leastdynv$ is a type such that $\leastdynv \ltdyn A$ for all $A$,
then in GTT with a strict initial object $0$, $\leastdynv \cong_{v}
@@ -3557,7 +3512,7 @@ If $\leastdync$ is a type such that $\leastdync \ltdyn \u B$ for all $\u
B$, and we have a terminal computation type $\top$, then $U \leastdync
\cong_{v} U \top$.
\end{theorem}
-\begin{proof}
+\begin{longproof}
We have stacks $\bullet : \top \dncast{\leastdync}{\top}{\bullet} :
\leastdync$ and $\bullet : \leastdync \vdash \{\} : \top$. The
composite at $\top$ is the identity by Lemma~\ref{lem:terminal}. However,
@@ -3577,10 +3532,9 @@ and the composite
y : U \top \vdash \upcast{U \leastdync}{U \top}{(\thunk{(\dncast{\leastdync}{\top}{(\force{x})})})} : U \top
\]
is the identity by uniqueness for $U \top$ (Lemma~\ref{lem:terminal}).
-\end{proof}
+\end{longproof}
This suggests taking $\bot_v := 0$ and $\bot_c := \top$.
-\end{longonly}
%% \begin{shortonly}
%% The dynamic types are the \emph{most} dynamic types; it is interesting
@@ -3661,7 +3615,6 @@ Dually, the casts determined by $\top \ltdyn \u B$ are
B$ gives the result.
\end{enumerate}
\end{longproof}
-\end{longonly}
\subsection{Upcasts are Values, Downcasts are Stacks}
\label{sec:upcasts-necessarily-values}
@@ -4489,7 +4442,6 @@ of the operational behavior of a standard Call-by-value cast calculus.
\end{itemize}
\end{proof}
-
\section{Contract Models of GTT}
\label{sec:contract}
@@ -10158,7 +10110,7 @@ policies or endorsements, either expressed or implied, of the United
States Air Force Research Laboratory, the U.S. Government, or Carnegie
Mellon University.
-\bibliographystyle{abbrv}
+\bibliographystyle{jfp}
\bibliography{max}
\end{document}
diff --git a/jfp-paper/max.bib b/jfp-paper/max.bib
index f8e9bb248368f8a3dc18862b3e27e5323fe1ceb0..5aab9b6bb72685deccf97c28894aab14f1435b54 100644
--- a/jfp-paper/max.bib
+++ b/jfp-paper/max.bib
@@ -90,6 +90,10 @@
@STRING{popl14 = popl # ", San Diego, California" }
@STRING{popl15 = popl # ", Mumbai, India" }
@STRING{popl16 = popl # ", St. Petersburg, Florida" }
+@STRING{popl17 = popl # ", Paris, France" }
+@STRING{popl18 = popl # ", Los Angeles, California" }
+@STRING{popl19 = popl # ", Cascais, Portugal" }
+@STRING{popl20 = popl # ", New Orleans, Louisiana" }
% ----
@STRING{icfp = "{I}nternational {C}onference on {F}unctional {P}rogramming
({ICFP})" }
@@ -124,6 +128,7 @@
@STRING{oopsla89 = oopsla }
@STRING{oopsla98 = oopsla # ", Vancouver, British Columbia" }
@STRING{oopsla08 = oopsla # ", Nashville, Tennessee" }
+@STRING{oopsla12 = oopsla # ", Tucson, Arizona" }
% ----
@STRING{lics = "IEEE Symposium on Logic in Computer Science (LICS)" }
@STRING{lics91 = lics # ", Amsterdam, The Netherlands" }
@@ -771,15 +776,6 @@ year = "2001"}
year = {2011},
}
-@article{extended,
- author = {Max S. New and
- Daniel R. Licata},
- title = {Call-by-name Gradual Type Theory},
- journal = {CoRR},
- year = {2018},
- url = {http://arxiv.org/abs/1802.00061},
-}
-
@article{newlicata2018-fscd,
author = {Max S. New and
Daniel R. Licata},
@@ -1112,14 +1108,14 @@ pages="396--410",
advisor = {Reddy, Uday},
title = {Parametricity As a Notion of Uniformity in Reflexive Graphs},
year = {2002},
- publisher = {University of Illinois at Urbana-Champaign},
+ school = {University of Illinois at Urbana-Champaign},
address = {Champaign, IL, USA},
}
@inproceedings{vitousekswordssiek:2017,
author = {Vitousek, Michael M. and Swords, Cameron and Siek, Jeremy G.},
title = {Big Types in Little Runtime: Open-world Soundness and Collaborative Blame for Gradual Type Systems},
- series = {POPL 2017},
+ booktitle=popl17,
year = {2017},
}
@@ -1188,7 +1184,7 @@ pages="36--54",
@inproceedings{greenberg-manifest,
author = {Greenberg, Michael and Pierce, Benjamin C. and Weirich, Stephanie},
title = {Contracts Made Manifest},
- series = {POPL '10},
+ booktitle = popl10,
year = 2010
}
@@ -1210,14 +1206,14 @@ year={2004}
@inproceedings{chaperonesimpersonators,
author = {Strickland, T. Stephen and Tobin-Hochstadt, Sam and Findler, Robert Bruce and Flatt, Matthew},
title = {Chaperones and Impersonators: Run-time Support for Reasonable Interposition},
- series = oopsla,
+ booktitle =oopsla12,
year = {2012},
}
@inproceedings{XuPJC09,
author = {Xu, Dana N. and Peyton Jones, Simon and Claessen, Koen},
title = {Static Contract Checking for Haskell},
- series = popl09,
+ booktitle = popl09,
year = {2009},
}
@@ -1236,10 +1232,12 @@ year="2006",
year = {2018},
url = {http://arxiv.org/abs/1802.00061},
}
-@Unpublished{newlicataahmed19:extended,
+
+@article{newlicataahmed19:extended,
author = {Max S. New and Daniel R. Licata and Amal Ahmed},
title = {Gradual Type Theory (Extend Version)},
year = {2018},
+journal = {CoRR},
url = {https://arxiv.org/abs/1811.02440},
}