# Functional Ownership through Fractional Uniqueness

Daniel Marshall  0000-0002-4284-3757 School of ComputingUniversity of
KentUnited Kingdom<EMAIL_ADDRESS>and  Dominic Orchard  0000-0002-7058-7842
School of ComputingUniversity of KentUnited Kingdom<EMAIL_ADDRESS>Department of Computer Science and TechnologyUniversity of CambridgeUnited
Kingdom<EMAIL_ADDRESS>
###### Abstract.

Ownership and borrowing systems, designed to enforce safe memory management
without the need for garbage collection, have been brought to the fore by the
Rust programming language. Rust also aims to bring some guarantees offered by
functional programming into the realm of performant systems code, but the type
system is largely separate from the ownership model, with type and borrow
checking happening in separate compilation phases. Recent models such as
RustBelt and Oxide aim to formalise Rust in depth, but there is less focus on
integrating the basic ideas into more traditional type systems. An approach
designed to expose an essential core for ownership and borrowing would open
the door for functional languages to borrow concepts found in Rust and other
ownership frameworks, so that more programmers can enjoy their benefits.

One strategy for managing memory in a functional setting is through
_uniqueness types_ , but these offer a coarse-grained view: either a value has
exactly one reference, and can be mutated safely, or it cannot, since other
references may exist. Recent work demonstrates that _linear_ and _uniqueness_
types can be combined in a single system to offer restrictions on program
behaviour and guarantees about memory usage. We develop this connection
further, showing that just as _graded_ type systems like those of Granule and
Idris generalise linearity, Rust’s _ownership_ model arises as a graded
generalisation of uniqueness. We combine fractional permissions with grading
to give the first account of ownership and borrowing that smoothly integrates
into a standard type system alongside linearity and graded types, and extend
Granule accordingly with these ideas.

##  1\. Introduction

The Rust programming language has dramatically grown in popularity in recent
years, having been adopted as the second official language of the Linux
kernel,111https://www.zdnet.com/article/rust-takes-a-major-step-forward-as-
linuxs-second-official-language/ and deployed in production code by companies
including AWS, Huawei, Google, Microsoft and Mozilla, all of whom are founding
members of the Rust Foundation.222https://foundation.rust-
lang.org/news/2021-02-08-hello-world/ This popularity is in large part due to
its focus on memory safety; Rust finds a happy medium between systems
programming languages like C which offer precise control but little in the way
of safety guarantees and the contrasting approach of higher-level languages
like Java or Go where memory is managed automatically through garbage
collection.

The intricate ownership system which characterises Rust’s approach to memory
management is inspired in part by the literature on using _linear types_
(Wadler, 1990) for tracking resource usage, based on _linear logic_ (Girard,
1987). Linear types have also been brought into the realm of practical
programming in recent years, for example in Haskell via the GHC compiler’s
linear types extension (Bernardy et al., 2017). The precise theoretical
relationship between linear types and the properties that can be enforced by
Rust’s borrow checker remains unclear, however, particularly since Rust lies
outside the traditional functional paradigm to which linearity is most suited,
opting for a more mixed imperative and functional approach.

Linear types require that every value is used exactly once, with the $!$
modality classifying non-linearity (arbitrary use). Modern resourceful type
systems go beyond this coarse restriction of linearity, enabling usage to be
classified more finely. Quantitative types, inspired by bounded linear logic
(Girard et al., 1992), capture an upper bound on the amount of (re)use of a
value by indexing the $!$ modality with natural numbers or polynomial terms.
This quantitative analysis is generalised further by _graded modal types_ , as
exemplified by the Granule programming language (Orchard et al., 2019), which
allows various properties of data use and data flow to be tracked smoothly in
a single type system via an indexed modality $!_{r}$ with some algebraic
structure on $r$ (Gaboardi et al., 2016; Orchard et al., 2019). In this work,
we seek a shared understanding between the precise resource reasoning of
graded type systems and concepts of uniqueness, borrowing, and ownership as
typified by Rust but also appearing in various other languages such as C++.

Many models of ownership from a type-theoretic perspective already exist. For
example, $\lambda_{\text{Rust}}$ developed as part of the RustBelt framework
provides a low-level model of Rust’s ownership and borrowing systems suitable
for formally verifying properties of Rust programs (Jung et al., 2017). Oxide
(Weiss et al., 2019) and FR (Pearce, 2021) provide more high-level theoretical
models. Our focus is _not_ on replicating these efforts; we do not aim to
directly model all the details of Rust’s particular approach to ownership.
Rather, we offer a different and complementary perspective: a single system
that relates general ownership and borrowing ideas to linear and graded types.
This integration enables type, resource, and memory safety to be enforced via
a single type system.

A natural place to start is _uniqueness types_ , which provide the concept
that a uniquely typed value has exactly one reference, and therefore is safe
to mutate (Smetsers et al., 1994; Barendsen and Smetsers, 1996; de Vries et
al., 2008). This gives a simplistic model of _ownership_ without borrowing—a
resource with a unique owner may be modified by that owner, but a broken
guarantee of uniqueness can never be recovered. Recent work developed a type
system that captures the relationship between linear and unique types: linear
values are restricted from being copied or discarded in the future, whilst
unique values are guaranteed to have never been copied in the past (Marshall
et al., 2022). We build upon this work as our foundation here but leverage the
generalisations of grading. In the ownership framework of Mycroft and Voigt
(2013), while uniqueness allows for memory-safe _temporal_ aliasing, borrowing
extends uniqueness by introducing the potential for safe patterns of _spatial_
aliasing, dramatically increasing flexibility for the programmer. Just as the
non-linearity modality $!$ can be generalised to a graded modality $!_{r}$ for
fine-grained reasoning about resource usage via $r$ and its algebraic
structure, we show that uniqueness types, represented modally, can be ‘graded’
to capture this idea that borrowing is a controlled relaxation of the
uniqueness guarantee.

Our approach allows many ideas from Rust, such as immutable and mutable
borrows, partial borrows and reborrowing to be explained explicitly in a
functional setting, all through the application of an elegant form of grading
based on Boyland’s fractional permissions (Boyland, 2003). Our work thus
integrates and relates within a unified framework the substructural type
systems of linearity, uniqueness, grading, ownership, and borrowing. This
offers a pathway to expressing memory safety properties naturally in
functional languages such as Haskell or Idris.

The outline of the paper is as follows. First, in Section 2 we recap the key
concepts of uniqueness and borrowing using Rust as a convenient exemplar. We
discuss how various programs making use of these ideas will later be rewritten
as Granule programs through our unified type system, in order to motivate the
rest of our work. We then recap Granule’s pre-existing core calculus in
Section 3, before moving on to the primary contributions of this paper:

  * •

In Section 4, we connect Granule’s unique and graded modal types with ideas
from Rust, discussing how unique ownership allows for safe mutation. We
generalise the connection between uniqueness and linearity, demonstrating that
uniqueness and precise grading can coexist within a single type system. We
leverage existential types over ‘identifiers’ for situations where multiple
references pointing to the same value need tracking.

  * •

In Section 5, we extend this idea to allow for multiple immutably borrowed
references at a time, by carefully tracking references that exist, similarly
to Boyland’s fractional permissions. We show that this allows for a more fine-
grained approach to tracking uniqueness in much the same way that grading
increases expressivity over pure linearity.

    * –

In Section 5.1, we develop an equational theory for our extension to Granule’s
type system, showing that the modality for unique ownership induces a
_relative functor_ over the new modality for mutable and immutable borrowing.

    * –

In Section 5.2, we discuss how using distributive laws can allow for borrowing
only part of a larger data structure while leaving the rest uniquely owned,
enabling a much wider variety of practical programming patterns.

  * •

In Section 6, we detail the semantics for the calculus developed thus far, and
prove various key properties—both standard notions like progress and
preservation but also borrow safety and uniqueness. The semantics is call-by-
value, representing a practical system, departing from most previous
operational models of grading in the literature.

Sections 7 and 8 discuss the many and varied areas of similar research that
have inspired this paper, and look at some possible avenues for future work.
All source code discussed will be made available in the artifact, along with
the implementation of our type system atop Granule.333If the reader wishes to
experiment with the Granule language, the latest releases are available from
https://github.com/granule-project/granule/releases.

##  2\. Key Concepts in Ownership and Borrowing

In order to develop a type system which integrates ownership and borrowing
concepts with the linear and graded types already present in Granule, we will
first need to understand the ideas in question. This section presents six key
patterns which we capture in our system in the rest of this paper, along with
simple Rust code examples to demonstrate the patterns in action. Each of these
examples relies on a single base value of type Colour(u32, u32,u32) \- a
struct containing three unsigned integers, representing a colour with red,
green and blue components.

#### Ownership

The first crucial concept is _owned_ values, where a value is ‘owned’ by a
particular _identifier_. Below, the value Colour(220, 20, 60) is owned by the
identifier scarlet. Each value can only be owned by a single identifier at any
given time. Rust enforces this via _move semantics_ : on the second line,
ownership of the value is _moved_ to the identifier x. Now the identifier
scarlet no longer owns the value, so attempting to use it again on the third
line gives an error.

` Rust ✗ It is fairly clear that the idea here in some way relates to
linearity, since linear values can only be used once which restricts them to
being passed around sequentially; indeed, much of the literature on Rust makes
mention of linear (or affine) types. We demonstrate through our unified type
system in Chapter 4 that in fact ownership can be better understood as an
extension of _uniqueness_ types, since each value having a single owner
implies that the owner holds the unique reference to said value. These are
similar to linear types in some ways but with important differences.

#### Immutable borrowing

Borrowing generalises the concept of ownership, permitting multiple references
to point to a single value simultaneously. Rust’s _borrow checker_ manages all
borrows that exist at a given time, ensuring that memory safety properties are
maintained until values are eventually returned to their owners. _Immutable_
borrows are one flavour of reference; any number of these can exist at a given
time, but mutation of a value is disallowed through an immutable borrow, since
this could result in data races. Below, two immutable borrows (x and y) both
reference the original persimmon value.

` Rust ✓

#### Mutable borrowing

It is also possible to borrow values and retain the capacity to mutate them,
but this comes at a price: as mentioned above, allowing mutation through
multiple references simultaneously is harmful to memory safety, so in order to
prevent this only a single mutable borrow is permitted at a time. Much like
owned values, mutably borrowing a value guarantees the sole capability for
destructive access to the underlying data. This is demonstrated below, where
attempting to create two _mutable_ borrows following the pattern of the above
example is disallowed.

` Rust ✗ Note, however, that the above example copied verbatim into a Rust
file will in fact compile successfully unless additional code is introduced
that makes use of the variables x and y; this is due to a feature called _non-
lexical lifetimes_ , through which the Rust compiler is able to _infer_ that
allowing two mutable borrows is safe as long as one of them is never used. We
do not linger on this, since we will not capture this behaviour in our type
system; our goal is to embed some essential ownership and borrowing patterns
_explicitly_. However, we will mention the possibility for extending our
system with more advanced ideas in Section 8.

#### Mixing mutable and immutable borrows

Rust also disallows immutable borrows of values that are already borrowed
mutably, since this invites similar problems: e.g., a value could be updated
through the mutable borrow whilst being read through the immutable borrow.
Hence, the following example wherein the second reference is borrowed
immutably rather than mutably is also forbidden by the borrow checker. In
Section 5, we demonstrate that both notions can be represented through a
graded generalisation of uniqueness typing to represent a borrower’s level of
access.

` Rust ✗

#### Partial borrowing

A useful pattern for working with larger data structures is to borrow only
_part_ of the structure while the original owner retains access to what
remains. This is valuable for allowing one part of a program to work with a
particular piece of data without restricting access to the entire structure,
enabling tasks to be carried out in parallel more easily. In the below
example, the red and green components of the indigo value are simultaneously
borrowed mutably. The Rust compiler allows this since the references point to
disjoint parts of the original struct:

` Rust ✓ In Section 5.2, we take advantage of Granule’s functional nature to
present a cohesive way of managing this kind of partial borrow at the type
level, including the possibility for working with disjoint components of the
original structure concurrently.

#### Reborrowing

The final pattern we aim to capture in our system, also essential for
practical programming, is the notion of _reborrowing_ , through which it is
possible to create a borrow of an identifier that itself references another
value. We will show in Section 5 that this behaviour falls out of our
generalisation of uniqueness naturally, without a need for additional
constructs. To illustrate the general idea, consider the following example;
here, the red component of the amethyst value is borrowed mutably as r, then
another immutable borrow x is created pointing to r. The value can now only be
read through x—both r and amethyst are inaccessible until the borrow is
complete.

` Rust ✓

##  3\. Core Calculus

We recap Granule’s core calculus which incorporates graded modal types into a
linear type theory (Orchard et al., 2019); we later extend this calculus with
our functional model of uniqueness and borrowing. This section covers the
syntax and static semantics (type system), whilst Section 6 gives an
operational semantics incorporating the various extensions discussed
throughout this work.

The calculus extends the linear $\lambda$-calculus with multiplicative
products and unit, and a _semiring-graded necessity modality_
$\Box_{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}r}}A$
where $r$ is an element of a pre-ordered semiring
$({\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathcal{R}},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}*},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}1},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}+},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}0},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\sqsubseteq})$
which includes a requirement that
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}*}$
and
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}+}$
must be monotonic with respect to the ordering
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\sqsubseteq}$.
This calculus gives a simplified monomorphic subset of Granule (Orchard et
al., 2019), and closely resembles other graded systems from the literature
(Brunel et al., 2014; Gaboardi et al., 2016; Petricek et al., 2014; Abel and
Bernardy, 2020; Atkey, 2018; Choudhury et al., 2021; McBride, 2016; Moon et
al., 2021). The extensions for uniqueness and borrowing we describe could be
made compatible with such systems, as they do not rely on particular details
of the core calculus in question. Beyond existing work, we add existential
types and type variables (restricted to a particular kind) to track
identifiers associated with resources (whose dataflow paths may fork and join,
due to the borrowing patterns we discuss later).

###  3.1. Syntax

Our syntax consists of the linear $\lambda$-calculus with multiplicative
products and unit (first line of syntax below), graded modal terms (second
line) and existentially quantified identifiers (third line):

