diff --git a/paper/gtt.tex b/paper/gtt.tex
index 692c3f4852b6140b892153c0a7d495ed83173d6f..6fc5fc67db315cd85ec905d54cb14a35294b3df6 100644
--- a/paper/gtt.tex
+++ b/paper/gtt.tex
@@ -165,6 +165,7 @@
\newcommand{\bigstepzero}{\bigstepsin{0}}
\newcommand{\pair}[2]{\{ \pi \mapsto {#1} \pipe \pi' \mapsto {#2}\}}
+\newcommand{\emptypair}[0]{\{\}}
\newcommand{\pairWtoXYtoZ}[4]{\{ #1 \mapsto {#2} \pipe #3 \mapsto {#4}\}}
\newcommand{\tru}{\texttt{true}}
\newcommand{\fls}{\texttt{false}}
@@ -198,8 +199,10 @@
\newcommand{\too}{\kw{to}}
\newcommand{\case}{\kw{case}}
\newcommand{\kw}[1]{\texttt{#1}\,\,}
+\newcommand{\absurd}{\kw{absurd}}
\newcommand{\caseofXthenYelseZ}[3]{\case #1 \{ #2 \pipe #3 \}}
\newcommand{\pmpairWtoXYinZ}[4]{\kw{split} #1\,\kw{to} (#2,#3). #4}
+\newcommand{\pmpairWtoinZ}[2]{\kw{split} #1\,\kw{to} (). #2}
\newcommand{\pmmuXtoYinZ}[3]{\kw{unroll} #1 \,\kw{to} \roll #2. #3}
\newcommand{\ret}{\kw{ret}}
\newcommand{\thunk}{\kw{thunk}}
@@ -207,6 +210,13 @@
\newcommand{\abort}{\kw {abort}}
\newcommand{\with}{\mathbin{\&}}
+\newcommand{\bnfalt}{\mathrel{\bf \,\mid\,}}
+\newcommand{\alt}{\bnfalt}
+\newcommand{\bnfdef}{\mathrel{\bf ::=}}
+\newcommand{\bnfadd}{\mathrel{\bf +::=}}
+\newcommand{\bnfsub}{\mathrel{\bf -::=}}
+
+
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{document}
@@ -616,8 +626,6 @@ Generalizing further, a stack out of an iterated function type $A_1
\subsection{Casts}
-
-
It is not immediately obvious how to add type casts to
call-by-push-value, but we can use previous work on call-by-value and
call-by-name gradual typing, combined with the embeddings of CBV and
@@ -706,6 +714,485 @@ TODO: do we actually know what would go wrong in that case?
%% Then for every type A, there are CBV coreflections (e(x) = inc; ret x | p(y) = dec; ret y)
+\begin{figure}
+ \[
+ \begin{array}{lcl}
+ A & ::= & \dynv \mid U \u B \mid 0 \mid A_1 + A_2 \mid 1 \mid A_1 \times A_2 \\
+ \u B & ::= & \dync \mid \u F A \mid \u B_1 \with \u B_2 \mid A \to \u B\\
+ \Gamma & ::= & \cdot \mid \Gamma, x : A \\
+ \Delta & ::= & \cdot \mid \bullet : \u B \\
+ \Phi & ::= & \cdot \mid \Phi, x \ltdyn x': A \ltdyn A' \\
+ \Psi & ::= & \cdot \mid \bullet \ltdyn \bullet : \u B \ltdyn \u B' \\
+ V & ::= & x \mid \upcast A {A'} V \mid \upcast {\u B} {\u B'} V \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}
+ \\
+ M & ::= & \bullet \mid \err \mid \letXbeYinZ V x M \mid \dncast A {A'} M \mid \dncast {\u B} {\u B'} M \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 \pair{M_1}{M_2} \mid \pi M \mid \pi' M
+ \\
+ T & ::= & A \mid \u B \\
+ E & ::= & V \mid M \\
+ \end{array}
+ \]
+ \caption{GTT Syntax}
+\end{figure}
+
+\begin{figure}
+ \begin{mathpar}
+ \inferrule{ }{A \ltdyn A}
+
+ \inferrule{A \ltdyn A' \and A' \ltdyn A''}
+ {A \ltdyn A''}
+
+ \inferrule{ }{\u B \ltdyn \u B'}
+
+ \inferrule{\u B \ltdyn \u B' \and \u B' \ltdyn \u B''}
+ {\u B \ltdyn \u B''}
+\\
+ \inferrule{ }{A \ltdyn \dynv}
+
+ \inferrule{\u B \ltdyn \u B'}
+ {U B \ltdyn U B'}
+
+ \inferrule{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+ {A_1 + A_2 \ltdyn A_1' + A_2'}
+
+ \inferrule{A_1 \ltdyn A_1' \and A_2 \ltdyn A_2' }
+ {A_1 \times A_2 \ltdyn A_1' \times A_2'}
+
+\\
+\inferrule{ }{\u B \ltdyn \dync}
+
+\inferrule{A \ltdyn A' }{ \u F A \ltdyn \u F A'}
+
+\inferrule{\u B_1 \ltdyn \u B_1' \and \u B_2 \ltdyn \u B_2'}
+ {\u B_1 \with \u B_2 \ltdyn \u B_1' \with \u B_2'}
+
+\inferrule{A \ltdyn A' \and \u B \ltdyn \u B'}
+ {A \to \u B \ltdyn A' \to \u B'}
+\\
+\inferrule{ }{\cdot \, \mathsf{ctx}}
+\and
+\inferrule{\Phi \, \mathsf{ctx} \and
+ A \ltdyn A'}
+ {\Phi, x \ltdyn x' : A \ltdyn A' \, \mathsf{ctx}}
+\and
+\inferrule{ }{\cdot \, \mathsf{cctx}}
+\and
+\inferrule{\u B \ltdyn \u B'}
+ {(\bullet \ltdyn \bullet : \u B \ltdyn \u B') \, \mathsf{cctx}}
+\end{mathpar}
+
+
+\caption{GTT Type and Context Dynamism}
+\end{figure}
+
+\begin{figure}
+\begin{small}
+ \begin{mathpar}
+ \inferrule
+ { }
+ {\Gamma,x : A,\Gamma' \vdash x : A}
+
+ \inferrule
+ { }
+ {\Gamma\pipe \bullet : \u B \vdash \bullet : \u B}
+
+ \inferrule
+ { }
+ {\Gamma \vdash \err : \u B}
+
+ %% FIXME: why?
+ \inferrule
+ {\Gamma \vdash V : A \and
+ \Gamma, x : A \vdash M : \u B
+ }
+ {\Gamma \vdash \letXbeYinZ V x M : \u B}
+\\
+ \inferrule
+ {\Gamma \vdash V : A \and A \ltdyn A'}
+ {\Gamma \vdash \upcast A {A'} V : A'}
+ \quad
+ \qquad
+ \inferrule
+ {\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}
+\\
+ \inferrule
+ {\Gamma \vdash V : 0}
+ {\Gamma \mid \Delta \vdash \abort V : T}
+
+ \inferrule
+ {\Gamma \vdash V : A_1}
+ {\Gamma \vdash \inl V : A_1 + A_2}
+
+ \inferrule
+ {\Gamma \vdash V : A_2}
+ {\Gamma \vdash \inr V : A_1 + A_2}
+
+ \inferrule
+ {
+ \Gamma \vdash V : A_1 + A_2 \\\\
+ \Gamma, x_1 : A_1 \mid \Delta \vdash E_1 : T \\\\
+ \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}
+ \\
+ \inferrule
+ { }
+ {\Gamma \vdash (): 1}
+ \qquad
+ \inferrule
+ {\Gamma \vdash V : 1 \and
+ \Gamma \mid \Delta \vdash E : T
+ }
+ {\Gamma \mid \Delta \vdash \pmpairWtoinZ V E : T}
+ \qquad
+ \inferrule
+ {\Gamma \vdash V_1 : A_1\and
+ \Gamma\vdash V_2 : A_2}
+ {\Gamma \vdash (V_1,V_2) : A_1 \times A_2}
+ \qquad
+ \inferrule
+ {\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
+ {\Gamma \mid \cdot \vdash M : \u B}
+ {\Gamma \vdash \thunk M : U \u B}
+
+ \inferrule
+ {\Gamma \vdash V : U \u B}
+ {\Gamma \pipe \cdot \vdash \force V : \u B}
+
+ \inferrule
+ {\Gamma \vdash V : A}
+ {\Gamma \pipe \cdot \vdash \ret V : \u F A}
+
+ \inferrule
+ {\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
+ {\Gamma, x: A \pipe \Delta \vdash M : \u B}
+ {\Gamma \pipe \Delta \vdash \lambda x : A . M : A \to \u B}
+
+ \inferrule
+ {\Gamma \pipe \Delta \vdash M : A \to \u B\and
+ \Gamma \vdash V : A}
+ {\Gamma \pipe \Delta \vdash M\,V : \u B }
+ \\
+ \inferrule{ }{\Gamma \mid \cdot \vdash \emptypair : \top}
+
+ \inferrule
+ {\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}
+
+ \inferrule
+ {\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
+ {\Gamma \mid \Delta \vdash \pi M : \u B_1}
+
+ \inferrule
+ {\Gamma \mid \Delta \vdash M : \u B_1 \with \u B_2}
+ {\Gamma \mid \Delta \vdash \pi' M : \u B_2}
+ \end{mathpar}
+ \caption{GTT Terms}
+\end{small}
+\end{figure}
+
+
+\begin{figure}
+ \begin{small}
+ \begin{mathpar}
+ \inferrule
+ { }
+ {x : A \vdash x \ltdyn \upcast A {A'} x : A \ltdyn A'}
+
+ \inferrule
+ { }
+ {x \ltdyn x' : A \ltdyn A' \vdash \upcast A {A'} x \ltdyn x' : A' }
+
+ \inferrule
+ { }
+ {\bullet : \u B' \vdash \dncast{\u B}{\u B'} \bullet \ltdyn \bullet : \u B \ltdyn \u B'}
+
+ \inferrule
+ { }
+ {\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \dncast{\u B}{\u B'} \bullet : \u B}
+
+ \inferrule
+ { }
+ {\caseofXthenYelseZ{\inl V}{x_1. E_1}{x_2. E_2} \equidyn E_1[V/x_1]}
+
+ \inferrule
+ { }
+ {\caseofXthenYelseZ{\inr V}{x_1. E_1}{x_2. E_2} \equidyn E_2[V/x_2]}
+
+ \inferrule
+ {\Gamma, x : A_1 + A_2 \vdash E : T}
+ {\Gamma, x : A_1 + A_2 \vdash E \equidyn \caseofXthenYelseZ x {x_1. E[\inl x_1/x]}{x_2. E[\inr x_2/x]} : T}
+
+ \inferrule
+ { }
+ {\pmpairWtoXYinZ{(V_1,V_2)}{x_1}{x_2}{E} \equidyn E[V_1/x_1,V_2/x_2]}
+
+ \inferrule
+ {\Gamma, x : A_1 \times A_2 \vdash E : T}
+ {\Gamma, x : A_1 \times A_2 \vdash E \equidyn \pmpairWtoXYinZ x {x_1}{x_2} E[(x_1,x_2)/x] : T}
+
+ \inferrule
+ {\Gamma, x : 1 \vdash E : T}
+ {\Gamma, x : 1 \vdash E \equidyn \pmpairWtoinZ{x}{E[()/x]} : T}
+ \\
+ \inferrule
+ { }
+ {\force\thunk M \equidyn M}
+
+ \inferrule
+ { }
+ {x : U \u B \vdash x \equidyn \thunk\force x : U \u B}
+ \\
+ %% why?
+ %% \inferrule
+ %% {}
+ %% {\letXbeYinZ V x M \equidyn M[V/x]}
+
+ \inferrule
+ { }
+ {\bindXtoYinZ {\ret V} x M \equidyn M[V/x]}
+
+ \inferrule
+ { }
+ {\bullet : \u F A \vdash \bullet \equidyn \bindXtoYinZ \bullet x \ret x : \u F A}
+
+ \inferrule
+ { }
+ {(\lambda x:A. M)\,V \equidyn M[V/x]}
+
+ \inferrule
+ { }
+ {\bullet : A \to \u B \vdash \bullet \equidyn \lambda x:A. \bullet\,x : A \to \u B}
+ \\
+ \inferrule
+ { }
+ {\pi \pair{M}{M'} \equidyn M}
+
+ \inferrule
+ { }
+ {\pi' \pair{M}{M'} \equidyn M'}
+
+ \inferrule
+ { }
+ {\bullet : \u B_1 \with \u B_2 \vdash \bullet \equidyn\pair{\pi \bullet}{\pi' \bullet} : \u B_1 \with \u B_2}
+
+ \inferrule{ }
+ {\bullet : \top \vdash \bullet \equidyn \{\} : \top}
+ \end{mathpar}
+ \end{small}
+ \caption{GTT Term Precision Axioms}
+\end{figure}
+
+\begin{figure}
+ \begin{mathpar}
+ \inferrule
+ {\Gamma \pipe \Delta \vdash M : \u F A' \and A \ltdyn A'}
+ {\Gamma \pipe \Delta \vdash \dncast {\u F A} {\u F A'} M : \u F A}
+
+ \inferrule
+ {\Gamma \vdash V : U \u B \and \u B \ltdyn \u B'}
+ {\Gamma \vdash \upcast {U \u B} {U \u B'} V : U \u B'}
+ \\
+ \inferrule
+ {A \ltdyn A' \and \Phi \vdash V \ltdyn V' : A \ltdyn A'}
+ {\Phi \vdash V \ltdyn \upcast {A'} {A''} {V'} : A \ltdyn A''}
+
+ \inferrule
+ {\Phi \vdash V \ltdyn V'' : A \ltdyn A''}
+ {\Phi \vdash \upcast A {A'} V \ltdyn V'' : A' \ltdyn A'' }
+
+ \inferrule
+ { \u B' \ltdyn \u B'' \and \Phi \mid \Psi \vdash M' \ltdyn M'' : \u B' \ltdyn \u B''}
+ { \Phi \mid \Psi \vdash \dncast{\u B}{\u B'} M' \ltdyn M'' : \u B \ltdyn \u B''}
+
+ \inferrule
+ { \Phi \mid \Psi \vdash M \ltdyn M'' : B \ltdyn B'' }
+ { \Phi \mid \Psi \vdash M \ltdyn \dncast{\u B'}{\u B''} M'' : \u B \ltdyn \u B''}
+ \end{mathpar}
+ \caption{Derived Cast Rules}
+\end{figure}
+
+\begin{figure}
+\begin{small}
+ \begin{mathpar}
+
+ \inferrule{ }{\Gamma \ltdyn \Gamma \vdash V \ltdyn V : A \ltdyn A}
+
+ \inferrule{\Gamma \ltdyn \Gamma' \vdash V \ltdyn V' : A \ltdyn A' \\\\
+ \Gamma' \ltdyn \Gamma'' \vdash V' \ltdyn V'' : A' \ltdyn A''
+ }
+ {\Gamma \ltdyn \Gamma'' \vdash V \ltdyn V'' : A \ltdyn A''}
+ \\
+ \inferrule{ }{\Gamma \ltdyn \Gamma \mid \Delta \ltdyn \Delta \vdash M \ltdyn M : \u B \ltdyn \u B}
+
+ \inferrule{\Gamma \ltdyn \Gamma' \mid \Delta \ltdyn \Delta' \vdash M \ltdyn M' : \u B \ltdyn \u B' \\\\
+ \Gamma' \ltdyn \Gamma'' \mid \Delta' \ltdyn \Delta'' \vdash M' \ltdyn M'' : \u B' \ltdyn \u B''
+ }
+ {\Gamma \ltdyn \Gamma'' \mid \Delta \ltdyn \Delta'' \vdash M \ltdyn M'' : \u B \ltdyn \u B''}
+
+ \inferrule
+ { }
+ {\Phi,x \ltdyn x' : A \ltdyn A',\Phi' \vdash x \ltdyn x' : A \ltdyn A'}
+
+ \inferrule
+ {\Phi \vdash V \ltdyn V' : A \ltdyn A' \\\\
+ \Phi, x \ltdyn x' : A \ltdyn A',\Phi' \pipe \Psi \vdash E \ltdyn E' : T \ltdyn T'
+ }
+ {\Phi \mid \Psi \vdash E[V/x] \ltdyn E'[V'/x'] : T \ltdyn T'}
+
+ \inferrule
+ { }
+ {\Phi \pipe \bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \bullet : \u B \ltdyn \u B'}
+
+ \inferrule
+ {\Phi \pipe \Psi \vdash M_1 \ltdyn M_1' : \u B_1 \ltdyn \u B_1' \\\\
+ \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'}
+ \end{mathpar}
+\end{small}
+\caption{GTT Term Precision (Identity and Substitution)}
+\end{figure}
+
+
+\begin{figure}
+\begin{small}
+ \begin{mathpar}
+%% FIXME: why?
+ %% \inferrule
+ %% {\Phi \vdash V \ltdyn V' : A \ltdyn A' \and
+ %% \Phi, x \ltdyn x' : A \ltdyn A' \pipe \Psi \vdash M \ltdyn M' : \u B \ltdyn \u B'
+ %% }
+ %% {\Phi \mid \Psi \vdash \letXbeYinZ V x M \ltdyn \letXbeYinZ {V'} {x'} {M'} : \u B \ltdyn \u B'}
+ \\
+ %% congruence for casts is derivable, right?
+ \inferrule
+ {\Phi \vdash V \ltdyn V' : 0 \ltdyn 0}
+ {\Phi \mid \Psi \vdash \abort V \ltdyn \abort V' : T \ltdyn T'}
+ \\
+ \inferrule
+ {\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'}
+
+ \inferrule
+ {\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'}
+
+ \inferrule
+ {
+ \Phi \vdash V \ltdyn V' : A_1 + A_2 \ltdyn A_1' + A_2' \\\\
+ \Phi, x_1 \ltdyn x_1' : A_1 \ltdyn A_1' \mid \Psi \vdash E_1 \ltdyn E_1' : T \ltdyn 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'}
+ \\
+
+ \inferrule
+ {\Phi \vdash V \ltdyn V' : 1 \ltdyn 1 \and
+ \Phi \mid \Psi \vdash E \ltdyn E' : T \ltdyn T'
+ }
+ {\Phi \mid \Psi \vdash \pmpairWtoinZ V E \ltdyn \pmpairWtoinZ V' E' : T \ltdyn T'}
+
+ \inferrule
+ {\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'}
+
+ \inferrule
+ {\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
+ {\Phi \mid \cdot \vdash M \ltdyn : \u B \ltdyn \u B'}
+ {\Phi \vdash \thunk M \ltdyn \thunk M' : U \u B \ltdyn U \u B'}
+
+ \inferrule
+ {\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'}
+ \\
+
+ \inferrule
+ {\Phi \vdash V \ltdyn V' : A \ltdyn A'}
+ {\Phi \pipe \cdot \vdash \ret V \ltdyn \ret V' : \u F A \ltdyn \u F A'}
+
+ \inferrule
+ {\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'}
+
+ \inferrule
+ {\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
+ {\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
+ {\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'}
+ \\
+ \inferrule
+ {\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'}
+
+ \inferrule
+ {\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{mathpar}
+ \caption{GTT Term Dynamism (Compatibility Rules)}
+\end{small}
+\end{figure}
+
+\begin{figure}
+ \begin{mathpar}
+ \inferrule
+ {\Gamma \vdash V : A \and A \ltdyn A'}
+ {\Gamma \vdash \upcast A {A'} V : A'}
+
+ \inferrule
+ {}
+ {x : A \vdash x \ltdyn \upcast A {A'} x : A \ltdyn A'}
+
+ \inferrule
+ {}
+ {x \ltdyn x' : A \ltdyn A' \vdash \upcast A {A'} x \ltdyn x' : A'}
+
+ \inferrule
+ {\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}
+
+ \inferrule
+ {}
+ {\bullet : \u B' \vdash \dncast{\u B}{\u B'} \bullet \ltdyn \bullet : \u B \ltdyn \u B'}
+
+ \inferrule
+ {}
+ {\bullet \ltdyn \bullet : \u B \ltdyn \u B' \vdash \bullet \ltdyn \dncast{\u B}{\u B'} \bullet : \u B}
+ \end{mathpar}
+ \caption{Casts in GTT}
+\end{figure}
+
\subsection{Dynamic Types and Errors}
Since our language has two different kinds of types, we have several
@@ -788,6 +1275,57 @@ by taking just the subset of types that are sensible in Call-by-value.
The key feature of call-by-value is that all of its types are
interpreted as value types in call-by-push-value.
+\begin{figure}
+ \begin{mathpar}
+ \begin{array}{lrcl}
+ \text{Types} & A & \bnfdef & 1 \alt (A + A) \alt (A \times A) \alt (A_1,\ldots,A_n) \to A\\
+ \text{Values} & V & \bnfdef & \upcast{A}{A'}V \alt () \alt \inl V \alt \inr V \alt (V,V) \alt \lambda (x_1:A_1,\ldots,x_n:A_n). M\\
+ \text{Terms} & M & \bnfdef & \err V \alt \alt \dncast{A}{A'}V \alt \caseofXthenYelseZ V {\inl x_1. M_1}{\inr x_2. M_2} \alt \pmpairWtoXYinZ V x y M \alt V(V_1,\ldots,V_n) \alt \bindXtoYinZ M x M \alt \letXbeYinZ V x M
+ \end{array}
+ \end{mathpar}
+
+ \begin{mathpar}
+ \inferrule
+ {\Gamma \vdash V : A \and A \ltdyn A'}
+ {\Gamma \vdash \upcast A {A'} V : A'}
+
+ \inferrule
+ {\Gamma \vdash V : A' \and A \ltdyn A'}
+ {\Gamma \vdash \dncast A {A'} V : A}
+
+ \inferrule
+ {}
+ {x : A' \vdash \dncast A A' x \ltdyn x : A \ltdyn A'}
+
+ \inferrule
+ {}
+ {x \ltdyn x' : A \ltdyn A' \vdash x \ltdyn \dncast A {A'} x : A}
+ \end{mathpar}
+ \caption{CBV GTT}
+\end{figure}
+
+\begin{figure}
+ \begin{mathpar}
+ \inferrule
+ {A \ltdyn A' \and B \ltdyn B'}
+ {f : A \to B \vdash \dncast{A\to B}{A' \to B'} f \equidyn \lambda (x:A). \bindXtoYinZ {f(\upcast{A}{A'}x)} y \dncast{B}{B'} y}
+
+ \inferrule
+ {
+ f \ltdyn \lambda (x:A). \bindXtoYinZ {f(x)} y y
+ \and
+ \inferrule
+ {\inferrule
+ {\inferrule{f \ltdyn f'\and x \ltdyn \upcast{A}{A'}x}{{f(x)} \ltdyn f'(\upcast{A}{A'}x)} \and {y \ltdyn y' \vdash y \ltdyn \dncast{B}{B'} y}}
+ {x \ltdyn x : A \vdash \bindXtoYinZ {f(x)} y y \ltdyn \bindXtoYinZ {f'(\upcast{A}{A'}x)} y' \dncast{B}{B'} y}
+ }
+ {\lambda (x:A). \bindXtoYinZ {f(x)} y y \ltdyn \lambda (x:A). \bindXtoYinZ {f'(\upcast{A}{A'}x)} y' \dncast{B}{B'} y}
+ }
+ {f \ltdyn f' : A \to B \ltdyn A' \to B'
+ \vdash f \ltdyn \lambda (x:A). \bindXtoYinZ {f'(\upcast{A}{A'}x)} y' \dncast{B}{B'} y'}
+ \end{mathpar}
+ \caption{Uniqueness Principle for CBV Functions}
+\end{figure}
\section{Theorems in Gradual Type Theory}
@@ -808,7 +1346,23 @@ Gradual Type Theory.
\subsection{Upcasts are Thunkable, Downcasts are Linear, a posteriori}
-While we have shown
+\begin{theorem}{Upcasts are (Complex) Values, Downcasts are (Complex) Stacks}
+ If the tagging upcasts are complex values and untagging downcasts
+ are stacks, then all upcasts are complex values and all downcasts
+ are complex stacks.
+\end{theorem}
+\begin{proof}
+
+\end{proof}
+
+\subsection{Retract Axiom}
+
+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.
+%
+
\subsection{Uniqueness Principles for Casts}
@@ -819,11 +1373,95 @@ principles of each type, given in figure TODO ref.
\begin{figure}
\begin{mathpar}
- TODO
+ \upcast{0}{A}V \equidyn \absurd V\\
+ \dncast{\u F 0}{\u F A} \equidyn \err\\
+
+ \dncast{1}{\u B} \equidyn \{\}\\
+ \upcast{U 1}{U \u B} \equidyn \thunk \err\\
\end{mathpar}
\caption{Uniqueness Principles for Casts}
\end{figure}
+To prove these uniqueness theorems, we use the fact that the
+specification of upcasts and downcasts by their right and left
+$\ltdyn$ rules defines them \emph{uniquely} up to $\equidyn$.
+%
+In category-theoretic terms this says that the upcasts and downcasts
+have a \emph{universal property}, and so we can show that something
+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}
+ If $A \ltdyn A'$ and $x : A \vdash V_u[x] : A'$ is a value such that
+ the following judgments are provable:
+ \begin{mathpar}
+ \inferrule
+ {}
+ {x : A \ltdyn x' : A' \vdash V_u[x] \ltdyn x' : A'}
+
+ \inferrule
+ {}
+ {x_2 : A \ltdyn x : A \vdash x_2 \ltdyn V_u[x] : A \ltdyn A'}
+ \end{mathpar}
+
+ then we can prove $x : A \vdash V_u[x] \equidyn x : A$.
+
+ Similarly, if $\u B \ltdyn \u B'$ and $\bullet : \u B' \vdash S_d :
+ \u B$ is a stack such that the following are provable:
+ \begin{mathpar}
+ \inferrule
+ {}
+ {\bullet \ltdyn \bullet : \u B' \vdash S_d \ltdyn \bullet : \u B \ltdyn \u B'}
+
+ \inferrule
+ {}
+ {\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}
+\begin{proof}
+ \begin{mathpar}
+ \inferrule*[right=substitution]
+ {x_1 \ltdyn x_2 \vdash x_1 \ltdyn \upcast{A}{A'}x_2 : A \ltdyn A' \and x_1 \ltdyn x_2' : A \ltdyn A' \vdash V_u[x_1] \ltdyn x_2' : A'}
+ {x_1 : A \ltdyn x_2 : A \vdash V_u[x_1] \ltdyn \upcast{A}{A'} x_2 : A'}
+ \end{mathpar}
+ The other direction is essentially the same, but swapping $V_u$ and
+ the upcast.
+\end{proof}
+
+The other key ingredient to the uniqueness theorems is the
+\emph{$\eta$ principle} and \emph{congruence rules} for each type.
+%
+The reason for this is that to show that an implementation of a cast
+$x : A \vdash V_u : A'$ is correct, we have to show that it is less
+than and greater than \emph{variables}: $x : A \ltdyn V_u[x]$ and $x
+\ltdyn x' \vdash V_u[x] \ltdyn x'$.
+%
+Since we know nothing about a variable except it's type, the only way
+to proceed is to $\eta$ expand it.
+%
+The uniqueness principles for casts arise when the two sides of the
+cast have the \emph{same} top-level connective, and thus the
+\emph{same} $\eta$ principle, so we $\eta$ expand both the lower
+bounding and upper bounding variable, and the cast itself is a kind of
+$\eta$-expansion \emph{up to cast at smaller type}.
+
+% TODO: can we take advantage of duality???
+%% 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
+
\section{Contract Translation to Call-by-push-value}
To show the soundness of our model, and demonstrate its relationship
@@ -2113,6 +2751,23 @@ the limit as $i \to \infty$.
equivalent to the graduality ordering.
\end{proof}
+In fact, we can prove the converse, that at least for the term case,
+our LR is \emph{complete} with respect to contextual graduality
+
+\begin{lemma}{Logical Preorder is Complete wrt Contextual Preorder}
+ For any $\apreorder$, if $\Gamma \vDash M \ctxize \apreorder N \in
+ \u B$, then $\Gamma \vDash M \ilrof\apreorder \omega {} N \in \u B$.
+\end{lemma}
+\begin{proof}
+ Let $S_1 \ilrof \apreorder i {\u B} S_2$ and $\gamma_1 \ilrof
+ \apreorder i \Gamma \gamma_2$. We need to show that
+ \[
+ S_1[M[\gamma_1]] \ix\apreorder i S_2[N[\gamma_2]]
+ \]
+ We use \emph{reflexivity} of the relation:
+ TODO: adapt the old proof of this below
+\end{proof}
+
This establishes that our logical relation can prove graduality, so it
only remains to show that our \emph{inequational theory} implies our
logical relation.
@@ -2192,7 +2847,40 @@ limit is a consequence.
TODO
\end{lemma}
-% Lemma: relation is a module of the ordering/infinite relation
+\begin{lemma}{$\precltdyn$ and $\ltdynsucc$ are Models of CBPV}
+ \begin{enumerate}
+ \item If $\Gamma \vdash M_1 \ltdyn M_2 : \u B$, then
+ \[ \Gamma \vDash M_1 \ix\precltdyn \omega M_2 \in \u B \]
+ and
+ \[ \Gamma \vDash M_1 \ix\ltdynsucc \omega M_2 \in \u B \]
+ \item If $\Gamma \vdash V_1 \ltdyn V_2 : A$, then
+ \[ \Gamma \vDash V_1 \ix\precltdyn \omega V_2 \in A
+ \]
+ \[ \Gamma \vDash V_1 \ix\ltdynsucc \omega V_2 \in A
+ \]
+ \item If $\Gamma \pipe \bullet : \u B \vdash S_1 \ltdyn S_2 : \u C$ , then
+ \[\Gamma \pipe \bullet : \u B \vDash S_1 \ix\precltdyn\omega S_2 \in \u C \]
+ and
+ \[\Gamma \pipe \bullet : \u B \vDash S_1 \ix\ltdynsucc\omega S_2 \in \u C \]
+ \end{enumerate}
+\end{lemma}
+
+\begin{theorem}{$\ctxize \ltdyn$ is a Model of CBPV}
+ \begin{enumerate}
+ \item If $\Gamma \vdash M_1 \ltdyn M_2 : \u B$, then
+ \[ \Gamma \vDash M_1 \ctxize\ltdyn M_2 \in \u B \]
+ \item If $\Gamma \vdash V_1 \ltdyn V_2 : A$, then
+ \[ \Gamma \vDash V_1 \ctxize\ltdyn V_2 \in A \]
+ \item If $\Gamma \pipe \bullet : \u B \vdash S_1 \ltdyn S_2 : \u C$, then
+ \[\Gamma \pipe \bullet : \u B \vDash S_1 \ctxize\ltdyn S_2 \in \u C \]
+ \end{enumerate}
+\end{theorem}
+\begin{proof}
+ TODO: prose
+ Logical by prev lemma
+ Logical => Contextual by soundness
+ Contextual of the 2 => Contextual ltdyn by earlier lemma
+\end{proof}
\begin{figure}
\begin{mathpar}