\section{Introduction}
  
% gradual typing, graduality
\subsection{Gradual Typing and Graduality}
In modern programming language design, there is a tension between \emph{static} typing
and \emph{dynamic} typing disciplines.
With static typing, the code is type-checked at compile time, while in dynamic typing,
the type checking is deferred to run-time. Both approaches have benefits: with static 
typing, the programmer is assured that if the program passes the type-checker, their
program is free of type errors, and moreover, soundness of the equational theory implies
that program optimizations are valid.
Meanwhile, dynamic typing allows the programmer to rapidly prototype
their application code without needing to commit to fixed type signatures for their
functions. Most languages choose between static or dynamic typing and as a result, programmers that initially write their code in a dynamically typed language
in order to benefit from faster prototyping and development time need to rewrite the
some or all of their codebase in a static language if they would like to receive the benefits of static
typing once their codebase has matured.

\emph{Gradually-typed languages} \cite{siek-taha06, tobin-hochstadt06} seek to resolve this tension
by allowing for both static and dynamic typing disciplines to be used in the same codebase,
and by supporting smooth interoperability between statically-typed and dynamically-typed code.
This flexibility allows programmers to begin their projects in a dynamic style and
enjoy the benefits of dynamic typing related to rapid prototyping and easy modification
while the codebase ``solidifies''. Over time, as parts of the code become more mature
and the programmer is more certain of what the types should be, the code can be
\emph{gradually} migrated to a statically typed style without needing to
rewrite the project in a completely different language.

%Gradually-typed languages should satisfy two intuitive properties.
% The following two properties have been identified as useful for gradually typed languages.

In order for this to work as expected, gradually-typed languages should allow for
different parts of the codebase to be in different places along the spectrum from
dynamic to static, and allow for those different parts to interact with one another.
Moreover, gradually-typed languages should support the smooth migration from
dynamic typing to static typing, in that the programmer can initially leave off the
typing annotations and provide them later without altering the meaning of the program.
% Sound gradual typing
Furthermore, the parts of the program that are written in a dynamic style should soundly
interoperate with the parts that are written in a static style.
That is, the interaction between the static and dynamic components of the codebase
should preserve the guarantees made by the static types.
In particular, while statically-typed code can error at runtime in a gradually-typed language,
such an error can always be traced back to a dynamically-typed term that
violated the typing contract imposed by statically typed code.

% Moreover, gradually-typed languages should allow for
% different parts of the codebase to be in different places along the spectrum from
% dynamic to static, and allow for those different parts to interact with one another.
% In a \emph{sound} gradually-typed language,
% this interaction should respect the guarantees made by the static types.

% Graduality property
One of the fundamental theorems for gradually typed languages is 
\emph{dynamic gradual guarantee}, originally defined by Siek, Vitousek, Cimini,
and Boyland \cite{siek_et_al:LIPIcs:2015:5031}, also called \emph{graduality} \cite{new-ahmed2018},
by analogy with parametricity.
Informally, graduality says that going from a dynamic to static style should only allow for the introduction of static or dynamic type errors, and not otherwise change the meaning of the program.
%
This is a way to capture programmer intuition that increasing type
precision corresponds to a generalized form assertions at runtime
only, and so they can trust that prior observed behavior of their
dynamically typed code will remain unchanged as long as it satisfies
the new stricter typing discipline.

Additionally, gradually typed languages should offer some of the
benefits of static typing. While classical type soundness, that
well-typed programs are free from runtime errors, is not compatible
with runtime type errors, we can instead focus on \emph{type-based
reasoning}. For instance, while dynamically typed $\lambda$ calculi
only satisfy $\beta$ equality for their type formers, statically typed
$\lambda$ calculi additionally satisfy type-dependent $\eta$
properties that ensure that functions are determined by their behavior
under application and that pattern matching on data types
is safe and exhaustive.

Our goal in this work is to provide a reusable semantic framework for
gradually typed languages that can be used to prove the aforementioned
properties: graduality and type-based reasoning.

\subsection{Limitations of Prior Work}

We give an overview of current approaches to proving graduality of
languages and why they do not meet our criteria of a reusable semantic
framework.

\subsubsection{From Static to Gradual}

