chapter04.tex

\chapter{Quantitative Type Theory}\label{cha:qtt}

\coloredlettrine{T}{ype systems} in the~previous two chapters have used
variables for two distinct purposes: either a~variable has been used for
formation of types during type checking, for example, the~term $\Int \times x$
depends on $x$ to form a~valid type, but was not available at runtime of
the~program; or, in the~linear type system, as a~resource that is consumed
during the~program runtime.

The~linear type system in the~previous chapter tracks the~distinction between
variable purposes by separating the~context into two parts, intuitionistic and
linear,
\[
  x_1 \is{} S_1, \dotsc, x_n \is{} S_n \mid y_1 \is{} T_1, \dotsc, y_m \is{} T_m
    \vdash M \is{} U.
\]
The~unrestricted variables $x_i$ may be used zero, one, or more times.
The~linear variables $y_i$, however, must be used exactly once. Type systems
that adhere to the~linear logic interpretation, which equates resource usage
with the~presence of a~variable in (the~second part of) a~context, are
restricted in what kinds of \emph{use} they can express: either variable is used
or it is not.

Another kind of restriction is that our formulation of the~linear type system
does not integrate dependent types. Although we have mentioned systems that
combine the~two, they do so by allowing the~linear variable types to dependent
on intuitionistic variables. This solution, however, would still not allow us to
formulate types that depend on linear variables.

Type system in this chapter removes these two restrictions. The~context does not
get separated into two parts, instead we track how a~variable can be used by
annotating it with an~element of some semiring. Several authors have used
semiring annotations of variables to attach information on how they can be
used~\citep{brunel_et_al_2014, ghica_smith_2014}, but \citet{mcbride_2016} was
first to use the~annotations to indicate whether variables are available for
computation or only available in the~formation of types. The~\lc
\citeauthor{mcbride_2016} uses has only the~dependent function type with its
abstraction and application. \citet{atkey_2018} fixed an~issue in
\citeauthor{mcbride_2016}'s idea and presented it as the~Quantitative Type
Theory (QTT) while also extending the~system with rules for dependent
multiplicative pair type and multiplicative unit type. \citet{weirich_2020}
relaxed some of the~restrictions that \citeauthor{atkey_2018} imposed on
the~system.

This work extends QTT with the~typing rules for the~dependent additive pair type
and the~additive unit.

\sectionwithtoc{Resource semirings}

In quantitative type theory, the~typing judgment takes the~form:
\[
  x_1 \is{\rho_1} S_1, \dotsc, x_n \is{\rho_n} S_n \vdash M \is{\sigma} T,
\]
where the~$\rho_1, \dotsc, \rho_n$ are elements of the~semiring indicating
how the~corresponding variable may be used. The~annotation $\rho_i$ tracks
the~computational usage of a~variable. The~usage $0$ indicates that the~variable
can only be used to form a~type and it has no presence in an~executing program.
The~output is annotated with usage $\sigma$, which is restricted to be either
the~$0$, or the~$1$ of the~semiring due to the~admissibility of
substitution~\citep{atkey_2018}.

\begin{definition}
  A~\emph{semiring} $\mathcal{R}$ is a~set equipped with two binary operations,
  addition ($+$) and multiplication ($\cdot$), and constants $0, 1 \in
  \mathcal{R}$, such that ($\mathcal{R}, +, 0$) is a~commutative monoid, i.e.
  for every $\rho, \pi, \phi \in \mathcal{R}$:
  \begin{align*}
    (\rho+\pi)+\phi = \rho+(\pi+\phi),&  &  &0 + \rho = \rho,&  &
    &\rho + \pi = \pi + \rho;
  \end{align*}
  ($\mathcal{R}, \cdot, 1$) is a~monoid, i.e. for every $\rho, \pi, \phi
  \in \mathcal{R}$:
  \begin{align*}
    (\rho \cdot \pi) \cdot \phi = \rho \cdot (\pi \cdot \phi),&  &
    &1 \cdot \rho = \rho \cdot 1 = \rho;
  \end{align*}
  multiplication left and right distributes over addition, i.e. for every $\rho,
  \pi, \phi \in \mathcal{R}$:
  \begin{align*}
    \rho \cdot (\pi + \phi) = (\rho \cdot \pi) + (\rho \cdot \phi),&  &
    &(\rho + \pi) \cdot \phi = (\rho \cdot \phi) + (\pi \cdot \phi);
  \end{align*}
  and for every $\rho \in \mathcal{R}$:
  \[
    0 \cdot \rho = \rho \cdot 0 = 0.
  \]
