More abstract, start casts section, stub relation to contextual isos

paper/gtt.tex

@@ -152,15 +152,36 @@
 \begin{document}
 
 \begin{abstract}
-  We present Gradual Type Theory: an axiomatic semantics of gradual
+  We present Gradual Type Theory (GTT): an axiomatic semantics of gradual
   typing.
   Gradual Type Theory gives specifications to the cast semantics that
   are normally part of the language definition of gradual typing.
-  Since it is based on Levy's Call-by-push-value language, it supports
-  embeddings of call-by-value and call-by-name gradually typed
-  languages, and proves uniqueness theorems for cast/contracts in
-  call-by-value and call-by-name languages with both positive and
-  negative type connectives.
+  These combine the axiomatics for effectful languages provided by
+  call-by-push-value with the graduality property that says that
+  making types more precise in a gradual program only adds errors, and
+  that casts produce minimal change in program semantics.
+  The use of call-by-push-value enables us to see distinctions that
+  were not previously observed in call-by-value gradually typed
+  languages: chief among them is that while upcasts are known to
+  always terminate, \emph{downcasts} satisfy a dual property that they
+  are \emph{linear}.
+
+  Furthermore, We show that the combination of effect-aware
+  $\beta\eta$ laws and graduality is \emph{only} satsified by
+  ``wrapping'' implementations of gradual typing, and ``eager''
+  semantics violate the $\eta$ principles.
+  On the other hand the structure of the dynamic type itself, which is
+  taken for granted to be a sum in previous work, is not uniquely
+  determined by the axiomatics.
+  
+  We give a translation of the axiomatic theory into
+  call-by-push-value with recursive types and errors.
+  We define a logical relation that models the logical notion of term
+  dynamism that is key to interpreting the dynamic gradual guarantee.
+  Using the rich types of call-by-push-value, we vary the structure of
+  the dynamic type and produce several translations that all model the
+  axioms of GTT to varying degrees of support for call-by-value and
+  call-by-name embeddings.
 \end{abstract}
 
 %% 2012 ACM Computing Classification System (CSS) concepts
