From c0fdabca473420288fa206d23c4d831d8690c191 Mon Sep 17 00:00:00 2001
From: Dan Licata <drl@cs.cmu.edu>
Date: Tue, 26 Jun 2018 12:16:12 -0400
Subject: [PATCH] typeset definitions of casts
---
paper/gtt.tex | 88 +++++++++++++++++++++++++++++++++++----------------
1 file changed, 61 insertions(+), 27 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index dd212cd..1b8c8bb 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -1024,21 +1024,22 @@ TODO: do we actually know what would go wrong in that case?
\bigskip
- \framebox{Error Universal Properties}
-
\begin{mathpar}
+ \framebox{Error Universal Properties}
+ \qquad
\inferrule{ \Gamma' \mid \cdot \vdash M' : \u B' }
{ \Gamma \ltdyn \Gamma' \mid \cdot \vdash \err \ltdyn M : \u B \ltdyn \u B'}
-
+ \qquad
\inferrule { \Gamma \mid x : \u B \vdash S : \u B'}
{\Gamma \mid \cdot \vdash S[\err_{\u B}] \ltdyn \err_{\u{B'}} : \u B'}
\end{mathpar}
\bigskip
- \framebox{Cast Success/Failure}
\[
+ \framebox{Cast Success/Failure}
+ \quad
\begin{array}{c}
%% TODO prove these:
%% x : A \vdash \dncast{\u F A}{\u F A'}{(\ret{(\upcast{A}{A'}{x})})} \ltdyn \ret{x} : \u F A \\
@@ -1400,31 +1401,64 @@ $\eta$-expansion \emph{up to cast at smaller type}.
\begin{theorem}{Characterization of Casts}
- \begin{enumerate}
-
- \item[+] $\upcast{A_1 + A_2}{A_1' + A_2'} \equidyn \ldots$
- and $\dncast{\u F (A_1' + A_2')}{\u F (A_1 + A_2)} \equidyn \ldots$
+ \begin{small}
+\[
+ \begin{array}{l}
+ \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})}}\\
+ \dncast{\u F (A_1' + A_2')}{\u F (A_1 + A_2)}{\bullet} \equidyn \\
+ \bindXtoYinZ{\bullet}{(s : (A_1' +
+ A_2'))}{}\\
+ \quad
+ {\caseofXthenYelseZ{s}
+ {x_1'.\bindXtoYinZ{(\dncast{\u F A_1}{\u F A_1'}{(\ret{x_1'})})}{x_1}{\ret{(\inl {x_1})}}}
+ {x_2'.\bindXtoYinZ{(\dncast{\u F A_2}{\u F A_2'}{(\ret{x_2'})})}{x_2}{\ret{(\inr {x_2})}}}}\\
+ \\
+ \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}{l}
+ \dncast{\u F (A_1' \times A_2')}{\u F (A_1 \times A_2)}{\bullet}
+ \equidyn \\
+ \qquad
+ \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 \\
+ \qquad
+ \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}\\
- \item[$\times$] $\upcast{A_1 \times A_2}{A_1' \times A_2'} \equidyn \ldots$
- and $\dncast{\u F (A_1' \times A_2')}{\u F (A_1 \times A_2)} \equidyn \ldots$
- (both orders)
+ \\
+ \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}{l}
+ \upcast{U (\u B_1 \with \u B_2)}{U (\u B_1' \with \u B_2')}{p} \equidyn\\
+ \thunk{\pair{\force{(\upcast{U \u B_1}{U \u B_1'}{(\thunk{\pi (\force{p})})})}}{\force{(\upcast{U \u B_2}{U \u B_2'}{(\thunk{\pi' (\force{p})})})}}}
+ \end{array}
+ \\
- \item[$\with$] $\dncast{\u B_1 \with \u B_2}{\u B_1' \with \u B_2'} \equidyn \ldots$
- and $\upcast{U (\u B_1 \with \u B_2)}{U (\u B_1' \with \u B_2')} \equidyn \ldots$
-
- \item[$\to$] $\dncast{A \to \u B}{A' \to \u B'} \equidyn \ldots$
- and $\upcast{U (A \to \u B)}{U (A' \to \u B')} \equidyn \ldots$
-
- \item[0]
- $\upcast{0}{A}V \equidyn \absurd V$ and
- $\dncast{\u F 0}{\u F A} \equidyn \err$
- \item[1]
- $\dncast{1}{\u B} \equidyn \{\}$ and
- $\upcast{U 1}{U \u B} \equidyn \thunk \err$
- \item[$\top$] $\dncast{\u B}{\top} \equiv \ldots$
- $\upcast{U \u B}{U \top} \equiv \ldots$
-
- \end{enumerate}
+ \\
+ \dncast{A \to \u B}{A' \to \u B'}{\bullet} \equidyn
+ \lambda{x}.{\dncast{B}{B'}{(\bullet \, (\upcast{A}{A'}{x}))}} \\
+ \begin{array}{l}
+ \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}
+ \\
+
+ \\
+ \upcast{0}{A}z \equidyn \absurd z\\
+ \dncast{\u F 0}{\u F A}{M} \equidyn \err\\
+
+ \\
+ \dncast{\top}{\u B}{\bullet} \equidyn \{\}\\
+ \upcast{U \top}{U \u B}{u} \equidyn \thunk \err
+ %% \item[$\top$] $\dncast{\u B}{\top} \equiv \ldots$
+ %% $\upcast{U \u B}{U \top} \equiv \ldots$
+ \end{array}
+ \]
+ \end{small}
\end{theorem}
\subsection{Upcasts are Thunkable, Downcasts are Linear, a posteriori}
--
GitLab