$\displaystyle\mathit{t}::=\;$
$\displaystyle\mathit{x}\mid\lambda\mathit{x}.\mathit{t}\mid\mathit{t_{{\mathrm{1}}}}\,\mathit{t_{{\mathrm{2}}}}\mid(\mathit{t_{{\mathrm{1}}}},\mathit{t_{{\mathrm{2}}}})\mid\textbf{let}\,(x,y)=\mathit{t_{{\mathrm{1}}}}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}\mid()\mid\textbf{let}\
()=\mathit{t_{{\mathrm{1}}}}\ \textbf{in}\ \mathit{t_{{\mathrm{2}}}}$
$\displaystyle\mid\;$
$\displaystyle[\mathit{t}]\mid\textbf{let}\,[\mathit{x}]=\mathit{t_{{\mathrm{1}}}}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}$
(terms) $\displaystyle\mid\;$ $\displaystyle\textbf{pack}\
\langle{\mathit{id},\mathit{t}}\rangle\mid\textbf{unpack}\
\langle{\mathit{id},\mathit{x}}\rangle=\mathit{t_{{\mathrm{1}}}}\ \textbf{in}\
\mathit{t_{{\mathrm{2}}}}$

Following the syntax of variables, we group terms above into pairs of
introduction and elimination forms, for functions, products, units, the graded
modality, and existential types respectively. The meaning of these terms is
explained in the next subsection with reference to their typing.

###  3.2. Type system

Typing judgments have the form $\Gamma\vdash\mathit{t}:\mathit{A}$, assigning
type $A$ to term $t$ under context $\Gamma$. Types are:

(types) $\displaystyle A,B::=\;$
$\displaystyle\mathit{A}\multimap\mathit{B}\mid\mathit{A}\otimes\mathit{B}\mid\mathsf{unit}\mid{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}\mid\exists\mathit{id}.\mathit{A}$

Hence, our type syntax comprises linear function types
$\mathit{A}\multimap\mathit{B}$, linear multiplicative products
$\mathit{A}\otimes\mathit{B}$, a linear multiplicative unit $(\mathsf{unit})$,
the graded modality
${{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}$
where
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}r}\in{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathcal{R}}$,
and existentially quantified types where $\mathit{id}:\mathsf{Name}$ for an
abstract kind of names $\mathsf{Name}$.

Contexts $\Gamma$ contain both linear assumptions $x:A$, graded assumptions
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{r}}$
which have originated from inside a graded modality, and type variables which
we write as $\mathit{id}$ due to their restricted purpose here, omitting the
kind which is the abstract type $\mathsf{Name}$:

(contexts)
$\displaystyle\Gamma::=\;\emptyset\mid\Gamma,\mathit{x}:\mathit{A}\mid\Gamma,{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{r}}\mid\Gamma,\mathit{id}$

Typing of the $\lambda$-calculus fragment is then by the following rules:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\end{array}}{0\cdot\Gamma,\mathit{x}:\mathit{A}\vdash\mathit{x}:\mathit{A}}\quad\\!\\!\\!\textsc{{$\textsc{var}$}{}}}\;\;\;\;{\displaystyle\frac{\begin{array}[]{l}\Gamma,\mathit{x}:\mathit{A}\vdash\mathit{t}:\mathit{B}\\\
\end{array}}{\Gamma\vdash\lambda\mathit{x}.\mathit{t}:\mathit{A}\multimap\mathit{B}}\quad\\!\\!\\!\textsc{{$\textsc{abs}$}{}}}\;\;\;\;{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}:\mathit{A}\multimap\mathit{B}&\;\,\Gamma_{{\mathrm{2}}}\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{A}\end{array}\\\
\end{array}}{\Gamma_{{\mathrm{1}}}+\Gamma_{{\mathrm{2}}}\vdash\mathit{t_{{\mathrm{1}}}}\,\mathit{t_{{\mathrm{2}}}}:\mathit{B}}\quad\\!\\!\\!\textsc{{$\textsc{app}$}{}}}\end{array}$

The var, abs, and app rules are the standard rules of the linear
$\lambda$-calculus, augmented with a notion of _contraction_ captured by the
$+$ operation on contexts coming from multiple sub-terms, which is only
defined when contexts are disjoint with respect to linear assumptions, and on
overlapping graded assumptions we add their grades, e.g.
$(\Gamma_{1},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{r}})+(\Gamma_{2},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{s}})=(\Gamma_{1}+\Gamma_{2}),{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{r+s}}$.
More explicitly, context addition is declaratively specified as follows:

$\displaystyle\begin{array}[]{cc}\begin{array}[]{rl}(\Gamma,\mathit{x}:\mathit{A})+\Gamma^{\prime}&=(\Gamma+\Gamma^{\prime}),\mathit{x}:\mathit{A}\quad\text{iff}\,\;x\not\in|\Gamma^{\prime}|\\\
\Gamma+(\Gamma^{\prime},\mathit{x}:\mathit{A})&=(\Gamma+\Gamma^{\prime}),\mathit{x}:\mathit{A}\quad\text{iff}\,\;x\not\in|\Gamma|\\\
(\Gamma,{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{r}})+(\Gamma^{\prime},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{s}})&=(\Gamma+\Gamma^{\prime}),{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{(r+s)}}\end{array}\\!&\\!\begin{array}[]{rl}\emptyset+\Gamma&=\Gamma\quad\text{(context
addition)}\\\ \Gamma+\emptyset&=\Gamma\\\
(\Gamma,\mathit{id})+(\Gamma^{\prime},\mathit{id})&=(\Gamma+\Gamma^{\prime}),\mathit{id}\\\
\end{array}\end{array}$

In the first two cases, $x$ may be $id$ with $A=\mathsf{Name}$ implicitly.
This is a declarative rather than algorithmic specification of $+$ as graded
assumptions of the same variable may appear in different positions within the
two contexts—for example, when typechecking the program ((x, y), (y,x)). The
var rule also embeds the notion of _weakening_ , allowing a context of
variables graded by $0$, using the partial operation of _scalar multiplication
of a context_ :

(context multiplication) $\displaystyle
r\cdot\emptyset=\emptyset\quad\;\,r\cdot(\Gamma,{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{s}})=(r\cdot\Gamma),{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{r*s}}\quad\;r\cdot(\Gamma,\mathit{id})=(r\cdot\Gamma),\mathit{id}$

scaling graded assumptions by $r$, preserving $\mathit{id}$s, but undefined if
$\Gamma$ contains linear assumptions.

The rules involving graded modalities are then:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\Gamma\vdash\mathit{t}:\mathit{A}&\;\,\neg\mathsf{resourceAllocator}(\mathit{t})\end{array}\\\
\end{array}}{r\cdot\Gamma\vdash[\mathit{t}]:{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}}\quad\\!\\!\\!\textsc{{$\textsc{pr}$}{}}}\quad{\displaystyle\frac{\begin{array}[]{l}\Gamma,\mathit{x}:\mathit{A}\vdash\mathit{t}:\mathit{B}\\\
\end{array}}{\Gamma,{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{1}}\vdash\mathit{t}:\mathit{B}}\quad\\!\\!\\!\textsc{{$\textsc{der}$}{}}}\\\\[15.00002pt]
{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}:{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}&\;\,\Gamma_{{\mathrm{2}}},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{r}}\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{B}\end{array}\\\
\end{array}}{\Gamma_{{\mathrm{1}}}+\Gamma_{{\mathrm{2}}}\vdash\textbf{let}\,[\mathit{x}]=\mathit{t_{{\mathrm{1}}}}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}:\mathit{B}}\quad\\!\\!\\!\textsc{{$\textsc{elim}$}{}}}\quad{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\Gamma,{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{r}},\Gamma^{\prime}\vdash\mathit{t}:\mathit{B}&\;\,r\sqsubseteq
s\end{array}\\\
\end{array}}{\Gamma,{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{s}},\Gamma^{\prime}\vdash\mathit{t}:\mathit{B}}\quad\\!\\!\\!\textsc{{$\textsc{approx}$}{}}}\end{array}$

The pr rule (_promotion_) introduces a graded modality with grade $r$,
implying that the result of $t$ can be used in an ‘$r$-like’ way and thus all
of the dependencies of $\mathit{t}$ must be scaled by $r$ to propagate usage
to the dependencies, none of which are allowed to be linear. Promotion also
contains an explicit restriction that the value to be promoted must not be a
_resource allocator_ , designed to avoid problems that otherwise arise when
promoting values with certain behaviours in a call-by-value setting; we will
discuss this in detail when we describe our interface for mutable arrays in
Section 5.

The elim rule eliminates a graded modality, capturing the idea that a
requirement for $x$ to be used in an ‘$r$-like’ way in $t_{2}$ can be matched
with the capability of $t_{1}$ described by its graded modal type. In Granule,
this construct is folded into pattern matching: we can ‘unbox’ (eliminate) a
graded modality to provide a graded variable in the body of the function (the
analogue to $t_{2}$ in this rule).

The der rule (_dereliction_) connects linear typing to graded typing, stating
that a requirement for a linear assumption is satisfied by an assumption
graded by $1$. The approx rule converts a grade $r$ to $s$ if $s$ approximates
$r$ according to the semiring’s pre-order $\sqsubseteq$.

One possible choice of semiring is that of natural numbers
$(\mathbb{N},*,+,0,1,\equiv)$ with _discrete ordering_ $\equiv$ such that
there is no approximation and we track the exact number of times a term has
been used. We could instead use the standard $\leq$ ordering on natural
numbers which would permit approximation, allowing for an _upper bound_ on a
term’s usage. Another useful semiring is on _intervals_ of natural numbers.
Here, we can use a grade such as 0..1 to represent a value which can be used
_either_ zero or one times; this captures the notion of an _affine_ value.
Other interesting semirings include lattices for security levels (Gaboardi et
al., 2016; Abel and Bernardy, 2020), hardware schedules (Ghica and Smith,
2014), and sets for abstract property tracking.

Finally, we have the rules for introducing and eliminating tensor products and
the multiplicative unit, which are standard, though it is important to
remember that products are _linear_ and so it is not possible to freely
discard either side: both elements must be used when consuming a product.

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}:\mathit{A}&\;\,\Gamma_{{\mathrm{2}}}\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{B}\end{array}\\\
\end{array}}{\Gamma_{{\mathrm{1}}}+\Gamma_{{\mathrm{2}}}\vdash(\mathit{t_{{\mathrm{1}}}},\mathit{t_{{\mathrm{2}}}}):\mathit{A}\otimes\mathit{B}}\quad\\!\\!\\!\textsc{{$\otimes_{I}$}{}}}\;\;\;\;{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}:\mathit{A}\otimes\mathit{B}&\;\,\Gamma_{{\mathrm{2}}},\mathit{x}:\mathit{A},\mathit{y}:\mathit{B}\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{C}\end{array}\\\
\end{array}}{\Gamma_{{\mathrm{1}}}+\Gamma_{{\mathrm{2}}}\vdash\textbf{let}\,(x,y)=\mathit{t_{{\mathrm{1}}}}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}:\mathit{C}}\quad\\!\\!\\!\textsc{{$\otimes_{E}$}{}}}\\\\[12.50002pt]
{\displaystyle\frac{\begin{array}[]{l}\end{array}}{0\cdot\Gamma\vdash():\mathsf{unit}}\quad\\!\\!\\!\textsc{{$1_{I}$}{}}}\;\;\;\;{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}:\mathsf{unit}&\;\,\Gamma_{{\mathrm{2}}}\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{B}\end{array}\\\
\end{array}}{\Gamma_{{\mathrm{1}}}+\Gamma_{{\mathrm{2}}}\vdash\textbf{let}\
()=\mathit{t_{{\mathrm{1}}}}\ \textbf{in}\
\mathit{t_{{\mathrm{2}}}}:\mathit{B}}\quad\\!\\!\\!\textsc{{$1_{E}$}{}}}\end{array}$

###### Example 3.1.

The following gives an example derivation assuming the natural number
semiring:

$\displaystyle\vspace{-1em}\inferrule*[right=$app$]{\inferrule*[right=$\textsc{abs}${}]{\inferrule*[right=$\otimes_{I}$]{\inferrule*[right=$\textsc{var}$]{\;}{\mathit{x}:\mathit{A}\otimes\mathit{A}\vdash\mathit{x}:\mathit{A}\otimes\mathit{A}}\inferrule*[right=$\textsc{var}$^{\prime}]{\;}{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{y}:[\mathit{A}]_{1}}\vdash\mathit{y}:\mathit{A}}}{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{y}:[\mathit{A}]_{1}},\mathit{x}:\mathit{A}\otimes\mathit{A}\vdash(\mathit{x},\mathit{y}):(\mathit{A}\otimes\mathit{A})\otimes\mathit{A}}}{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{y}:[\mathit{A}]_{1}}\vdash\lambda\mathit{x}.(\mathit{x},\mathit{y}):\mathit{A}\otimes\mathit{A}\multimap(\mathit{A}\otimes\mathit{A})\otimes\mathit{A}}\;\inferrule*[right=$\otimes_{I}${}]{\emptyset\vdash\mathit{v}:\mathit{A}\quad\inferrule*[right=$\textsc{var}$^{\prime}]{\;}{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{y}:[\mathit{A}]_{1}}\vdash\mathit{y}:\mathit{A}}}{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{y}:[\mathit{A}]_{1}}\vdash(\mathit{v},\mathit{y}):\mathit{A}\otimes\mathit{A}}}{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{y}:[\mathit{A}]_{2}}\vdash(\lambda\mathit{x}.(\mathit{x},\mathit{y}))\,(\mathit{v},\mathit{y}):(\mathit{A}\otimes\mathit{A})\otimes\mathit{A}}$

where (var’) is a synonym for the (var) rule followed by dereliction (der).

As a first taste of Granule syntax (which resembles Haskell, apart from the
presence of the graded modal type constructs), the following captures the same
idea as this example:

