diff --git a/jfp-paper/jfp-gtt.tex b/jfp-paper/jfp-gtt.tex
index 44b3def25e9af611a40526a4630607b7ca447fe4..fd52e2ba88a8719fca582dee076e2433fae9936c 100644
--- a/jfp-paper/jfp-gtt.tex
+++ b/jfp-paper/jfp-gtt.tex
@@ -1852,143 +1852,10 @@ In this section, we show that the axiomatics of gradual type theory
determine most properties of casts, which shows that these behaviors of
casts are forced in any implementation of gradual typing satisfying
graduality and $\beta,\eta$.
-\begin{shortonly}
- For proofs, see the extended version of the paper.
-\end{shortonly}
-
-\begin{longonly}
-\subsection{Properties inherited from CBPV}
-
-Because the GTT term equidynamism relation $\equidyn$ includes the
-congruence and $\beta\eta$ axioms of the CBPV equational theory, types
-inherit the universal properties they have there~\cite{levy03cbpvbook}. We recall
-some relevant definitions and facts.
-
-\begin{definition}[Isomorphism] ~
- \begin{enumerate}
- \item We write $A \cong_v A'$ for a \emph{value isomorphism between
- $A$ and $A'$}, which consists of two complex values $x : A \vdash V'
- : A'$ and $x' : A' \vdash V : A$ such that $x : A \vdash V[V'/x']
- \equidyn x : A$ and $x' : A' \vdash V'[V/x] \equidyn x' : A'$.
- \item We write $\u B \cong_c \u B'$ for a \emph{computation
- isomorphism between $\u B$ and $\u B'$}, which consists of two
- complex stacks $\bullet : \u B \vdash S' : \u B'$ and $\bullet' : \u
- B' \vdash S : \u B$ such that $\bullet : \u B \vdash S[S'/x']
- \equidyn \bullet : \u B$ and $\bullet' : \u B' \vdash S'[S/\bullet]
- \equidyn \bullet' : \u B'$.
- \end{enumerate}
-\end{definition}
-Note that a value isomorphism is a strong condition, and an
-isomorphism in call-by-value between types $A$ and $A'$ corresponds to
-a computation isomorphism $\u F A \cong \u F A'$, and
-dually~\cite{levy17popl}.
-
-\smallskip
-
-\begin{lemma}[Initial objects] ~ \label{lem:initial}
- \begin{enumerate}
- \item For all (value or computation) types $T$, there exists a unique
- expression $x : 0 \vdash E : T$.
- \item For all $\u B$, there exists a unique stack $\bullet : \u F 0
- \vdash S : \u B$.
- \item
- 0 is strictly initial: Suppose there is a type $A$ with a complex
- value $x : A \vdash V : 0$. Then $V$ is an isomorphism $A \cong_v
- 0$.
-
- \item $\u F 0$ is not provably \emph{strictly} initial among computation types.
- \end{enumerate}
-\end{lemma}
-\begin{proof}~
- \begin{enumerate}
- \item Take $E$ to be $x : 0 \vdash \abort{x} : T$. Given any $E'$,
- we have $E \equidyn E'$ by the $\eta$ principle for $0$.
-
- \item Take $S$ to be $\bullet : \u F 0 \vdash
- \bindXtoYinZ{\bullet}{x}{\abort{x}} : \u B$. Given another $S'$,
- by the $\eta$ principle for $F$ types, $S' \equidyn
- \bindXtoYinZ{\bullet}{x}{S'[\ret x]}$. By congruence, to show $S
- \equidyn S'$, it suffices to show $x : 0 \vdash \abort{x} \equidyn
- S[\ret{x}] : \u B$, which is an instance of the previous part.
-
- \item
- We have $y : 0 \vdash \abort{y} : A$. The composite $y : 0 \vdash
- V[\abort{y}/x] : 0$ is equidynamic with $y$ by the $\eta$
- principle for $0$, which says that any two complex values with
- domain $0$ are equal.
+%% \begin{shortonly}
+%% For proofs, see the extended version of the paper.
+%% \end{shortonly}
- The composite $x : A \vdash \abort{V} : A$ is equidynamic
- with $x$, because
- \[
- x : A, y : A, z : 0 \vdash x \equidyn \abort{z} \equidyn y : A
- \]
- where the first is by $\eta$ with $x : A, y : A, z : 0 \vdash E[z] :=
- x : A$ and the second with $x : 0, y : 0 \vdash E[z] := y : A$ (this
- depends on the fact that $0$ is ``distributive'', i.e. $\Gamma,x:0$
- has the universal property of $0$). Substituting $\abort{V}$ for $y$
- and $V$ for $z$, we have $\abort{V} \equidyn x$.
-
- %% \item We have $\bullet : \u F 0 \vdash
- %% \bindXtoYinZ{\bullet}{x}{\abort{x}} : \u B$, and the composite at
- %% $\u F 0$ is the identity by part (2). But $\bullet : \u
- %% B \vdash \bindXtoYinZ{S}{x}{\abort{x}} \equidyn \bullet : \u B$
- %% doesn't seem to be true?
-\item $\u F 0$ is not \emph{strictly} initial among computation types,
- though. Proof sketch: a domain model along the lines of
- \citep{newlicata2018-fscd} with only non-termination and type errors shows this,
- because there $\u F 0$ and $\top$ are isomorphic (the same object is
- both initial and terminal), so if $\u F 0$ were strictly initial (any
- type $\u B$ with a stack $\bullet : B \vdash S : \u F 0$ is isomorphic
- to $\u F 0$), then because every type $\u B$ has a stack to $\top$
- (terminal) and therefore $\u F 0$, every type would be isomorphic to
- $\top$/$\u F 0$---i.e. the stack category would be trivial. But there
- are non-trivial computation types in this model.
- \end{enumerate}
-\end{proof}
-\begin{lemma}[Terminal objects] ~ \label{lem:terminal}
- \begin{enumerate}
- \item For any computation type $\u B$, there exists a unique stack
- $\bullet : \u B \vdash S : \top$.
- \item (In any context $\Gamma$,) there exists a unique complex value
- $V : U \top$.
- \item (In any context $\Gamma$,) there exists a unique complex value
- $V : 1$.
- \item $U \top \cong_v 1$
- \item $\top$ is not a strict terminal object.
- \end{enumerate}
-\end{lemma}
-\begin{proof} ~
- \begin{enumerate}
- \item Take $S = \{\}$. The $\eta$ rule for $\top$, $\bullet : \top
- \vdash \bullet \equidyn \{\} : \top$, under the substitution of
- $\bullet : \u B \vdash S : \top$, gives $S \equidyn
- \{\}[S/\bullet] = \{\}$.
-
- \item Take $V = \thunk{\{\}}$. We have $x : U \top \vdash x
- \equidyn \thunk{\force{x}} \equidyn \thunk{\{\}} : U \top$ by the
- $\eta$ rules for $U$ and $\top$.
-
- \item Take $V = ()$. By $\eta$ for $1$ with $x : 1 \vdash E[x] :=
- () : 1$, we have $x : 1 \vdash () \equidyn \pmmuXtoYinZ{x}{()} :
- 1$. By $\eta$ fro $1$ with $x : 1 \vdash E[x] := x : 1$, we have
- $x : 1 \vdash x \equidyn \pmmuXtoYinZ{x}{()}$. Therefore $x : 1
- \vdash x \equidyn () : 1$.
-
- \item We have maps $x : U \top \vdash () : 1$ and $x : 1 \vdash
- \thunk{\{\}} : U \top$. The composite on $1$ is the identity by
- the previous part. The composite on $\top$ is the identity by
- part (2).
-
- \item Proof sketch: As above, there is a domain model with
- $\top \cong \u F 0$, so if $\top$ were a strict terminal object,
- then $\u F 0$ would be too. But $\u F 0$ is also initial, so it
- has a map to every type, and therefore every type would be
- isomorphic to $\u F 0$ and $\top$. But there are non-trivial
- computation types in the model.
- \end{enumerate}
-\end{proof}
-\end{longonly}
-
\subsection{Derived Cast Rules}
As noted above, monotonicity of type dynamism for $U$ and $\u F$ means
@@ -2007,12 +1874,12 @@ that we have the following as instances of the general cast rules:
\end{mathpar}
\end{small}
\end{lemma}
-\begin{longproof}
+\begin{proof}
They are instances of the general upcast and downcast rules, using the
fact that $U$ and $\u F$ are congruences for type dynamism, so in the
first rule $\u F A \ltdyn \u F A'$, and in the second, $U \u B \ltdyn
U \u B'$.
-\end{longproof}
+\end{proof}
The cast universal properties in Figure~\ref{fig:gtt-term-dyn-axioms}
imply the following seemingly more general rules for reasoning about
@@ -2103,12 +1970,13 @@ Figure~\ifshort\ref{fig:gtt-term-dynamism-structural}\else\ref{fig:gtt-term-dyna
\end{mathpar}
\end{small}
\end{lemma}
-\begin{longproof}
+\begin{proof}
In all cases, uses the invertible and then non-invertible rule for the
-cast. For the first rule, by upcast left, it suffices to show $x \ltdyn
+cast. For the first rule, by upcast left, it suffices to show $x \ltdyn
x' : A \ltdyn A' \vdash {x} \ltdyn \upcast{A'}{A''}{x'} : A \ltdyn A''$
-which is true by upcast right, using $x \ltdyn x'$ in the premise.
+which is true by upcast right, using $x \ltdyn x'$ in the premise. \begin{shortonly} The other cases follow by a similar argument \end{shortonly}.
+\begin{longonly}
For the second, by upcast left, it suffices to show
$x : A \vdash {x} \ltdyn \upcast{A}{A''}{x} : A \ltdyn A''$,
which is true by upcast right.
@@ -2120,7 +1988,8 @@ which is true by downcast left, using $\bullet' \ltdyn \bullet''$ in the premise
For the fourth, by downcast right, it suffices show
$\dncast{\u B}{\u B''}{\bullet''}\ltdyn {\bullet''} : \u B \ltdyn \u B''$,
which is true by downcast left.
-\end{longproof}
+\end{longonly}
+\end{proof}
Next, while it is important to identify that upcasts between value
types are pure values and downcasts between computation types are
@@ -2392,7 +2261,6 @@ the retraction property for general casts:
\subsection{Unique Implementations of Casts}
-\begin{longonly}
\begin{definition}
Let a \emph{type constructor} $C$ be a (value or computation) type that
well-formed according to the grammar in Figure~\ref{fig:gtt-syntax-and-terms} with
@@ -2596,11 +2464,8 @@ Dually, we have
\]
gives the result.
\end{proof}
-\end{longonly}
-\begin{longonly}
\subsubsection{Functions, Products, and Sums}
-\end{longonly}
Together, the universal property for casts and the $\eta$ principles for
each type imply that the casts must behave as in lazy cast semantics:
@@ -3253,9 +3118,7 @@ possible implementations will.
\end{enumerate}
\end{longproof}
-\begin{longonly}
\subsubsection{Shifts}
-\end{longonly}
In GTT, we assert the existence of value upcasts and computation
downcasts for derivable type dynamism relations. While we do not assert
@@ -3418,9 +3281,7 @@ U \u B$ of $F \dashv U$:
\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}
+\subsubsection{Derived Rules for Call-by-value Function Types}
Recall that for value types $A_1$ and $A_2$, the CBV function type is
$U(A_1 \to \u F A_2)$. As a corollary of
@@ -3477,139 +3338,6 @@ 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.
-\subsection{Least Dynamic Types}
-
-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}
- 0$.
-\end{theorem}
-\begin{proof}
-We have the upcast $x : \leastdynv \vdash \upcast{\leastdynv}{0}{x} :
-0$, so Lemma~\ref{lem:initial} gives the result.
-\end{proof}
-The fact that $\leastdynv$ is strictly initial seems to depend on the
-fact that we have a strictly initial object: In GTT without a $0$ type,
-it seems that we cannot prove that $x : \leastdynv \vdash
-\upcast{\leastdynv}{A}{x} : A$ is the unique such map.
-
-\begin{theorem}[Least Dynamic Computation Type]
-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{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,
-because $\top$ is not a strict terminal object, the dual of the above
-argument does not give a stack isomorphism $\leastdync \cong_c \top$.
-
-However, using the retract axiom, we have
-\[
-\begin{array}{c}
- x : U \leastdync \vdash \upcast{U \leastdync}{U \top}{x} : U \top\\
- y : U \top \vdash \thunk{(\dncast{\leastdync}{\top}{(\force{x})})} : U \leastdync\\
- x : U \leastdync \vdash \thunk{(\dncast{\leastdync}{\top}{(\force{(\upcast{U \leastdync}{U \top}{x})})})} \equidyn x : U \leastdync
-\end{array}
-\]
-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{longproof}
-
-This suggests taking $\bot_v := 0$ and $\bot_c := \top$.
-
-%% \begin{shortonly}
-%% The dynamic types are the \emph{most} dynamic types; it is interesting
-%% to consider what the \emph{least} dynamic types would be. A least
-%% dynamic value type should have an upcast complex value into every type,
-%% which the empty type $0$ does. A least dynamic computation type should
-%% have a complex stack from every type, which the \emph{unit} type $\top$
-%% does. Thus, it is sensible to extend GTT with the type dynamism axioms
-%% $0 \ltdyn A$ and $\top \ltdyn \u B$, in which case we have:
-%% \end{shortonly}
-\begin{theorem}
-The casts determined by $0 \ltdyn A$ are
-\[
-\upcast{0}{A}z \equidyn \absurd z \qquad \dncast{\u F 0}{\u F A}{\bullet} \equidyn \bindXtoYinZ{\bullet}{\_}{\err}
-\]
-Dually, the casts determined by $\top \ltdyn \u B$ are
-\[
-\dncast{\top}{\u B}{\bullet} \equidyn \{\} \qquad \upcast{U \top}{U \u B}{u} \equidyn \thunk \err
-\]
-\end{theorem}
-
-\begin{longproof}
- \begin{enumerate}
- \item $x : 0 \vdash \upcast{0}{A}{x} \equidyn \abort{x} : A$ is
- immediate by $\eta$ for $0$.
-
- \item First, to show
- $\bullet : \u F A \vdash \bindXtoYinZ{\bullet}{\_}{\err} \ltdyn \dncast{\u F 0}{\u F A}{\bullet}$,
- we can $\eta$-expand the right-hand side into
- $\bindXtoYinZ{\bullet}{x:A}{\dncast{\u F 0}{\u F A}{\ret{x}}}$,
- at which point the result follows by congruence
- and the fact that type error is minimal, so
- $\err \ltdyn {\dncast{\u F 0}{\u F A}{\ret{x}}}$.
-
- Second, to show
- $\bullet : \u F A \vdash \dncast{\u F 0}{\u F A}{\bullet} \ltdyn \bindXtoYinZ{\bullet}{\_}{\err}$,
- we can $\eta$-expand the left-hand side to
- $\bullet : \u F A \vdash \bindXtoYinZ{\dncast{\u F 0}{\u F A}{\bullet}}{y}{\ret y}$,
- so we need to show
- \[
- \bullet: \u F A \vdash \bindXtoYinZ{\dncast{\u F 0}{\u F A}{\bullet}}{y:0}{\ret y} \ltdyn \bindXtoYinZ{\bullet}{y':A}{\err} : \u F 0
- \]
- We apply congruence, with $\bullet : \u F A \vdash {\dncast{\u F
- 0}{\u F A}{\bullet}} \ltdyn \bullet : 0 \ltdyn A$ by the
- universal property of downcasts in the first premise, so it suffices
- to show
- \[
- y \ltdyn y' : 0 \ltdyn A \vdash \ret{y} \ltdyn \err_{\u F 0} : \u F 0
- \]
- By transitivity with $y \ltdyn y' : 0 \ltdyn A \vdash \err_{\u F 0}
- \ltdyn \err_{\u F 0} : \u F 0 \ltdyn \u F 0$, it suffices to show
- \[
- y \ltdyn y : 0 \ltdyn 0 \vdash \ret{y} \ltdyn \err_{\u F 0} : \u F 0
- \]
- But now both sides are maps out of $0$, and therefore equal by
- Lemma~\ref{lem:initial}.
-
- \item The downcast is immediate by $\eta$ for $\top$,
- Lemma~\ref{lem:terminal}.
-
- \item First,
- \[
- u : U \top \vdash \thunk \err \ltdyn \thunk{(\force{(\upcast{U \top}{U \u B}{u})})} \equidyn {\upcast{U \top}{U \u B}{u}} : U \u B
- \]
- by congruence, $\eta$ for $U$, and the fact that error is minimal.
- Conversely, to show
- \[
- u : U \top \vdash {\upcast{U \top}{U \u B}{u}} \ltdyn \thunk \err : U \u B
- \]
- it suffices to show
- \[
- u : U \top \vdash u \ltdyn \thunk \err_{\u B} : U \top \ltdyn U \u B
- \]
- by the universal property of an upcast. By Lemma~\ref{lem:terminal},
- any two elements of $U \top$ are equidynamic, so in particular $u
- \equidyn \thunk{\err_{\top}}$, at which point congruence for
- $\mathsf{thunk}$ and $\err_\top \ltdyn \err_{\u B } : \top \ltdyn \u
- B$ gives the result.
- \end{enumerate}
-\end{longproof}
-
\subsection{Upcasts are Values, Downcasts are Stacks}
\label{sec:upcasts-necessarily-values}
@@ -3626,7 +3354,6 @@ casts between \emph{ground} types and $\dynv$/$\dync$. For this section, we def
\u G ::= \dynv \to \dync \mid \top \mid \dync \with \dync \mid \u F \dynv
\]
-\begin{longonly}
\begin{definition}[Ground type dynamism]
Let $A \ltdyn' A'$ and $\u B \ltdyn' \u B'$ be the relations defined
by the rules in Figure~\ref{fig:gtt-type-dynamism}
@@ -3651,7 +3378,6 @@ A \ltdyn \u F \dynv \ltdyn \dync$.
$A \ltdyn A'$ iff $A \ltdyn' A'$ and $\u B \ltdyn \u B'$ iff $\u B
\ltdyn' \u B'$
\end{lemma}
-
\begin{proof}
The ``if'' direction is immediate by induction because every rule of
$\ltdyn'$ is a rule of $\ltdyn$. To show $\ltdyn$ is contained in
@@ -3659,7 +3385,6 @@ $\ltdyn'$, we do induction on the derivation of $\ltdyn$, where every
rule is true for $\ltdyn'$, except $A \ltdyn \dynv$ and $\u B \ltdyn
\dync$, and for these, we use Lemma~\ref{lem:find-ground-type}.
\end{proof}
-\end{longonly}
Let GTT$_G$ be the fragment of GTT where the only primitive casts are
those between ground types and the dynamic types, i.e. the cast terms
@@ -3802,7 +3527,6 @@ are unique by an argument analogous to Theorem~\ref{thm:casts-unique},
the postulated casts must be equal to these.
\end{proof}
-\begin{longonly}
Indeed, the following a priori even more general assumption provides no
more flexibility:
\begin{theorem}[Upcasts are Necessarily Values, Downcasts are Necessarily Stacks II]
@@ -3832,12 +3556,33 @@ Again, Lemma~\ref{lem:casts-admissible} constructs $\defupcast{A}{A'}$
and $\defdncast{\u B}{\u B'}$, so the proof of part (5) of
Theorem~\ref{thm:monadic-comonadic-casts} gives the result.
\end{proof}
-\end{longonly}
-
-\begin{longonly}
\subsection{Equidynamic Types are Isomorphic}
+Because the GTT term equidynamism relation $\equidyn$ includes the
+congruence and $\beta\eta$ axioms of the CBPV equational theory, types
+inherit the universal properties they have there~\cite{levy03cbpvbook}. We recall
+some relevant definitions and facts.
+
+\begin{definition}[Isomorphism] ~
+ \begin{enumerate}
+ \item We write $A \cong_v A'$ for a \emph{value isomorphism between
+ $A$ and $A'$}, which consists of two complex values $x : A \vdash V'
+ : A'$ and $x' : A' \vdash V : A$ such that $x : A \vdash V[V'/x']
+ \equidyn x : A$ and $x' : A' \vdash V'[V/x] \equidyn x' : A'$.
+ \item We write $\u B \cong_c \u B'$ for a \emph{computation
+ isomorphism between $\u B$ and $\u B'$}, which consists of two
+ complex stacks $\bullet : \u B \vdash S' : \u B'$ and $\bullet' : \u
+ B' \vdash S : \u B$ such that $\bullet : \u B \vdash S[S'/x']
+ \equidyn \bullet : \u B$ and $\bullet' : \u B' \vdash S'[S/\bullet]
+ \equidyn \bullet' : \u B'$.
+ \end{enumerate}
+\end{definition}
+Note that a value isomorphism is a strong condition, and an
+isomorphism in call-by-value between types $A$ and $A'$ corresponds to
+a computation isomorphism $\u F A \cong \u F A'$, and
+dually~\cite{levy17popl}.
+
\begin{theorem}[Equidynamism implies Isomorphism]
\begin{enumerate}
\item
@@ -3873,28 +3618,273 @@ Theorem~\ref{thm:monadic-comonadic-casts} gives the result.
The other composite is the same proof with $\u B$ and $\u B'$ swapped.
\end{enumerate}
\end{proof}
-\end{longonly}
-%% \subsection{Retract Axiom}
+\subsection{Least Dynamic Types}
-%% In the call-by-name version of GTT (\cite{GTT}), there was an explicit
-%% axiom that states that every pair of upcasts and downcasts forms a
-%% section-retraction pair: i.e., that the downcast applied to the upcast
-%% is the identity.
+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 $\bot$. Having a least
+dynamic type causes issues with certain definitions. For instance
+sometimes the type consistency relation $A \sim A'$ is defined as
+existence of a type more precise than each: $\exists A_l. A_l \ltdyn A
+\wedge A_l \ltdyn A'$, but this definition would be trivial given the
+presence of a least dynamic type.
+
+We consider here the \emph{semantic} consequences of having a least
+dynamic value type $\leastdynv$ or computation type $\leastdync$,
+which are quite mild.
+%
+In the case of the most precise value type $\leastdynv$, we have a
+pure value $x : \leastdynv \vdash \upcast{\leastdynv}{A}x : A$ for
+every value type $A$.
+%
+This suggests that the empty type $0$ is a candidate to be
+$\leastdynv$, and in fact we can show the two are isomorphic.
+
+To prove this we first recall some general facts about the empty type,
+in category theoretic terms that it is a \emph{strictly initial}
+object.
+\begin{lemma}[(strictly) initial object] ~ \label{lem:initial}
+ \begin{enumerate}
+ \item For all (value or computation) types $T$, there exists a
+ unique expression $x : 0 \vdash E : T$. In category-theoretic
+ terms, $0$ is initial in the category of value types and values.
+ \item For all $\u B$, there exists a unique stack $\bullet : \u F 0
+ \vdash S : \u B$. In category-theoretic terms, $\u F 0$ is initial
+ in the category of computation types and stacks.
+ \item Suppose there is a type $A$ with a complex value $x : A \vdash
+ V : 0$. Then $V$ is an isomorphism $A \cong_v 0$. In
+ category-theoretic terms, $0$ is \emph{strictly} initial.
+ \end{enumerate}
+\end{lemma}
+\begin{longproof}~
+ \begin{enumerate}
+ \item Take $E$ to be $x : 0 \vdash \abort{x} : T$. Given any $E'$,
+ we have $E \equidyn E'$ by the $\eta$ principle for $0$.
-%% With the large number of connectives comes a large number of proofs.
-%% %
-%% For each connective, we need four proofs: left and right rules for the
-%% upcast and left and right rules for the downcast.
-%% %
-%% However, we can take advantage of the duality between upcasts and
-%% downcasts and the duality between $\ltdyn$ and $\gtdyn$ to save some
-%% effort, so that if we constrain our proof, we can mechanically turn a
-%% single case, say the left rule for upcast into proofs of the other 3
-%% cases.
-%% %
-%% In order for this duality to be \emph{perfect}, we use the version of
-%% casts that are \emph{not} assumed to be
+ \item Take $S$ to be $\bullet : \u F 0 \vdash
+ \bindXtoYinZ{\bullet}{x}{\abort{x}} : \u B$. Given another $S'$,
+ by the $\eta$ principle for $F$ types, $S' \equidyn
+ \bindXtoYinZ{\bullet}{x}{S'[\ret x]}$. By congruence, to show $S
+ \equidyn S'$, it suffices to show $x : 0 \vdash \abort{x} \equidyn
+ S[\ret{x}] : \u B$, which is an instance of the previous part.
+
+ \item
+ We have $y : 0 \vdash \abort{y} : A$. The composite $y : 0 \vdash
+ V[\abort{y}/x] : 0$ is equidynamic with $y$ by the $\eta$
+ principle for $0$, which says that any two complex values with
+ domain $0$ are equal.
+
+ The composite $x : A \vdash \abort{V} : A$ is equidynamic
+ with $x$, because
+ \[
+ x : A, y : A, z : 0 \vdash x \equidyn \abort{z} \equidyn y : A
+ \]
+ where the first is by $\eta$ with $x : A, y : A, z : 0 \vdash E[z] :=
+ x : A$ and the second with $x : 0, y : 0 \vdash E[z] := y : A$ (this
+ depends on the fact that $0$ is ``distributive'', i.e. $\Gamma,x:0$
+ has the universal property of $0$). Substituting $\abort{V}$ for $y$
+ and $V$ for $z$, we have $\abort{V} \equidyn x$.
+
+ %% \item We have $\bullet : \u F 0 \vdash
+ %% \bindXtoYinZ{\bullet}{x}{\abort{x}} : \u B$, and the composite at
+ %% $\u F 0$ is the identity by part (2). But $\bullet : \u
+ %% B \vdash \bindXtoYinZ{S}{x}{\abort{x}} \equidyn \bullet : \u B$
+ %% doesn't seem to be true?
+%% \item $\u F 0$ is not \emph{strictly} initial among computation types,
+%% though. Proof sketch: a domain model along the lines of
+%% \citep{newlicata2018-fscd} with only non-termination and type errors shows this,
+%% because there $\u F 0$ and $\top$ are isomorphic (the same object is
+%% both initial and terminal), so if $\u F 0$ were strictly initial (any
+%% type $\u B$ with a stack $\bullet : B \vdash S : \u F 0$ is isomorphic
+%% to $\u F 0$), then because every type $\u B$ has a stack to $\top$
+%% (terminal) and therefore $\u F 0$, every type would be isomorphic to
+%% $\top$/$\u F 0$---i.e. the stack category would be trivial. But there
+%% are non-trivial computation types in this model.
+ \end{enumerate}
+\end{longproof}
+Note however that we cannot prove that $\u F 0$ is \emph{strictly}
+initial in the category of stacks.
+
+With this lemma in hand, we can show that $\leastdynv$ must be
+value-isomorphic to $0$:
+\begin{theorem}[Least Dynamic Value Type]
+ If $\leastdynv$ is a type such that $\leastdynv \ltdyn A$ for all $A$,
+ then in GTT with $0$, $\leastdynv \cong_{v} 0$.
+\end{theorem}
+\begin{proof}
+We have the upcast $x : \leastdynv \vdash \upcast{\leastdynv}{0}{x} :
+0$, so Lemma~\ref{lem:initial} gives the result.
+\end{proof}
+However, note that unless we already know there is an empty type $0$,
+we see no way to prove that $\leastdynv$ is initial in that all terms
+$x : \leastdynv \vdash M$ are equivalent.
+
+Thinking dually, a most precise computation type would have a linear
+stack $\bullet : \u B \vdash \dncast{\leastdync}{\u B}\bullet :
+\leastdync$ for every computation type $\u B$, so an obvious candidate
+would be the lazy unit $\top$, the dual of the empty type. However,
+the duality here is not perfect and we will only be able to prove the
+weaker fact that $U \top$ and $U \leastdync$ are isomorphic.
+
+To prove this, we first recall the defining property of $\top$, that
+it is in category-theoretic terms a \emph{terminal object}, but not
+provably a \emph{strictly} terminal object, breaking the precise
+duality with $0$.
+\begin{lemma}[Terminal objects] ~ \label{lem:terminal}
+ \begin{enumerate}
+ \item For any computation type $\u B$, there exists a unique stack
+ $\bullet : \u B \vdash S : \top$, i.e., $\top$ is a terminal
+ object in the category of computation types and stacks.
+ \item (In any context $\Gamma$,) there exists a unique complex
+ value $V : U \top$, i.e., $U\top$ is a terminal object in the
+ category of value types and values.
+ \item (In any context $\Gamma$,) there exists a unique complex value
+ $V : 1$, i.e., $1$ is also a terminal object.
+ \item $U \top \cong_v 1$
+ \end{enumerate}
+\end{lemma}
+\begin{longproof} ~
+ \begin{enumerate}
+ \item Take $S = \{\}$. The $\eta$ rule for $\top$, $\bullet : \top
+ \vdash \bullet \equidyn \{\} : \top$, under the substitution of
+ $\bullet : \u B \vdash S : \top$, gives $S \equidyn
+ \{\}[S/\bullet] = \{\}$.
+
+ \item Take $V = \thunk{\{\}}$. We have $x : U \top \vdash x
+ \equidyn \thunk{\force{x}} \equidyn \thunk{\{\}} : U \top$ by the
+ $\eta$ rules for $U$ and $\top$.
+
+ \item Take $V = ()$. By $\eta$ for $1$ with $x : 1 \vdash E[x] :=
+ () : 1$, we have $x : 1 \vdash () \equidyn \pmmuXtoYinZ{x}{()} :
+ 1$. By $\eta$ fro $1$ with $x : 1 \vdash E[x] := x : 1$, we have
+ $x : 1 \vdash x \equidyn \pmmuXtoYinZ{x}{()}$. Therefore $x : 1
+ \vdash x \equidyn () : 1$.
+
+ \item We have maps $x : U \top \vdash () : 1$ and $x : 1 \vdash
+ \thunk{\{\}} : U \top$. The composite on $1$ is the identity by
+ the previous part. The composite on $\top$ is the identity by
+ part (2).
+
+ %% \item Proof sketch: As above, there is a domain model with
+ %% $\top \cong \u F 0$, so if $\top$ were a strict terminal object,
+ %% then $\u F 0$ would be too. But $\u F 0$ is also initial, so it
+ %% has a map to every type, and therefore every type would be
+ %% isomorphic to $\u F 0$ and $\top$. But there are non-trivial
+ %% computation types in the model.
+ \end{enumerate}
+\end{longproof}
+Note that we cannot show that $\top$ is strictly terminal. Next, we
+can show that $U \leastdync$ is isomorphic to $U \top$.
+\begin{theorem}[Least Dynamic Computation Type]
+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}
+First, though we can define stacks $\bullet : \top
+\dncast{\leastdync}{\top}{\bullet} : \leastdync$ and $\bullet :
+\leastdync \vdash \{\} : \top$, we can only prove one direction of the
+isomorphism:
+\[ \{\}[\dncast{\leastdync}{\top}\bullet] \equidyn \{\} \equidyn \bullet\]
+Since $\top$ is not a strict terminal object, the dual of the above
+argument does not give the other property of a stack isomorphism
+$\leastdync \cong_c \top$.
+
+On the other hand, we can define values
+\[
+\begin{array}{c}
+ x : U \leastdync \vdash \upcast{U \leastdync}{U \top}{x} : U \top\\\\
+ y : U \top \vdash \defdncast{U \leastdync}{U \top} y : U \leastdync
+\end{array}
+\]
+And these do exhibit the isomorphism $U \leastdync \cong_v
+U\top$. First, by the retract axiom
+\[ x : U \leastdync \vdash \defdncast{U\leastdync }{U \top}\upcast{U \leastdync}{U \top}{x} \equidyn x : U \leastdync
+\]
+and the opposite composite
+\[
+y : U \top \vdash \upcast{U \leastdync}{U \top}\defdncast{U \leastdync}{U \top} : U \top
+\]
+is the identity by uniqueness for $U \top$ (Lemma~\ref{lem:terminal}).
+\end{proof}
+
+Given these two
+Theorems \label{thm:least-valty}, \label{thm:least-compty}, it is then
+sensible to ask what are the consequences of \emph{defining} $0$ and
+$\top$ to be most precise types. If this is the case then, like in
+Section~\label{sec:uniq-impl}, we can derive what the behavior of
+their casts would be.
+\begin{theorem}
+ If $0 \ltdyn A$, then
+ \[
+ \upcast{0}{A}z \equidyn \absurd z \qquad \dncast{\u F 0}{\u F A}{\bullet} \equidyn \bindXtoYinZ{\bullet}{\_}{\err}
+ \]
+
+ If $\top \ltdyn \u B$, then
+ \[
+ \dncast{\top}{\u B}{\bullet} \equidyn \{\} \qquad \upcast{U \top}{U \u B}{u} \equidyn \thunk \err
+ \]
+\end{theorem}
+\begin{longproof}
+ \begin{enumerate}
+ \item $x : 0 \vdash \upcast{0}{A}{x} \equidyn \abort{x} : A$ is
+ immediate by $\eta$ for $0$.
+
+ \item First, to show
+ $\bullet : \u F A \vdash \bindXtoYinZ{\bullet}{\_}{\err} \ltdyn \dncast{\u F 0}{\u F A}{\bullet}$,
+ we can $\eta$-expand the right-hand side into
+ $\bindXtoYinZ{\bullet}{x:A}{\dncast{\u F 0}{\u F A}{\ret{x}}}$,
+ at which point the result follows by congruence
+ and the fact that type error is minimal, so
+ $\err \ltdyn {\dncast{\u F 0}{\u F A}{\ret{x}}}$.
+
+ Second, to show
+ $\bullet : \u F A \vdash \dncast{\u F 0}{\u F A}{\bullet} \ltdyn \bindXtoYinZ{\bullet}{\_}{\err}$,
+ we can $\eta$-expand the left-hand side to
+ $\bullet : \u F A \vdash \bindXtoYinZ{\dncast{\u F 0}{\u F A}{\bullet}}{y}{\ret y}$,
+ so we need to show
+ \[
+ \bullet: \u F A \vdash \bindXtoYinZ{\dncast{\u F 0}{\u F A}{\bullet}}{y:0}{\ret y} \ltdyn \bindXtoYinZ{\bullet}{y':A}{\err} : \u F 0
+ \]
+ We apply congruence, with $\bullet : \u F A \vdash {\dncast{\u F
+ 0}{\u F A}{\bullet}} \ltdyn \bullet : 0 \ltdyn A$ by the
+ universal property of downcasts in the first premise, so it suffices
+ to show
+ \[
+ y \ltdyn y' : 0 \ltdyn A \vdash \ret{y} \ltdyn \err_{\u F 0} : \u F 0
+ \]
+ By transitivity with $y \ltdyn y' : 0 \ltdyn A \vdash \err_{\u F 0}
+ \ltdyn \err_{\u F 0} : \u F 0 \ltdyn \u F 0$, it suffices to show
+ \[
+ y \ltdyn y : 0 \ltdyn 0 \vdash \ret{y} \ltdyn \err_{\u F 0} : \u F 0
+ \]
+ But now both sides are maps out of $0$, and therefore equal by
+ Lemma~\ref{lem:initial}.
+
+ \item The downcast is immediate by $\eta$ for $\top$,
+ Lemma~\ref{lem:terminal}.
+
+ \item First,
+ \[
+ u : U \top \vdash \thunk \err \ltdyn \thunk{(\force{(\upcast{U \top}{U \u B}{u})})} \equidyn {\upcast{U \top}{U \u B}{u}} : U \u B
+ \]
+ by congruence, $\eta$ for $U$, and the fact that error is minimal.
+ Conversely, to show
+ \[
+ u : U \top \vdash {\upcast{U \top}{U \u B}{u}} \ltdyn \thunk \err : U \u B
+ \]
+ it suffices to show
+ \[
+ u : U \top \vdash u \ltdyn \thunk \err_{\u B} : U \top \ltdyn U \u B
+ \]
+ by the universal property of an upcast. By Lemma~\ref{lem:terminal},
+ any two elements of $U \top$ are equidynamic, so in particular $u
+ \equidyn \thunk{\err_{\top}}$, at which point congruence for
+ $\mathsf{thunk}$ and $\err_\top \ltdyn \err_{\u B } : \top \ltdyn \u
+ B$ gives the result.
+ \end{enumerate}
+\end{longproof}
\section{Application: Deriving Call-by-value Operational Semantics}