\section{Discussion}

\subsection{Related Work}
% Discuss Joey Eremondi's thesis on gradual dependent types
Eremondi \cite{Eremondi_2023} uses guarded type theory to
define a syntactic model for a gradually-typed source
language with dependent types. By working in guarded type theory, they are
able to give an exact semantics to non-terminating computations in a language
which is logically consistent, allowing for metatheoretic results about the
source language to be proven.
%
Similarly to our approach, they define a guarded lift monad to model potentially-
nonterminating computations and use guarded recursion to model the dynamic type.
However, they do not give a denotational semantics to term precision and it is unclear
how to prove the gradual guarantee in this setting.
The work includes a formalization of the syntactic model in Guarded Cubical Agda.

% Discuss Jeremy Siek's work on graduality in Agda
Siek and Chen \cite{siek-chen2021} give a proof in Agda of graduality
for an operational semantics. While they do not use the Guarded
Cubical extension, they do use a guarded logic of propositions
shallowly embedded in Agda. Our denotational approach requires full
guarded type theory not just guarded logic. An advantage of the
denotational approach is that it easily validates equational
reasoning, not just graduality, and it is completely independent of
any particular syntax of gradual typing.

\subsection{Mechanization}
% Discuss Guarded Cubical Agda and mechanization efforts
In parallel with developing the theory discussed in this paper,
we are mechanizing our results and developing a reusable framework
for proving graduality in Guarded Cubical Agda \cite{veltri-vezzosi2020}.
%
As of this writing, the work is in progress, but we have
constructed most parts of the concrete model discussed in
Section \ref{sec:concrete-model}. For instance, we have defined
types for predomains, error domains, and their morphisms and relations,
and we used the guarded features to define the guarded lift + error monad
and the dynamic type.

We plan to formalize the construction of perturbations and 
quasi-representable relations, but we have yet to decide
whether to follow the approach we take in this work and define
the abstract notion of intensional model and formalize the constructions in that setting,
and then apply those abstract constructions to the concrete model.
Alternatively, it may be better from a mechanization standpoint
to carry out those abstract constructions explicitly in the concrete model,
i.e., our representation of objects in the concrete model of predomains
would include a field for the perturbations and our notion of relations
would include fields for the push-pull property and quasi-representability.
We leave this investigation to future work.

Lastly, we plan to formalize the adequacy result discussed in
Section \ref{sec:adequacy}. This will involve adding axioms about
clock quantification as well as about the clock-irrelevance of
booleans and natural numbers, since as of this writing these
axioms are not built-in to Guarded Cubical Agda. As an experiment, we have 
formalized some basic results involving clocks as part of our development.

\begin{comment}
% prove graduality in the syntax of 
% GTLC, which involves the construction of the abstract model described in 
% \ref{sec:concrete-model} and the extensional model with external dynamic 
% type. We also plan to formalize the adequacy result in \ref{sec:appendix-adequacy}.

% step-2 
Then we plan to construct the step-2 intensional model. Besides all the 
data in step-1, we need to include perturbations, functors $\times$, $\arr$, $U$, and $F$ that preserve 
perturbations and push/pull properties for all morphisms on value and 
computation types. Notice that for any object $A$ which has value type, 
we will take not only the monoid of perturbations $P^V_A$ and the monoid 
homomorphism $\ptbv_A : \pv_A \to \vf(A,A)$ on itself, but also $P^C_{F A}
$ and $\ptbe_{F A} : \pe_{F A} \to \ef(F A,F A)$ on $F A$, which have 
computation types. Similarly, for any computation object $B$, we will 
construct the perturbations on $U B$ besides the monoid $P^C_B$ and 
monoid homomorphism $\ptbe_B : \pe_B \to \ef(B,B)$. Also, for functors 
that preserves perturbations, we need to include the ones in the context 
of Kleisli category. For this part, we need to define the perturbation on 
not only the objects itself, but also the global lift and delay of objects, 
which requires us to provide each piece of supporting constructor. This step 
and futher steps towards to the model construction are still 
work-in-progress, but once it's finished, we will provide a complete 
framework which takes formalization on an explicit type and obtains an 
extensional model.