Current approaches to constructing languages that satisfy the
graduality property include the methods of Abstracting Gradual Typing
\cite{garcia-clark-tanter2016} and the formal tools of the Gradualizer
\cite{cimini-siek2016}.  These allow the language developer to start
with a statically typed language and derive a gradually typed language
that satisfies the gradual guarantee. The main downside to these
approaches lies in their inflexibility: since the process in entirely
mechanical, the language designer must adhere to the predefined
framework.  Many gradually typed languages do not fit into either
framework, e.g., Typed Racket \cite{tobin-hochstadt06,
  tobin-hochstadt08} and the semantics produced is not always the
desired one.
%
Furthermore, while these frameworks do prove graduality of the
resulting languages, they do not show the correctness of the
equational theory, which is equally important to sound gradual typing.

%% For example, programmers often refactor their code, and in so doing they rely
%% implicitly on the validity of the laws in the equational theory.
%% Similarly, correctness of compiler optimizations rests on the validity of the
%% corresponding equations from the equational theory. It is therefore important
%% that the languages that claim to be gradually typed have provably correct
%% equational theories.

% The approaches are too inflexible... the fact that the resulting semantics are too lazy
% is a consequence of that inflexibility.
% The validity of the equational theory captures the programmer's intuitive thinking when they refactor their code

%The downside is that
%not all gradually typed languages can be derived from these frameworks, and moreover, in both
%approaches the semantics is derived from the static type system as opposed to the alternative
%in which the semantics determines the type checking. Without a clear semantic interpretation of type
%dynamism, it becomes difficult to extend these techniques to new language features such as polymorphism.


% [Eric] I moved the next two paragraphs from the technical background section
% to here in the intro.
\subsubsection{Double Categorical Semantics}

New and Licata \cite{new-licata18} developed an axiomatic account of
the graduality relation on a call-by-name cast calculus terms and
showed that the graduality proof could be modeled using semantics in
certain kinds of \emph{double categories}, categories internal to the
category of categories. A double category extends a category with a
second notion of morphism, often a notion of ``relation'' to be paired
with the notion of functional morphism, as well as a notion of
functional morphisms preserving relations. In gradual typing the
notion of relation models type precision and the squares model the
term precision relation. This approach was influenced by the semantics
of parametricity using reflexive graph categories
\cite{ma-reynolds,dunphythesis,reynoldsprogramme}: reflexive graph
categories are essentially double categories without a notion of
relational composition. In addition to capturing the notions of type
and term precision, the double categorical approach allows for a
\emph{universal property} for casts: upcasts are the \emph{universal}
way to turn a relation arrow into a function in a forward direction
and downcasts are the dual universal arrow.  Later, New, Licata and
Ahmed \cite{new-licata-ahmed2019} extended this axiomatic treatment from
call-by-name to call-by-value as well by giving an axiomatic theory of
type and term precision in call-by-push-value. This left implicit any
connection to a ``double call-by-push-value'', which we make explicit
in Section~\ref{sec:cbpv}.

With this notion of abstract categorical model in hand, denotational
semantics is then the work of constructing concrete models that
exhibit the categorical construction. New and Licata
\cite{new-licata18} present such a model using categories of
$\omega$-CPOs, and this model was extended by Lennon-Bertrand,
Maillard, Tabareau and Tanter to prove graduality of a gradual
dependently typed calculus $\textrm{CastCIC}^{\mathcal G}$. This
domain-theoretic approach meets our criteria of being a semantic
framework for proving graduality, but suffers from the limitations of
classical domain theory: the inability to model viciously
self-referential structures such as higher-order extensible state and
similar features such as runtime-extensible dynamic types. Since these
features are quite common in dynamically typed languages, we seek a
new denotational framework that can model these type system features.

The standard alternative to domain theory that scales to essentially
arbitrary self-referential definitions is \emph{step-indexing} or its
synthetic form of \emph{guarded recursion}. A series of works
\cite{new-ahmed2018, new-licata-ahmed2019, new-jamner-ahmed19}
developed step-indexed logical relations models of gradually typed
languages based on operational semantics. Unlike classical domain
theory, such step-indexed techniques are capable of modeling
higher-order store and runtime-extensible dynamic types
\cite{appelmcallester01,ahmed06,neis09,new-jamner-ahmed19}. However,
their proof developments are highly repetitive and technical, with
each development formulating a logical relation from first-principles
and proving many of the same tedious lemmas without reusable
mathematical abstractions. Our goal in the current work is to extract
these reusable mathematical principles from these explicit
step-indexed to make formalization of realistic gradual languages
tractible.