` Granule The type
${{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}$
is instead written postfix as A [r], and Granule uses $\rightarrow$ for its
linear function types. Existential types have standard introduction and
elimination typing forms, but restricted only to type variables of kind
$\mathsf{Name}$ (whose kind is omitted here for simplicity due to this
restriction):
$\displaystyle\inferrule*[right=$pack${}]{\Gamma\vdash\mathit{t}:\mathit{A}\quad\;\mathit{id}\not\in\mathsf{dom}(\Gamma)}{\Gamma\vdash\textbf{pack}\
\langle{\mathit{id^{\prime}},\mathit{t}}\rangle:\exists\mathit{id}.\mathit{A}[\mathit{id}/\mathit{id^{\prime}}]}\;\;\;\inferrule*[right=$unpack${}]{\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}:\exists\mathit{id}.\mathit{A}\quad\;\Gamma_{{\mathrm{2}}},\mathit{id},\mathit{x}:\mathit{A}\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{B}\quad\;\mathit{id}\not\in\mathsf{fv}(\mathit{B})}{\Gamma_{{\mathrm{1}}}+\Gamma_{{\mathrm{2}}}\vdash\textbf{unpack}\
\langle{\mathit{id},\mathit{x}}\rangle=\mathit{t_{{\mathrm{1}}}}\ \textbf{in}\
\mathit{t_{{\mathrm{2}}}}:\mathit{B}}$

#### Note on Linear Haskell

As mentioned at the start of this section, we aim for the extensions we
develop throughout this work to be compatible with other graded type systems
after some adaptation. One particular system of interest is the calculus
underlying the recent extension which introduces linear types to Haskell
(Bernardy et al., 2017). This extension uses a graded type system below the
surface in order to implement linearity; all function types are given a
‘multiplicity’ annotation $r$ written (a %r $\rightarrow$ b) akin to a type
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}A\multimap
B$ here, where the annotation can currently be either ’One or ’Many
representing either linear or unrestricted usage respectively. Work on
formalising the precise connection between systems such as this where all
function types come with a grade (sometimes called ‘graded base’) and systems
such as Granule’s where values are linear by default and graded values are
wrapped inside a modality (called ‘linear base’) is ongoing.

##  4. One of a Kind: Uniqueness and Sharing

The first extension we make to the core calculus is to represent _ownership_ :
values that have a unique owner can mutate the value freely because they are
in possession of the only reference that exists. It turns out this matches
closely with the idea of _uniqueness_ types; if it is possible to guarantee
that a reference to a value is unique (i.e., it is the only reference that
exists), then whichever part of the program (e.g., a given thread or process)
holds that reference must be the owner.

Uniqueness types were introduced into Granule’s core type system in previous
work (Marshall et al., 2022), but we will extend this in two ways: first, we
generalise the rules of Marshall et al. (2022) to allow for a graded necessity
modality parameterised by an arbitrary semiring rather than the simple non-
linear $\oc$, and second, we incorporate the identifiers described in Section
3 into the typing, which will become important when multiple references need
to be tracked.

As with uniqueness typing, the crucial insight for integrating owned values
with linear and graded values is to consider any linear or graded value to
have no ownership information attached; these values have their memory managed
in other ways, such as explicitly by the programmer or implicitly by a garbage
collector. We then introduce a modality, written
${\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}$
(akin to Marshall et al.’s uniqueness modality) to type values that are
_uniquely owned_ , meaning that the type system must ensure only one reference
exists at any given time. We extend the syntax of terms and types:

$\displaystyle\begin{array}[]{c}\mathit{t}::=\ldots\mid\mathbf{share}\,\mathit{t}\mid\mathbf{clone}\,\mathit{t_{{\mathrm{1}}}}\,\textbf{as}\,\mathit{x}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}\qquad\quad\mathit{A},\mathit{B}::=\ldots\mid{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{\mathit{A}}\end{array}$

The two constructs for this uniqueness modality
${\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}$
provide sharing and cloning, with types:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\Gamma\vdash\mathit{t}:{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{\mathit{A}}\\
\end{array}}{\Gamma\vdash\mathbf{share}\,\mathit{t}:{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}}\quad\!\!\!\textsc{{$\textsc{share}$}{}}}\;\;\;\;{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}1\sqsubseteq
r&\;\,\mathsf{cloneable}(\mathit{A})\end{array}\\
\begin{array}[]{cc}\Gamma_{{\mathrm{1}}},\overline{\mathit{id}}\vdash\mathit{t_{{\mathrm{1}}}}:{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}&\;\,\Gamma_{{\mathrm{2}}},\mathit{x}:\exists\overline{\mathit{id^{\prime}}}.{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{(\mathit{A}[\overline{\mathit{id^{\prime}}}/\overline{\mathit{id}}])}\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{B}\end{array}\\
\end{array}}{(\Gamma_{{\mathrm{1}}}+\Gamma_{{\mathrm{2}}}),\overline{\mathit{id}}\vdash\mathbf{clone}\,\mathit{t_{{\mathrm{1}}}}\,\textbf{as}\,\mathit{x}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}:\mathit{B}}\quad\!\!\!\textsc{{$\textsc{clone}$}{}}}\end{array}$

The Share construct allows a guarantee of unique ownership to be discarded,
though this means that memory must now once again be managed automatically
just as with any other Granule values where ownership is not tracked. Any
grade $r$ can be selected here, though the shared value must eventually be
either discarded (requiring $0\sqsubseteq r$) or fully consumed via pattern
matching.

The Clone construct makes a _deep copy_ of the value
$\mathit{t_{{\mathrm{1}}}}$, where we take a value that does not necessarily
have a unique owner and make a unique copy of it; we take ownership of the
copy, binding it the scope of $\mathit{t_{{\mathrm{2}}}}$. We can guarantee
uniqueness since this is now the only reference that exists to the newly
copied value. We must update any identifiers along the way, however, to ensure
that this is genuinely understood as a separate value to the original, in case
other references still exist. This is mediated by existential types, where all
identifiers $\overline{\mathit{id}}$ used in typing
$\mathit{t_{{\mathrm{1}}}}$ are bound under an existential quantifier (the
predicate $\mathsf{cloneable}(\mathit{A})$ ensures the value is of a resource
type—such as a reference—or a product of resources). The side-condition
$1\sqsubseteq r$ explains that we must be able to accommodate a usage of the
input $\mathit{t_{{\mathrm{1}}}}$ since clone consumes the
$\mathit{t_{{\mathrm{1}}}}$ value once in copying it.

Our implementation of these ideas in Granule follows the above typing. We
recap the initial ownership example from Section 2 here in our new extension
of Granule using a data type Colour which acts as an alias for a triple of
type (Int, (Int, Int)).

The following code illustrates that linear types already require us to obey
the laws of _move semantics_ for owned values, where we move ownership of
scarlet to x and then to y:

` Granule We can have multiple variables which all point to the initial value
of type Colour via the share operation; this explicitly exempts the value from
being managed by the ownership system. Here, we share at the interval grade
0..2, capturing the idea that the value must be used somewhere between zero
and two times (where here it happens to be used twice). ` Granule The share
and clone operations have the following equations showing their interaction:
(unitL)
$\displaystyle\mathbf{clone}\,(\mathbf{share}\,\mathit{v})\,\textbf{as}\,\mathit{x}\,\textbf{in}\,\mathit{t}$
$\displaystyle\equiv\mathit{t}[\textbf{pack}\
\langle{\overline{\mathit{id}},\mathit{v}}\rangle/\mathit{x}]$ (assoc)
$\displaystyle\mathbf{clone}\,\mathit{t_{{\mathrm{1}}}}\,\textbf{as}\,\mathit{x}\,\textbf{in}\,(\mathbf{clone}\,\mathit{t_{{\mathrm{2}}}}\,\textbf{as}\,\mathit{y}\,\textbf{in}\,\mathit{t_{{\mathrm{3}}}})$
$\displaystyle\equiv\mathbf{clone}\,(\mathbf{clone}\,\mathit{t_{{\mathrm{1}}}}\,\textbf{as}\,\mathit{x}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}})\,\textbf{as}\,\mathit{y}\,\textbf{in}\,\mathit{t_{{\mathrm{3}}}}\quad(x\not\in\mathsf{FV}(t_{3}))$
The (unitL) axiom states that sharing a value $\mathit{v}$ (term with no
further reductions—see Section 6) and cloning it to create a new owned $x$ in
the scope of $t$ is equivalent to substituting the original $\mathit{v}$ for
$x$ in $t$ (with its identifiers packed in an existential). The (assoc) axiom
is associativity of cloning. The presence of identifiers necessitates the
existential typing. The need for identifiers is shown in the next section once
we move to a generalisation of uniqueness with the ability to separate
_immutable borrows_ from _mutable borrows_ , where existential types will
allow for tighter control of the _lifetime_ of borrowed values with
identifiers.

##  5. Immutably Borrowed is Fractionally Unique

We now generalise from the above system which incorporates uniqueness into the
core calculus to a system that allows for the uniqueness guarantees to be
temporarily broken in controlled ways, such that we can continue to ensure
memory safety and more closely approximate Rust-like ownership and borrowing
rules. We take inspiration from the fractional permissions of Boyland (2003)
(which themselves served as partial inspiration for Rust’s notion of
ownership) and from recent literature on integrating linear types with
fractional permissions (Makwana and Krishnaswami, 2019).

Just as grading non-linearity gives a more precise account of resource usage,
we introduce borrowing as a graded form of non-_uniqueness_ denoted
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}\mathit{A}$,
allowing precise control of references:

(types, extended) $\displaystyle\mathit{A},\mathit{B}$
$\displaystyle::=\ldots\mid{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}\mathit{A}$
(permissions) $\displaystyle p,q$ $\displaystyle::=\ast\mid
f\qquad\qquad(\textit{where $f\in\mathbb{Q},0<f\leq 1$})$

where $p$ is a new form of grade for tracking borrowing, called a
_permission_. Permissions are either rational numbers $f$ between $0$ and $1$
or a special permission $\ast$ representing unique ownership (described
below). A _mutable borrow_ is represented by
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{1}}}\mathit{A}$
which allows temporary mutable access to a value while preserving the
guarantee that it will be eventually returned to its original owner. Note that
$0$ is excluded: the typing rules we provide can never produce a value with
permission $0$.

For working with the borrowing graded modality, terms are extended as follows:

(terms, extended) $\displaystyle\mathit{t}::=\ldots\mid\textbf{withBorrow}\
\mathit{t_{{\mathrm{1}}}}\ \mathit{t_{{\mathrm{2}}}}\mid\textbf{split}\
\mathit{t}\mid\textbf{join}\ \mathit{t_{{\mathrm{1}}}}\
\mathit{t_{{\mathrm{2}}}}$

The creation of mutable borrows is via withBorrow with the following typing:

$\displaystyle{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}:{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{\mathit{A}}&\;\,\Gamma_{{\mathrm{2}}}\vdash\mathit{t_{{\mathrm{2}}}}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{1}}}\mathit{A}\multimap{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{1}}}\mathit{B}\end{array}\\
\end{array}}{\Gamma_{{\mathrm{1}}}+\Gamma_{{\mathrm{2}}}\vdash\textbf{withBorrow}\
\mathit{t_{{\mathrm{1}}}}\
\mathit{t_{{\mathrm{2}}}}:{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{\mathit{B}}}\quad\!\!\!\textsc{{$\textsc{with}\with$}{}}}$

Here, we allow for a uniquely owned
${{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{\mathit{A}}$
value to be borrowed and manipulated in a mutable way by some function
$\mathit{t_{{\mathrm{2}}}}$ which expects a
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{1}}}\mathit{A}$
as input, so long as it returns the mutable borrow as a
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{1}}}\mathit{B}$
in the output so that the original owner can reclaim this as a unique
reference
(${{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{\mathit{B}}$).
By encapsulating the mutable borrow behaviour inside a continuation, we ensure
that it is impossible to construct a closed term with a borrowed type, which
means borrowed references to values must always eventually return full access
to the owner of said value.

#### Uniqueness as uniquely borrowed

We absorb the development of Section 4 by the inclusion of $*\in p$ and a type
identity
${{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{\mathit{A}}\equiv{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{\ast}}}\mathit{A}$.
Thus, the borrowing graded modality captures both (uniquely) owned and
borrowed values and hence functions polymorphic in their permission can range
over both kinds of ownership. Furthermore, this enables us to later define
operations that can work over uniquely owned or mutably borrowed values
without needing multiple primitives.

#### Immutable borrows

We generalise further to _immutable borrows_ , wherein multiple references to
a value can exist at any given time as long as they are unable to be mutated
(as otherwise this would violate memory safety and lead to, e.g., data races).
Mutable borrows are already graded with permission $1$, representing full
unfettered access to a value, so both reads and writes are permissible (shown
later for resources). The split and join constructs generalise mutable
borrows, with typing:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\Gamma\vdash\mathit{t}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}\mathit{A}\\
\end{array}}{\Gamma\vdash\textbf{split}\
\mathit{t}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{\frac{p}{2}}}}\mathit{A}\otimes{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{\frac{p}{2}}}}\mathit{A}}\quad\!\!\!\textsc{{$\textsc{split}$}{}}}\;\;\;\;{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\begin{array}[]{cc}\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}\mathit{A}&\;\,\Gamma_{{\mathrm{2}}}\vdash\mathit{t_{{\mathrm{2}}}}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{q}}}\mathit{A}\end{array}&\;\,p+q\leq
1\end{array}\\
\end{array}}{\Gamma_{{\mathrm{1}}}+\Gamma_{{\mathrm{2}}}\vdash\textbf{join}\
\mathit{t_{{\mathrm{1}}}}\
\mathit{t_{{\mathrm{2}}}}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p+q}}}\mathit{A}}\quad\!\!\!\textsc{{$\textsc{join}$}{}}}\end{array}$

where split takes a borrowed reference and splits it into two borrowed
references to the same value, each graded by half of the original
permission.444split could be generalised to produce a vector with any number
$n$ of
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{{p}/{\mathit{n}}}}}\mathit{A}$,
or even to arbitrary permissions $q$ and $q^{\prime}$ such that
$q+q^{\prime}=p$, but here we restrict to halving for simplicity. The dual
join (re)combines two borrows into one with their permissions added. Due to
the interfaces for manipulating resources (shown later), the type $A$ above
will always contain a resource identifier, so it is never possible to combine
references to two different values. The addition and halving operations are
defined only for fractions $f$, not $*$.

These rules do not encompass every detail of Rust’s intricate ownership
system; they instead aim to represent the _core_ concepts of ownership and
borrowing in such a way that they can integrate into an existing graded type
system, leaving room for potential extensions. In particular, as was mentioned
in Section 2, we only support _lexical_ lifetimes, meaning that there is a
class of programs which are accepted by Rust’s compiler but cannot be
represented in this calculus. We focus on being able to represent notions of
ownership _explicitly_ in the types, rather than using a complex static
analysis like Rust’s borrow checker to _infer_ which programs are safe.

The following code demonstrates how all of these new primitives can be put
together in a simple Granule program. This example makes use of a function
called observe which operates over borrowed values; the precise behaviour of
this function is elided, but it does not perform any unsafe behaviours such as
mutation and so it is polymorphic in the permission:

` Granule In persimmon, we _mutably_ borrow the value c as b, split this into
two _immutable_ borrows x and y, and apply the observe function to x before
rejoining the borrows and returning the value to its owner. The unsafe
patterns demonstrated by the viridian and cerulean examples in Section 2 are
also unrepresentable in Granule. It is impossible for two mutable borrows or
for a mutable borrow and an immutable borrow to coexist here, since splitting
a borrow must reduce the permission in its type by the nature of the split
primitive. We can, however, represent _reborrowing_ ; this simply involves
continuing to split immutable borrows further, where recovering the original
value now requires collecting all of the borrows once more. The following
example illustrates this. ` Granule

#### Resources

Enforcing which behaviours should be allowed for different permissions on a
given resource is mediated by said resource’s interface. We will give two in-
depth examples in this paper to demonstrate the flexibility of our ownership
and borrowing interface. The first is mutable arrays of floats that can be
created, read from, written to and deleted (each at differing levels of
access). This allows us to illustrate one of the key practical benefits of
ownership, which is that unique access to an owned value allows for safe
mutation (the original pun behind “Linear Types can Change the World” (Wadler,
1990)). The second example will be polymorphic references which store a
pointer to a value of any type. First, we extend our calculus with a primitive
type of resources:

(types, extended)
$\displaystyle\mathit{A}::=\ldots\mid\mathit{Res}_{\mathit{id}}\
\mathit{A}\mid\mathbb{N}\mid\mathbb{F}\qquad\mathit{Res}::=\mathsf{Array}\mid\mathsf{Ref}$

where $\mathbb{N}$ are natural numbers used for sizes and indices and
$\mathbb{F}$ are floating-point numbers, and resources $\mathit{Res}$ (ranging
over arrays or references for our purposes) are indexed by an identifier.
Then, our interface for mutable arrays provides the following primitives (with
built-in weakening):

$\displaystyle\begin{array}[]{lll}0\cdot\Gamma\vdash&\textbf{newArray}&:\mathbb{N}\multimap\exists\mathit{id}.{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{(\mathsf{Array}_{\mathit{id}}\
\mathbb{F})}\\
0\cdot\Gamma\vdash&\textbf{readArray}&:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathsf{Array}_{\mathit{id}}\
\mathbb{F})\multimap\mathbb{N}\multimap\mathbb{F}\otimes{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathsf{Array}_{\mathit{id}}\
\mathbb{F})\\
0\cdot\Gamma\vdash&\textbf{writeArray}&:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathsf{Array}_{\mathit{id}}\
\mathbb{F})\multimap\mathbb{N}\multimap\mathbb{F}\multimap{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathsf{Array}_{\mathit{id}}\
\mathbb{F})\quad(\textit{where}\ p\equiv 1\ \vee\ p\equiv\ast)\\
0\cdot\Gamma\vdash&\textbf{deleteArray}&:{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{(\mathsf{Array}_{\mathit{id}}\
\mathbb{F})}\multimap\mathsf{unit}\end{array}$

where, unless bound, $\mathit{id}$ and $p$ are metavariables for identifier
types and permissions respectively. Thus, we treat these primitives as part of
the typing rules rather than functions that are in scope.

This interface resembles Granule’s existing interface for array mutation using
modal uniqueness types, but with some crucial differences owing to the
introduction of borrowing. First, array types are now indexed by an identifier
pointing to a particular array object in the heap, generated by the
existential type in newArray and within the scope of the clone rule. This
allows us to keep track of which array is being referenced now that multiple
borrows pointing to the same array are permitted to exist. The other key
difference is that reading and writing no longer require sole ownership.
Reading can be carried out at any permission, since this is safe no matter how
many references exist, but writing is restricted to either a mutable-borrowed
or uniquely-owned array.

The interface for polymorphic references is similar, with primitives:

$\displaystyle\begin{array}[]{lll}0\cdot\Gamma\vdash&\textbf{newRef}&:\mathit{A}\multimap\exists\mathit{id}.{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{(\mathsf{Ref}_{\mathit{id}}\
\mathit{A})}\\
0\cdot\Gamma\vdash&\textbf{readRef}&:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathsf{Ref}_{\mathit{id}}\
({{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r+1}}}\mathit{A}))\multimap\mathit{A}\otimes{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathsf{Ref}_{\mathit{id}}\
({{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}))\\
0\cdot\Gamma\vdash&\textbf{swapRef}&:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathsf{Ref}_{\mathit{id}}\
\mathit{A})\multimap\mathit{A}\multimap\mathit{A}\otimes{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathsf{Ref}_{\mathit{id}}\
\mathit{A})\quad(\textit{where}\ p\equiv 1\ \vee\ p\equiv\ast)\\
0\cdot\Gamma\vdash&\textbf{deleteRef}&:{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{(\mathsf{Ref}_{\mathit{id}}\
\mathit{A})}\multimap\mathit{A}\end{array}$

The crucial differences follow from the value encapsulated in the reference
being of any type, rather than only floats which are inherently duplicable and
discardable. Thus, swapRef must enforce linear usage for both the existing and
new values. Similarly deleteRef must return the value in the reference to obey
linearity. The readRef primitive requires the value to be of a graded type
which permits the additional usage accrued with the appropriate type-level
accounting.

#### Resource allocators

Here, the restriction introduced on the promotion rule in Section 3 meaning
that ‘resource allocators’ are forbidden from being promoted becomes crucial
for ensuring soundness in the call-by-value setting of this work. Consider the
following snippet of Granule code (eliding packing and unpacking of
existentials), which would be allowed given unrestricted promotion:

` Granule ✗ On the first line, this program creates a reference x to a new
array of size $1$, but under a promotion, with the type explaining that we
want to use the resulting value twice (given by the explicit type signature
here). This promotion then allows two uses of the array on the second line.
Under a call-by-name semantics, as in previous work on embedding uniqueness
types in Granule (Marshall et al., 2022) (and accessible in Granule via the
extension language CBN), this program executes successfully and produces an
array which contains the value written on line 2. The key is that call-by-name
reduction substitutes the call to newArray into the two uses of the variable
x, and so these point to two entirely separate arrays. However, under the
call-by-value semantics of this paper (and Granule’s default), the first line
is fully evaluated, and so both uses of x point to the same array. Thus the
second line attempts to write to an array after it has been deleted, which
would cause a runtime error. In a call-by-value setting this program must not
be permitted. The solution we apply here (also used in recent work on graded
session types (Marshall and Orchard, 2022b)) is to syntactically restrict
promotion to terms which do not allocate resources, i.e., that do not use
newArray or newRef in a reduction position. The predicate
$\mathsf{resourceAllocator}(\mathit{t})$ classifies precisely these terms, as
a kind of specialised “value restriction”; note in particular that
$\neg\mathsf{resourceAllocator}(\lambda\mathit{x}.\textbf{newArray}\,\mathit{t})$
since reduction does not happen underneath an abstraction (Section 6 defines
the reduction semantics). The appendix includes the full inductive definition.
Other work resolves this same problem relating to promotion of resource
allocators through different techniques. Originally, the linear types
extension to Haskell got around this difficulty by only ever allocating
resources inside a specialised continuation, which is passed around at every
step until deallocation to prevent the allocator itself from ever being used
non-linearly. More recently, this strategy has been generalised by introducing
a “linear constraint” (Spiwack et al., 2022) called Linearly. This constraint,
which must itself be used in a linear fashion, is assumed whenever a new
resource is allocated. A continuation is still necessary for the initial
assumption of Linearly, but the same qualification may now be used generically
for varying resource types.