% step-3
In the step-3 intensional model, we will enhance it with 
quasi-representability. For any value relation $c : A \rel A'$, we need 
to show that there exists a left-representation structure for $c$ and a 
right-representation structure for $F\ c$. Correspondingly, for any 
computation relation $d : B \rel B'$, we will show there exists a 
right-representation structure for $d$ and a left-representation 
structure for $U\ d$. As we define the quasi-representability for value 
and computation relation, we will construct the quasi-representability on 
the function and product of the relation, which makes it necessary to 
have the dual version of quasi-representability.

% step-4 construct a concrete dynamic type and apply it to the abstract model
After defining the abstract model and its interface, we will model GTLC 
by providing explicit construction triples of dynamic type at each step, 
which includes defining Dyn as a predomain, its pure and Kleisli 
perturbation monoids, push/pull property for pure and Kleisli 
perturbation, as well as quasi-representability. The 
quasi-representability involves explicit rules which show that Nat is 
more precise than Dyn (Inj-Nat) and Dyn $\to$ Dyn is more precise than 
Dyn (Inj-Arr). Currently, we have formalized the concrete construction of 
Dyn in Cubical Agda and it was more challenging than expected because we 
define Dyn using the technique of guarded recursion and fixed point, which 
means that every time we analyze the case inside of Dyn, we need to unfold 
it and add corresponding proof. 

% adequacy
Besides the abstract model and its concrete construction on dynamic type, 
we will also formalize the adequacy result in \ref{sec:appendix-adequacy}, 
which involves clock quantification of the lift monad, the weak bisim 
relation, and the lock-step error ordering. In order to prove adequacy, 
we will first prove that the global lift of X is isomorphic to Delay(1 + X)
whether X is clock-irrelevant or not. Then, we aim to prove the equivalence 
between the global lock-step error ordering and the error ordering observed 
in Delay(1 + X) and equivalence between the global weak bisimilarity 
relation and the weak bisimilarity relation on Delay(1 + X). We have 
finished some prerequisite proofs on clock quantification and postulated 
some theorems on clock globalization.
\end{comment}

\subsection{Comparison to Explicit Step-Indexing}

Working internally to guarded type theory reduces the overhead of
needing to carry around the step-indices in the proofs as is required
when using explicit step-indexing. Additionally, the logical relations
constructed to prove graduality in prior work \cite{new-ahmed2018,new-licata-ahmed2019,new-giovannini-licata-2022} suffer
from technical complications of requiring two separate expression
relations, one that counts steps on the left and the other on the
right, and there is no analogue of this in our approach. However,
using two expression relations allows some but not all transitivite
reasoning of term precision to be recovered. In the future we aim to
explore if this approach is feasible in guarded semantics.

\subsection{Synthetic Ordering}
A key to managing the complexity of our concrete construction is in
using a \emph{synthetic} approach to step-indexing rather than working
analytically with presheaves. This has helped immensely in our ongoing
mechanization in cubical Agda as it sidesteps the need to formalize
these constructions internally. 
%
However, there are other aspects of the model, the bisimilarity and
the monotonicity, which are treated analytically and are similarly
tedious.
%
It may be possible to utilize further synthetic techniques to reduce
this burden as well, and have all type intrinsically carry a notion of
bisimilarity and ordering relation, and all constructions to
automatically preserve them.
%
A synthetic approach to ordering is common in (non-guarded) synthetic
domain theory and has also been used for synthetic reasoning for cost
models \cite{fiore_1997,GrodinNSH24}.

\subsection{Future Work}

In the future, we plan to apply our approach to give a denotational
semantics for languages that feature higher-order state or
runtime-extensible dynamic typing
\cite{DBLP:journals/corr/abs-2210-02169} as well as richer type
disciplines such as gradual dependent types and effect systems.

%% to gradually-typed
%% languages with algebraic effects, building on prior work on gradual typing for effect handlers
%% \cite{greff}. In particular, that work proves graduality via a complicated step-indexed logical relation,
%% and we hope to prove their results by building a denotational model for GrEff.
%% This would serve as a step towards applying our techniques to prove graduality for languages
%% with other advanced features.

%% The extensional model we construct differs from the usual notion of extensional
%% model considered in prior work on gradual typing in that it lacks horizontal composition of squares.
%% We would like to clarify the relationship between our notion of model and prior extensional models,
%% with the aim of determining whether our approach could allow for the construction of such a model.