From 67676982e7427502be3b162a9ae212db4d59f530 Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Mon, 2 Jul 2018 23:50:54 -0400
Subject: [PATCH] initial/terminal casts
---
paper/gtt.tex | 210 +++++++++++++++++++++++++++++---------------------
1 file changed, 123 insertions(+), 87 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 1980c9d..1aa2f65 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1851,7 +1851,7 @@ Dually, we have
\end{lemma}
-\begin{theorem}{Characterization of Casts}
+\begin{theorem}{Functorial Casts}
\begin{small}
\[
\begin{array}{l}
@@ -2306,19 +2306,21 @@ Dually, we have
\subsection{Least Dynamic Types}
-The type $0$ is \emph{strict initial object}:
+In what follows, ``unique'' means up to $\equidyn$.
+
\begin{lemma}[Intitial objects] \label{lem:initial}
\begin{enumerate}
- \item For all $T$, there exists a unique $x : 0 \vdash E : T$.
- \item For all $\u B$, there exists a unique stack $\bullet : \F 0
+ \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 intitial: 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 strictly initial: Suppose there is a type $\u B$
- with a complex stack $\bullet : \u B \vdash S : \u F 0$. Then $S$
- is an isomorphism $\u F 0 \cong_c \u B$.
+
+ \item $\u F 0$ is not provably \emph{strictly} initial among computation types.
+ \end{enumerate}
\end{lemma}
\begin{proof}
\begin{enumerate}
@@ -2328,7 +2330,7 @@ The type $0$ is \emph{strict initial object}:
\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
- \bind{\bullet}{x}{S'[\ret x]}$. By congruence, to show $S
+ \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.
@@ -2338,22 +2340,36 @@ The type $0$ is \emph{strict initial object}:
principle for $0$, which says that any two complex values with
domain $0$ are equal.
- The composite $x : A \vdash \abort{\upcast{\leastdynv}{0}{x}} :
- \leastdynv$ is equidynamic with $x$, because
+ The composite $x : A \vdash \abort{V} : A$ is equidynamic
+ with $x$, because
\[
- x : 0, y : 0 \vdash x \equidyn \abort{x} \equidyn y : 0
+ x : A, y : A, z : 0 \vdash x \equidyn \abort{z} \equidyn y : A
\]
- where the first is by $\eta$ with $x : 0, y : 0 \vdash E[x] := x : 0$
- and the second with $x : 0, y : 0 \vdash E[\_] := y : 0$ (this depends
- on the fact that $0$ is ``distributive'', i.e. $\Gamma,x:0$ has the
- universal property of $0$). Substituting $\abort{V[x]}$ and $x$ into
- this, we have $\abort{V[x]} \equidyn x$.
-
- \item TODO
+ 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{cbn-gtt} 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]
+
+ \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$.
@@ -2362,6 +2378,7 @@ The type $0$ is \emph{strict initial object}:
\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}
@@ -2371,13 +2388,13 @@ The type $0$ is \emph{strict initial object}:
$\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 = \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
+ 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$.
@@ -2385,11 +2402,16 @@ The type $0$ is \emph{strict initial object}:
\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}
- The computation type $\top$ is not required to be a strict terminal
- object: there can be types $\u B$ with $\bullet : \top \vdash S : \u
- B$ without $\top \cong_c \u B$.
+
\begin{theorem}[Least Dynamic Value Type]
If $\leastdynv$ is a type such that $\leastdynv \ltdyn A$ for all $A$,
@@ -2398,7 +2420,7 @@ The type $0$ is \emph{strict initial object}:
\end{theorem}
\begin{proof}
We have the upcast $x : \leastdynv \vdash \upcast{\leastdynv}{0}{x} :
-0$, so Lemma~\ref{lem:0-strict-initial} gives the result.
+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,
@@ -2412,11 +2434,10 @@ B$, and we have a terminal computation type $\top$, then $U \leastdynv
\end{theorem}
\begin{proof}
We have stacks $\bullet : \top \dncast{\leastdync}{\top}{\bullet} :
-\leastdync$ and $\bullet : \leastdync \vdash \{\} : \top$, and the
-composite at $\top$ is the identity, because the $\eta$ principle for
-$\top$ is that there is a unique stack $x : \top \vdash S : \top$.
-However, because $\top$ is not a strict terminal object, the dual of the
-above argument does not give a stack isomorphism $\leastdynv \cong_c \top$.
+\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 $\leastdynv \cong_c \top$.
However, using the retract axiom, we have
\[
@@ -2430,64 +2451,79 @@ 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}
+This suggests taking $\bot_v := 0$ and $\bot_c := \top$.
+\begin{theorem}
+The casts determined $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}
-%% and the casts determined $0 \ltdyn A$ are
-%% \[
-%% \upcast{0}{A}z \equidyn \absurd z \qquad \dncast{\u F 0}{\u F A}{M} \equidyn \err
-%% \]
-%% Dually, if $\leastdync$ is a type such that $\leastdync \ltdyn \u B$ for
-%% all $\u B$, then $\leastdync \cong_{c} \top$ and the casts determined by
-%% this are
-%% \[
-%% \dncast{\top}{\u B}{\bullet} \equidyn \{\}\\ \upcast{U \top}{U \u B}{u} \equidyn \thunk \err
-%% \]
-%% \end{theorem}
+\begin{proof}
+ \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}.
-%% \begin{proof}
-%% Suppose we add the axiom $\leastdynv \ltdyn A$ to GTT. Then we have a
-%% complex value upcast $\bullet : \leastdynv \vdash
-%% \upcast{\leastdynv}{0} : 0$ and a complex value $x : \leastdynv \vdash
-%% \abort{x} : \leastdynv$. The composite $x : 0 \vdash
-%% \upcast{\leastdynv}{0}{\abort{x}}$ is equidynamic with $x$ by the
-%% $\eta$ principle for $0$, which says that any two complex values with
-%% domain $0$ are equal. The composite $y : \leastdynv \vdash
-%% \abort{\upcast{\leastdynv}{0}{y}} : \leastdynv$ is also the identity,
-%% because we have ${\upcast{\leastdynv}{0}{y}} : 0$, and in the presence
-%% of a complex value of type $0$, any two complex values $V : A$ and $V'
-%% : A$ are equidynamic, because both are equal to
-%% $\abort{\upcast{\leastdynv}{0}{y}} : A$.
-
-%% Suppose we add the axiom $\leastdync \ltdyn \u B$ to GTT. Then we
-%% have a complex stack downcast $\bullet : {\top} \vdash
-%% \dncast{\leastdync}{\top}{\bullet} : \leastdync$ and a complex stack
-%% $\bullet : \leastdync \vdash \{\} : \top$. The composite $\bullet :
-%% \top \vdash \{\} : \top$ is equidynamic with $\bullet$ by the $\eta$
-%% principle for $\top$. For the composite $\bullet : \leastdync \vdash
-%% \dncast{\leastdync}{\top}{\{\}} : \leastdync$, we have to show each
-%% direction separately. First for $\bullet : \leastdync \vdash
-%% \dncast{\leastdync}{\top}{\{\}} \ltdyn \bullet : \leastdync \ltdyn
-%% \leastdync$, we have $\bullet : \top \vdash
-%% \dncast{\leastdync}{\top}{\bullet} \ltdyn \bullet : \leastdync \ltdyn
-%% \top$.
-
-
-
- %% \item To show $\dncast{\u F 0}{\u F A}{M} \equidyn \err$, it
- %% suffices to show $\dncast{\u F 0}{\u F A}{M} \ltdyn \err$, because
- %% the converse is immediate by the universal property for error. By
- %% $\eta$ for $\u F$ types, we have
- %% \[
- %% \begin{array}{l}
- %% \dncast{\u F 0}{\u F A}{M} \equidyn \\
- %% \bindXtoYinZ{M}{x:A}{ \dncast{\u F 0}{\u F A}{\ret{x}}} \equidyn\\
- %% \bindXtoYinZ{M}{x:A}{ \bindXtoYinZ{\dncast{\u F 0}{\u F A}{\ret{x}}}{y:0}{\ret y}}
- %% \end{array}
- %% \]
+ \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}
%% \item $\dncast{\top}{\u B}{\bullet} \equidyn \{\}$ is immediate by
%% $\eta$ for $\top$.
@@ -2536,7 +2572,7 @@ y : U \top \vdash \upcast{U \leastdync}{U \top}{(\thunk{(\dncast{\leastdync}{\to
%% \[
%% \bindXtoYinZ{N}{(x : 0)}{\err} \ltdyn \err
%% \]
-
+\end{proof}
\subsection{Upcasts are Thunkable, Downcasts are Linear, a posteriori}
--
GitLab