dynamic types

paper/gtt.tex

@@ -706,9 +706,75 @@ 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)
 
-\subsection{Dynamic Type(s)}
+\subsection{Dynamic Types and Errors}
 
-\subsection{Embedding Call-by-Value}
+Since our language has two different kinds of types, we have several
+choices in deciding what our dynamic type should be: either the
+dynamic type should be a value type, or a computation type, or we
+should have \emph{two} dynamic types: a dynamic value type and a
+dynamic computation type.
+%
+Fortunately our modular type-theoretic presentation of gradual typing
+allows us to easily explore all of these options, though we find that
+(surprisingly) having both dynamic value and computation types gives
+the most natural implementation (TODO: forward reference).
+
+Regardless, the dynamic types each have a simple definition: the
+dynamic value type $\dynv$ is the most dynamic value type and the
+dynamic computation type is the most dynamic computation type!
+%
+The reason for this simplicity is that we are leaving abstract what
+the actual implementation of the dynamic type so that we can prove
+quite general theorems.
+%
+Because of this, we have ``stuck'' terms in some sense: for example we
+cannot prove in the theory that $\dncast{\u F 1+1}{\u
+  F\dynv}\upcast{1}{\dynv}$ reduces to an error, and there are valid
+models in which it is not an error, for instance if the unique value
+of $1$ is represented as the boolean false.
+
+To model runtime errors, we add an error term to every computation
+type.
+%
+We also add two axioms about the error type: first, it should be the
+least term of every computation type, which models the graduality
+ordering.
+%
+Second, since stacks force their evaluation position, a stack applied
+to an error $S[\err]$ should be equivalent to an error.
+
+\begin{figure}
+  \inferrule
+  {}
+  {\dynv \vtype}
+
+  \inferrule
+  {}
+  {\dync \ctype}
+
+  \inferrule
+  {}
+  {A \ltdyn \dynv}
+
+  \inferrule
+  {}
+  {\u B \ltdyn \dync}
+
+  \inferrule
+  {}
+  {\Gamma \vdash \err_{\u B} : \u B}
+
+  \inferrule
+  {}
+  {\Phi \vdash \err \ltdyn M : \u B}
+
+  \inferrule
+  {}
+  {\Phi \vdash S[\err] \ltdyn \err : \u B}
+  \caption{Dynamic Types and Type Errors}
+\end{figure}
+
+\subsection{Embedding Gradual 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
@@ -721,7 +787,6 @@ 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}