%% \subsubsection{Classical Domain Models}

%%  and gave a denotational
%% model of this calculus using classical domain theory based on
%% $\omega$-CPOs. This semantics has scaled up to an analysis of a
%% dependently typed gradual calculus in \cite{asdf}. This meets our
%% criterion of being a reusable mathematical theory, as general semantic
%% theorems about gradual domains can be developed independent of any
%% particular syntax and then reused in many different denotational
%% models. However, it is widely believed that such classical domain
%% theoretic techniques cannot be extended to model higher-order store, a
%% standard feature of realistic gradually typed languages such as Typed
%% Racket. Thus if we want a reusable mathematical theory of gradual
%% typing that can scale to realistic programming languages, we need to
%% look elsewhere to so-called ``step-indexed'' techniques.

%% \subsubsection{Operational Reduction Proofs}


% Alternative phrasing:
\begin{comment}
\subsubsection{Embedding-Projection Pairs}

The series of works by New, Licata, and Ahmed \cite{new-licata18,new-ahmed2018,new-licata-ahmed2019}
develop an axiomatic account of gradual typing involving \emph{embedding-projection pairs}.
This allows for a particularly elegant formulation of the gradual guarantee.
Moreover, their axiomatic account of program equivalence allows for type-based reasoning about program equivalences.

In \cite{new-licata18}, New and Licata construct a denotational model of the axioms of
gradual typing using tools from classical domain theory. The benefit to this approach is that it is a reusable mathematical theory:
general semantic theorems about gradual domains can be developed independent of any particular syntax and then reused in many different denotational models.
Unfortunately, however, it is unclear how to extend these domain-theoretic techniques to incorporate more advanced language features such as higher-order store, a standard feature of realistic gradually typed languages such as Typed
Racket.
Thus, if we want a reusable mathematical theory of gradual typing that can scale to realistic programming languages, we need to look to different techniques.

In \cite{new-ahmed2018,new-licata-ahmed2019}, a more traditional operational semantics for gradual typing is derived from the axioms.
% The axioms are then proven to be sound with respect to this operational semantics by constructing a logical relation.
A logical relations model is constructed and used to prove that the axioms are sound with respect to the operational semantics.
The downside of this approach is that each new language requires a different logical relation
to prove graduality, even though the logical relations for different languages end up sharing many commonalities.
Furthermore, the logical relations tend to be quite complicated due to a technical requirement known as \emph{step-indexing},
where the stepping behavior of terms must be accounted for in the logical relation.
As a result, developments using this approach tend to require vast effort, with the
corresponding technical reports having 50+ pages of proofs.

% In this approach, a logical relation is constructed and used to show that the equational theory
% is sound with respect to the operational semantics.

% Additionally, while the axioms of gradual type theory are compositional at a ``global'' level,
% they do not compose in the step-indexed setting. One of the main goals of the present work
% is to formulate a composable theory of gradual typing in a setting where the stepping behavior
% is tracked.
\end{comment}

An alternative approach, which we
investigate in this paper, is provided by \emph{synthetic guarded
domain theory}\cite{birkedal-mogelberg-schwinghammer-stovring2011}.
The techniques of synthetic guarded domain theory allow us to
internalize the step-indexed reasoning normally required in logical
relations proofs of graduality, ultimately allowing us to specify the
logical relation in a manner that looks nearly identical to a typical,
non-step-indexed logical relation. In fact, guarded domain theory goes
further, allowing us to define step-indexed \emph{denotational
semantics} not just step-indexed relations, just as easily as
constructing an ordinary set-theoretic semantics.

In this paper, we develop an adequate denotational semantics that
satisfies graduality and soundness of the equational theory of cast
calculi using the techniques of SGDT.  Our longer-term goal is to
mechanize these proofs in a reusable way in the Guarded Cubical Agda
proof assistant, thereby providing a framework to use to more easily
and conveniently prove that existing languages satisfy graduality and
have sound equational theories. Moreover, the aim is for designers of
new languages to utilize the framework to facilitate the design of new
provably-correct gradually-typed languages with more complex features.

\subsection{Contributions}

The main contribution of this work is a categorical and denotational
semantics for gradually typed langauges that models not just the term
language but the graduality property as well.
\begin{enumerate}
\item First, we give a simple abstract categorical model of GTT using CBPV double categories.
\item Next, we modify this semantics to develop reflexive graph- and
  double categorical models that abstract over the details of
  step-indexed models, and provide a method for constructing such models.