\end{definition}
As usual, we omit the~symbol $\cdot$ from notation and write $\rho\pi$ instead
of $\rho\cdot\pi$. For the~use of in annotations, we also require that
the~semiring is \emph{positive}, meaning that $\rho + \pi = 0$ implies that
$\rho = 0$ and $\pi = 0$, and has the~\emph{zero-product} property:
$\rho\pi = 0$ implies $\rho = 0$ or $\pi = 0$. These two properties are required
for the~admissibility of substitution in the~system we will define.

The~properties of semirings make $0$ well suited for identifying the~use in
types. Since adding $0$ to an~existing use, $0 + \rho = \rho$, retains
the~original, we can always combine a~computational usage with a~use in a~type;
and because $0\rho = 0$, nesting an~otherwise computational use within a~type
results in the~whole usage being noncomputational.

Semirings that form type systems with interesting properties include:
\begin{itemize}
  \item the~singleton $\{0\}$, which produces the~intuitionistic type system we
    saw in \autoref{cha:typesystems};
  \item the~semiring $\{0, 1\}$ corresponds to the~linear type system from
    \autoref{cha:linear};
  \item the~zero-one-many semiring $\{0, 1, \omega\}$, where $\rho + \omega =
    \omega$ and $\omega \cdot \omega = \omega$. The~$0$ value restricts
    the~resource usage to types only, $1$ requires linear usage, and $\omega$
    has no usage restrictions.
\end{itemize}
This work is accompanied by an~interpreter that uses the zero-one-many semiring.

\sectionwithtoc{Terms \& contexts}

As with previous systems, we will start with pseudo-contexts and pseudo-terms,
and then we will use the~deduction rules to identify which terms are properly
typed.

