From 32578d2e09a096f66f3193bb3ff7578765be6334 Mon Sep 17 00:00:00 2001
From: Max New <maxsnew@gmail.com>
Date: Mon, 18 Jun 2018 09:11:42 -0400
Subject: [PATCH] dynamic types
---
paper/gtt.tex | 71 ++++++++++++++++++++++++++++++++++++++++++++++++---
1 file changed, 68 insertions(+), 3 deletions(-)
diff --git a/paper/gtt.tex b/paper/gtt.tex
index e6d7de5..692c3f4 100644
--- a/paper/gtt.tex
+++ b/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}
--
GitLab