###  5.1. Equational theory

The with typing suggests a close relationship between
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{\ast}}}\mathit{A}$
and
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{1}}}\mathit{A}$.
By analogy to the notion of a relative monad used in prior work (Marshall et
al., 2022),
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{\ast}}}\mathit{A}$
acts as a ‘relative functor’ with regard to
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{1}}}\mathit{A}$,
where withBorrow equates to mapping a function involving mutable borrows onto
a function between uniquely owned values. The following axioms for functors
then hold:

($\with$unit) $\displaystyle\textbf{withBorrow}\
(\lambda\mathit{x}.\mathit{x})\ \mathit{t}$ $\displaystyle\equiv\mathit{t}$
($\with$assoc) $\displaystyle\textbf{withBorrow}\
(\lambda\mathit{x}.f\,(\mathit{g}\,\mathit{x}))\ \mathit{t}$
$\displaystyle\equiv\textbf{withBorrow}\ f\ (\textbf{withBorrow}\ \mathit{g}\
\mathit{t})$

The first axiom states that borrowing a reference to an owned value and simply
returning it via the identity function without making use of it is equivalent
to doing nothing at all, as one might expect. The second axiom is an
associativity axiom, giving us the result that borrowing a value to apply one
function and then borrowing the value again to apply a second function is
equivalent to simply borrowing the value once and applying the functions in
sequence.

Lastly, split and join have additional properties which form an isomorphism:

$\displaystyle(\textbf{let}\,(x,y)=(\textbf{split}\
\mathit{t})\,\textbf{in}\,(\textbf{join}\ \mathit{x}\
\mathit{y}))\equiv\mathit{t}\qquad\qquad\textbf{split}\ (\textbf{join}\
\mathit{t_{{\mathrm{1}}}}\
\mathit{t_{{\mathrm{2}}}})\equiv(\mathit{t_{{\mathrm{1}}}},\mathit{t_{{\mathrm{2}}}})$

###  5.2. Divide and conquer: partial views via distributive laws

One particularly useful borrowing pattern when writing practical programs is
the ability to take a composite data structure and borrow only _part_ of it,
such that the original owner retains access to the remaining structure. This
introduces the possibility of multiple threads working with parts of a data
structure in parallel, where it is no longer necessary to take ownership of
the full data structure in order to mutate the only part for which access is
required.

