gtlc.tex

\documentclass{article}

\usepackage{amssymb}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{tikz-cd}
\usepackage{mathpartir}
\usepackage{stmaryrd}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{nonnum-theorem}{Theorem}[section]
\newtheorem{corollary}{Corollary}[section]
\newtheorem{definition}{Definition}[section]
\newtheorem{lemma}{Lemma}[section]

\newcommand{\bool}{2}
\newcommand{\dyn}{\text{Dyn}}
\newcommand{\dynv}{\text{Dyn}^+}
\newcommand{\dync}{\text{Dyn}^-}
\newcommand{\good}[1]{\text{good}_{#1}}
\newcommand{\prop}{\mathbb P}
\newcommand{\smallU}{\mathbb U}
\newcommand{\bigU}{\mathbb V}
\newcommand{\with}{\mathrel{\&}}
\newcommand{\eqv}{\simeq}
\newcommand{\soln}{\text{Sol}}
\newcommand{\police}[1]{\text{police}_{#1}}
\newcommand{\later}{{\blacktriangleright}}
\newcommand{\errp}[1]{\mho_{#1}}
\newcommand{\kerrp}[2]{\mho^{#1}_{#2}}
\newcommand{\err}{\mho}
\newcommand{\errlift}{L_\err}
\newcommand{\ostar}{\circledast}

\newcommand{\ltdynp}[1]{\mathrel{\sqsubseteq_{#1}}}
\newcommand{\ltdynlift}[1]{\mathrel{\sqsubseteq_{\errlift#1}}}
\newcommand{\ltprecp}[1]{\mathrel{\sqsubseteq^{\prec}_{\errlift #1}}}
\newcommand{\ltsuccp}[1]{\mathrel{\sqsubseteq^{\succ}_{#1}}}

\newcommand{\kltp}[2]{\mathrel{\sqsubseteq^{#1}_{#2}}}

\newcommand{\ltgt}[1]{\mathbin{\langle\mspace{-1mu}#1\mspace{-1mu}\rangle}}
\newcommand{\fmap}{\ltgt{\$}}
\newcommand{\monto}{\mathrel{\to_{m}}}
\newcommand{\predom}{\text{$\mho$PreDom}}
\newcommand{\dom}{\text{Dom}}
\newcommand{\linto}{\multimap}
\newcommand{\Next}{\text{next}}
\newcommand{\thinkp}[1]{\theta_{#1}}

\begin{document}

\title{Semantics of Gradual Types in SGDT}
\author{Max S. New}

\maketitle

\section{Goals}

We want to define a denotational semantics for the core language of
GTLC and prove graduality.
%
For lazy gradual typing, based on New and Licata, we need to construct
a vertically thin cartesian closed pro-arrow equipment with a greatest
type, least element of each hom set and a weak boolean type.

New and Licata used a denotational semantics based on classical
analytic domain theory to construct such models. Here we will use
\emph{synthetic guarded domain theory} to sidestep any side-conditions
on constructing solutions to domain equations. We work internal to a
model of multi-clock synthetic guarded domain theory. We use two
universes $\mathbb U \leq \mathbb V$.

For gradual typing we need to develop a notion of domain that includes
an \emph{error ordering} with respect to which all constructions in
the language are monotone and and the errors and gradual type casts
are characterized by universal properties. We also need to construct
in each model a \emph{universal} (pre-)domain to interpret the
``dynamic'' type.

For instance, for a CBN gradual language with functions and booleans a
suitable domain can be constructed as:
\[ \dync \cong \errlift \bool \times (\later \dync \monto \later \dync) \]
where $\errlift$ is an appropriate combination of the error and lift
monads, $\later$ provides the necessary guarding and $\monto$ is the
set of \emph{monotone} functions.  A CBV gradual language with
functions and booleans could instead use
\[ \dynv \cong \bool + (\later \dynv \monto \errlift(\later\dynv))\]

\section{Error predomains and domains}

We start by defining our notion of predomain and domain and showing
how to solve recursive domain equations.
%
All of the constructions (later, fix, etc) in this section are
parameterized by an arbitrary clock variable $k : K$, but to avoid
clutter we leave it implicit.

Our notion of predomain is simply that of a (constructive)
\emph{preorder}, and our notion of domain is a predomain with a least
element.
\begin{definition}
  An error predomain $X$ consists of
  \begin{enumerate}
  \item A type $X_0 : \smallU$
  \item An order ``relation'' $\ltdynp X : X_0 \to X_0 \to \smallU$
  \item Satisfying reflexivity, i.e., $x \ltdynp X x$ for every $x$.
  \item And transitivity, if $x \ltdynp X y$ and $y \ltdynp X z$ then
    $x \ltdynp X z$.
  \end{enumerate}
  We write the universe of predomains as $\predom : \bigU$.

  A monotone function $f : X \to Y$ between error predomains consists
  of
  \begin{enumerate}
  \item A function on the underlying sets $f_0 : X_0 \to Y_0$
  \item That preserves the ordering: $f_1 : (x \ltdynp X x') \to (f_0x \ltdynp X f_0 x')$
  \end{enumerate}

  We write the type of monotone functions from $X$ to $Y$ as $X \monto Y : \smallU$
  Furthermore, the type of monotone functions can be extended to a
  predomain with pointwise ordering. We abusively also write $X \monto
  Y : \predom$
\end{definition}

Strangely enough for our purposes it is important that the preorder is
not in a proof-irrelevant universe, but we do not seem to care about
the equality of ordering proofs. So we seem to have a weird
intermediate point between proper preorders and categories where there
might be many different proofs but we impose no ``laws'' on the
manipulation of these proofs. Michael Arntzenius calls these ``lawless
categories''.

Next, to solve recursive domain equations, we need to prove that the
universe of error predomains is a domain in the sense of guarded
domain theory that there is a $\later$-algebra $\theta : \later
\predom \to \predom$

\begin{definition}
  Given $X^\later : \later \predom$, define a predomain $\later X^\later$ as
  follows:
  \begin{enumerate}
  \item $(\later X^\later)_0 = \later[X \leftarrow X^\later] X_0$
  \item $x^\later \ltdynp {\later X^\later} y^\later = \later[X \leftarrow X^\later, x \leftarrow x^\later, y \leftarrow y^\later] x \ltdynp X y$
  \item Given $x^\later$,
    \begin{align*}
      \later[X \leftarrow X^\later, x \leftarrow x^\later, y \leftarrow x^\later] x \ltdynp X y
      &\equiv \later[X \leftarrow X^\later, x \leftarrow x^\later] x \ltdynp X x
    \end{align*}
    Which we can prove as
    \[ \Next[X \leftarrow X^\later, x \leftarrow x^\later] \text{refl}_X x\]
    or in applicative style
    \[ \Next\,\text{refl} \ostar X^\later \ostar x^\later \]
  \item Given $p_{xy}^\later : x^\later \ltdynp {\later X^\later} y^\later$ and
    $p_{yz}^\later : y^\later \ltdynp {\later X^\later} z^\later$, we need to show
    \begin{align*}
      \later[X \leftarrow X^\later, x \leftarrow x^\later, z \leftarrow z^\later] x \ltdynp X z
      &\equiv \later[X \leftarrow X^\later, x \leftarrow x^\later,y\leftarrow y^\later, z \leftarrow z^\later] x \ltdynp X z
    \end{align*}
    Which we prove as
    \[ \Next[X \leftarrow X^\later, x \leftarrow x^\later,y\leftarrow y^\later, z \leftarrow z^\later,p_{xy}\leftarrow p_{xy}^\later, p_{yz}\leftarrow p_{yz}^\later] \text{trans}_X p_{xy} p_{yz} \]
    or in applicative style
    \[ \Next\,\text{trans} \ostar X^\later \ostar x^\later\ostar y^\later\ostar z^\later \ostar p_{xy}^\later \ostar p_{yz}^\later \]
  \end{enumerate}
\end{definition}
When $X : \predom$, we will write $\later X$ for $\later (\Next\,X)$

We can then define our notion of \emph{error domain} as error
predomains that have a suitable notion of error and have a
\emph{monotone} $\later$-algebra.
\begin{definition}
  An error domain $X$ is an error predomain with furthermore
  \begin{enumerate}
  \item An element $\errp X : X_0$ that is the least element $\errp X \ltdynp X x$
  \item A monotone function $\thinkp X : \later X \to X$
  \end{enumerate}
  We write the universe of error domains as $\dom : \bigU$ and we will
  (usually?) suppress the obvious coercion $U : \dom \to \predom$

  When $X$ is an error predomain and $Y$ is an error domain, $X \monto
  Y$ is an error domain with
  \begin{enumerate}
  \item $\errp {X \monto Y} = \lambda x. \errp Y$
  \item $\thinkp {X \monto Y} f = \lambda x. \thinkp Y (f \ostar (\Next\, x)) $
  \end{enumerate}
\end{definition}

And finally we can define the error-lift monad, which defines the free
error domain from an error predomain.
\begin{definition}
  Given any predomain $X : \predom$, we define the error lift $\errlift X$ as follows

  \begin{enumerate}
  \item First, $(\errlift X)_0$ is defined as the solution to the
    guarded domain equation:
    \[ (\errlift X)_0 \cong (X_0 + 1 + \later (\errlift X)_0) \]

    We label the three injections as follows:
    \begin{align*}
      \eta &: X \to \errlift X\\
      \err &: \errlift X\\
      \theta &: \later \errlift X \to \errlift X
    \end{align*}

  \item We define the order relation, $\ltdynp {\errlift X}$ as the
    transitive closure of $\wr$, which is defined as:

    \begin{align*}
      \err \wr r &= 1\\
      (\eta x) \wr (\eta y) &= x \ltdynp X y\\
      (\theta s) \wr (\theta t) &= (\Next\; \wr) \ostar s \ostar t\\
      (\eta x) \wr (\theta t) &= \Sigma_{n:\mathbb N}\Sigma_{y:X_0} (\theta t = \delta^n (\eta y)) \times (x \ltdynp X y)\\
      (\theta s) \wr (\eta y) &= \Sigma_{n:\mathbb N}\Sigma_{x:X_0} (\theta s = \delta^n (\eta x)) \times (x \ltdynp X y)\\
    \end{align*}
  \end{enumerate}
  
  Define the error-lift type as a solution to the guarded recursive
  domain equation:


  This carries the structure of a strong monad, with $\eta$ as the
  unit and the join defined by L\"ob induction as follows:
  \begin{align*}
    \mu(\eta x) &= x\\
    \mu(\mho) &= \mho\\
    \mu(\theta(u)) &= \theta (\mu^\later \ostar u)
  \end{align*}
  With map (implying strength) defined as
  \begin{align*}
    \errlift f(\eta x) &= f x\\
    \errlift f(\mho) &= \mho\\
    \errlift f(\theta(u)) &= \theta ((\errlift f)^\later \ostar u)
  \end{align*}
  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
  morphism of error domains additionally satisfying
  \begin{enumerate}
  \item Error preservation $S^k \err^k_X = \err^k_Y$
  \item Thunk preservation $S^k (\theta^k_X x) = \theta^k_Y (S^k \fmap x)$
  \end{enumerate}
\end{definition}

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
guarded recursive uses.
\[ \dyn_+ \cong \errlift (2 + (\later \dyn_+ \monto \later \dyn_+)) \]
The second is slightly closer to untyped lambda calculus: we take a
product rather than a sum, and only need to lift the base type itself.
\[ \dyn_- \cong \errlift 2 \times (\later \dyn_- \monto \later \dyn_-) \]
The idea here is that any dynamically typed term can be safely applied
to any number of arguments and at some point ``projected'' to return a
boolean, which will actually cause computation to occur as indicated
by the $\errlift$.

To construct these domains we need to be able to solve recursive
domain equations \emph{of error domains}. To do this we simply need to
show that the universe of error predomains is a predomain.

%% \begin{definition}
%%   Define $\theta_{\predom} : \later \predom \to \predom$ as follows
%%   \begin{align*}
%%     \theta_{\predom}P &= (\later[(X,\ltdynp X) \leftarrow P] X, )
%%   \end{align*}
%% \end{definition}


\end{document}