\begin{definition}
  Assume that we are given an~infinite sequence of expressions $\mathbf{v}_0,
  \mathbf{v}_1, \mathbf{v}_2, \dots$ called \emph{variables}. The~set of
  \emph{pseudo-terms} is defined inductively: if $x, x', y$ and $z$ are
  variables; $\pi$ is a~semiring element; and $M, N, O, P$ and $Q$ are
  pseudo-terms, then:
  \begin{enumerate}
    \item every variable is a~pseudo-term;
    \item atomic type $\univ$ is a~pseudo-term;
    \item \emph{dependent function} type formation, abstraction, and application
      are pseudo-terms:
      \begin{mathpar}
        \depq x \pi M N \and \lam {x \is\pi M} N \and M \: N
      \end{mathpar}
    \item \emph{dependent multiplicative pair} type formation, its constructor
      and eliminator are pseudo-terms:
      \begin{mathpar}
        (x \is\pi M) \otimes N \and \mpair M N \and
        \letpair {(x'\, \is\pi O) \otimes P} [z] x y M [Q] N
      \end{mathpar}
    \item \emph{multiplicative unit} type, the~unit and its eliminator are
      pseudo-terms:
      \begin{mathpar}
        \1 \and \munit \and \letu [x] M [O] N
      \end{mathpar}
    \item \emph{dependent additive pair} type formation, its constructor and
      eliminators are pseudo-terms:
      \begin{mathpar}
        (x \is{} M) \with N \and \apair M N \and \fst M \and \snd M
      \end{mathpar}
    \item \emph{additive unit} type and the~unit are pseudo-terms:
      \begin{mathpar}
        \top \and \aunit
      \end{mathpar}
  \end{enumerate}
\end{definition}
The~pseudo-terms in this definition are a~straightforward combination of
the~dependently-typed terms in \autoref{def:pseudo-term} and the~two variations
for pair and unit types as distinguished by the~linear types.

The~unit types are denoted as before; in particular, we keep using \1, because
it is the~usual linear logic notation for the~multiplicative unit type. Although
there should be no confusion, note the~difference between a~semiring element,
$1$, and a~multiplicative unit type, \1.

Pseudo-contexts are now sequences of the~form:
\[
  x_1 \is{\rho_1} S_1, \dotsc, x_n \is{\rho_n} S_n,
\]
where $\rho_1, \dotsc, \rho_n$ are arbitrary elements of the~semiring. We define
scaling of pseudo-contexts by a~semiring element and an~addition of
pseudo-contexts:
\begin{definition}
  Given a~pseudo-context $\Gamma$ and a~semiring element $\pi$,
  the~\emph{scaling} $\pi\Gamma$ is defined by:
  \begin{align*}
    \pi (\diamond) = \diamond&  &  &\pi(\Gamma, x \is\rho S) = \pi\Gamma,
    x \is{\pi\rho} S
  \end{align*}
  The~\emph{addition} $\Gamma_1 + \Gamma_2$ is the~pseudo-context that contains
  $x \is\pi S$, if:
  \begin{enumerate}
    \item $x \is{\rho_1} S$ is in $\Gamma_1$ and $x \is{\rho_2} S$ is in
      $\Gamma_2$, and $\pi = \rho_1 + \rho_2$;
    \item $x \is\pi S$ is in $\Gamma_1$, and $x \is\rho T$ is not in $\Gamma_2$;
    \item $x \is\pi S$ is in $\Gamma_2$, and $x \is\rho T$ is not in $\Gamma_1$.
  \end{enumerate}
\end{definition}
The~zeroing $0\Gamma$ sets all the~annotations to $0$, due to the~semiring laws.
We do not define the~addition $\Gamma_1 + \Gamma_2$ if $S \not\equiv T$, for
some $x \is\rho S$ in $\Gamma_1$ and $x \is\pi T$ in $\Gamma_2$.

\sectionwithtoc{Typing rules}

As we have done in the~\nameref{sec:dtlc} section, we formulate mutually
recursive rules that define how are the~well-formed contexts and
well-typed terms derived.

Contexts are identified within pseudo-contexts by the~judgment $\Gamma \vdash$,
defined by the~following rules:
\begin{mathpar}
  \inferrule*[right=Emp]
  { }
  {\diamond \vdash}

  \inferrule*[right=Ext]
  {\Gamma \vdash \\ 0\Gamma \vdash S \is0 \univ}
  {\Gamma, x \is\rho S \vdash}
\end{mathpar}
The~rule \ir{Emp} determines empty pseudo-context as valid. The~rule \ir{Ext}
extends the~context $\Gamma$ with a~new variable $x$ of type $S$, with usage
annotation $\rho$, which means that the~new context provides for a~$\rho$ uses
of $x$.

The~rules that derive a~valid typing judgment take the~form:
\[
  \Gamma \vdash M \is\sigma S,
\]
where $\sigma$ is either $0$, or $1$. When $\sigma = 0$, we are indicating that
the~constructed term has no computational content; thus, all the~usage
annotations in the~context are necessarily also $0$. Stated as
a~lemma~\citep[Lemma~2.3]{atkey_2018}:
\begin{lemma}[Zero needs nothing]\label{lem:zero_needs_nothing}
  If $\; \Gamma \vdash M \is0 S$,\; then $\; 0\Gamma = \Gamma$.
\end{lemma}

All type formation rules bellow yield well-formedness judgments $\Gamma \vdash S
\is0 \univ$, meaning that type formation requires no computational resources.
When $\sigma = 1$, the~annotation indicates that we are constructing
computationally relevant data.

We start with these three rules:
\begin{mathpar}
  \inferrule*[right=Var]
  {0\Gamma_1, x \is\sigma S, 0\Gamma_2 \vdash}
  {0\Gamma_1, x \is\sigma S, 0\Gamma_2 \vdash x \is\sigma S}

  \inferrule*[right=Univ]
  {0\Gamma \vdash}
  {0\Gamma \vdash \univ \is0 \univ}

  \inferrule*[right=Conv]
  {
    \Gamma \vdash M \is\sigma S \\
    0\Gamma \vdash S \is0 \univ \\
    0\Gamma \vdash T \is0 \univ \\
    S =_\beta T
  }
  {\Gamma \vdash M \is\sigma T}
\end{mathpar}
The~variable rule, \ir{Var}, selects a~single variable from the~context and all
the~other variables that do not take a~computational part in this judgment are
marked with $0$ usage. The~conversion rule, \ir{Conv}, is almost identical to
one in the~intuitionistic type theory, except that the~types are judged in
a~context with no resources. The~\ir{Univ} rule is only available if
$\sigma = 0$; we cannot construct a~type that has a~runtime presence. In
the~same vein, every type formation rule in the~upcoming paragraphs, \ir{$\to$},
\ir{$\otimes$}, \ir{\1}, \ir{$\with$}, and \ir{$\top$}, forms a~type with usage
$\sigma =0$ and thus assumes a~zeroed-out context, consequence of
\autoref{lem:zero_needs_nothing}. The~introduction and elimination rules combine
the~type parametrisation of \nameref{sec:dtlc} with the~resource tracking of
\nameref{sec:ltlc}.

The~\emph{dependent function type} \depq x \pi S T adds an~annotation $\pi$,
which records how the~function will use its argument. The~formation,
introduction, and elimination rules are:
\begin{mathpar}
  \inferrule*[right=$\to$-F]
  {
    0\Gamma \vdash S \is0 \univ \\
    0\Gamma, x \is0 S \vdash T \is 0 \univ
  }
  {0\Gamma \vdash \depq x \pi S T \is 0 \univ}

  \inferrule*[right=$\to$-I]
  {\Gamma, x \is{\sigma\pi} S \vdash M \is\sigma T}
  {\Gamma \vdash (\lam{x \is{\pi} S} M) \is\sigma \depq x \pi S T}

  \inferrule*[right=$\to$-E$_0$]
  {
    \Gamma \vdash M \is\sigma \depq x \pi S T \\\\
    \sigma\pi = 0 \\
    0\Gamma \vdash N \is0 S
  }
  {\Gamma \vdash M \: N \is\sigma T}

  \inferrule*[right=$\to$-E$_1$]
  {
    \Gamma_1 \vdash M \is\sigma \depq x \pi S T \\
    \Gamma_2 \vdash N \is1 S
  }
  {\Gamma_1 + \sigma\pi\Gamma_2 \vdash M \: N \is\sigma T}
\end{mathpar}
In the~type formation rule \ir{$\to$-F}, the~annotation $\pi$ is not use used to
judge the~well-formedness of the~type, which follows from all type formation
rules being judged in a~context of $0$ usage. The~introduction rule uses $\pi$
to track how the~parameter $x$ is used and the~multiplication by $\sigma$
enforces the~zero-needs-nothing property of \autoref{lem:zero_needs_nothing};
namely, if we use the~function $0$-times, we also need $x$ $0$-times.
We have two distinct elimination rules, except for the~semiring $\{0\}$ where
the~rules are identical. The~rule \ir{$\to$-E$_0$} is applicable if $M \: N$ is
already being judged with $0$ usage ($\sigma = 0$), or if the~function does not
use its argument ($\pi = 0$). The~rule \ir{$\to$-E$_1$} is applicable otherwise,
but since the~term has a~computational usage ($\sigma \neq 0$), we must make
sure that the~$\sigma$ function uses have $\pi$ arguments' worth of resources,
hence the~$\sigma\pi$ scaling of the~context of the~function argument.

The~\emph{dependent multiplicative pair type} $(x \is \pi S) \otimes T$, like
the~function type, adds an~annotation $\pi$; it records how many times the~first
element may be used. The~formation, introduction, and elimination rules are:
\begin{mathpar}
  \inferrule*[right=$\otimes$-F]
  {
    0\Gamma \vdash S \is0 \univ \\
    0\Gamma, x \is0 S \vdash T \is0 \univ
  }
  {0\Gamma \vdash (x \is\pi S) \otimes T \is0 \univ} \\

  \inferrule*[right=$\otimes$-I$_0$]
  {
    \sigma\pi = 0 \\
    0\Gamma \vdash M \is0 S \\\\
    \Gamma \vdash N \is\sigma T[M/x]
  }
  {\Gamma \vdash \mpair M N \is\sigma (x \is\pi S) \otimes T}

  \inferrule*[right=$\otimes$-I$_1$]
  {
    \Gamma_1 \vdash M \is1 S \\
    \Gamma_2 \vdash N \is\sigma T[M/x]
  }
  {
    \sigma\pi \Gamma_1 + \Gamma_2
      \vdash \mpair M N \is\sigma (x \is\pi S) \otimes T
  }

  \inferrule*[right=$\otimes$-E]
  {
    \Gamma_1 \vdash M \is\sigma (x \is\pi S) \otimes T \\
    0\Gamma_1, z \is0 (x \is\pi S) \otimes T \vdash U \is0 \univ \\
    \Gamma_2, x \is{\sigma \pi} S, y \is\sigma T
      \vdash N \is\sigma U[\mpair x y /z]
  }
  {
    \Gamma_1 + \Gamma_2
      \vdash \letpair {(x \is\pi S) \otimes T} [z] x y M [U] N \is\sigma U[M/z]
  }
\end{mathpar}
The~introduction rule \ir{$\otimes$-I$_0$} is applicable, if $\mpair M N$ is
already being judged with $0$ usage ($\sigma = 0$), or if the~pair does not use
its first element computationally ($\pi = 0$). If $M$ has a~computational
presence, applying rule \ir{$\otimes$-I$_1$}, we have to scale $\Gamma_1$ by
$\sigma\pi$ to ensure that enough resources is available for $\sigma$ uses of
the~pair, each with $\pi$ uses of the~first element. The~elimination rule
ensures that both parts of the~pair are used.

For the~\emph{multiplicative unit type} \1, type formation is again judged in
the~erased part of the~theory; the~introduction rule also needs no resources to
construct however many {\munit}s; the~elimination adds the~resource usage of $M$
and $N$:
\begin{mathpar}
  \inferrule*[Right=\1-F]
  {0\Gamma \vdash}
  {0\Gamma \vdash \1 \is0 \univ}

  \inferrule*[right=\1-I]
  {0\Gamma \vdash}
  {0\Gamma \vdash \munit \is\sigma \1}

  \inferrule*[right=\1-E]
  {
    \Gamma_1 \vdash M \is\sigma \1 \\\\
    0\Gamma_1, x \is0 \1 \vdash S \is0 \univ \\
    \Gamma_2 \vdash N \is \sigma S[\munit/x]
  }
  {
    \Gamma_1 + \Gamma_2 \vdash \letu [x] M [S] N \is\sigma S[M/x]
  }
\end{mathpar}
The~exponential type for QTT can be derived by combining $\otimes$ and \1:
\[
  \oc_\pi S = (x \is\pi S) \otimes \1.
\]

The~\emph{dependent additive pair type} $(x \is{} S) \with T$ is without
the~semiring annotation on $x$, because these use cases are already handled by
the~multiplicative pair type. The~formation, introduction, and elimination rules
are:
\begin{mathpar}
  \inferrule*[right=$\with$-F]
  {
    0\Gamma \vdash S \is 0 \univ \\
    0\Gamma, x \is 0 S \vdash T \is 0 \univ
  }
  {0\Gamma \vdash (x \is{} S) \with T \is 0 \univ}

  \inferrule*[right=$\with$-I]
  {
    \Gamma \vdash M \is \sigma S \\
    \Gamma \vdash N \is \sigma T[M/x]
  }
  {\Gamma \vdash \langle M, N \rangle \is \sigma (x \is{} S) \with T}

  \inferrule*[right=$\with$-Efst]
  {\Gamma \vdash M \is \sigma (x \is{} S) \with T}
  {\Gamma \vdash \fst M \is \sigma S}

  \inferrule*[right=$\with$-Esnd]
  {\Gamma \vdash M \is \sigma (x \is{} S) \with T}
  {\Gamma \vdash \snd M \is \sigma T[\fst M/x]}
\end{mathpar}
The~elimination rule \ir{$\with$-Esnd} uses $\fst M$ in the~type, which
consumes zero resources, so all resources that are available for $M$ are also
available for $\snd M$.

The~\emph{additive unit type}
The~formation and introduction are:
\begin{mathpar}
  \inferrule*[right=$\top$-F]
  {0\Gamma \vdash}
  {0\Gamma \vdash \top \is 0 \univ}

  \inferrule*[right=$\top$-I]
  {0\Gamma \vdash}
  {0\Gamma \vdash \aunit \is \sigma \top}
\end{mathpar}

\sectionwithtoc{Semiring order}

This section focuses on the~zero-one-many semiring. Consider the~judgment
\[
x \is\omega S \vdash M \is\sigma T.
\]
Currently, to discharge the~hypothesis $x \is\omega S$, term $M$ has to contain
at least two uses of $x$ at multiplicity $1$, or one use at $\omega$. This
behaviour can be relaxed by optionally adding a~Weakening rule to the~system.
In QTT, Weakening is defined using an~ordering~$\leq$ on
the~semiring~\citep{mcbride_2016}. The~$\leq$ relation should be reflexive and
transitive and it has to respect the~semiring operations when we add
the~Weakening rule. The~relation extends pointwise to contexts:
\begin{definition}
  Given contexts $\Gamma_1$ and $\Gamma_2$, we say that $\Gamma_1 \leq \Gamma_2$
  if for every $x \is\pi S$ in $\Gamma_1$, there is $x \is\rho S$ in $\Gamma_2$
  and $\pi \leq \rho$.
\end{definition}

Then the~Weakening rule allows us to have more resources in the~context than
we consume in the~term:
\begin{mathpar}
  \inferrule*[right=Weak]
  {\Gamma_1 \vdash M \is\sigma S \\ \Gamma_1 \leq \Gamma_2}
  {\Gamma_2 \vdash M \is\sigma S}
\end{mathpar}

There are a~few sensible choices for the~order:
\begin{enumerate}
  \item order $1 \leq \omega$ captures computational relevancy using $\omega$:
    a~resource with quantity $\omega$ has to be used during runtime, but it does
    not matter if it is used once or more;
  \item order $0 \leq 1 \leq \omega$ creates affine typing system: a~linear
    resource is not required to be used exactly once, so, while it cannot be
    duplicated, it can be used zero-times during runtime, i.e. \emph{dropped};
  \item order $0, 1 \leq \omega$ (but not $0 \leq 1$) makes quantity $\omega$
    represent an~intuitionistic resource. Then $\depq x \omega S T$ behaves like
    an~intuitionistic function while $\depq x 1 S T$ behaves like a~linear one.
    This is the~order that is used in our interpreter.
\end{enumerate}