@@ -463,7 +484,88 @@ 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
+CBN into CBPV for guidance.
+%
+In both CBV and CBN, we add a type dynamism judgment $A \ltdyn B$ and
+for every such pair, we add an upcast from $A$ to $B$: $\ucpast A B M$
+and a downcast from $B$ to $A$: $\dncast A B M$.
+%
+Then because CBV types are associated to CBPV value types and CBN
+types are associated to CBPV computation types, it seems reasonable to
+simply have a value type dynamism $A \ltdyn A'$ and computation type
+dynamism $\u B \ltdyn \u B'$ and an upcast and downcast form for each
+corresponding to the CBV and CBN casts.
+%
+A CBV terms $x : A \vdash M : A'$ is in CBPV a term $x : A \vdash M :
+\u F A'$, because in call by value values are passed as arguments,
+then effects are performed and possibly a value is returned.
+%
+A CBN term $x : \u B \vdash M : \u B'$ is in CBPV a term $x : U \u
+B\vdash M : \u B'$, because in CBN unevaluated thunks are passed as
+arguments and terms satisfy the $\eta$ laws of the computation type.
+
+\begin{figure}
+  \begin{mathpar}
+    \inferrule
+    {\Gamma \vdash V : A \and A \ltdyn A'}
+    {\Gamma \vdash \upcast {A}{A'} V : \u F A'}
+
+    \inferrule
+    {\Gamma \vdash V' : A' \and A \ltdyn A'}
+    {\Gamma \vdash \dncast {A}{A'} V' : \u F A}
+
+    \inferrule
+    {\Gamma \vdash V : U \u B \and \u B \ltdyn \u B'}
+    {\Gamma \vdash \upcast {\u B}{\u B'} V : \u B'}
+
+    \inferrule
+    {\Gamma \vdash V' : U \u B' \and \u B \ltdyn \u B'}
+    {\Gamma \vdash \dncast {\u B}{\u B'} V' : \u B'}
+  \end{mathpar}
+  \caption{Na\"ive Interpretation of Casts}
+  \label{Bad Casts}
+\end{figure}
+
+So to reproduce this in GTT, we could add casts to the language as in
+figure \ref{bad-casts}, which we call the ``na\"ive'' interpretation
+of casts.
+%
+We call it na\"ive because it is problematic for multiple reasons:
+some syntactic and some semantic.
+
+First, semantically, it is \emph{insufficient} to recover all of the
+known properties of casts in CBV: specifically that in CBV, upcasts
+always terminate without performing any effects, and in some systems
+upcasts are defined to be values.
+%
+In previous work on a logical relation for call-by-value gradual
+typing, it was possible to prove from the properties we axiomatized
+that all upcasts had this property, but this was only because we were
+working in a language whose only effects were divergence and error.
+%
+In a more
+
+The na\"ive casts are also problemantic syntactically.
+%
+The first issue is that they violate a type theoretic principle of
+\emph{modularity}: 
+
+%% Counterexample
+
+%% consider a language whose only effects are error and incrementing
+%% and decrementing an integer counter.
+%%
 
+%% Then for closed programs with unit output, P <= P' when P ->* err
+%% or P ->* (n, ()) and P' ->* (n', ()) and n = n', where n,n' are the
+%% final counts
+
+%% Then for every type A, there are CBV coreflections (e(x) = inc; ret x | p(y) = dec; ret y)
+
+\subsection{Dynamic Type(s)}
 
 \subsection{Embedding Call-by-Value}
 
@@ -483,6 +585,19 @@ interpreted as value types in call-by-push-value.
 
 \section{Theorems in Gradual Type Theory}
 
+From the axiomatics of Gradual Type Theory, we can derive many
+consequences.
+
+\begin{theorem}{Casts (de)composition}
+  For any $A \ltdyn A' \ltdyn A''$ and $\u B \ltdyn \ltdyn \u B' \ltdyn \u B''$:
+  \begin{enumerate}
+  \item $x \vdash \upcast A A x \equidyn x$
+  \item $x \vdash \upcast A {A''}x \equidyn \upcast{A'}{A''}\upcast A{A'} x$
+  \item $\bullet \vdash \dncast {\u B}{\u B} \bullet \equidyn \bullet$
+  \item $\bullet \vdash \dncast {\u B}{\u B''} \bullet \equidyn \dncast{\u B}{\u B'}\dncast{\u B'}{\u B''} \bullet$
+  \end{enumerate}
+\end{theorem}
+
 \section{Contract Translation to Call-by-push-value}
 
 \subsection{Cast to Contract Translation}
@@ -499,6 +614,25 @@ interpreted as value types in call-by-push-value.
 
 \paragraph{Casts as Galois Connections}
 
+\paragraph{Thunkable, Linear, Contextual Isomorphisms}
+
+Our use of complex values for upcasts and complex stacks for downcasts
+seems closely related to the use of thunkable isomorphisms and linear
+isomorphisms in polarized languages like call-by-push-value and
+sequent calculi.
+%
+Thunkability and linearity are semantic properties that say when terms
+are ``essentially'' values and stacks respectively.
+%
+Levy has proposed a notion of \emph{contextual} isomorphism of types
+that in call-by-push-value and other polarized languages correctly
+identifies that isomorphisms between value types should be thunkable
+and between computation types should be linear.
+%
+However, a slightly strange property is that in Levy's paper, all
+contextual morphisms are isomorphisms so we are not sure how this
+relates to our system.
+
 \paragraph{Abstracting Gradual Typing}
 
 As mentioned before, our gradual record types are not quite the same
@@ -554,7 +688,7 @@ downcasts to (negative) computation types
 
 The $\eta$ law for function types, even in the appropriate form for
 call-by-value is \emph{not} satisfied by so-called \emph{eager} cast
-semantics.
+semantics, which is what is produced by AGT.
 %
 TODO: see the cbn gtt repo.
 %