Our core calculus provides some capacity for structured data in the form of
product types. We introduce two additional constructs for distributing the
borrowing graded modality into and out of products, enabling the pattern of
partial borrowing:555One might wonder whether the $\Box_{r}$ modality also
distributes in this way; the answer is not in general, though some choices of
semiring permit this behaviour. This question has been explored in depth in
prior work (Hughes et al., 2021a).

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\Gamma\vdash\mathit{t}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathit{A}\otimes\mathit{B})\\\
\end{array}}{\Gamma\vdash\mathbf{push}\,\mathit{t}:({{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}\mathit{A})\otimes({{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}\mathit{B})}\quad\\!\\!\\!\textsc{{$\textsc{push}$}{}}}\;\;\;\;{\displaystyle\frac{\begin{array}[]{l}\Gamma\vdash\mathit{t}:({{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}\mathit{A})\otimes({{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}\mathit{B})\\\
\end{array}}{\Gamma\vdash\mathbf{pull}\,\mathit{t}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}(\mathit{A}\otimes\mathit{B})}\quad\\!\\!\\!\textsc{{$\textsc{pull}$}{}}}\end{array}$

We can derive an operation akin to withBorrow for borrowing one component of a
product: use push to move ownership onto the values inside the product, use
withBorrow to borrow the required component, and then once we are done, use
pull to recover the original pair. We demonstrate this concept in action with
the following example. We assume a function alter : & 1 Int $\rightarrow$ & 1
Int which operates over borrowed components of Colour, possibly mutating them
and so requiring a whole permission. We then employ this strategy for partial
borrowing:

` Granule This notion extends gracefully to structures containing more than
two components. For example, to borrow a single element from a unique tuple of
three values, leaving the remaining two values available to their original
owner, we can use nested products, e.g.
${{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{(\mathit{A}\otimes(\mathit{B}\otimes\mathit{C}))}$,
and push and pull to then access just one part, similarly to in indigo. We may
need to push twice in order to distribute the modality over the entire product
depending on which component we are borrowing, but in the same way as above we
can use withBorrow to extract the desired data (for example,
${{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{1}}}\mathit{A}$)
while applying pull to recover the remaining structure (in this case, of type
${{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{(\mathit{B}\otimes\mathit{C})}$).
Partial borrowing allows safe mutation of disjoint parts of a single data
structure _concurrently_ without risking a data race, e.g., using par for
concurrent threads (Marshall and Orchard, 2022b): ` Granule Building on this
core concept in the more expressive setting of Granule’s full type system
could involve notions such as borrowing from any algebraic data type, or
borrowing a ‘slice’ of multiple values. One low-hanging fruit is to extend the
push and pull primitives in order to derive generic operations for arbitrary
data structures, following patterns described in prior work (Hughes et al.,
2021b). We do not formalise this again here, but the approach allows for
writing programs like: ` Granule Here, the borrow modality is distributed into
the Maybe data type using a derived push operation. This general pattern for
partial borrowing relates closely to McBride’s notion of computing the
_derivative_ of a data type by finding its type of one-hole contexts (McBride,
2001), where the derivative describes the structure that remains after
borrowing one element. Under this interpretation, borrowing a slice of
multiple values would be akin to taking the derivative of a data type _with
respect to_ another type—an idea described elsewhere in recent work (Marshall
and Orchard, 2022c).

##  6. Semantics and Meta-theory

We define an operational semantics here for the calculus which serves to
further explain the details of arrays, mutation, copying, and borrowing. We
adapt the approach of Choudhury et al. (2021) and Marshall et al. (2022) for
giving an operational semantics to a graded system, with some degree of
accounting for grades and references in order to relate the dynamic semantics
back to the static semantics of typing (Section 6.3). With the exception of
Granule and Multi-Graded Featherweight Java (Bianchini et al., 2023), much of
the preceding work on operational models for graded systems is based on call-
by-name. Here we opted for call-by-value for the purpose of describing real-
world practical functional languages; call-by-name is prohibitively expensive
with unpredictable performance and poor interaction with side effects.

###  6.1. Preliminary definitions

#### Values

We first define the subset of terms that are _values_ in the semantics, i.e.,
normal forms (terms that have no further reduction), via the grammar:

(value terms sub-grammar)
$\displaystyle\mathit{v}::=(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\mid()\mid[\mathit{v}]\mid\lambda\mathit{x}.\mathit{t}\mid\mathit{n}\mid
p\mid\textbf{pack}\ \langle{\mathit{id},\mathit{v}}\rangle$

including pairs of values, the unit value, boxed values, abstractions, natural
numbers $n$, or primitives $p$ which may also be partially applied to other
values: newArray, readArray, $\textbf{readArray}\,\mathit{v}$, etc.

#### Runtime terms and typing

We extend the syntax of terms (and values) with several runtime
representations which appear only in the semantics, i.e., they cannot be
written by users in programs:

(runtime terms) $\displaystyle\mathit{t}$
$\displaystyle::=\ldots\mid\ast\mathit{t}\mid\textbf{unborrow}\
\mathit{t}\mid\mathit{ref}$ (runtime values) $\displaystyle\mathit{v}$
$\displaystyle::=\ldots\mid\ast\mathit{v}\mid\textbf{unborrow}\
\mathit{v}\mid\mathit{ref}$

where $\ast\mathit{t}$ represents unique and borrowed terms,
$\textbf{unborrow}\ \mathit{t}$ is the inverse to borrowed terms (used to
implement withBorrow), and $\mathit{ref}$ are references to resources bound in
the heap.

In order to type runtime terms with references, the syntax of contexts is
extended to include assumptions $\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A}$ which are treated as a different syntactic category of variables.
A _runtime context_ $\gamma$ is a context containing only references, i.e.:
$\gamma::=\emptyset\mid\gamma,\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A}$.

Context scalar multiplication and addition extend as follows (eliding a
symmetric case for brevity):

$\displaystyle(\Gamma,\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A})+(\Gamma^{\prime},\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A})$
$\displaystyle=(\Gamma+\Gamma^{\prime}),\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A}$ $\displaystyle(\Gamma,\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A})+\Gamma^{\prime}$
$\displaystyle=(\Gamma+\Gamma^{\prime}),\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A}\;(\textit{where}\ \mathit{ref}\not\in\Gamma^{\prime})$ (context
operations) $\displaystyle
r\cdot(\Gamma,\mathit{ref}:\mathit{Res}_{\mathit{id}}\ \mathit{A})$
$\displaystyle=(r\cdot\Gamma),\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A}$

Runtime terms are typed by the following rules:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\gamma\vdash\mathit{t}:\mathit{A}\\
\end{array}}{0\cdot\Gamma,\gamma\vdash\ast\mathit{t}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{p}}}\mathit{A}}\quad\!\!\!\textsc{{$\textsc{nec}$}{}}}\;{\displaystyle\frac{\begin{array}[]{l}\Gamma\vdash\mathit{t}:{{\color[rgb]{0.1328125,0.3984375,0.1328125}\definecolor[named]{pgfstrokecolor}{rgb}{0.1328125,0.3984375,0.1328125}\&_{1}}}\mathit{A}\\
\end{array}}{\Gamma\vdash\textbf{unborrow}\
\mathit{t}:{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{\mathit{A}}}\quad\!\!\!\textsc{{$\textsc{unborrow}$}{}}}\;{\displaystyle\frac{\begin{array}[]{l}\end{array}}{0\cdot\Gamma,\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A}\vdash\mathit{ref}:\mathit{Res}_{\mathit{id}}\
\mathit{A}}\quad\!\!\!\textsc{{$\textsc{ref}$}{}}}\end{array}$

#### Heaps and configurations

Heaps map program variables to values (our semantics does not use syntactic
substitution), and also map references to identifiers $\mathit{id}$ and
identifiers to values:

(heaps) $\displaystyle H$ $\displaystyle::=\emptyset\mid
H,\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{r}}\mathit{v}:\mathit{A}\mid
H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id}\mid
H,\mathit{id}\mapsto v_{r}$ (heap resource terms) $\displaystyle v_{r}$
$\displaystyle::=\textbf{arr}\mid\gamma\vdash\mathit{v}:\mathit{A}\qquad\textbf{arr}::=\mathsf{init}\mid\textbf{arr}[\mathit{n}]=\mathit{v}$

Thus, a heap can be extended in three ways: (1) with an assignment of a
program variable $x$ to a value $\mathit{v}$, storing the grade of the
variable
${{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}r}}$
(which comes from the typing) with the type of the value; (2) with an
assignment of a reference $\mathit{ref}$ to an identifier $id$ with permission
${{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}p}}$;
(3) with an assignment of an identifier $id$ to a resource term. Identifiers
and references are separated since we may need multiple references to point to
the same identifier, e.g., in the case of immutable borrows (one can think of
identifiers like abstract memory addresses in the semantics).

Array terms arr in the heap are either an empty array $\mathsf{init}$ or an
array storing value $\mathit{v}$ at index $\mathit{n}$.

A _configuration_ comprises a pair of a _heap_ $H$ and a term $\mathit{t}$,
written as $H\vdash\mathit{t}$, where
$\mathsf{fv}(v)\subseteq\mathsf{dom}(H)$, and
$\mathsf{refs}(\mathit{v})\subseteq\mathsf{dom}(H)$ (where $\mathsf{refs}$ is
the set of all resource references $\mathit{ref}$ in the term).

###  6.2. Single-step reduction

Single-step reductions map source configurations to target configurations,
with the judgment:

$\displaystyle
H_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}\,\leadsto_{s}\,H_{{\mathrm{2}}}\vdash\mathit{t_{{\mathrm{2}}}}$

where $H_{{\mathrm{1}}}$ and $H_{{\mathrm{2}}}$ are input and output heaps
respectively, $\mathit{t_{{\mathrm{1}}}}$ is the source term and
$\mathit{t_{{\mathrm{2}}}}$ the target. The grade $s$ denotes the _usage
context_ of this rule. We explain the reduction rules for our operational
semantics in detail. Throughout, $x\#\overline{t}$ means that $x$ is a fresh
name with respect to some terms $\overline{t}$.

#### Lambda calculus

The $\lambda$-calculus core of the operational semantics has rules:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\exists
r^{\prime}.\ s+r^{\prime}\sqsubseteq r\\
\end{array}}{H,\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{r}}\mathit{v}:\mathit{A}\vdash\mathit{x}\,\leadsto_{s}\,H,\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{r}}\mathit{v}:\mathit{A}\vdash\mathit{v}}\quad\!\!\!\textsc{{$\leadsto_{{\textsc{var}}}$}{}}}\quad{\displaystyle\frac{\begin{array}[]{l}\mathit{y}\#\{H,\mathit{v},\mathit{t}\}\\
\end{array}}{H\vdash(\lambda\mathit{x}.\mathit{t})\,\mathit{v}\,\leadsto_{s}\,H,\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{s}}\mathit{v}:\mathit{A}\vdash\mathit{t}[\mathit{y}/\mathit{x}]}\quad\!\!\!\textsc{{$\leadsto_{\beta}$}{}}}\\[15.00002pt]
{\displaystyle\frac{\begin{array}[]{l}H\vdash\mathit{t_{{\mathrm{1}}}}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}_{{\mathrm{1}}}}\\
\end{array}}{H\vdash\mathit{t_{{\mathrm{1}}}}\,\mathit{t_{{\mathrm{2}}}}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}_{{\mathrm{1}}}}\,\mathit{t_{{\mathrm{2}}}}}\quad\!\!\!\textsc{{$\leadsto_{\textsc{appL}}$}{}}}\quad{\displaystyle\frac{\begin{array}[]{l}H\vdash\mathit{t_{{\mathrm{2}}}}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}_{{\mathrm{2}}}}\\
\end{array}}{H\vdash\mathit{v}\,\mathit{t_{{\mathrm{2}}}}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{v}\,\mathit{t^{\prime}_{{\mathrm{2}}}}}\quad\!\!\!\textsc{{$\leadsto_{\textsc{appR}}$}{}}}\end{array}$

The rules for function application are fairly standard. In the
$\leadsto_{{\textsc{var}}}$ rule, a variable $x$ is reduced to a value $v$
which was assigned to $x$ in the heap. The annotation $r$ is preserved in the
output heap, with the side condition in the premise ensuring that the grade
$r$ will be enough to capture the usage $s$ required by the reduction. In the
$\leadsto_{\beta}$ rule, rather than using a substitution to enact
$\beta$-reduction, the resulting term is the body of the function $t$ with the
heap extended with a $y$ assigned to the argument value $v$. The grade $s$
(parameterising the reduction) annotates $x$ in the heap.

#### Existential types and names

The semantics of existentials is standard, with a beta rule:

$\displaystyle{\displaystyle\frac{\begin{array}[]{l}\mathit{y}\#\{H,\mathit{v},\mathit{t}\}\\
\end{array}}{H\vdash\textbf{unpack}\
\langle{\mathit{id},\mathit{x}}\rangle=\textbf{pack}\
\langle{\mathit{id^{\prime}},\mathit{v}}\rangle\ \textbf{in}\
\mathit{t}\,\leadsto_{s}\,H,\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{r}}\mathit{v}\vdash\mathit{t}[\mathit{y}/\mathit{x}]}\quad\!\!\!\textsc{{$\leadsto_{\exists\beta}$}{}}}$

and two standard congruence rules for $\mathsf{pack}$ and $\mathsf{unpack}$
(elided for brevity).

#### Tensors and units

Tensor products have the following rules for their introduction and
elimination forms, with three congruence rules and one $\beta$-rule:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}H\vdash\mathit{t_{{\mathrm{1}}}}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}_{{\mathrm{1}}}}\\
\end{array}}{H\vdash(\mathit{t_{{\mathrm{1}}}},\mathit{t_{{\mathrm{2}}}})\,\leadsto_{s}\,H^{\prime}\vdash(\mathit{t^{\prime}_{{\mathrm{1}}}},\mathit{t_{{\mathrm{2}}}})}\quad\!\!\!\textsc{{$\leadsto_{\otimes\textsc{L}}$}{}}}\;{\displaystyle\frac{\begin{array}[]{l}H\vdash\mathit{t_{{\mathrm{1}}}}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}_{{\mathrm{1}}}}\\
\end{array}}{H\vdash\textbf{let}\,(x,y)=\mathit{t_{{\mathrm{1}}}}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}\,\leadsto_{s}\,H^{\prime}\vdash\textbf{let}\,(x,y)=\mathit{t^{\prime}_{{\mathrm{1}}}}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}}\quad\!\!\!\textsc{{$\leadsto_{\textsc{let}\otimes}$}{}}}\\[15.00002pt]
{\displaystyle\frac{\begin{array}[]{l}H\vdash\mathit{t_{{\mathrm{2}}}}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}_{{\mathrm{2}}}}\\
\end{array}}{H\vdash(\mathit{v},\mathit{t_{{\mathrm{2}}}})\,\leadsto_{s}\,H^{\prime}\vdash(\mathit{v},\mathit{t^{\prime}_{{\mathrm{2}}}})}\quad\!\!\!\textsc{{$\leadsto_{\otimes\textsc{R}}$}{}}}\;{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\mathit{x^{\prime}}\#\{H,\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}},\mathit{t}\}&\;\,\mathit{y^{\prime}}\#\{H,\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}},\mathit{t}\}\end{array}\\
\end{array}}{H\vdash\textbf{let}\,(x,y)=(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})\,\textbf{in}\,\mathit{t}\,\leadsto_{s}\,H,\mathit{x^{\prime}}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{s}}\mathit{v_{{\mathrm{1}}}}:\mathit{A},\mathit{y^{\prime}}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{s}}\mathit{v_{{\mathrm{2}}}}:\mathit{B}\vdash\mathit{t}[\mathit{y^{\prime}}/\mathit{y}][\mathit{x^{\prime}}/\mathit{x}]}\quad\!\!\!\textsc{{$\leadsto_{\otimes\beta}$}{}}}\end{array}$

In the case of ($\leadsto_{\otimes\beta}$), we extend the heap with
assignments for (fresh names) $x^{\prime}$ and $y^{\prime}$ to
$\mathit{v_{{\mathrm{1}}}}$ and $\mathit{v_{{\mathrm{2}}}}$ respectively,
continuing on with the body term $\mathit{t}$. Similarly to the $\beta$-rule
for functions, the freshening avoids variable capture. We elide the rules for
the unit type as they are similar.

###### Example 6.1.

The following gives a reduction sequence for the term
$(\lambda\mathit{x}.(\mathit{x},\mathit{y}))\,(\mathit{v},\mathit{y})$ under a
heap
$H=\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{2}}\mathit{v}:\mathit{A}$,
until a normal form is reached:

$\displaystyle\begin{array}[]{rll}&\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{2}}\mathit{v}:\mathit{A}\vdash(\lambda\mathit{x}.(\mathit{x},\mathit{y}))\,(\mathit{v},\mathit{y})&\\
(\textit{$\leadsto_{\textsc{appL}}${},$\leadsto_{\otimes\textsc{R}}${},$\leadsto_{{\textsc{var}}}${}})\leadsto_{1}&\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{2}}\mathit{v}:\mathit{A}\vdash(\lambda\mathit{x}.(\mathit{x},\mathit{y}))\,(\mathit{v},\mathit{v})&\\
(\textsc{$\leadsto_{\beta}${}})\leadsto_{1}&\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{2}}\mathit{v}:\mathit{A},\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{1}}(\mathit{v},\mathit{v}):(\mathit{A}\otimes\mathit{A})\vdash(\mathit{x},\mathit{y})&\\
(\textsc{$\leadsto_{\textsc{appL}}${},$\leadsto_{\otimes\textsc{L}}${},$\leadsto_{{\textsc{var}}}${}})\leadsto_{1}&\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{2}}\mathit{v}:\mathit{A},\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{1}}(\mathit{v},\mathit{v}):(\mathit{A}\otimes\mathit{A})\vdash((\mathit{v},\mathit{v}),\mathit{y})&\end{array}$

#### Graded modalities

The rules for graded modalities are structured similarly to the standard
lambda calculus rules above, but we need to do some additional management of
grades in the heap.

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}H\vdash\mathit{t}\,\leadsto_{s*r}\,H^{\prime}\vdash\mathit{t^{\prime}}&\;\,\Gamma\vdash[\mathit{t}]:{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}\end{array}\\
\end{array}}{H\vdash[\mathit{t}]\,\leadsto_{s}\,H^{\prime}\vdash[\mathit{t^{\prime}}]}\quad\!\!\!\textsc{{$\leadsto_{\square}$}{}}}\;{\displaystyle\frac{\begin{array}[]{l}H\vdash\mathit{t_{{\mathrm{1}}}}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}_{{\mathrm{1}}}}\\
\end{array}}{H\vdash\textbf{let}\,[\mathit{x}]=\mathit{t_{{\mathrm{1}}}}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}\,\leadsto_{s}\,H^{\prime}\vdash\textbf{let}\,[\mathit{x}]=\mathit{t^{\prime}_{{\mathrm{1}}}}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}}\quad\!\!\!\textsc{{$\leadsto_{\textsc{let}\square}$}{}}}\\[12.50002pt]
{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\Gamma\vdash[\mathit{v}]:{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}&\;\,\mathit{y}\#\{H,\mathit{v},\mathit{t}\}\end{array}\\
\end{array}}{H\vdash\textbf{let}\,[\mathit{x}]=[\mathit{v}]\,\textbf{in}\,\mathit{t}\,\leadsto_{s}\,H,\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{(s*r)}}\mathit{v}:\mathit{A}\vdash\mathit{t}[\mathit{y}/\mathit{x}]}\quad\!\!\!\textsc{{$\leadsto_{\square\beta}$}{}}}\end{array}$

In the $\leadsto_{\square}$ rule, to construct a reduction with the required
grade $s$ then we need to be able to reduce inside the box at grade $s*r$, to
account for the additional usage required by the modality’s $r$ grade. In the
$\leadsto_{\square\beta}$ rule, the $x$ in the heap is annotated not only with
$s$ as in the regular $\leadsto_{\beta}$ rule but with $s*r$, again to account
for the additional usage the modality requires.

#### Arrays

In the body of the paper we present only the reduction rules for arrays, for
brevity; the corresponding (and very similar) rules for polymorphic references
are included in the appendix. Note that we do not explicitly track the sizes
of arrays in our semantics, for simplicity. New arrays are created by the
newArray primitive, with reduction rule:

$\displaystyle{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\mathit{ref}\#H&\;\,\mathit{id}\#H\end{array}\\
\end{array}}{H\vdash\textbf{newArray}\,\mathit{n}\,\leadsto_{s}\,H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{1}}\mathit{id},\mathit{id}\mapsto\mathsf{init}\vdash\textbf{pack}\
\langle{\mathit{id},\ast\mathit{ref}}\rangle}\quad\!\!\!\textsc{{$\leadsto_{\textsc{newArray}}$}{}}}$

where $\mathit{ref}$ and $id$ are fresh for the heap $H$. The resulting array
is initialised to the empty array ($\mathsf{init}$), and the result is a
unique array reference $\ast\mathit{ref}$. In the heap, $\mathit{ref}$ is
marked with the whole permission $1$. Arrays are read and written via:

$\displaystyle{\displaystyle\frac{\begin{array}[]{l}\end{array}}{H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id},\mathit{id}\mapsto\textbf{arr}[\mathit{i}]=\mathit{v}\vdash\textbf{readArray}\,(\ast\mathit{ref})\,\mathit{i}\,\leadsto_{s}\,H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id},\mathit{id}\mapsto\textbf{arr}[\mathit{i}]=\mathit{v}\vdash(\mathit{v},\ast\mathit{ref})}\quad\!\!\!\textsc{{$\leadsto_{\textsc{readArray}}$}{}}}$
$\displaystyle{\displaystyle\frac{\begin{array}[]{l}\end{array}}{H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id},\mathit{id}\mapsto\textbf{arr}\vdash\textbf{writeArray}\,(\ast\mathit{ref})\,\mathit{i}\,\mathit{v}\,\leadsto_{s}\,H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id},\mathit{id}\mapsto\textbf{arr}[\mathit{i}]=\mathit{v}\vdash\ast\mathit{ref}}\quad\!\!\!\textsc{{$\leadsto_{\textsc{writeArray}}$}{}}}$

For writeArray, $p$ should be $1$ or $\ast$, but this is mediated by the type
system rather than being enforced in the semantics; the following rule is
similar in this regard for deleting unique arrays:

$\displaystyle{\displaystyle\frac{\begin{array}[]{l}\end{array}}{H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id},\mathit{id}\mapsto\textbf{arr}\vdash\textbf{deleteArray}\,(\ast\mathit{ref})\,\leadsto_{s}\,H\vdash()}\quad\!\!\!\textsc{{$\leadsto_{\textsc{deleteArray}}$}{}}}$

#### Sharing and cloning

Sharing reduces permissions to $0$ and cloning involves copying heap terms:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}H\vdash\mathit{t}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}}\\
\end{array}}{H\vdash\mathbf{share}\,\mathit{t}\,\leadsto_{s}\,H^{\prime}\vdash\mathbf{share}\,\mathit{t^{\prime}}}\quad\!\!\!\textsc{{$\leadsto_{\textsc{share}}$}{}}}\quad{\displaystyle\frac{\begin{array}[]{l}\mathsf{dom}(H)\equiv\mathsf{refs}(\mathit{v})\\
\end{array}}{H,H^{\prime}\vdash\mathbf{share}\,(\ast\mathit{v})\,\leadsto_{s}\,({{[H]}_{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}0}}}),H^{\prime}\vdash[\mathit{v}]}\quad\!\!\!\textsc{{$\leadsto_{\textsc{share}\beta}$}{}}}\\[12.50002pt]
{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\begin{array}[]{cc}\begin{array}[]{cc}\Gamma\vdash[\mathit{v}]:{{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\Box_{r}}}\mathit{A}&\;\,\mathsf{dom}(H^{\prime})\equiv\mathsf{refs}(\mathit{v})\end{array}&\;\,(H^{\prime\prime},\theta,\overline{\mathit{id}})=\mathsf{copy}(H^{\prime})\end{array}&\;\,\mathit{y}\#\{H,\mathit{v},\mathit{t}\}\end{array}\\
\end{array}}{H,H^{\prime}\vdash\mathbf{clone}\,[\mathit{v}]\,\textbf{as}\,\mathit{x}\,\textbf{in}\,\mathit{t_{{\mathrm{2}}}}\,\leadsto_{s}\,H,H^{\prime},H^{\prime\prime},\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{s}}\textbf{pack}\
\langle{\overline{\mathit{id}},\ast(\theta(\mathit{v}))}\rangle:{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast\mathit{A}}}\vdash\mathit{t_{{\mathrm{2}}}}[\mathit{y}/\mathit{x}]}\quad\!\!\!\textsc{{$\leadsto_{\textsc{clone}\beta}$}{}}}\end{array}$

In the $\leadsto_{\textsc{share}\beta}$ rule, the incoming heap is split into
two parts, where $H$ is such that it provides the allocations for all resource
references in $\mathit{v}$ (enforced by the premise). The unique value
$\ast\mathit{v}$ is wrapped in the graded box modality in the result as
$[\mathit{v}]$, and thus all its references are now annotated with $0$ in the
heap via
$({{[H]}_{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}0}}})$,
e.g.:

$\displaystyle H^{\prime},\mathit{id}\mapsto
v_{r},\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{1}}\mathit{id}\vdash\mathbf{share}\,(\ast\mathit{a})\leadsto
H^{\prime},\mathit{id}\mapsto
v_{r},\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{0}}\mathit{id}\vdash[\mathit{ref}]\mid\emptyset$

The $\leadsto_{\textsc{clone}\beta}$ rule enacts a ‘deep copy’, where
$\mathsf{dom}(H^{\prime})\equiv\mathsf{refs}(\mathit{v})$ marks the part of
the heap with resource references coming from $\mathit{v}$. Then
$\mathsf{copy}(H^{\prime})$ copies the resources in this part of the heap,
creating a heap fragment $H^{\prime\prime}$ and a renaming operator $\theta$
which maps from old references to new copied references. This renaming is
applied to $\mathit{v}$ in the freshly bound unique variable $x$, such that
the value $\ast(\theta(\mathit{v}))$ refers to any newly copied resources.
Lastly, we pack the renamed unique value with new identifiers
$\overline{\mathit{id}}$ generated by $\mathsf{copy}$.

We elide the straightforward congruence rule for clone.

#### Borrowing

We elide the congruence rules for withBorrow which ensure that we reduce the
two argument terms left to right until they are values, after which we can
reduce as follows:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\mathit{y}\#\{H,\mathit{v},\mathit{t}\}\\
\end{array}}{H\vdash\textbf{withBorrow}\ (\lambda\mathit{x}.\mathit{t})\
(\ast\mathit{v})\,\leadsto_{s}\,H,\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{s}}(\ast\mathit{v})\vdash\textbf{unborrow}\
\mathit{t}[\mathit{y}/\mathit{x}]}\quad\!\!\!\textsc{{$\leadsto_{\textsc{with}\with}$}{}}}\end{array}$

Here, the $\beta$-reduction that comes from applying the function
$\lambda\mathit{x}.\mathit{t}$ to the value $\mathit{v}$ is enacted as a
substitution, with the resulting value being wrapped inside the uniqueness
wrapper as a representation of the fact that within the context of withBorrow
it is now a borrowed term.

For a term to escape withBorrow it must eventually be ‘unborrowed’; the
runtime term unborrow encapsulating the resulting term represents this idea,
and obeys the following rules:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}H\vdash\mathit{t}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}}\\
\end{array}}{H\vdash\textbf{unborrow}\
\mathit{t}\,\leadsto_{s}\,H^{\prime}\vdash\textbf{unborrow}\
\mathit{t^{\prime}}}\quad\!\!\!\textsc{{$\leadsto_{\textsc{unborrow}}$}{}}}\quad{\displaystyle\frac{\begin{array}[]{l}\end{array}}{H\vdash\textbf{unborrow}\
(\ast\mathit{v})\,\leadsto_{s}\,H\vdash\ast\mathit{v}}\quad\!\!\!\textsc{{$\leadsto_{\textsc{un}\with}$}{}}}\end{array}$

Aside from the congruence, which is standard, the
$\leadsto_{\textsc{un}\with}$ rule simply unwraps the value from the $\with$
modality, allowing the semantics to treat said value as a unique term once
more.

#### Push and pull

The reduction rules for push and pull are fairly simple; they simply
distribute the modality into or out of the product term in a way that matches
the typing of the given rule.

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\end{array}}{H\vdash\mathbf{push}\,(\ast(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}}))\,\leadsto_{s}\,H\vdash(\ast\mathit{v_{{\mathrm{1}}}},\ast\mathit{v_{{\mathrm{2}}}})}\quad\!\!\!\textsc{{$\leadsto_{\textsc{push}\ast}$}{}}}\quad{\displaystyle\frac{\begin{array}[]{l}\end{array}}{H\vdash\mathbf{pull}\,(\ast\mathit{v_{{\mathrm{1}}}},\ast\mathit{v_{{\mathrm{2}}}})\,\leadsto_{s}\,H\vdash\ast(\mathit{v_{{\mathrm{1}}}},\mathit{v_{{\mathrm{2}}}})}\quad\!\!\!\textsc{{$\leadsto_{\textsc{pull}\ast}$}{}}}\end{array}$

The heap is left unchanged. The above rules are for unique terms; there are
two equivalent rules for push and pull on borrowed terms, but these are
identical aside from the modality on the term.

Push and pull also have congruence rules which are straightforward and elided.

#### Split and join

Join and split also have congruence rules which are straightforward and
elided. There are two primary reduction rules for each of split and join: one
for the case where the terms are references and one for the case where the
terms are pairs of values:

$\displaystyle\begin{array}[]{c}{\displaystyle\inferrule*[right=\,\!\!\!\textsc{{$\leadsto_{\textsc{split}\textsc{Ref}}$}{}}]{\begin{array}[]{l}\begin{array}[]{cc}\mathit{ref_{{\mathrm{1}}}}\#H&\;\,\mathit{ref_{{\mathrm{2}}}}\#H\end{array}\\
\end{array}}{H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id},\mathit{id}\mapsto\mathit{v}\vdash\textbf{split}\
(\ast\mathit{ref})\,\leadsto_{s}\,H,\mathit{ref_{{\mathrm{1}}}}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{\frac{p}{2}}}\mathit{id},\mathit{ref_{{\mathrm{2}}}}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{\frac{p}{2}}}\mathit{id},\mathit{id}\mapsto\mathit{v}\vdash(\ast\mathit{ref_{{\mathrm{1}}}},\ast\mathit{ref_{{\mathrm{2}}}})}}\\[10.00002pt]
{\displaystyle\inferrule*[right=\,\!\!\!\textsc{{$\leadsto_{\textsc{join}\textsc{Ref}}$}{}}]{\begin{array}[]{l}\mathit{ref}\#H\\
\end{array}}{H,\mathit{ref_{{\mathrm{1}}}}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id},\mathit{ref_{{\mathrm{2}}}}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{q}}\mathit{id},\mathit{id}\mapsto\mathit{v}\vdash\textbf{join}\
(\ast\mathit{ref_{{\mathrm{1}}}})\
(\ast\mathit{ref_{{\mathrm{2}}}})\,\leadsto_{s}\,H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{(p+q)}}\mathit{id},\mathit{id}\mapsto\mathit{v}\vdash\ast\mathit{ref}}}\\[10.00002pt]
{\displaystyle\inferrule*[right=\,\!\!\!\textsc{{$\leadsto_{\textsc{split}\otimes}$}{}}]{\begin{array}[]{l}H\vdash\textbf{split}\
(\ast\mathit{v})\,\leadsto_{s}\,H^{\prime}\vdash(\ast\mathit{v_{{\mathrm{1}}}},\ast\mathit{v_{{\mathrm{2}}}})\\
H^{\prime}\vdash\textbf{split}\
(\ast\mathit{w})\,\leadsto_{s}\,H^{\prime\prime}\vdash(\ast\mathit{w_{{\mathrm{1}}}},\ast\mathit{w_{{\mathrm{2}}}})\\
\end{array}}{H\vdash\textbf{split}\
(\ast(\mathit{v},\mathit{w}))\,\leadsto_{s}\,H^{\prime\prime}\vdash(\ast(\mathit{v_{{\mathrm{1}}}},\mathit{w_{{\mathrm{1}}}}),\ast(\mathit{v_{{\mathrm{2}}}},\mathit{w_{{\mathrm{2}}}}))}}{\displaystyle\inferrule*[right=\,\!\!\!\textsc{{$\leadsto_{\textsc{join}\otimes}$}{}}]{\begin{array}[]{l}H\vdash\textbf{join}\
(\ast\mathit{v_{{\mathrm{1}}}})\
(\ast\mathit{v_{{\mathrm{2}}}})\,\leadsto_{s}\,H^{\prime}\vdash\ast\mathit{v}\\
H^{\prime}\vdash\textbf{join}\ (\ast\mathit{w_{{\mathrm{1}}}})\
(\ast\mathit{w_{{\mathrm{2}}}})\,\leadsto_{s}\,H^{\prime\prime}\vdash\ast\mathit{w}\\
\end{array}}{H\vdash\textbf{join}\
(\ast(\mathit{v_{{\mathrm{1}}}},\mathit{w_{{\mathrm{1}}}}))\
(\ast(\mathit{v_{{\mathrm{2}}}},\mathit{w_{{\mathrm{2}}}}))\,\leadsto_{s}\,H^{\prime\prime}\vdash\ast(\mathit{v},\mathit{w})}}\end{array}$

In the reference case, split removes the initial reference from the heap and
generates two fresh references pointing to the same identifier. These are each
annotated with half of the permission belonging to the original reference, to
match the typing. As one might expect, join for references behaves dually; it
deletes two existing references from the heap, and generates one fresh
reference, with its permission being the sum of the constituent parts.

For pairs, the reduction rules are defined inductively: as long as we can
split or join on the two components of the pair, we are allowed to reduce on
the overall pair itself. In this way, we construct a reduction which ensures
that all references contained within the pair are split or joined as required,
no matter how deeply nested the pair may be.

#### Multi-step reductions

Lastly, we define a relation that composes single-step reductions into a
sequence of reductions, called a multi-reduction:

$\displaystyle{\displaystyle\frac{\begin{array}[]{l}\end{array}}{H\vdash\mathit{t}\
\Rightarrow_{s}\
H\vdash\mathit{t}}\quad\!\!\!\textsc{{$\textsc{refl}$}{}}}\quad{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}H\vdash\mathit{t_{{\mathrm{1}}}}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t_{{\mathrm{2}}}}&\;\,H^{\prime}\vdash\mathit{t_{{\mathrm{2}}}}\
\Rightarrow_{s}\ H^{\prime\prime}\vdash\mathit{t_{{\mathrm{3}}}}\end{array}\\
\end{array}}{H\vdash\mathit{t_{{\mathrm{1}}}}\ \Rightarrow_{s}\
H^{\prime\prime}\vdash\mathit{t_{{\mathrm{3}}}}}\quad\!\!\!\textsc{{$\textsc{ext}$}{}}}$

###  6.3. Theorems

We now consider the relationship between typing and the operational semantics.
First, we must build a foundation via checking some preliminary results and
noting some crucial definitions.

Two useful results, which extend those found elsewhere in the literature, are
that substitution is admissible for our calculus, coming in both linear and
graded variants:

###### Lemma 6.2 (Linear substitution is admissible, extending (Orchard et
al., 2019)).

If $\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{1}}}}:\mathit{A}$ and
$\Gamma_{{\mathrm{2}}},\mathit{x}:\mathit{A}\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{B}$
then
$\Gamma_{{\mathrm{2}}}+\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{2}}}}[\mathit{t_{{\mathrm{1}}}}/\mathit{x}]:\mathit{B}$.

###### Lemma 6.3 (Graded substitution is admissible, extending (Orchard et
al., 2019)).

If
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}[\Gamma_{{\mathrm{1}}}]}\vdash\mathit{t_{{\mathrm{1}}}}:\mathit{A}$
and
$\Gamma_{{\mathrm{2}}},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{r}}\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{B}$
(where
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}[\Gamma_{{\mathrm{1}}}]}$
represents a context $\Gamma_{{\mathrm{1}}}$ containing only graded
assumptions) and $\neg\mathsf{resourceAllocator}(\mathit{t_{{\mathrm{1}}}})$
then
$\Gamma_{{\mathrm{2}}}+r\cdot\Gamma_{{\mathrm{1}}}\vdash\mathit{t_{{\mathrm{2}}}}[\mathit{t_{{\mathrm{1}}}}/\mathit{x}]:\mathit{B}$.

#### Type safety

Key to ensuring type safety is the notion of _heap compatibility with a typing
context_.

###### Definition 6.4 (Heap compatibility).

A heap $H$ is compatible with free variable context $\Gamma$, denoted
$H\bowtie\Gamma$, if the grades in the heap match those of the context, and
any values stored in the heap have their resources accounted for in the rest
of the heap. The relation is defined inductively over the syntax of heaps and
contexts:

$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\end{array}}{\emptyset\bowtie\emptyset}\quad\!\!\!\textsc{{{empty}}{}}}\;\;{\displaystyle\frac{\begin{array}[]{l}H,\mathit{id}\mapsto
v_{r}\bowtie\Gamma\\
\end{array}}{H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id},\mathit{id}\mapsto
v_{r}\bowtie(\Gamma,\mathit{a}:\mathit{Res}_{\mathit{id}}\
\mathit{A})}\quad\!\!\!\textsc{{{extRef}}{}}}\;\;{\displaystyle\frac{\begin{array}[]{l}H\bowtie\emptyset\\
\end{array}}{H,\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id}\bowtie\emptyset}\quad\!\!\!\textsc{{{GCArr}}{}}}\end{array}$
$\displaystyle\begin{array}[]{c}{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\begin{array}[]{cc}\begin{array}[]{cc}H\bowtie\Gamma+s\cdot\Gamma^{\prime}&\;\,\mathit{x}\not\in\mathsf{dom}(H)\end{array}&\;\,\Gamma^{\prime}\vdash\mathit{v}:\mathit{A}\end{array}&\;\,\exists
r^{\prime}.\ s+r^{\prime}\equiv r\end{array}\\
\end{array}}{(H,\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{r}}\mathit{v}:\mathit{A})\bowtie(\Gamma,{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{s}})}\quad\!\!\!\textsc{{{ext}}{}}}\\[12.50002pt]
{\displaystyle\frac{\begin{array}[]{l}\begin{array}[]{cc}\begin{array}[]{cc}\begin{array}[]{cc}H\bowtie\Gamma+\Gamma^{\prime}&\;\,\mathit{x}\not\in\mathsf{dom}(H)\end{array}&\;\,\Gamma^{\prime}\vdash\mathit{v}:\mathit{A}\end{array}&\;\,\exists
r^{\prime}.\ 1+r^{\prime}\equiv r\end{array}\\
\end{array}}{(H,\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{r}}\mathit{v}:\mathit{A})\bowtie(\Gamma,\mathit{x}:\mathit{A})}\quad\!\!\!\textsc{{{extLin}}{}}}\end{array}$

Thus, a context extended with a runtime type of a resource reference (extRef)
is compatible with a heap which contains that resource reference, pointing to
some resource term with the corresponding identifier that the resource points
to. In the premise of (extRef), the resource term with its identifier is
preserved in the heap since there may be other references pointing to it
(e.g., generated from a split). The (GCArr) rule then allows heap
compatibility to ‘garbage collect’ any remaining resources.

The (ext) rule says that a context with graded assumption
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{s}}$
is compatible with a heap as long as the heap contains a binding for $x$ to
some value $v$ and heap grade $r$ that can accommodate the usage of $s$ (via
the constraint $\exists r^{\prime}.\ s+r^{\prime}\equiv r$) and as long as the
free variables $\Gamma^{\prime}$ of $\mathit{v}$ are also compatible with the
heap (scaled by $s$ to reflect the usage of $x$). The (extLin) rule is similar
to (ext), but _effectively_ where $s=1$; the variable $x$ is used in a linear
fashion.

###### Example 6.5.

As an illustrative example, the context
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{1}},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{y}:[\mathit{B}]_{2}}$
is compatible with the heap
$\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{7}}\mathit{v_{{\mathrm{1}}}}:\mathit{A},\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{2}}\mathit{v_{{\mathrm{2}}}}:\mathit{B}$
assuming the typing
${\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{3}}\vdash\mathit{v_{{\mathrm{2}}}}:\mathit{B}$,
with heap compatibility derivation:

$\displaystyle\vspace{-1em}\inferrule*[right=\textsc{ext}{}]{\inferrule*[right=\textsc{ext}{}]{\inferrule*[right=\textsc{empty}{}]{\quad}{\emptyset\bowtie\emptyset}\quad}{\emptyset,\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{7}}\mathit{v}:\mathit{A}\bowtie{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{7}}}\quad{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{3}}\vdash\mathit{v_{{\mathrm{2}}}}:\mathit{B}}{(\emptyset,\mathit{x}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{7}}\mathit{v_{{\mathrm{1}}}}:\mathit{A},\mathit{y}{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mapsto_{2}}\mathit{v_{{\mathrm{2}}}}:\mathit{B})\bowtie({\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{x}:[\mathit{A}]_{1}},{\color[rgb]{0.02734375,0.3125,0.81640625}\definecolor[named]{pgfstrokecolor}{rgb}{0.02734375,0.3125,0.81640625}\mathit{y}:[\mathit{B}]_{2}})}$

Heap compatibility allows us to establish key properties for our calculus in
conjunction with the operational semantics. We begin with syntactic type
safety, by verifying progress and preservation. These are largely standard,
though preservation links with heap compatibility in its second conjunct.

###### Theorem 6.6 (Progress).

Given $\Gamma\vdash\mathit{t}:\mathit{A}$, then $\mathit{t}$ is either a
value, or for all grades $s$ and contexts $\Gamma_{{\mathrm{0}}}$ then if
$H\bowtie\Gamma_{{\mathrm{0}}}+s\cdot\Gamma$ there exists a heap $H^{\prime}$
and term $\mathit{t^{\prime}}$ such that
$H\vdash\mathit{t}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}}$.

###### Theorem 6.7 (Type Preservation).

For a well-typed term $\Gamma\vdash\mathit{t}:\mathit{A}$ and all $s$,
$\Gamma_{{\mathrm{0}}}$, and $H$ such that
$H\bowtie(\Gamma_{{\mathrm{0}}}+s\cdot\Gamma)$ and a reduction
$H\vdash\mathit{t}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}}$ we
have:

$\exists\Gamma^{\prime},H^{\prime}.\;\;\Gamma^{\prime}\vdash\mathit{t^{\prime}}:\mathit{A}\;\
\wedge\;\ H^{\prime}\bowtie(\Gamma_{{\mathrm{0}}}+s\cdot\Gamma^{\prime})$

In addition to preservation, Marshall et al. (2022) also proved a
_conservation_ property, ensuring that resource usage is respected (in
particular, that resource usage accrued in a given reduction plus remaining
resources in the resulting heap are approximated by the resources in the
original heap plus the specified resource usage from any variable bindings
encountered along the way). Their semantics was call-by-name, which is more
natural for conservation; checking that a modified form of conservation still
holds in our setting is future work, though various other graded type systems
with similar properties are also call-by-value (Orchard et al., 2019;
Bianchini et al., 2022).

We now move on to establishing perhaps the most interesting properties here,
which are related to the safety of ownership and borrowing and how these
notions relate to the references present in the heap. First, we ensure that
taking a single step preserves the total of fractional permision annotations
on references (unless we have stopped tracking ownership information for the
given reference, in which case it should be annotated with $0$):

###### Lemma 6.8 (Borrow safety).

For a well-typed term $\Gamma\vdash\mathit{t}:\mathit{A}$ and all
$\Gamma_{{\mathrm{0}}}$ and heaps $H$ such that
$H\bowtie(\Gamma_{{\mathrm{0}}}+s\cdot\Gamma)$, and given a single-step
reduction
$H\vdash\mathit{t}\,\leadsto_{s}\,H^{\prime}\vdash\mathit{t^{\prime}}$ then
for all $\mathit{id}\in\mathsf{dom}(H)$:

$\displaystyle\sum_{\footnotesize{\begin{array}[]{c}\forall\mathit{ref}\in\mathsf{refs}(\mathit{t}).\\
\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id}\in
H\end{array}}}p\;\;=1\quad\implies\sum_{\footnotesize{\begin{array}[]{c}\forall\mathit{ref}\in\mathsf{refs}(\mathit{t^{\prime}}).\\
\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p^{\prime}}}\mathit{id}\in
H^{\prime}\end{array}}}p^{\prime}\;\;\in\{0,1\}$

i.e., for all resources with identifier $\mathit{id}$ in the incoming heap and
all references in the term pointing to this resource, if the sum of all
permissions pointing to this resource are $1$ in the incoming heap then either
this is preserved in the outgoing heap _or_ the total permissions in the
output heap is $0$, i.e., this resource has now been fully shared and has no
ownership tracking now.

Furthermore, any resources in the outgoing heap that did not appear in the
initial heap with references in the final term should have permissions summing
to $1$. That is, for all
$\mathit{id^{\prime}}\in\mathsf{dom}(H^{\prime})\wedge\mathit{id^{\prime}}\not\in\mathsf{dom}(H)$:

$\displaystyle\sum_{\footnotesize{\begin{array}[]{c}\forall\mathit{ref^{\prime}}\in\mathsf{refs}(\mathit{t^{\prime}}).\\
\mathit{ref^{\prime}}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{q}}\mathit{id^{\prime}}\in
H^{\prime}\end{array}}}q\;\;=1$

When we extend this result to multi-step reductions, we are able to restrict
the result further, and prove that if the resulting term is of unique type,
then not only is the sum of fractions preserved throughout the overall
reduction (which we verify inductively using the above result) but also that
in the final term the reference to the resource we are considering must itself
be unique.

###### Lemma 6.9 (Multi-reduction borrow safety).

For a well-typed term $\Gamma\vdash\mathit{t}:\mathit{A}$ and all
$\Gamma_{{\mathrm{0}}}$ and $H$ such that
$H\bowtie(\Gamma_{{\mathrm{0}}}+s\cdot\Gamma)$, and multi-step reduction
$H\vdash\mathit{t}\ \Rightarrow_{s}\ H^{\prime}\vdash\mathit{v}$, then for all
$\mathit{id}\in\mathsf{dom}(H)$:

$\displaystyle\sum_{\footnotesize{\begin{array}[]{c}\forall\mathit{ref}\in\mathsf{refs}(\mathit{t}).\\
\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{p}}\mathit{id}\in
H\end{array}}}p\;\;=1\implies\exists!\mathit{ref^{\prime}}.\mathit{ref^{\prime}}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{1}}\mathit{id}\in
H^{\prime}$

i.e., for all resources with identifier $\mathit{id}$ in the incoming heap and
all references in the term pointing to this resource, if the sum of all
permissions pointing to this resource are $1$ in the incoming heap then their
total permission of $1$ is preserved from the incoming heap to the resulting
term, with this permission now contained in a single reference
$\mathit{ref^{\prime}}$.

Furthermore, any new references in the final term should uniquely point to an
identifier, and thus have permission $1$. That is, for all
$\mathit{id^{\prime}}\in\mathsf{dom}(H^{\prime})\wedge\mathit{id^{\prime}}\not\in\mathsf{dom}(H)$
then:

$\displaystyle\forall\mathit{ref}\in\mathsf{refs}(\mathit{v}).\;\exists!\mathit{ref^{\prime}}.\;\,\mathit{ref^{\prime}}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{1}}\mathit{id^{\prime}}\in
H^{\prime}$

The uniqueness theorem presented by Marshall et al. (2022) now follows as a
direct corollary of the multi-step borrow safety theorem we described above.

###### Corollary 6.10 (Uniqueness).

For a well-typed term
$\Gamma\vdash\mathit{t}:{{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\ast}}{\mathit{A}}$
and all $\Gamma_{{\mathrm{0}}}$ and $H$ such that
$H\bowtie(\Gamma_{{\mathrm{0}}}+s\cdot\Gamma)$ and multi-reduction to a value
$H\vdash\mathit{t}\ \Rightarrow_{s}\ H^{\prime}\vdash\ast\mathit{v}$, for all
$\mathit{id}\in\mathsf{dom}(H)$ then:

$\displaystyle\forall\mathit{ref}\in\mathsf{refs}(\mathit{t}).(\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{1}}\mathit{id}\in
H\implies\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{1}}\mathit{id}\in
H^{\prime})$ $\displaystyle\wedge$
$\displaystyle\quad\forall\mathit{id^{\prime}}\in\mathsf{dom}(H^{\prime})\wedge\mathit{id^{\prime}}\not\in\mathsf{dom}(H^{\prime}).\;\forall\mathit{ref}\in\mathsf{refs}(\mathit{v}).\;\exists!\mathit{ref^{\prime}}.\mathit{ref}{\color[rgb]{0.76171875,0.0078125,0.1953125}\definecolor[named]{pgfstrokecolor}{rgb}{0.76171875,0.0078125,0.1953125}\mapsto_{1}}\mathit{id^{\prime}}\in
H^{\prime}$

i.e., any references contributing to the final term that are unique in the
incoming heap stay unique in the resulting term, and any new references
contributing to the final term are also unique.

Finally, we see that the operational semantics we have defined (extended to
full $\beta$-reduction) supports the equational theory we have gradually
developed throughout this work.

###### Theorem 6.11 (Soundness with respect to the equational theory).

For all $\mathit{t_{{\mathrm{1}}}},\mathit{t_{{\mathrm{2}}}}$ such that
$\Gamma\vdash\mathit{t_{{\mathrm{1}}}}:\mathit{A}$ and
$\Gamma\vdash\mathit{t_{{\mathrm{2}}}}:\mathit{A}$ and
$\mathit{t_{{\mathrm{1}}}}\equiv\mathit{t_{{\mathrm{2}}}}$ and given $H$ such
that $H\bowtie\Gamma$, there exists multi-reductions to values that are equal
under full $\beta$-reduction and evaluating any references to the value they
point to in the resulting heaps:

$\displaystyle H\vdash\mathit{t_{{\mathrm{1}}}}\ \Rightarrow_{1}\
H^{\prime}\vdash\mathit{v_{{\mathrm{1}}}}\quad\wedge\quad
H\vdash\mathit{t_{{\mathrm{2}}}}\ \Rightarrow_{1}\
H^{\prime\prime}\vdash\mathit{v_{{\mathrm{2}}}}\quad\wedge\quad
H^{\prime}(\mathit{v_{{\mathrm{1}}}})=H^{\prime\prime}(\mathit{v_{{\mathrm{2}}}})$

Full proofs for the above theorems may be found in the appendices for this
paper, provided as supplementary material, along with collected typing and
reduction rules.

##  7. Related Work

###  7.1. Linear and graded types

The notion of linearity originated with Girard’s linear logic (Girard, 1987),
which treats information in a resourceful way by restricting the structural
rules of intuitionistic logic. This was soon adopted by programming language
researchers who were interested in the resourceful behaviour of data, rapidly
developing into the concept of _linear types_ (Wadler, 1990, 1993), but it
took substantial time for them to emerge into the realm of practical
programming. Lately, linear types have seen a renaissance due to their
adoption as an extension to the Haskell language (Bernardy et al., 2017);
other languages incorporating pure linearity (or affine types, which are
similar but allow weakening) include ATS (Zhu and Xi, 2005), Alms (Tov and
Pucella, 2011) and Mezzo (Balabonski et al., 2016).

This binary view was later refined by the notion of _bounded_ linear logic
(Girard et al., 1992), which introduces a family of operators indexed by a
polynomial giving an upper bound on the usage of a resource. Further
generalisations of this idea to be able to track a broader range of
increasingly fine-grained properties are what led to the introduction of
_graded_ types, which allow for annotating values with precise information
about how they interact with their environment.

Granule’s particular approach to graded modalities draws heavily from
literature on _coeffects_ , which describe how programs _depend_ on their
context (Petricek et al., 2014), though it also incorporates ideas from effect
systems which we focus on less here. This was developed concurrently with
other work which approached the same target from a different angle—through
attempting to find generalisations for bounded linear logic (Ghica and Smith,
2014). Other instantiations of graded types include Quantitative Type Theory
(QTT) (Atkey, 2018) upon which the type system for Idris 2 is built (Brady,
2021), the core calculus underlying Linear Haskell (Bernardy et al., 2017;
Spiwack et al., 2022), and others (Abel and Bernardy, 2020; Gaboardi et al.,
2016; Wood and Atkey, 2022).

###  7.2. Uniqueness types

Uniqueness types originated in the Clean language (Smetsers et al., 1994),
where they are used in lieu of monadic computation and for efficiency gains
offered by in-place update. In Clean, computation is based on graph rewriting
and reduction; constants are graphs, and functions are graph rewriting
formulas. This gives the type system a different feel to those of more recent
functional programming languages. Recent work has attempted to capture
benefits of uniqueness while allowing a more modern programming style;
examples include Cogent (O’Connor et al., 2021), Mercury (Somogyi et al.,
1996) and the prior iteration of uniqueness in Granule (Marshall et al.,
2022).

Theoretical work on understanding uniqueness began with Harrington’s
uniqueness logic (Harrington, 2006); this was followed by a substantial amount
of theoretical groundwork on Clean’s particular strategy for uniqueness (de
Vries et al., 2008). This paper clarified the distinction between Clean’s type
system and systems based on the $\lambda$-calculus. Further work made headway
on distinguishing uniqueness from other substructural systems, allowing for
applications such as polymorphic programming and concurrency (de Vries, 2013;
de Vries et al., 2009). This laid a foundation for Granule’s orthogonal
approach to uniqueness, allowing for uniqueness and linearity to be integrated
in a single system, which lead to the extensions developed in the present
work.

###  7.3. Region-based memory management

Regions (Tofte et al., 2004) were conceived to bring benefits of traditional
stack-based memory management into higher-order functional languages. Regions
divide values using lifetimes; as with modern ownership systems, they
eliminate the need for garbage collection, by using region type information to
allow safe allocation and deallocation. Historically, region type systems have
typically been used for effect systems (Jouvelot and Gifford, 1991; Lucassen
and Gifford, 1988).

Later work on regions extends this stack-based foundation by making use of
uniqueness information (Walker et al., 2000); a unique reference ensures that
a region has no aliases, so it can be deallocated efficiently. Similarly to
lifetimes in ownership systems, regions act as equivalence classes for a “may
alias” relation; values which do not share a region may not alias with one
another, so if a value does not share a region with any other then it can be
safely mutated.

Work on Cyclone (a ‘safe dialect’ of C (Hicks et al., 2004)) clarified the
relationship between references and regions, observing that “unique pointers
are essentially lightweight, dynamic regions that hold exactly one object
(Fluet et al., 2006).” Rust’s lifetimes were inspired by regions. One
extension of ML supports both linearity and borrowing using regions (Radanne
et al., 2020).

###  7.4. Ownership and borrowing

Ownership was developed as a framework for understanding aliasing in object-
oriented languages (Mycroft and Voigt, 2013; Clarke et al., 1998), with
related work in this area having introduced notions like islands (Hogg, 1991),
balloon types (Almeida, 1997) and external uniqueness (Clarke and Wrigstad,
2003). The intent of ownership is to give a high-level structural view of
objects and references, akin to type systems which allow for a high-level
structural view of data.

More recently, ownership is pervasively used in Rust in order to help ensure
memory safety. Multiple formalisations for Rust’s ownership model have been
attempted; RustBelt (Jung et al., 2017) gives a lower-level encoding of Rust
intended for formal verification while Oxide (Weiss et al., 2019) is a higher-
level encoding designed for theoretical work, among others (Jung et al., 2019;
Pearce, 2021). Rust is not the only modern language to make use of ownership;
other languages like Swift incorporate similar ideas, and work on introducing
ownership into languages with manual memory management is ongoing (Sammler et
al., 2021). Lorenzen et al. (2023) describe how to use related ideas to
determine which functional programs can be executed in-place without
allocation.

Rust also provides an _unsafe_ mode (a superset of the safe portion of Rust).
While in Rust memory is managed through ownership and borrowing by default
with memory for unsafe code needing to be managed manually, in languages like
Granule managing memory automatically through a garbage collector is the
default. Using our extension to obviate the need for garbage collection is a
special case applying to some subset of a program. If the user does not wish
for ownership to be taken into consideration, they can use Granule’s pre-
existing type system as before.

##  8. Conclusions and Future Work

#### Performance improvements.

This paper has generalised uniqueness and linearity in order to develop a
unified framework for reasoning about ownership and grading. While we have an
implementation of this built upon the Granule compiler, the practical benefits
it can offer for resourceful programming have not been fully explored. We hope
to evaluate performance improvements that introducing precise ownership
tracking into a functional language can offer through obviating garbage
collection for a subset of a program, by collecting examples involving
ownership and borrowing and benchmarking them against equivalent functional
code.

#### Guarantees.

Linearity is only one property that can be tracked via _coeffects_ , the
flavour of grading we consider; many others have been described in prior work
(Petricek et al., 2014). If uniqueness dualises linearity, translating the
same relationship onto other coeffects may result in other interesting
properties that can be tracked in a similar manner; for example, it has been
noted that in the realm of information flow tracking for security,
_confidentiality_ can be understood as a coeffect with _integrity_ as its dual
(Marshall and Orchard, 2022a). It would be valuable to find an analogy for the
ownership generalisation developed here in the context of security, and also
to go further and develop a _general_ algebraic theory for guarantees about
global program behaviour.

#### Counting permissions.

Fractional permissions and the general notion of dividing a single mutable
borrow into many immutable borrows is not the only model for representing
borrowing that we considered. One interesting path for future research would
be to explore an alternative strategy for graded uniqueness that is less
symmetrical but instead privileges the original owner, allowing for a more
exact count of other extant references. This model, based on counting
permissions (Bornat et al., 2005), involves having many references with only
read permissions, and a designated owner that keeps a count of how many such
references exist, so that uniqueness can still be recovered.

#### Non-lexical lifetimes.

The model of ownership developed here was _not_ intended to be a complete
model of every aspect of Rust’s ownership system, instead aiming to extract
essential features and develop a framework where they coexist with more
traditional linear and graded types. It would still be of interest to pursue
this further and capture Rust’s more advanced features, however—in particular,
incorporating notions such as non-lexical lifetimes would increase the power
of the described system. This may eventually allow for a potential encoding
study between Granule’s calculus and a more faithful representation of Rust’s
type system such as $\lambda_{\text{Rust}}$ (Jung et al., 2017).

#### Categorical model.

Finally, alongside the operational heap semantics model presented in this
paper it would be interesting to explore a categorical model based on
adjunctions. Benton’s linear/non-linear (LNL) logic (Benton, 1995) is well-
known, and progress has been made on using similar tools to understand more
advanced substructural systems involving graded types (Eades III and Orchard,
2020), much like the core calculus of Granule covered in this paper. Despite
the close theoretical relationship between linearity and uniqueness, the
categorical background of uniqueness types has been only briefly explored
(Harrington, 2006), and for more complex systems of ownership and borrowing
even less so. This would be a fruitful pathway for further research.

#### Conclusion

Graded type systems and ownership with borrowing are both ways of carefully
and precisely managing the usage of data built upon the foundation of linear