\item We instantiate the abstract construction to provide a concrete
  semantics in informal guarded type theory.
\item We prove that the resulting denotational model is
  \emph{adequate} for the graduality property: a closed term precision
  $M \ltdyn N : \nat$ has the expected semantics, that $M$ errors or
  $M$ and $N$ have the same extensional behavior.
\end{enumerate}

%% \subsection{Outline of Remainder of Paper}

%% \max{this is entirely out of date, update later}

%% % In Section \ref{sec:overview}, we give an overview of the gradually-typed lambda
%% % calculus and the graduality theorem.
%% %
%% In Section \ref{sec:technical-background}, we provide technical background on synthetic guarded domain theory.
%% % 
%% In Section \ref{sec:gtlc-terms}, we formally introduce the gradually-typed cast calculus
%% for which we will prove graduality. We give a semantics to the terms using
%% synthetic guarded domain theory.
%% % Important here are the notions of syntactic
%% % type precision and term precision. For reasons we describe below, we
%% % introduce two related calculi, one in which the stepping behavior of terms is
%% % implicit (an \emph{extensional} calculus, $\extlc$), and another where this behavior
%% % is made explicit (an \emph{intensional} calculus, $\intlc$).
%% %

%% In Section \ref{sec:gtlc-precision}, we define the term precision ordering for
%% the gradually-typed lambda calculus and describe our approach to assigning a
%% denotational semantics to this ordering.
%% This approach builds on the semantics constructed in the previous section,
%% but extending it to the term ordering presents new challenges.


%% % In Section \ref{sec:domain-theory}, we define several fundamental constructions
%% % internal to SGDT that will be needed when we give a denotational semantics to
%% % the gradual lambda calculus.
%% %This includes the Lift monad, predomains and error domains.
%% %
%% % In Section \ref{sec:semantics}, we define the denotational semantics for the
%% % intensional gradually-typed lambda calculus using the domain theoretic
%% % constructions defined in the previous section.
%% %
%% In Section \ref{sec:graduality}, we outline in more detail the proof of graduality for the
%% gradual lambda calculus.
%% %
%% In Section \ref{sec:discussion}, we discuss the benefits and drawbacks to our approach in comparison
%% to the traditional step-indexing approach, as well as possibilities for future work.

%% \subsection{Overview of Results}\label{sec:overview}

%% % This section used to be part of the intro.
%% % \subsection{Proving Graduality in SGDT}
%% % TODO This section should probably be moved to after the relevant background has been introduced?

%% % TODO introduce the idea of cast calculus and explicit casts?

%% In this paper, we will utilize SGDT techniques to prove graduality for a particularly
%% simple gradually-typed cast calculus, the gradually-typed lambda calculus.
%% Before stating the graduality theorem, we introduce some definitions related to gradual typing.

%% % Cast calculi
%% % TODO move this to earlier?
%% Gradually typed languages are generally elaborated to a \emph{cast calculus}, in which run-time type checking
%% that is made explicit. Elaboration inserts \emph{type casts} at the boundaries between static and dynamic code.
%% In particular, cast insertion happens at the elimination forms of the language (e.g., pattern matching, field reference, etc.).
%% The original gradually typed language that is elaborated to a cast calculus is called the \emph{surface language}.

%% % Up and down casts
%% In a cast calculus, there is a relation $\ltdyn$ on types such that $A \ltdyn B$ means that
%% $A$ is a \emph{more precise} type than $B$.
%% There a distinguished type $\dyn$, the \emph{dynamic type}, with the property that $A \ltdyn\, \dyn$ for all $A$.
%% The parts of the code that are dynamically typed will be given type $\dyn$ in the cast calculus.
%% %
%% If $A \ltdyn B$, a term $M$ of type $A$ may be \emph{up}casted to $B$, written $\up A B M$,
%% and a term $N$ of type $B$ may be \emph{down}casted to $A$, written $\dn A B N$.
%% Upcasts always succeed, while downcasts may fail at runtime, resulting in a type error.
%% Cast calculi have a term $\mho$ representing a run-time type error for any type $A$.

