start describing stacks, add blame stub to discussion

paper/gtt.tex

@@ -165,23 +165,24 @@
 
 %% 2012 ACM Computing Classification System (CSS) concepts
 %% Generate at 'http://dl.acm.org/ccs/ccs.cfm'.
-\begin{CCSXML}
-<ccs2012>
-<concept>
-<concept_id>10011007.10011006.10011008</concept_id>
-<concept_desc>Software and its engineering~General programming languages</concept_desc>
-<concept_significance>500</concept_significance>
-</concept>
-<concept>
-<concept_id>10003456.10003457.10003521.10003525</concept_id>
-<concept_desc>Social and professional topics~History of programming languages</concept_desc>
-<concept_significance>300</concept_significance>
-</concept>
-</ccs2012>
-\end{CCSXML}
-
-\ccsdesc[500]{Software and its engineering~General programming languages}
-\ccsdesc[300]{Social and professional topics~History of programming languages}
+%% TODO
+%% \begin{CCSXML}
+%% <ccs2012>
+%% <concept>
+%% <concept_id>10011007.10011006.10011008</concept_id>
+%% <concept_desc>Software and its engineering~General programming languages</concept_desc>
+%% <concept_significance>500</concept_significance>
+%% </concept>
+%% <concept>
+%% <concept_id>10003456.10003457.10003521.10003525</concept_id>
+%% <concept_desc>Social and professional topics~History of programming languages</concept_desc>
+%% <concept_significance>300</concept_significance>
+%% </concept>
+%% </ccs2012>
+%% \end{CCSXML}
+
+%% \ccsdesc[500]{Software and its engineering~General programming languages}
+%% \ccsdesc[300]{Social and professional topics~History of programming languages}
 %% End of generated code
 
 
@@ -343,8 +344,6 @@ Note that these properties \emph{uniquely define} the casts (up to
 mutual refinement) because two greatest elements must each be greater
 than the other and dually for least elements.
 
-
-
 Previous work has built towards this goal from two directions.
 %
 First, \cite{cbn-gtt} provided an axiomatic semantics for the
@@ -395,8 +394,93 @@ embeddings.
 
 \section{Axiomatic Gradual Type Theory}
 
+\subsection{Call-by-Push-Value, Gradualized}
+
+In figure \ref{judge} we present the syntax of Gradual Type Theory.
+%
+For the types inherited from CBPV, we follow the dogma of
+gradualization: everything is monotone with respect to the ordering,
+and to axiomatize strong type soundness we include the $\beta$ and
+$\eta$ principles of CBPV as order equivalences, but otherwise
+unmodified.
+
+\paragraph{Stacks}
+
+The most unusual feature of call-by-push-value to someone used to
+call-by-value is the \emph{stack} judgment, which is the dual to the
+value judgment.
+%
+Semantically, we can think of open values as equivalent to those terms
+that are ``pure'' in that they never perform any effects.
+%
+On the other hand, we can think of stacks as equivalent to those terms
+between computation types that \emph{reflect all effects} of their
+input.
+%
+This is formalized with the following equivalence rules that say if a
+term is a stack filled with a term performing an effect, then that is
+equivalent to first performing the effect, and then running $M$ with
+the same stack.
+
+\begin{mathpar}
+  \inferrule
+  {\Gamma \pipe \u B \vdash S : \u C}
+  {\Gamma \vdash S[\error] \equidyn \error}
+
+  \inferrule
+  {\Gamma \pipe \u B \vdash S : \u C \and \Gamma \vdash M : \u B \and \Gamma \vdash V : \texttt{Char}}
+  {\Gamma \vdash S[\print V; M] \equidyn \print V; S[M] : \u C}
+\end{mathpar}
+
+While these rules are very intuitive when the input and output types
+of the stack are $\u F A$ for some value type (which is always the
+case in call-by-value), when we have stacks between computation types
+that are not $\u F A$, we can observe this property to be quite
+strong.
+
+For instance, consider a stack $A \to \u B \vdash S : \u F A$ between
+a function type and a $\u F$ree value type.
+%
+Consider what happens when we apply the stack to a function that
+prints.
+%
+In CBN and CBPV evaluation, $\print c; \lambda x:A. M$ is equivalent
+to $\lambda x:A.\print c; M$ because the printing only happens when
+the expression is called.
+
+\begin{align*}
+  S[\lambda x : A. \print c; M] &\equidyn S[\print c; \lambda x:A. M]\\
+  &\equidyn \print c; S[\lambda x:A. M] \\
+\end{align*}
+
+This shows us that a stack out of a function type \emph{calls the
+  function exactly once}.
+%
+Generalizing further, a stack out of an iterated function type $A_1
+\to A_2 \to \u B$ \emph{supplies all of the arguments}
+%
+
+
+\subsection{Casts}
+
+
+
 \subsection{Embedding Call-by-Value}
 
+One of the key features of call-by-push-value is that it
+\emph{subsumes} call-by-value and call-by-name in that they can be
+``fully faithfully'' embedded into CBPV: two CBV programs are
+equivalent if and only if their embeddings into CBPV are equivalent
+and every CBPV program with a CBV type can be back-translated to CBV.
+%
+By the same turn, we can study equivalence of call-by-value programs
+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.
+%
+
+
 \section{Theorems in Gradual Type Theory}
 
 \section{Contract Translation to Call-by-push-value}
@@ -405,6 +489,7 @@ embeddings.
 
 \subsection{Graduality Logical Relation}
 
+
 \begin{figure}
   
   \caption{Observational Approximation Logical Relation}
@@ -445,6 +530,26 @@ omega paper?)
 It should be the case that the terms in AGT are the subset of ours
 that are definable using the upcasts and downcasts in that language.
 
+\paragraph{Blame and the Tangram Theorem}
+
+We do not give a treatment of blame but our axiomatic language is
+sufficiently similar to cast calculi that it should be clear how to
+add it, and in our contract implementation we can parameterize the
+upcasts and downcasts by a blame label and raise an error with the
+blame information rather than the uninformative $\err$.
+%
+Also, our judicious division of casts into upcasts and downcasts
+naturally pairs with the blame soundness properties given in
+\cite{wadler-findler}: upcasts never raise positive blame, so only
+need to be parameterized by a negative label and downcasts never raise
+negative blame so only need to be parameterized by a positive label.
+
+TODO: can we relate this and the tangram theorem more directly to what
+we're doing?
+%
+The association we propose of upcasts to (positive) value types and
+downcasts to (negative) computation types
+
 \paragraph{$\eta$ Law in Practice}
 
 The $\eta$ law for function types, even in the appropriate form for