From 0901b60ca8c8ecac6b9a729aeb98d11fdae6735b Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Thu, 5 Jul 2018 23:12:57 -0400
Subject: [PATCH] shifted casts
---
paper/gtt.tex | 490 +++++++++++++++++++++++++++++++++++++++++++++-----
1 file changed, 449 insertions(+), 41 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index 3ab8c0c..82b67e2 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -12,8 +12,8 @@
\newif\ifshort
\newif\iflong
%% Pick long or short version:
-\shorttrue
-%%\longtrue
+%% \shorttrue
+\longtrue
%% Note: Authors migrating a paper from PACMPL format to traditional
%% SIGPLAN proceedings format should change 'acmlarge' to
@@ -1692,7 +1692,7 @@ Some helpful derived rules:
U \u B'$.
\end{proof}
-\begin{lemma}[Upcast and downcast left and right rules]
+\begin{lemma}[Upcast and downcast left and right rules] \label{lem:cast-left-right}
The following are derivable:
\begin{mathpar}
\inferrule
@@ -1745,7 +1745,7 @@ gives $\bullet \ltdyn \bullet'' : \u B \ltdyn \u B'' \vdash \bullet \ltdyn \dnca
and then substitution of the premise into this gives the conclusion.
\end{proof}
-\begin{lemma}[Cast congruence rules]
+\begin{lemma}[Cast congruence rules] \label{lem:cast-congruence}
The following congruence rules for casts are derivable:
\begin{mathpar}
\inferrule
@@ -1989,7 +1989,7 @@ else is equivalent to the upcast or downcast by showing that it has
the \emph{same} property.
%
-\begin{lemma}{Specification for Casts is a Universal Property}
+\begin{theorem}{Specification for Casts is a Universal Property} \label{thm:casts-unique}
If $A \ltdyn A'$ and $x : A \vdash V_u[x] : A'$ is a value such that
the following judgments are provable:
\begin{mathpar}
@@ -2016,7 +2016,7 @@ the \emph{same} property.
{\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn S_d : \u B}
\end{mathpar}
then we can prove $\bullet : \u B' \vdash S_d \equidyn \dncast{\u B}{\u B'}\bullet : \u B$
-\end{lemma}
+\end{theorem}
\begin{proof}
\begin{mathpar}
\inferrule*[right=substitution]
@@ -2088,7 +2088,7 @@ upcast from $C[A_i/X_i,\u B_i/\u Y_i]$ to $C[A_i'/X_i,\u B_i'/\u Y_i]$.
\begin{lemma}[Upcast Lemma] \label{lem:upcast}
Let $X_1 \vtype, \ldots X_n \vtype, \u Y_1 \ctype, \ldots \u Y_n
\ctype \vdash C \vtype$ be a value type constructor. We abbreviate
- the instantiatiation $C[A_1/X_1,\ldots,A_n/X_n,\u B_1/\u Y_i,\ldots,\u
+ the instantiatiation \\ $C[A_1/X_1,\ldots,A_n/X_n,\u B_1/\u Y_i,\ldots,\u
B_m/\u Y_m]$ by $C[A_i,\u B_i]$.
Suppose $\defupcast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{-}$ is a complex
@@ -2168,9 +2168,9 @@ upcast from $C[A_i/X_i,\u B_i/\u Y_i]$ to $C[A_i'/X_i,\u B_i'/\u Y_i]$.
Dually, we have
\begin{lemma}[Downcast Lemma] \label{lem:downcast}
Let $X_1 \vtype, \ldots X_n \vtype, \u Y_1 \ctype, \ldots \u Y_n
- \ctype \vdash C \ctype$ be a computation type constructor. We abbreviate
- the instantiatiation $C[A_1/X_1,\ldots,A_n/X_n,\u B_1/\u Y_i,\ldots,\u
- B_m/\u Y_m]$ by $C[A_i,\u B_i]$.
+ \ctype \vdash C \ctype$ be a computation type constructor. We
+ abbreviate the instantiatiation \\
+ $C[A_1/X_1,\ldots,A_n/X_n,\u B_1/\u Y_i,\ldots,\u B_m/\u Y_m]$ by $C[A_i,\u B_i]$.
Suppose $\defdncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{-}$ is a complex
stack (depending on $C$ and each $A_i,A_i',\u B_i,\u B_i'$) such that
@@ -2210,7 +2210,44 @@ Dually, we have
\end{lemma}
\begin{proof}
- FIXME
+ To show
+ \[
+ \bullet : C[A_i',\u B_i'] \vdash \dncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet} \ltdyn \defdncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet} : C[A_i,\u B_i]
+ \]
+ we have $\bullet : C[A_i',\u B_i'] \vdash \dncast{C[A_i,\u
+ B_i]}{C[A_i',\u B_i']}{\bullet} \ltdyn \bullet : C[A_i,\u B_i]
+ \ltdyn C[A_i',\u B_i']$ by the defining property of an upcast, and
+ substituting into assumption (2) part 2 gives
+ \[
+ \defdncast{C[A_i,\u B_i]}{C[A_i,\u B_i]}{\dncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet}} \ltdyn \defdncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet}
+ \]
+
+ Then transitivity with the right-to-left direction of assumption (3)
+ instantiated as follows
+ \[
+ {\dncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet}}
+ \ltdyn
+ \defdncast{C[A_i,\u B_i]}{C[A_i,\u B_i]}{\dncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet}}
+ \]
+ gives the result.
+
+ To show
+ \[
+ \defdncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet} \ltdyn \dncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet}
+ \]
+ by the downcast right rule, it suffices to show
+ \[
+ \defdncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet} \ltdyn \bullet : {C[A_i,\u B_i]} \ltdyn {C[A_i',\u B_i']}
+ \]
+ By assumption (2) part 1, we have
+ \[
+ \defdncast{C[A_i,\u B_i]}{C[A_i',\u B_i']}{\bullet} \ltdyn \defdncast{C[A_i',\u B_i']}{C[A_i',\u B_i']}{\bullet} : C[A_i,\u B_i] \ltdyn C[A_i',\u B_i']
+ \]
+ so transitivity with the left-to-right direction of assumption (3)
+ \[
+ \defdncast{C[A_i',\u B_i']}{C[A_i',\u B_i']}{\bullet} \ltdyn \bullet
+ \]
+ gives the result.
\end{proof}
@@ -2328,8 +2365,105 @@ Dually, we have
\end{array}
\]
- \item Sums downcast. FIXME
-
+ \item Sums downcast. We use the downcast lemma with $X_1 \vtype, X_2
+ \vtype \vdash \u F(X_1 + X_2) \ctype$. Let
+ \[
+ \bullet' : \u F (A_1' + A_2') \vdash \defdncast{\u F (A_1 + A_2)}{\u F (A_1' + A_2')}{\bullet'} : \u F (A_1 + \u A_2)
+ \]
+ stand for
+ \[
+ \bindXtoYinZ{\bullet}{(s : (A_1' +
+ A_2'))}{}
+ {\caseofXthenYelseZ{s}
+ {x_1'.\bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}{\ret{(\inl {x_1})}}}
+ {\ldots}}\\
+ \]
+ (where, as in the theorem statement, $\mathsf{inr}$ branch is
+ analogous), which has the correct type for the lemma's assumption
+ (1).
+
+ For assumption (2), we first need to show
+ \begin{small}
+ \[
+ \bullet : {\u F (A_1' + A_2')} \vdash
+ \defdncast{\u F (A_1 + A_2)}{\u F (A_1' + A_2')}{\bullet'}
+ \ltdyn
+ \defdncast{\u F (A_1' + A_2')}{\u F (A_1' + A_2')}{\bullet'}
+ : {\u F (A_1 + A_2)} \ltdyn {\u F (A_1' + A_2')}
+ \]
+ \end{small}
+ i.e.
+ \begin{small}
+ \[
+ \begin{array}{c}
+ \bindXtoYinZ{\bullet}{(s' : (A_1' + A_2'))}{}
+ {\caseofXthenYelseZ{s'}
+ {x_1'.\bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}{\ret{(\inl {x_1})}}}
+ {\ldots}}\\
+ \ltdyn\\
+ \bindXtoYinZ{\bullet}{(s' : (A_1' + A_2'))}{}
+ {\caseofXthenYelseZ{s'}
+ {x_1'.\bindXtoYinZ{(\dncast{\u F A_1'}{\u F A_1'}{(\ret{x_1'})})}{x_1'}{\ret{(\inl {x_1'})}}}
+ {\ldots}}
+ \end{array}
+ \]
+ \end{small}
+ which is true by the congruence rules for $\mathsf{bind}$,
+ $\mathsf{case}$, downcasts, $\mathsf{ret}$, and $\mathsf{inl}/\mathsf{inr}$.
+
+ Next, we need to show
+ \begin{small}
+ \[
+ \bullet \ltdyn \bullet' : {\u F (A_1 + A_2)} \ltdyn {\u F (A_1' + A_2')} \vdash
+ \defdncast{\u F (A_1 + A_2)}{\u F (A_1 + A_2)}{\bullet}
+ \ltdyn
+ \defdncast{\u F (A_1 + A_2)}{\u F (A_1' + A_2')}{\bullet'}
+ : {\u F (A_1 + A_2)}
+ \]
+ \end{small}
+ i.e.
+ \begin{small}
+ \[
+ \begin{array}{c}
+ \bindXtoYinZ{\bullet}{(s : (A_1 + A_2))}{}
+ {\caseofXthenYelseZ{s}
+ {x_1.\bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1}{(\ret{x_1})})}{x_1}{\ret{(\inl {x_1})}}}
+ {\ldots}}\\
+ \ltdyn\\
+ \bindXtoYinZ{\bullet}{(s' : (A_1' + A_2'))}{}
+ {\caseofXthenYelseZ{s'}
+ {x_1'.\bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}{\ret{(\inl {x_1})}}}
+ {\ldots}}\\
+ \end{array}
+ \]
+ \end{small}
+ which is also true by congruence.
+
+ Finally, for assumption (3), we show
+ \begin{small}
+ \[
+ \begin{array}{lll}
+ \bindXtoYinZ{\bullet}{(s : (A_1 + A_2))}{}
+ {\caseofXthenYelseZ{s}
+ {x_1.\bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1}{(\ret{x_1})})}{x_1}{\ret{(\inl {x_1})}}}
+ {\ldots}} & \equidyn & \\
+ \bindXtoYinZ{\bullet}{(s : (A_1 + A_2))}{}
+ {\caseofXthenYelseZ{s}
+ {x_1.\bindXtoYinZ{({(\ret{x_1})})}{x_1}{\ret{(\inl {x_1})}}}
+ {\ldots}} & \equidyn & \\
+ \bindXtoYinZ{\bullet}{(s : (A_1 + A_2))}{}
+ {\caseofXthenYelseZ{s}
+ {x_1.{\ret{(\inl {x_1})}}}
+ {x_2.{\ret{(\inr {x_2})}}}} & \equidyn & \\
+ \bindXtoYinZ{\bullet}{(s : (A_1 + A_2))}{}
+ {\ret{s}} & \equidyn &\\
+ \bullet
+ \end{array}
+ \]
+ \end{small}
+ using the downcast identity, $\beta$ for $\u F$ types, $\eta$ for
+ sums, and $\eta$ for $\u F$ types.
+
\item Eager product upcast. We use Lemma~\ref{lem:upcast} with the type
constructor $X_1 \vtype, X_2 \vtype \vdash X_1 \times X_2 \vtype$.
Let
@@ -2377,7 +2511,105 @@ Dually, we have
p
\]
- \item Eager product downcast. FIXME
+ \item Eager product downcast.
+
+ We use the downcast lemma with $X_1 \vtype, X_2 \vtype \vdash \u
+ F(X_1 \times X_2) \ctype$. Let
+ \[
+ \bullet' : \u F (A_1' \times A_2') \vdash \defdncast{\u F (A_1 \times A_2)}{\u F (A_1' \times A_2')}{\bullet'} : \u F (A_1 \times \u A_2)
+ \]
+ stand for
+ \begin{small}
+ \[
+ \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) }}}}
+ \]
+ \end{small}
+ which has the correct type for the lemma's assumption (1).
+
+ For assumption (2), we first need to show
+ \begin{small}
+ \[
+ \bullet : {\u F (A_1' \times A_2')} \vdash
+ \defdncast{\u F (A_1 \times A_2)}{\u F (A_1' \times A_2')}{\bullet'}
+ \ltdyn
+ \defdncast{\u F (A_1' \times A_2')}{\u F (A_1' \times A_2')}{\bullet'}
+ : {\u F (A_1 \times A_2)} \ltdyn {\u F (A_1' \times A_2')}
+ \]
+ \end{small}
+ i.e.
+ \begin{small}
+ \[
+ \begin{array}{c}
+ \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) }}}}\\
+ \ltdyn\\
+ \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') }}}}
+ \end{array}
+ \]
+ \end{small}
+ which is true by the congruence rules for $\mathsf{bind}$,
+ $\mathsf{split}$, downcasts, $\mathsf{ret}$, and pairing.
+
+ Next, we need to show
+ \begin{small}
+ \[
+ \bullet \ltdyn \bullet' : {\u F (A_1 \times A_2)} \ltdyn {\u F (A_1' \times A_2')} \vdash
+ \defdncast{\u F (A_1 \times A_2)}{\u F (A_1 \times A_2)}{\bullet}
+ \ltdyn
+ \defdncast{\u F (A_1 \times A_2)}{\u F (A_1' \times A_2')}{\bullet'}
+ : {\u F (A_1 + A_2)}
+ \]
+ \end{small}
+ i.e.
+ \begin{small}
+ \[
+ \begin{array}{c}
+ \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) }}}}\\
+ \ltdyn\\
+ \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) }}}}\\
+ \end{array}
+ \]
+ \end{small}
+ which is also true by congruence.
+
+ Finally, for assumption (3), we show
+ \begin{small}
+ \[
+ \begin{array}{lll}
+ \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{{\ret x_1}}{x_1}{
+ \bindXtoYinZ{{\ret x_2}}{x_2} {\ret (x_1,x_2) }}}} & \equidyn & \\
+ \bindXtoYinZ{\bullet}{p}{\pmpairWtoXYinZ{p}{x_1}{x_2}{{\ret (x_1,x_2) }}} & \equidyn & \\
+ \bindXtoYinZ{\bullet}{p}{\ret p} & \equidyn & \\
+ \bullet \\
+ \end{array}
+ \]
+ \end{small}
+ using the downcast identity, $\beta$ for $\u F$ types, $\eta$ for
+ eager products, and $\eta$ for $\u F$ types.
+
+ An analogous argument works if we sequence the downcasts of the
+ components in the opposite order:
+ \begin{small}
+ \[
+ \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{small}
+ (the only facts about downcasts used above are congruence and the
+ downcast identity), which shows that these two implementations of
+ the downcast are themselves equidynamic.
\item Lazy product downcast.
We use Lemma~\ref{lem:downcast} with
@@ -2752,46 +2984,183 @@ Dually, the casts determined by $\top \ltdyn \u B$ are
\end{enumerate}
\end{proof}
-\subsection{Upcasts are Thunkable, Downcasts are Linear, a posteriori}
+\subsection{Monadic/Comonadic Casts}
+
+In GTT, we assert the existence of value upcasts and computation
+downcasts for derivable type dynamism relation. While we do not assert
+the existence of all value downcasts and computation upcasts, we can
+define their universal property:
\begin{definition}[Computation upcasts/value downcasts]
\item
- An \emph{upcast between $\u F$ types} is a stack $\bullet : \u F A
- \vdash \upcast{\u F A}{\u F A'} \bullet : \u F A'$ that satisfies the
- term dynamisms rules of an upcast for the stack judgement:
+ If $\u B \ltdyn \u B'$, a \emph{computation upcast from $B$ to $B'$}
+ is a stack $\bullet : \u B \vdash \defupcast{\u B}{\u B'} \bullet : \u
+ B'$ that satisfies the dynamism rules of an upcast:
\[
-{\bullet : \u F A \vdash \bullet \ltdyn \upcast{\u F A}{\u F A'} \bullet : \u F A \ltdyn \u F A'}
-\qquad
- {\bullet \ltdyn \bullet : \u F A \ltdyn \u F A' \vdash \upcast{\u F A}{\u F A'} \bullet \ltdyn \bullet : \u F A'}
+ {\bullet : \u B \vdash \bullet \ltdyn \defupcast{\u B}{\u B'} \bullet : \u B \ltdyn \u B'}
+ \qquad
+ {\bullet \ltdyn \bullet' : \u B \ltdyn \u B' \vdash \defupcast{\u B}{\u B'} \bullet \ltdyn \bullet' : \u B'}
\]
-\item A \emph{downcast betweeen $U$ types} is a complex value Suppose we
- have a value $\bullet : U \u B' \vdash \dncast{U \u B}{U \u B'}
- \bullet : U \u B'$ that satisfies the term dynamisms rules of an
- upcast for the stack judgement:
+
+\item If $A \ltdyn A'$, a \emph{value downcast from $A'$ to $A$} is a
+ complex value $x : A' \vdash \defdncast{A}{A'} x : A$ that satisfies
+ the term dynamism rules of a downcast:
\[
-{\bullet : U \u B' \vdash \bullet \ltdyn \dncast{U \u B}{U \u B'} \bullet : U \u B \ltdyn U \u B'}
-\qquad
- {\bullet \ltdyn \bullet : U \u B \ltdyn U \u B' \vdash \bullet \ltdyn \dncast{U \u A}{U \u A'} \bullet \ltdyn \bullet : U \u A'}
+ {x : A' \vdash \defdncast{A}{A'}{x} \ltdyn x : A \ltdyn A'}
+ \qquad
+ {x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn \dncast{A}{A'} x' : A}
\]
\end{definition}
-\begin{theorem}
-\item The stack $\bullet : {\u F A} \vdash
- \bindXtoYinZ{\bullet}{(x:A)}{\ret{\upcast{A}{A'}{x}}} : {\u F A'}$
- is an upcast between $\u F$ types, and any other upcast from $\u F
- A$ to $\u F A'$ is equidynamic with it:
-\[
-\bullet : {\u F A} \vdash \upcast{\u F A}{\u F A'} \bullet \equidyn \bindXtoYinZ{\bullet}{(x:A)}{\ret{\upcast{A}{A'}{x}}} : {\u F A'}
-\]
-\item
-\end{theorem}
+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 computation
+upcasts and value downcasts as well.
-Proof: TODO
+Some value downcasts and computation upcasts do exist, leading to a
+characterization of the casts for the monad/comonad of $F \dashv U$:
+\begin{theorem} Suppose $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 computation upcast.
+
+ \item If $\defupcast{\u B}{\u B'}$ is a computation 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 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})}}
+ \]
-\begin{theorem}
-Then
+ \item In particular,
+ \[
+ \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}
+ \]
+ \end{enumerate}
\end{theorem}
+\begin{proof}
+ \begin{enumerate}
+ \item
+ To show
+ \[
+ \bullet : \u F A \vdash \bullet \ltdyn
+ \bindXtoYinZ{\bullet}{x:A}{\ret{(\upcast{A}{A'}{x})}} : \u F A
+ \ltdyn \u F A'
+ \]
+ we can $\eta$-expand $\bullet \equidyn
+ \bindXtoYinZ{\bullet}{x}{\ret{x}}$ on the left, at which point by
+ congruence it suffices to show $x \ltdyn \upcast{A}{A'}{x}$, which
+ is true up upcast right. To show
+ \[
+ \bullet \ltdyn \bullet' : \u F A \ltdyn \u F A' \vdash
+ \bindXtoYinZ{\bullet}{x:A}{\ret{(\upcast{A}{A'}{x})}}
+ \ltdyn
+ \bullet'
+ : \u F A'
+ \]
+ we can $\eta$-expand $\bullet' \equidyn
+ \bindXtoYinZ{\bullet'}{x'}{\ret{x'}}$ on the right,
+ and then apply congruence, the assumption that $\bullet \ltdyn
+ \bullet'$, and upcast left.
+
+ \item We apply the upcast lemma with the type constructor $\u Y \ctype
+ \vdash U \u Y \vtype$. The term $\thunk{(\defupcast{\u B}{\u
+ B'}{(\force x)})}$ has the correct type for assumption (1). For
+ assumption (2), we show
+ \[
+ x : U \u B \vdash \thunk{(\defupcast{\u B}{\u B}{(\force x)})} \ltdyn
+ \thunk{(\defupcast{\u B}{\u B'}{(\force x)})} : U \u B \ltdyn U \u B'
+ \]
+ by congruence for $\mathsf{thunk}$, $\defupcast{\u B}{\u B}$ (proved
+ analogously to Lemma~\ref{lem:cast-congruence}), and $\mathsf{force}$.
+ We show
+ \[
+ x \ltdyn x' : U \u B \ltdyn U \u B' \vdash
+ \thunk{(\defupcast{\u B}{\u B'}{(\force x)})}
+ \thunk{(\defupcast{\u B'}{\u B'}{(\force x')})}
+ : U \u B'
+ \]
+ by congruence as well.
+ Finally, for assumption (3), we have
+ \[
+ \begin{array}{cc}
+ \thunk{(\defupcast{\u B}{\u B}{(\force x)})} & \equidyn \\
+ \thunk{({(\force x)})} & \equidyn \\
+ x
+ \end{array}
+ \]
+ using $\eta$ for $U$ types and the identity principle for
+ $\defupcast{\u B}{\u B}$ (proved analogously to
+ Theorem~\ref{thm:decomposition}).
+
+ \item To show
+ \[
+ x' : U \u B' \vdash \thunk{(\dncast{\u B}{\u B'}{(\force x')})} \ltdyn x' : U \u B \ltdyn U \u B'
+ \]
+ we can $\eta$-expand $x'$ to $\thunk{\force{x'}}$, and then by
+ congruence it suffices to show $\dncast{\u B}{\u B'}{(\force x')}
+ \ltdyn \force{x'} : \u B \ltdyn \u B'$, which is downcast left.
+ Conversely, for
+ \[
+ x \ltdyn x' : U \u B \ltdyn U \u B' \vdash x \ltdyn \thunk{(\dncast{\u B}{\u B'}{(\force x')})} : U \u B
+ \]
+ we $\eta$-expand $x$ to $\thunk{(\force{x})}$, and then it suffices
+ to show $\dncast{\u B}{\u B'}{(\force{x})} \ltdyn \force{x'}$, which
+ is true by downcast right and congruence of $\mathsf{force}$ on the
+ assumption $x \ltdyn x'$.
+
+ \item We use the downcast lemma with $X \vtype \vdash \u F X \ctype$,
+ where $\bindXtoYinZ{\bullet}{x':A'}{\ret{(\defdncast{A}{A'}{x})}}$
+ has the correct type for assumption (1). For assumption (2), we
+ show
+ \[
+ \bullet : \u F A' \vdash
+ \bindXtoYinZ{\bullet}{x':A'}{\ret{(\defdncast{A}{A'}{x})}}
+ \ltdyn
+ \bindXtoYinZ{\bullet}{x':A'}{\ret{(\defdncast{A'}{A'}{\bullet})}}
+ \]
+ by congruence for $\mathsf{bind}$, $\mathsf{ret}$, and
+ $\defdncast{A'}{A'}$ (which is proved analogously to
+ Lemma~\ref{lem:cast-congruence}).
+ We also show
+ \[
+ \bullet \ltdyn \bullet' : \u F A \ltdyn \u F A' \vdash
+ \bindXtoYinZ{\bullet}{x:A}{\ret{(\defdncast{A}{A}{x})}}
+ \ltdyn
+ \bindXtoYinZ{\bullet}{x':A'}{\ret{(\defdncast{A}{A'}{\bullet'})}}
+ : \u F A
+ \]
+ by congruence.
+ Finally, for assumption (3), we have
+ \[
+ \begin{array}{rc}
+ \bindXtoYinZ{\bullet}{x:A}{\ret{(\defdncast{A}{A}{x})}} & \equidyn \\
+ \bindXtoYinZ{\bullet}{x:A}{\ret{({x})}} & \equidyn \\
+ \bullet
+ \end{array}
+ \]
+ using the identity principle for $\defdncast{A}{A}$ (proved
+ analogously to Theorem~\ref{thm:decomposition}) and $\eta$ for $F$
+ types.
+
+ \item Combining parts (1) and (2) gives the first equation, while
+ combining parts (3) and (4) gives the second equation.
+ \end{enumerate}
+\end{proof}
+
+\subsection{Upcasts are Values, Downcasts are Stacks}
\begin{theorem}{Upcasts are (Complex) Values, Downcasts are (Complex) Stacks}
If the tagging upcasts are complex values and untagging downcasts
@@ -2802,6 +3171,45 @@ Then
\end{proof}
+
+\subsection{Equidynamic Types are Isomorphic}
+
+\begin{theorem}
+ \begin{enumerate}
+ \item
+ If $A \ltdyn A'$ and $A' \ltdyn A$ then $A \cong_v A'$.
+ \item
+ If $\u B \ltdyn \u B'$ and $\u B' \ltdyn \u B$ then $\u B \cong_c \u B'$.
+ \end{enumerate}
+\end{theorem}
+\begin{proof}
+ \begin{enumerate}
+ \item We have upcasts $x : A \vdash \upcast{A}{A'}{x} : A'$ and $x' : A' \vdash \upcast{A'}{A}{x'} : A$.
+ For the composites, to show
+ $x : A \vdash \upcast{A'}{A}{\upcast{A}{A'}{x}} \ltdyn x$
+ we apply upcast left twice, and conclude $x \ltdyn x$ by assumption.
+ To show,
+ $x : A \vdash x \ltdyn \upcast{A'}{A}{\upcast{A}{A'}{x}}$,
+ we have $x : A \vdash x \ltdyn {\upcast{A}{A'}{x}} : A \ltdyn A'$
+ by upcast right, and therefore
+ $x : A \vdash x \ltdyn \upcast{A'}{A}{\upcast{A}{A'}{x}} : A \ltdyn A$
+ again by upcast right.
+ The other composite is the same proof with $A$ and $A'$ swapped.
+
+ \item We have downcasts $\bullet : \u B \vdash \dncast{\u B}{\u B'}{\bullet} : \u B'$ and
+ $\bullet : \u B' \vdash \dncast{\u B'}{\u B}{\bullet} : \u B$.
+
+ For the composites, to show $\bullet : \u B' \vdash \bullet \ltdyn
+ \dncast{\u B'}{\u B}{\dncast{\u B}{\u B'}}{\bullet}$, we apply
+ downcast right twice, and conclude $\bullet \ltdyn \bullet$. For
+ $\dncast{\u B'}{\u B}{\dncast{\u B}{\u B'}}{\bullet} \ltdyn
+ \bullet$, we first have $\dncast{\u B}{\u B'}{\bullet} \ltdyn
+ \bullet : \u B \ltdyn \u B'$ by downcast left, and then the result
+ by another application of downcast left.
+ The other composite is the same proof with $\u B$ and $\u B'$ swapped.
+ \end{enumerate}
+\end{proof}
+
%% \subsection{Retract Axiom}
%% In the call-by-name version of GTT (\cite{GTT}), there was an explicit
--
GitLab