And the equational laws of a monad can be proven using L\"ob
induction.
\end{definition}
This can be seen as simply a composition of two monads using a
distributive law: the error monad and the recursive lift monad.
%
However, we present them as one combined monad because in gradual
typing we are interested in a specific ordering relation called the
\emph{error ordering} where $\err$ is the least element. This is
\emph{not} the composition of the lift and error monad, which would
instead have the error as an isolated, maximal element.
We can define this error ordering as a variation on the weak
simulation relations of prior work:
\begin{definition}
Let $X$ be a type and $\sqsubseteq_X$ a binary relation. We define
$\ltdynp{\errlift X} : \errlift X \to\errlift X \to\prop$ as follows:
\begin{align*}
\err\ltdynlift X d &= \top\\
\eta x \ltdynlift X \eta y &= x \ltdynp X y\\
\eta x \ltdynlift X \err&= \bot\\
\eta x \ltdynlift X \theta t &= \exists{n:\mathbb N}.\exists{y: X}. \theta t = \delta^n (\eta y) \wedge x \ltdynp X y\\
\theta s \ltdynlift X \eta y &= \exists{n:\mathbb N}.(\theta s = \delta^n \err)\vee(\exists{y: X}. \theta t = \delta^n (\eta y) \wedge x \ltdynp X y)\\
\theta s \ltdynlift X \err&= \exists{n:\mathbb N}.\theta s = \delta^n \err\\
\theta s \ltdynlift X \theta t &= \later[l \leftarrow s,r\leftarrow t] s \ltdynlift X t
\end{align*}
\end{definition}
\begin{lemma}
When $\ltdynp X$ is reflexive, so is $\ltdynlift X$.
\end{lemma}
\begin{proof}
By L\"ob induction on the proposition $\forall d: \errlift X. d
\ltdynlift X d$. Error and return cases are immediate. We need to
show
\[\theta t \ltdynlift X \theta t =\later[l \leftarrow t,r\leftarrow t] l \ltdynlift X r =\later[l \leftarrow t] l \ltdynlift X l \]
The inductive hypothesis $h : \later(\forall d: \errlift X. d \ltdynlift X d)$
We can then conclude
\[\text{next}[f \leftarrow h, l \leftarrow t]. h l \]
\end{proof}
Unfortunately, transitivity is not preserved.
%
The problematic case is of the form $\theta s \ltdynlift X \theta t
\ltdynlift X \eta z$. In this case we know $\theta t =\delta^n (\eta
y)$ but we cannot conclude that $\theta s$ must eventually terminate!
In fact this is false in the semantics because it might be that
$\theta s$ is only related to $\theta t$ because we ran out of fuel,
and actually $s$ is a diverging computation.
However, this should support transitive reasoning \emph{in the limit},
i.e., if the equivalence holds for \emph{all} levels of approximation
then eventually if $\theta t$ terminates, at high enough level of
approximation it will no longer be related to the diverging
computation.
%
This reasoning \emph{in the limit} is accomplished analytically by
quantification over all steps.
%
Here we accomplish it by using \emph{clocks} and \emph{clock
quantification}.
%
That is rather than a denotation of a syntactic type being a type it
will be given by a ``clocked'' type:
\begin{definition}
A \emph{clocked} type $X$ is an element of $K \to U$.
We call $\forall k:K. X k$, the \emph{limit} of $X$.
\end{definition}
Note that, similar to the interval in cubical type theory, $K$ is not
a type, but only a ``pseudo-type'' that we can quantify over in the
type $\Pi_{k:K} B$.
%
Next, we need a ``clocked'' error ordering associated to every type.
%
This will be assumed to be reflexive at each level of approximation,
but only transitive in the limit.
\begin{definition}
A \emph{clocked} preorder on a clocked type $X : K \to U$ is a
clocked relation $\kltp{} X : \forall k. X_k \to X_k \to\prop$ satisfying
\begin{enumerate}
\item Clocked Reflexivity $\forall k. \prod_{x:X_k} x \kltp k X x$
\item Transitivity in the limit $\prod_{x,y,z:\forall k. X_k} x \kltp\omega X y \to y \kltp\omega X z \to x \kltp\omega X z$
\end{enumerate}
Where
\[ x \kltp\omega X y =\forall k. x_k \kltp k X y_k \]
A \emph{monotone function} is a function $f : \forall k. X_0 k \to
Y_0 k$ satisfying monotonicity:
\[\forall k.\prod_{x,x':X_0^k} x \kltp k X x' \to f_k x \kltp k Y f_k x' \]
\end{definition}
For any clocked preorder we can construct the delayed preorder by
\begin{definition}
Define $\later : K \to(K \to U)\to(K \to U)$ by
\[(\later X)^k =\later^k X^k \]
and on preorders by:
\begin{align*}
x \kltp k {\later X} y &= \later^k[l\leftarrow x, r\leftarrow y].~l \kltp k {X} r
\end{align*}
\end{definition}
Then we can define our semantic notions
\begin{definition}
An \emph{error predomain}$X$ consists of
\begin{enumerate}
\item A clocked type $X_0$
\item A clocked preorder $\kltp{} X$ on $X_0$
\end{enumerate}
A morphism of error predomains is a monotone function.
An \emph{error domain} is an error predomain $X$ with
\begin{enumerate}
\item A least element $\kerrp{} X : \forall k. X$, i.e., it
satisfies $\forall k. \prod_{x:X_k}\kerrp k X \kltp k X x$.
\item A monotone ``thunk'' function $\theta_X : \later X \to X$
\end{enumerate}
A morphism of error domains is a morphism of the underlying error
predomains.
A \emph{linear} morphism of error domains $S : X \multimap Y$ is a
Finally we can return to our original goal of defining the monad for our semantics!
%
\begin{lemma}
next and $\delta$ are monotone
\end{lemma}
\begin{definition}
Let $X$ be an error predomain a binary relation. We define the error
domain $\errlift X$ as
TODO: put the ks in the right spots
\begin{enumerate}
\item$(\errlift X)_0^k =\mu L. X_0^k +1+\later^k L$
\item Ordering defined by cases:
\begin{align*}
\err\kltp k {\errlift X} d &= \top\\
\eta x \kltp k {\errlift X}\eta y &= x \ltdynp X y\\
\eta x \kltp k {\errlift X}\err&= \bot\\
\eta x \kltp k {\errlift X}\theta t &= \exists{n:\mathbb N}.\exists{y: X}. \theta t = \delta^n (\eta y) \wedge x \ltdynp X y\\
\theta s \kltp k {\errlift X}\eta y &= \exists{n:\mathbb N}.(\theta s = \delta^n \err)\vee(\exists{y: X}. \theta t = \delta^n (\eta y) \wedge x \ltdynp X y)\\
\theta s \kltp k {\errlift X}\err&= \exists{n:\mathbb N}.\theta s = \delta^n \err\\
\theta s \kltp k {\errlift X}\theta t &= \later[l \leftarrow s,r\leftarrow t] s \kltp k {\errlift X} t
\end{align*}
\item reflexive: as above
\item TODO: transitive in the limit
\item TODO: strong monad
\end{enumerate}
\end{definition}
\begin{lemma}
$\errlift X$ is the free error domain on $X$, i.e., it is left
adjoint to the forgetful functor from the category of error domains
and linear maps to the category of predomains.
\end{lemma}
\begin{lemma}
The adjunction is monadic: error domains are precisely algebras of
the free error domain. Is this true?
\end{lemma}
\section{Lazy Semantics}
To define a semantics for lazy gradually typed language, we first need
to define our \emph{universal} error domain. Unless we add in features
like pattern matching on the dynamic type, there is some freedom in
this choice. We present two natural solutions:
The first is a classic-looking dynamic type: the lift of the sum of
the base type and the function type. A notable difference are the