%% % Syntactic term precision
%% We also have a notion of \emph{syntactic term precision}.
%% If $A \ltdyn B$, and $M$ and $N$ are terms of type $A$ and $B$ respectively, we write
%% $M \ltdyn N : A \ltdyn B$ to mean that
%% $M$ is ``syntactically more precise'' than $N$, or equivalently, $N$ is 
%% ``more dynamic'' than $M$. Intuitively, this models the situation where $M$ and $N$
%% behave the same except that $M$ may error more.
%% Term precision is defined by a set of axioms that capture this intuitive notion.
%% The specific rules for term precision depend on the specifics of the language, but
%% many of the rules can be derived from the typing rules in a straightforward way.
%% % Cast calculi also have a term $\mho$ representing a run-time type error for any type $A$,
%% % and since
%% Since $\mho$ always errors, there is a term precision rule stating that $\mho \ltdyn M$ for all $M$.

%% % GTLC
%% The gradually-typed lambda calculus is the usual simply-typed lambda calculus with a dynamic
%% type $\dyn$ such that $A \ltdyn\, \dyn$ for all types $A$, as well as upcasts and downcasts
%% between any types $A$ and $B$ such that $A \ltdyn B$. The complete definition will be provided in
%% Section \ref{sec:gtlc-precision}.

%% With these definitions, we can state the graduality theorem for the gradually-typed lambda calculus.

%% % \begin{theorem}[Graduality]
%% %   If $M \ltdyn N : \nat$, then either:
%% %   \begin{enumerate}
%% %     \item $M = \mho$
%% %     \item $M = N = \zro$
%% %     \item $M = N = \suc n$ for some $n$
%% %     \item $M$ and $N$ diverge
%% %   \end{enumerate}
%% % \end{theorem}

%% \begin{theorem}[Graduality]
%%   Let $\cdot \vdash M \ltdyn N : \nat$. 
%%   If $M \Downarrow v_?$ and $N \Downarrow v'_?$, then either $v_? = \mho$, or $v_? = v'_?$.
%% \end{theorem}

%% Note:
%% \begin{itemize}

%%   \item $\cdot \Downarrow$ is a relation between terms that is defined such that $M \Downarrow$ means
%%   that $M$ terminates, either with a run-time error or a value $n$ of type $\nat$.

%%   \item $v_?$ is shorthand for the syntactic representation of a term that is either equal to
%%   $\mho$, or equal to the syntactic representation of a value $n$ of type $\nat$.
%% \end{itemize}

%% % We also should be able to show that $\mho$, $\zro$, and $\suc\, N$ are not equal.

%% To prove graduality and validate the equational theory, we construct a model of the types
%% and terms and show that all of the axioms for term precision and for equality of terms
%% hold in this model. Modeling the dynamic type presents a challenge in the presence of a
%% language with functions: we want the dynamic type to represent a sum of all possible types
%% in the language, so we write down an recursive equation that the semantic object modeling
%% dynamic type should satisfy. When the language includes function types, this equation involves a
%% negative occurrence of the variable for which we are solving, and so the equation 
%% does not have inductive or coinductive solutions.
%% %
%% To model the dynamic type, we therefore use guarded recursion to define a suitable
%% semantic object that satisfies the unfolding isomorphism expected of the dynamic type.
%% The key is that we do not actually get an exact solution to the equation in the style
%% of traditional domain theory; rather, we get a ``guarded'' solution that holds ``up to a time step''.
%% %
%% That is, we introduce a notion of ``time'' and in the equation for the dynamic type,
%% we guard the negative occurrences of the variable by a special operator that
%% specifies that its argument is available ``later''.
%% %This can be seen as a logic that internalizes the notion of step-indexing.
%% See Section \ref{sec:technical-background} for more details on guarded type theory.

%% At a high level, the key parts of our proof are as follows:

%% % TODO revise this
%% \begin{itemize}
%%   \item Our first step toward proving graduality is to formulate a \emph{step-sensitive},
%%   or \emph{intensional}, gradual lambda calculus, which we call $\intlc$, in which the
%%   computation steps taken by a term are made explicit.
%%   The ``normal'' gradual lambda calculus for which we want to prove graduality will be called the
%%   \emph{surface}, \emph{step-insensitive}, or \emph{extensional}, gradual lambda calculus,
%%   denoted $\extlc$.

%%   \item We define a translation from the surface syntax to the intensional syntax, and
%%   prove a theorem relating the term precision in the surface to term precision in the
%%   intensional syntax.
  
%%   \item We define a semantics for the intensional syntax in guarded type theory, for both the
%%   terms and for the term precision ordering $\ltdyn$.

%% \end{itemize}