Skip to content
Snippets Groups Projects
Commit ad6508ee authored by Dan Licata's avatar Dan Licata
Browse files

one sfo->ewr worth of typesetting

parent 83904411
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 452 additions and 0 deletions
paper/gtt.tex
+ 452
− 0
View file @ ad6508ee
......@@ -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}}
......@@ -201,6 +202,7 @@
\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}}
......@@ -712,6 +714,456 @@ 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
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment