Special Delivery

Programming with Mailbox Types (Extended Version)

Simon Fowler
University of GlasgowUK

Duncan Paul Attard
University of GlasgowUK

Franciszek Sowul
University of GlasgowUK

Simon J. Gay
University of GlasgowUK

Phil Trinder
University of GlasgowUK

The asynchronous and unidirectional communication model supported by
mailboxes is a key reason for the success of actor languages like Erlang
and Elixir for implementing reliable and scalable distributed systems.

While many actors may send messages to some actor, only the actor may
(selectively) receive from its mailbox.

Although actors eliminate many of the issues stemming from shared memory
concurrency, they remain vulnerable to communication errors such as protocol
violations and deadlocks.

Mailbox types are a novel behavioural type system for mailboxes first
introduced for a process calculus by de'Liguoro and Padovani in 2018, which
capture the contents of a mailbox as a commutative regular expression.

Due to aliasing and nested
evaluation contexts, moving from a process calculus to a programming language is

This paper presents , the first programming language design
incorporating mailbox types, and describes an algorithmic type system.
We make essential use of quasi-linear typing to tame some of the
complexity introduced by aliasing. Our algorithmic type system is
necessarily co-contextual, achieved through a novel use of backwards
bidirectional typing, and we prove it sound and complete with respect to our
declarative type system.

We implement a prototype type checker, and use it to demonstrate the
expressiveness of   on a factory automation case study
and a series of examples from the Savina actor benchmark suite.

§ INTRODUCTION

Software is increasingly concurrent and distributed, but coordinating
concurrent computations introduces a host of additional correctness
issues like communication mismatches and deadlocks. Communication-centric
languages such as Go, Erlang, and Elixir make it possible to avoid
many of the issues stemming from shared memory concurrency by
structuring applications as lightweight processes that
communicate through explicit message passing. There are two main
classes of communication-centric language. In channel-based
languages like Go or Rust, processes communicate over channels, where a
+send+ in one process is paired with a [language=]+receive+
in the recipient
process. In actor languages like Erlang or Elixir, a message is
sent to the mailbox of the recipient process, which is an incoming
message queue; in certain actor languages, the recipient can choose
which message from the mailbox to handle next.

Although communication-centric languages eliminate many coordination
issues, some remain. For example, a process may still receive a message
that it is not equipped to handle, or wait for a message that it will
never receive.  Such communication errors often occur sporadically and
unpredictably after deployment, making them difficult to locate and

Behavioural type systems <cit.> encode correct communication behaviour
to support correct-by-construction concurrency. Behavioural
type systems, in particular session types <cit.>, have been extensively applied to specify communication protocols in channel-based
languages <cit.>.

There has, however, been far less application of behavioural typing to actor
languages. Existing work either imposes restrictions on the actor model to
retrofit session types <cit.> or relies on dynamic typing <cit.>. We discuss these systems further in sec:related.

Our approach is based on

mailbox types, a behavioural type system for mailboxes first introduced in the
context of a process calculus <cit.>. We present the first programming language design incorporating mailbox types and we detail an algorithmic
type system, an implementation, and a range of benchmarks and a factory case study. Due to aliasing and nested evaluation contexts, the move from a
process calculus to a programming language is challenging. We make
essential and novel use of quasi-linear
typing <cit.> to tame some of the
complexity introduced by aliasing, and our algorithmic type system is
necessarily co-contextual <cit.>, achieved through a novel use of backwards
bidirectional typing <cit.>.

§.§ Channel-based vs Actor Communication

Channel-based languages comprise anonymous
processes that communicate over named channels, whereas actor-based
languages comprise named processes each equipped with a mailbox.

Figure <ref> contrasts the approaches, and is taken from
a detailed comparison <cit.>.

Channel- and actor-based languages <cit.>

Actor languages have proven to be effective for implementing
reliable and scalable distributed systems <cit.>.
Communication in actor languages is asynchronous and
unidirectional: many actors may send messages to an actor $A$, whereas
only $A$ may receive from its mailbox.
Mailboxes provide data locality as each message
is stored with the process that will handle it.
Since channel-based languages allow channel names to be sent, they must
either sacrifice locality and reduce performance, or rely on complex
distributed algorithms <cit.>.

Although it is straightforward to add a type system to channel-based languages,
adding a type system to actor languages is less straightforward, as process
names (process IDs or PIDs) must be parameterised by a type that supports all
messages that can be received. The type is therefore less precise, requiring
subtyping <cit.> or
synchronisation <cit.> to avoid a total loss
of modularity <cit.>.

The situation becomes even more pronounced when considering behavioural type
systems: communication errors might be prevented by giving one end of a channel
the session type ${!}\mkwd{Int}.{!}\mkwd{Int}.{?}\mkwd{Bool}.\mkwd{End}$ (send
two integers, and receive a Boolean), and the other end the dual type
${?}\mkwd{Int}.{?}\mkwd{Int}.{!}\mkwd{Bool}.\mkwd{End}$. Behavioural type
systems for actor languages are much less straightforward due to the asymmetric
communication model.

In practice, designers of session type systems for actor languages either
emulate session-typed channels <cit.>, or use multiparty
session types to govern the communication actions performed by a process,
requiring a fixed communication topology <cit.>.

§.§ Mailbox types

<cit.> observe that session types require a strict ordering
of messages, whereas most actor systems use selective receive to
process messages out-of-order.
Concentrating on unordered interactions enables behavioural typing for
mailboxes with many writers.

*Mailbox typing by example: a future variable.
Rather than reasoning about the behaviour of a process, mailbox types
reason about the contents of a mailbox. Consider a future
variable, which is a placeholder in a concurrent computation. A future can receive
many +get+ messages that are only fulfilled after a +put+
message initialises the future with
a value. After the future is initialised, it fulfils all +get+
messages by sending its value; a second +put+ message is explicitly

We can implement a future straightforwardly in Erlang:

empty_future() ->
put, X  -> full_future(X)
full_future(X) ->
get, Pid  ->
Pid !  reply, X ,
put, _  ->
erlang:error("Multiple writes")

client() ->
Future = spawn(future, empty_future, []),
Future !  put, 5 ,
Future !  get, self() ,
reply, Result  ->
io:fwrite(" w n", [Result])

The empty_future function awaits a put message to set
the value of the future (lines 2–4), and transitions to the full_future state.
A full_future receives get messages (lines 6–12) containing a process
ID used to reply with the future's value.

The client function spawns a future (line 14), sends a
put message followed by a get message (lines 15–16),
and awaits the result (lines 17–20). The program prints the number 5.

Several communication errors can arise in this example:

* Protocol violation.
Sending two put messages to the future will result in a
runtime error.

* Unexpected message.
Sending a message other than get or put to the
future will silently succeed, but the message will never be retrieved, resulting in a memory leak.

* Forgotten reply.
If the future fails to send a reply message after
receiving a get message the client will be left
waiting forever.

* Self-deadlock.
If the client attempts to receive a reply message before
sending a get message it will be left waiting forever.

All of the above issues can be solved by mailbox typing. We can write the
following types:

\[
\begin{array}{rcl}
\mkwd{EmptyFuture} & \defeq &
\tyrecvp{\msg{Put}{\mkwd{Int}} \patconcat
\many{\msg{Get}{\mkwd{ClientSend}}}}\\
\mkwd{FullFuture} & \defeq & \tyrecv{\many{\msg{Get}{\mkwd{ClientSend}}}} \\
\end{array}
\]

\[
\begin{array}{rcl}
\mkwd{ClientSend} & \defeq & \tysend{\msg{Reply}{\mkwd{Int}}} \\
\mkwd{ClientRecv} & \defeq & \tyrecv{\msg{Reply}{\mkwd{Int}}} \\
\end{array}
\]

A mailbox type combines a capability (either $\texttt{!}$ for an output
capability, analogous to a PID in Erlang; or $\texttt{?}$ for
an input capability) with a pattern. A pattern is a commutative
regular expression: in the context of a send mailbox type, the pattern will
describe the messages that must be sent; in the context of a receive mailbox
type, it describes the messages that the mailbox may contain.

A mailbox name (, Future) may have
different types at different points in the program.
$\mkwd{EmptyFuture}$ types an input capability of an empty future mailbox,
and denotes that the mailbox
may contain a single $\msgtag{Put}$ message with an $\mkwd{Int}$ payload, and
potentially many ($\many{}$) $\msgtag{Get}$ messages each with a $\mkwd{ClientSend}$ payload.
$\mkwd{FullFuture}$ types an input capability of the future after a
$\msgtag{Put}$ message has been received, and requires that the mailbox
only contains $\msgtag{Get}$ messages.

$\mkwd{ClientSend}$ is an output mailbox type which requires that a
$\msgtag{Reply}$ message must be sent; $\mkwd{ClientRecv}$ is an input
capability for receiving the $\msgtag{Reply}$.

For each mailbox name, sends and receives must “balance out”: if a message is
sent, it must eventually be received.

<cit.> introduce a small extension of the asynchronous
$\pi$-calculus <cit.>, which they call the mailbox calculus, and
endow it with mailbox types. They express the Future example in
the mailbox calculus as follows, where the mailbox is denoted $\var{self}$.

\[
\bl
\begin{array}{rcl}
\mkwd{emptyFuture}(\var{self}) & \defeq &
\var{self}?\msgtag{Put}(x) \then \mkwd{fullFuture}(\var{self}, \var{x}) \\
\mkwd{fullFuture}(\var{self}, \var{x}) & \defeq & \calcwd{free}\; \var{self} \then \calcwd{done} \\
& +      &
\var{self}?\msgtag{Get}(\var{sender}) \then
(\send{\var{sender}}{Reply}{x} \parallel \mkwd{fullFuture}(\var{self}, \var{x}))
\\
& +      & \var{self} \mathop{\tt ?} \msgtag{Put}(x) \then \fail \; \var{self}
\end{array}
} \vspace{0.5em} \\
{\begin{array}{l@{\hspace {0em}}l}
\resconf{\var{future}}{& \mkwd{emptyFuture}(\var{future}) \parallel
\send{\var{future}}{Put}{5} \parallel \\
& \resconf{\var{self}}{\send{\var{future}}{Get}{\var{self}} \parallel
(\var{self}\mathop{\tt ?}\msgtag{Reply}(x) \then \calcwd{free}\; \var{self} \then
\mkwd{print}(\mkwd{intToString}(x)}}
\end{array}
\el
\]

A process calculus is useful for expressing the essence of concurrent
computation, but there is a large gap between a process calculus and a
programming language design, the biggest being the separation of static and
dynamic terms. A programming language specifies the program that a user
writes, whereas a process calculus provides a snapshot of the system at a given

A particular difference comes with name generation: in a process calculus, we
can write name restrictions directly; in a programming language, we
instead have a language construct (like $\mbnew$) which is evaluated
to create a fresh name at runtime.

Further complexities come with nested evaluation contexts, sequential
evaluation, and aliasing. We explore these challenges in greater detail
in sec:whatstheissue.

We propose [<https://en.wikipedia.org/wiki/Postman_Pat>], a first-order programming language
that supports mailbox types, in which we express the future example as follows ($\var{self}$ is again the mailbox).

\[
\bl
\fndefthree{\mkwd{emptyFuture}}{\var{self}: \mkwd{EmptyFuture}}{\one} \\
\quad \guardanntwo{\var{self}}{\msgtag{Put} \patconcat \many{\msgtag{Get}}} \\
\qquad
\receive{Put}{x}{\var{self}}{\mkwd{fullFuture}(\var{self}, \var{x})} \\
\quad \} \\
\}\vspace{0.5em}
\\
\fndefthree{\mkwd{fullFuture}}{\var{self}: \mkwd{FullFuture}, \var{value}: \mkwd{Int}}{\one} \\
\quad \guardanntwo{\var{self}}{\many{\msgtag{Get}}} \\
\qquad \free{()} \\
\qquad
\receivethree{Get}{\var{user}}{\var{self}} \\
\qquad \quad \send{\var{user}}{Reply}{\var{value}}; \\
\qquad \quad \mkwd{fullFuture}(\var{self}, \var{value}) \\
\quad \} \\
\} \\
\el
\]

\[
\bl
\fndefthree{\mkwd{client}}{}{\one} \\
\quad \letintwo{\var{future}}{\mbnew} \\
\quad \spawn{\mkwd{emptyFuture}(\var{future})}; \\
\quad \letintwo{\var{self}}{\mbnew} \\
\quad \send{\var{future}}{Put}{5}; \\
\quad \send{\var{future}}{Get}{\var{self}}; \\
\quad \guardanntwo{\var{self}}{\msgtag{Reply}} \\
\qquad \receivethree{Reply}{\var{result}}{\var{self}} \\
\qquad \quad \sugarfree{\var{self}};\\
\qquad \quad \mkwd{print}(\mkwd{intToString}(\var{result})) \\
\quad \} \\
\}
\el
\]

The  program has a similar structure to the
Erlang example with $\mkwd{client}$, emptyFuture and fullFuture functions, and the mailbox types are similar to those in the mailbox calculus specification. There are, however, some differences compared with the  Erlang future. The first is that in  mailboxes are first-class: we create
a new mailbox with $\mbnew$, and receive from it using the $\calcwd{guard}$
expression. A guard  acts on a mailbox

and may contain several guards: $\free{\tma}$ frees the mailbox if  there
are no other references to it and evaluates $\tma$; and
$\receive{m}{\seq{x}}{\var{y}}{\tma}$  retrieves a message with tag
$\msgtag{m}$ from the mailbox, binding its payloads to $\seq{x}$ and re-binding
the mailbox variable (with an updated type) to $\var{y}$ in continuation $\tma$.

There is also $\fail$
denoting that a mailbox is in an invalid state, but the type system ensures
that this guard is never evaluated.
In the above code, $\sugarfree{\var{self}}$ is syntactic sugar
(see sec:declarative).

has all of the characteristics of  a programming
language, unlike the mailbox calculus. Static and dynamic terms are
distinguished, , we do not need to write name restrictions with dynamic
names known a priori.  provides $\calcwd{let}$-bindings, which
enable full sequential composition along with nested evaluation contexts; and we
have data types and return types.
Crucially all of the concurrency errors described earlier result in a type error, i.e. protocol violations, unexpected messages,
forgotten replies, and self-deadlocks are all detected statically.

Despite being a convincing proposal for behavioural typing for actor languages,
mailbox typing has received little attention since its introduction in 2018.

The overarching contribution of this paper, therefore, is the first design and
implementation of a concurrent programming language with support for mailbox
types.  Concretely, we make four main contributions:

* We introduce a declarative type system for
sec:declarative, a first-order
programming language with support for mailbox types, making essential
and novel use of quasi-linear types.

We show type preservation, mailbox conformance, and a progress result.

* We introduce a co-contextual algorithmic type system for
making use of backwards bidirectional typing. We prove that the
algorithmic type system is sound and complete with respect to the
declarative type system.

* We extend $\langname$ with sum and product types; interfaces; and
higher-order functions sec:extensions.

* We detail our implementation sec:implementation,
and demonstrate the expressiveness of   by encoding all
of the examples from <cit.>, and 10 of the 11
Savina benchmarks <cit.> used
by <cit.> in their evaluation of multiparty session types for
actor languages sec:implementation:examples.

Our tool is available as an artifact and on GitHub

§ MAILBOX TYPES IN A PROGRAMMING LANGUAGE: WHAT ARE THE ISSUES?

\begin{array}{>{\stepcounter{myrow}\themyrow\:\:}l}
\fndefthree{\mkwd{client}}{}{\one} \\
\quad \letintwo{\var{future}}{\mbnew} \\
\quad \spawn{\mkwd{emptyFuture}(\var{future})}; \\
\quad \letintwo{\var{self}}{\mbnew} \\
\quad \send{\var{future}}{Put}{5}; \\
\quad \send{\var{future}}{Get}{\var{self}}; \\
\quad \guardanntwo{\var{self}}{\msgtag{Reply}} \\
\qquad \receivethree{Reply}{\var{result}}{\var{self}} \\
\qquad \quad \sugarfree{\var{self}};\\
\qquad \quad \mkwd{print}(\mkwd{intToString}(\var{result})) \\
\quad \} \\
\}
\el
\vspace{-0.5em}
\caption{Send and receive uses of \var{future}}
\label{fig:multi-use}
\end{wrapfigure}

Session typing was originally studied in the context of process calculi
(e.g.,~\cite{HondaVK98, Vasconcelos12}), but later work~\cite{GayV10,
Wadler14,FowlerKDLM21} introduced session types for languages based
on the linear $\lambda$-calculus.
The more relaxed view of linearity in the mailbox calculus makes
language integration far more challenging. A mailbox name may be used
several times to \emph{send} messages, but only once to
\emph{receive} a message. The intuition is that while sends simply add
messages to a mailbox, it is a receive that determines the future
behaviour of the actor. To illustrate, Fig.~\ref{fig:multi-use}
shows a fragment of the future example from~\secref{sec:introduction}
with two sends to the $\var{future}$ mailbox  (lines 5 and 6), and a single
receive (line 8).
In the mailbox calculus, a name remains constant and cannot be aliased; this is
at odds with idiomatic programming where expressions are aliased with
$\calcwd{let}$ bindings or function application. Moreover functional languages
provide nested evaluation contexts and sequential evaluation.

\begin{figure}
\begin{subfigure}[t]{0.3\textwidth}
\[
\bl
\fndefthree{\mkwd{useAfterFree1}}{x: \tyrecv{\many{\msg{Msg}{\one}}}}{\one} \\
\quad \guardanntwo{x}{\many{\msgtag{Msg}}} \\
\qquad \receivethree{Msg}{y}{z} \\
\qquad \quad \send{x}{Msg}{}; \\
\qquad \quad \mkwd{useAfterFree1}(z) \\
\qquad \kwfree \mapsto \send{x}{Msg}{} \\
\quad \} \\
\} \\ \\
\el
\]
\caption{Using old name}
\label{subfig:use-after-free-1}
\end{subfigure}
\hfill
\begin{subfigure}[t]{0.3\textwidth}
\[
\bl
\fndefthree{\mkwd{useAfterFree2}}{x: \tyrecv{\many{\msg{Msg}{\one}}}}{\one} \\
\quad \letintwo{a}{x} \\
\quad \guardanntwo{a}{\many{\msgtag{Msg}}} \\
\qquad \receivethree{Msg}{y}{z} \\
\qquad \quad \send{x}{Msg}{}; \\
\qquad \quad \mkwd{useAfterFree2}(z) \\
\qquad \kwfree \mapsto \send{x}{Msg}{} \\
\quad \} \\
\}
\el
\]
\caption{Renaming}
\label{subfig:use-after-free-2}
\end{subfigure}
\hfill
\begin{subfigure}[t]{0.3\textwidth}
\[
\bl
\fndefthree{\mkwd{useAfterFree3}}{x: \tyrecv{\many{\msg{Msg}{\one}}}}{\one} \\
\quad \calcwd{let} \; \_ = \\
\qquad \guardanntwo{x}{\many{\msgtag{Msg}}} \\
\quad \qquad \receivethree{Msg}{y}{z} \\
\qquad \qquad \send{x}{Msg}{}; \\
\qquad \qquad \mkwd{useAfterFree3}(z) \\
\qquad \quad \kwfree \mapsto \send{x}{Msg}{} \\
\quad \}
\; \calcwd{in}
\; \send{x}{Msg}{} \\
\}
\el
\]
\caption{Evaluation contexts}
\label{subfig:use-after-free-3}
\end{subfigure}
\caption{Use-after-free via aliasing}
\end{figure}

\subsection{Challenge: Mailbox Name Aliasing}\label{sec:by-example:aliasing}

Ensuring appropriate mailbox use is challenging in the presence of aliasing: for
example, we can write a function that attempts to use a mailbox after it has
been freed (Fig.~\ref{subfig:use-after-free-1}). Unlike in our situation,
use-after-free errors are not an issue with a fully linear type system, since we
\emph{cannot} use a resource after it has been consumed.

We could require that a name cannot be used after it has been guarded upon by
insisting that the subject and body of a $\calcwd{guard}$ expression are typable
under disjoint type environments. Indeed, such an approach correctly rules out
the error in Fig.~\ref{subfig:use-after-free-1}, but the check can easily be circumvented.
Fig.~\ref{subfig:use-after-free-2} aliases the output capability for the mailbox, and
the new name prevents the typechecker from realising that it has been used in
the body of the guard.
Similarly, Fig.~\ref{subfig:use-after-free-3} uses nested evaluation contexts,
meaning that the next use of a mailbox variable is not necessarily contained
within a subexpression of the guard.

Much of the intricacy arises from using a mailbox name many times as
an output capability. In each process, we can avoid the problems above
using three principles:

\begin{enumerate}
\item No two distinct variables should represent the same underlying mailbox
\item Once let-bound to a different name, a mailbox variable is considered
out-of scope.
\item A mailbox name cannot be used after it has been used in a
$\calcwd{guard}$ expression.
\end{enumerate}

These principles ensure syntactic hygiene: the first and second handle the disconnect
between static names and their dynamic counterparts, allowing us to reason that
two syntactically distinct variables indeed refer to different mailboxes.
The third ensures that a mailbox name is correctly `consumed' by a
$\calcwd{guard}$ expression, allowing us to correctly update its type.

\paragraph*{Aliasing through communication.}
Consider the following example, where mailbox $a$ receives the message
$\msg{m}{b}$, where $b$ is already free in the continuation of the
$\calcwd{receive}$ clause:

\begin{minipage}{0.6\textwidth}
\[
\begin{array}{rcl}
\sentmsg{a}{m}{b}
\parallel
\bl
\guardanntwo{a}{\msgtag{m}} \\
\quad \receivethree{m}{x}{\var{y}} \\
\qquad \send{b}{n}{x}; \\
\qquad \sugarfree{y} \\
\}
\el
\end{array}
\]
\end{minipage}
\begin{minipage}{0.2\textwidth}
\[
\bl
\qquad \send{b}{n}{b}; \\
\qquad \sugarfree{a} \\
\el
\]
\end{minipage}

Here, although the code suggests that $x$ and $b$ are distinct, aliasing is
introduced through communication (violating principle 1).

\subsection{Mailbox Calculus Solution: Dependency Graphs}\label{sec:dgs}
\begin{wrapfigure}[6]{l}{0.3\textwidth}
\vspace{-1em}
\bl
\letintwo{a}{\mbnew} \\
\letintwo{b}{\mbnew} \\
\send{a}{m}{b}; \:
\spawn{(\sugarfree{b})}; \\
\guardanntwo{a}{\msgtag{m}} \\
\quad \receive{m}{x}{\var{a}}{\sugarfree{a}} \\
\}
\el
\end{wrapfigure}
The mailbox calculus uses a \emph{dependency graph} (DG) both to avoid issues
with aliasing and to eliminate cyclic dependencies and hence deadlocks.
As an example, the mailbox calculus process
$(\nu a)(\nu b)(\send{a}{m}{b} \parallel \calcwd{free} \: \var{b} \parallel
\var{a}?\msg{m}{x} \then \calcwd{free} \: \var{a})$ would have DG $(\nu
a)(\nu b)(\set{a, b})$ due to the dependency arising from sending $b$ over $a$.
Alas, a language implementation \emph{cannot} use
this approach as it relies on knowing runtime names directly. To see why,
consider the \langname program on the left, which evaluates
to an analogous configuration.
The first issue is how to create a scoped DG from $\mbnew$: one option is
to introduce a scoped construct
$\calcwd{let}\:\calcwd{mailbox}\:x\:\calcwd{in}\:\tma$, but this approach
fails as soon as we rename $x$ using a $\calcwd{let}$-binder.
A more robust approach is to follow~\citet{AhmedFM07} and~\citet{Padovani19} and
endow mailbox types with a type-level identity by giving $\calcwd{new}$ an
existential type and introducing a scoped $\calcwd{unpack}$ construct.
However there still remain two issues: first, it is unclear how to extend DGs to
capture the more complex scoping and sequencing induced by nested contexts.
Second, each mailbox type would require an identity (\eg\
${!}^{\iota}\msgtag{Msg}$) which
becomes too restrictive, since we would need to include identities in message
payload types when communicating names. As an example, each client of the
$\mkwd{Future}$ example from~\secref{sec:introduction} would require a separate
message type.

\subsection{The \langname Solution: Quasi-linear Typing}\label{sec:quasi-linear-typing}
The many-sender, single-receiver pattern is closely linked to \emph{quasi-linear
typing}~\cite{Kobayashi99:quasilinear}; our
formulation is closer to that of~\citet{EnnalsSM04}.  Quasi-linear types were
originally designed to overcome some limitations of full linear types in the
context of memory management and programming convenience and allow a value to
be used once as a \emph{first-class} (returnable) value, but several times as a
\emph{second-class} value~\cite{OsvaldEWAR16}. A second-class value can be
\emph{consumed} within an expression, for example as the subject of a send
operation, but cannot escape the scope in which it is defined.

This distinction maps directly onto the many-writer, single-reader communication model used
by the mailbox calculus. We augment mailbox types with a \emph{usage}: either
$\returnable$, a \emph{returnable} reference that allows a
type to appear in the return type of an expression; or $\usable$, a
`second-class' reference. The subject of a $\calcwd{guard}$ must be
returnable.  With usage information we can ensure that:

\begin{enumerate}
\item there is \emph{only one} returnable reference for each mailbox name in a
\item only returnable references can be renamed, avoiding problems with aliasing
\item the returnable reference is the final lexical use of a mailbox name
in a process
\end{enumerate}

Quasi-linear types rule out all three of the previous examples.
In \mkwd{useAfterFree}, $x$ is consumed by the $\calcwd{guard}$ expression and
cannot be used thereafter.  In \mkwd{useAfterFree2}, since $x$ is the subject of
a \calcwd{let} binding, it must be returnable and therefore cannot be used in
the body of the binding. In \mkwd{useAfterFree3}, since $x$ is used as the
subject of a $\calcwd{guard}$ expression, that use must be first-class and
therefore the last lexical occurrence of $x$, ruling out the use of $x$ in the
outer evaluation context.
Quasi-linear typing cannot account for inter-process deadlocks, but can still
rule out self-deadlocks.

\paragraph*{Ruling out aliasing through communication.}
Quasi-linear types alone do not safeguard against introducing aliasing through
communication, and we cannot use DGs for the reasons stated above.  However,
treating all received names as second-class, coupled with some simple syntactic
restrictions (\eg\ by ensuring that either all message payloads or all variables
free in the body of the $\calcwd{receive}$ clause have base types) eliminates
unsafe aliasing.

\paragraph*{Summary.} Quasi-linear types and the lightweight syntactic
checks outlined above ensure that mailboxes are used safely in a
concurrent language that allows aliasing, and obviate the need for
the static global dependency graph used in the mailbox calculus. We
show that the checks are not excessively restrictive by expressing all
of the examples shown by~\citet{dP18:mbc}, and 10 of the 11 Savina
benchmarks~\cite{ImamS14a:savina} used by~\citet{NeykovaY16} to
demonstrate expressiveness of behavioural type systems for actor
\section{Pat: A Core Language with Mailbox Types}\label{sec:declarative}
This section introduces $\langname$, a core first-order programming language
with mailbox types, along with a declarative type system and an operational

\subsection{Syntax}

\begin{figure}[t]
\begin{minipage}{0.4\textwidth}
\[
\begin{array}{lrcl}
\text{Mailbox types} & \mbtya, \mbtyb & ::= & \tysend{\pata} \midspace \tyrecv{\pata} \\
\text{Mailbox patterns} & \pata, \patb & ::= & \mbzero \midspace \mbone \midspace
\msgtag{m} \midspace \patplustwo{\pata}{\patb} \\
& & \midspace & \patconcattwo{\pata}{\patb} \midspace \many{\pata}
\end{array}
\]
\end{minipage}
\hfill
\begin{minipage}{0.5\textwidth}
\[
\begin{array}{lrcl}
\text{Base types} & \basety & ::= & \one \midspace \mkwd{Int} \midspace \mkwd{String} \midspace \cdots \\
\text{Types} & \pretya, \pretyb & ::= & \basety \midspace \mbtya \\
\text{Usage annotations} & \usage & ::= & \usable \midspace \returnable \\
\text{Usage-annotated types} & \tya, \tyb & ::= & \basety \midspace \usagety{\mbtya} \\
\end{array}
\]
\end{minipage}

\[
\begin{array}{lrcl}
\text{Variables} & x, y, z \\
\text{Definition names} & f \\
\text{Definitions} & D & ::= & \fndef{f}{\seq{x: \tya}}{\tyb}{\tma} \\
\text{Values} & \vala, \valb & ::= & x \midspace c \\
\text{Terms} & \tmc, \tma, \tmb & ::=  & \vala \midspace
\letin[\pretya]{x}{\tma}{\tmb} \midspace \fnapp{f}{\seq{V}} \\
&         & \mid & \spawn{\tma} \midspace \mbnew
\midspace \send{\vala}{m}{\seq{\valb}} \midspace
\guardann{\vala}{\pata}{\seq{G}} \\
\text{Guards} & G & ::= & \fail \midspace \free{\tma} \midspace \receive{m}{\seq{x}}{y}{\tma}
\\ \\
\text{Type environments} & \tyenv & ::= & \cdot \midspace \tyenv, x : \tya
\end{array}
\]

\caption{The syntax of  \langname, a core language with mailbox types}
\label{fig:declarative:syntax}
\end{figure}

Figure~\ref{fig:declarative:syntax} shows the syntax for \langname. We defer
discussion of types to~\secref{sec:declarative-typing-rules}.

\paragraph*{Programs and Definitions.}
A program $\progdef{\sigs}{\seq{D}}{\tma}$ consists of
a \emph{signature} $\sigs$ which maps message tags to payload types;
a set of \emph{definitions} $D$; and an
\emph{initial term} $\tma$.
Each definition $\fndef{f}{\seq{x : \tya}}{\tyb}{\tma}$ is
a function with name $f$, annotated arguments $\seq{x : \tya}$, return type
$\tyb$, and body $\tma$. We write $\prog(f)$ to retrieve the
definition for function $f$, and $\prog(\msgtag{m})$ to
retrieve the payload types for message $\msgtag{m}$.

\paragraph*{Values.}
It is convenient for typing to introduce a syntactic distinction between values
and computations, inspired by \emph{fine-grain call-by-value}~\cite{LPT03}.
Values $\vala, \valb$ include variables $x$ and constants $c$; we assume that
the set of constants includes at least the unit value $()$ of type $\one$.

\paragraph*{Terms.}
The functional fragment of the language is largely standard.
Every value is a term. The only evaluation context is
$\letin[\pretya]{x}{\tma}{\tmb}$, which evaluates term $\tma$ of type
$\pretya$, binding its result to $x$ in continuation $\tmb$. The type
annotation is a technical convenience and  is not necessary in our
Function application $\fnapp{f}{\seq{V}}$ applies function $f$ to arguments $\seq{V}$.
As usual, we use $\tma; \tmb$ as sugar for
$\letin[\one]{x}{\tma}{\tmb}$, where $x$ does not occur in $\tmb$.

In the concurrent fragment of the language, $\spawn{M}$ spawns term $M$ as a
separate process, and $\mbnew$ creates a fresh mailbox name. Term
$\send{\vala}{m}{\seq{\valb}}$ sends message $\msgtag{m}$ with payloads
$\seq{W}$ to mailbox $\vala$.

The $\guardann{V}{\pata}{\seq{\gd}}$ expression asserts that mailbox $\vala$
contains pattern $\pata$, and invokes a guard in $\seq{\gd}$.
The $\fail$ guard is triggered when an unexpected
message has arrived; $\free{M}$ is triggered when a mailbox is empty and there are no
more references to it in the system;
and $\receive{m}{\seq{x}}{y}{\tma}$ is triggered when the mailbox contains
a message with tag $\msgtag{m}$, binding its payloads to $\seq{x}$ and
continuation mailbox with updated mailbox type to $y$ in continuation term $\tma$.
We write $\sugarfree{V}$ as syntactic sugar for $\guardann{V}{\mbone}{\free{()}}$, and
$\sugarfail{\vala}$ as syntactic sugar for $\guardann{V}{\mbzero}{\fail}$.
We require that each clause within a $\calcwd{guard}$ expression is unique.

\subsection{Type system}\label{sec:declarative-typing-rules}

This section describes a declarative type system for $\langname$. We begin
by discussing mailbox types in more depth, in particular showing how to define
subtyping and equivalence.

\subsubsection{Types}
A mailbox type consists of a \emph{capability}, either \emph{output} $\texttt{!}$
or \emph{input} $\texttt{?}$, and a \emph{pattern}. A system can contain multiple
references to a mailbox as an output capability, but only one as an input
A \emph{pattern} is a \emph{commutative} regular expression, \ie, a regular expression
where composition is unordered. The $\mbone$ pattern is the unit of pattern
composition $\patconcat$, denoting the empty mailbox.
The $\mbzero$ pattern denotes the \emph{unreliable} mailbox, which has received
an unexpected message. It is not possible to send to, or receive from, an
unreliable mailbox, but we will show that reduction does not cause a mailbox to
become unreliable.
The pattern $\msgtag{m}$ denotes a mailbox containing a single message
Unlike in~\secref{sec:introduction}, our formalism does not pair a
message tag with its payload; instead, tags are associated with payload types
via the program signature. This design choice allows us to more easily compare the declarative
system with the algorithmic system in~\secref{sec:algorithmic}, and
unlike~\cite{dP18:mbc} means we need not define types and subtyping
Pattern choice $\pata \patplus \patb$ denotes that the mailbox
contains either messages conforming to pattern $\pata$ or $\patb$. Pattern
composition $\pata \patconcat \patb$ denotes that the mailbox contains messages
pertaining to $\pata$ and $\patb$ (in either order).
Finally, $\many{\pata}$ denotes replication
of $\pata$, so $\many{\msgtag{m}}$ denotes that the mailbox can
contain zero or more instances of message $\msgtag{m}$.
Mailbox patterns obey the usual laws of commutative regular expressions:
$\mbone$ is the unit for $\patconcat$, while $\mbzero$ is the unit for
$\patplus$ and is cancelling for $\patconcat$. Composition $\patconcat$ is
associative, commutative, and distributes over $\patplus$; and $\patplus$ is
associative and commutative.

\paragraph*{Pattern semantics.}
It follows that different syntactic representations of patterns may have the
same meaning, \eg\ patterns $\mbone \patplus \mbzero
\patplus (\msgtag{m} \patconcat \msgtag{n})$ and $\mbone \patplus (\msgtag{n}
\patconcat \msgtag{m})$.
Following~\cite{dP18:mbc}, we define a set-of-multisets semantics for mailbox
patterns; the intuition is that each multiset defines a configuration
of messages that could be present in the mailbox. For example the semantic
representation of both of the  patterns above is $\set{\multiset{},
\multiset{\msgtag{m}, \msgtag{n}}}$. We let $\mseta, \msetb$ range over

\vspace{-1em}
\begin{mathpar}
\sem{\mbzero} = \emptyset

\sem{\mbone} = \{ \multiset{} \}

\sem{E \patplus F} = \sem{E} \cup \sem{F}

\sem{E \patconcat F} = \{ \mseta \uplus \msetb \mid \mseta \in \sem{E}, \msetb
\in \sem{F} \}

\sem{\msgtag{m}} = \{ \multiset{\msgtag{m}} \}

\sem{\many{E}} = \sem{\mbone} \cup \sem{E} \cup \sem{E \patconcat E} \cup
\cdots
\end{mathpar}
\vspace{-1.25em}

The pattern $\mbzero$ is interpreted as an empty set; $\mbone$ as the
empty multiset; $\patplus$ as set union; $\patconcat$ as pointwise multiset
union; $\msgtag{m}$ as the singleton multiset; and $\many{\pata}$ as the infinite
set containing any number of concatenations of interpretations of $\pata$.

\paragraph*{Usage annotations.}
A type $\pretya$ can be a \emph{base type} $\basety$, or a mailbox type
$\mbtya$. As discussed in~\secref{sec:whatstheissue},
\emph{quasi-linearity} is used to avoid aliasing issues. \emph{Usage-annotated}
types $\tya, \tyb$ annotate mailbox types with a usage: either second class
($\usable$), or returnable ($\returnable$). There are no restrictions on the
use of a base type. Only values with a returnable type can be returned from an
evaluation frame.

\subsubsection{Operations on types.}
We say that a type is \emph{returnable}, written $\returnablepred{\tya}$, if
$\tya$ is a base type $\basety$ or a returnable mailbox type $\retty{\mbtya}$.
The $\makereturnable{-}$ operator ensures that a type is returnable,
while the $\makeusable{-}$ operator ensures that a mailbox type is second-class:

\vspace{-1em}
\begin{mathpar}
\makereturnable{\basety} = \basety

\makereturnable{\pretya} = \retty{\pretya}

\makeusable{\basety} = \basety

\makeusable{\pretya} = \usablety{\pretya}
\end{mathpar}
\vspace{-1.25em}

We also extend the operators to usage-annotated types (\eg\
$\makeusable{\retty{J}} = \usablety{J}$) and type environments.

\paragraph*{Subtyping.}
With a semantics defined, we can consider subtyping.
A pattern $\pata$ is \emph{included} in a pattern $\patb$, written $\pata \incll
\patb$, if every multiset in the semantics of $\pata$ also occurs in the
semantics of pattern $\patb$, \ie, $\pata \incll \patb \defeq \sem{\pata}
\subseteq \sem{\patb}$.

\begin{definition}[Subtyping]
The \emph{subtyping} relation is defined by the following rules:

\vspace{-1em}
\begin{mathpar}
\inferrule
{ }
{ \basety \subtype \basety }

\inferrule
{ \pata \subpatone \patb \\ \usage_1 \subusage \usage_2 }
{ \usageann{\usage_1}{\tyrecv{\pata}} \subtype \usageann{\usage_2}{\tyrecv{\patb}}  }

\inferrule
{ \patb \subpatone \pata \\ \usage_1 \subusage \usage_2 }
{ \usageann{\usage_1}{\tysend{\pata}} \subtype \usageann{\usage_2}{\tysend{\patb}}  }
\end{mathpar}
\vspace{-0.25em}

\emph{Usage subtyping} is defined as the smallest reflexive
operator defined by axioms $\usage \subusage \usage$ and ${\returnable}
\subusage {\usable}$.
We write $\tya \tyequiv \tyb$ if both $\tya \subtype \tyb$ and $\tyb \subtype
\tya$, \ie\ either $\tya, \tyb$ are the same base type, or are mailbox types
with the same capability and pattern semantics.
\end{definition}

Base types are subtypes of themselves. As with previous accounts
of subtyping in actor languages~\cite{HeWT14:takka}, subtyping is
\emph{covariant} for
mailbox types with a receive capability: a mailbox can safely be replaced with
another that can receive more messages.
Likewise  subtyping is \emph{contravariant} for mailboxes with a
send capability: a mailbox can safely be replaced with another that can send
a smaller set of messages.
Intuitively, as returnable usages are more powerful than second-class usages,
returnable types can be used when only a second-class type is required.

Following~\citet{dP18:mbc} we introduce names for particular classes of mailbox
types. Intuitively, relevant mailbox names \emph{must} be used, whereas
irrelevant names need not be. Likewise reliable and usable names \emph{can} be
used, whereas unreliable and unusable names cannot.

\begin{definition}[Relevant, Reliable, Usable]
A mailbox type $\mbtya$ is \emph{relevant} if $\mbtya \not\subtype \mbsendone$, and
\emph{irrelevant} otherwise;
\emph{reliable} if $\mbtya \not\subtype \mbrecvzero$ and
\emph{unreliable} otherwise; and
\emph{usable} if $\mbtya \not\subtype \mbsendzero$ and
\emph{unusable} otherwise.
\end{definition}

\begin{definition}[Unrestricted and Linear Types]
We say that a type $\tya$ is \emph{unrestricted}, written $\un{\tya}$, if
$\tya = \basety$, or $\tya = \usablety{\mbsendone}$.
Otherwise, we say that $\pretya$ is \emph{linear}.
\end{definition}

Our type system ensures that variables with a linear type must be used, whereas
variables with an unrestricted type can be discarded.
We extend subtyping to type environments, making it possible to combine
type environments, as in~\cite{CrafaP17, dP18:mbc}.

\begin{definition}[Environment subtyping]
Environment subtyping $\tyenv_1 \subtype \tyenv_2$ is
defined as follows:
\vspace{-1em}

\begin{mathpar}
\inferrule
{ }
{ \cdot \subtype \cdot }

\inferrule
{ \un{\tya} \\
x \not\in \dom{\tyenv'} \\ \tyenv \subtype \tyenv' }
{ \tyenv, x : \tya \subtype \tyenv' }

\inferrule
{ \tya \subtype \tyb \\ \tyenv \subtype \tyenv' }
{ \tyenv, x : \tya \subtype \tyenv', x : \tyb }
\end{mathpar}
\end{definition}

We include a notion of weakening into the subtyping relation, so an
environment $\tyenv$ can be a subtype environment of $\tyenv'$ if it
contains additional entries of unrestricted type.

\paragraph{Type combination.}
Mailbox types ensure that sends and receives ``balance out'', meaning that every
send is matched with a receive. For example, using a mailbox at type
$\tysend{\msgtag{Put}}$ and $\tyrecvp{\msgtag{Put} \patconcat
\many{\msgtag{Get}}}$ results in a mailbox type $\tyrecvp{\many{\msgtag{Get}}}$.
The key technical device used to achieve this goal is \emph{type
combination}: combining a mailbox type $\tysend{\pata}$ and a
mailbox type $\tysend{\patb}$ results in an output mailbox type which must send
\emph{both} $\pata$ \emph{and} $\patb$; combining an input and an output
capability results in an input capability that no longer needs to receive the
output pattern. We can also combine  identical base types.
Note that it is \emph{not} possible to combine two input capabilities as this
would permit simultaneous reads of the same mailbox.

\begin{definition}[Type combination]
\emph{Type combination} $\mbcombtwo{\pretya}{\pretyb}$ is the commutative
partial binary operator defined by the following axioms:
\vspace{-1em}

\begin{mathpar}
\mbcombtwo{\basety}{\basety} = \basety

\mbcombtwo{\tysend{\pata}}{\tysend{\patb}} = \tysendp{\pata \patconcat \patb}

\mbcombtwo{\tysend{\pata}}{\tyrecvp{\pata \patconcat \patb}} = \tyrecv{\patb}

\mbcombtwo{\tyrecvp{\pata \patconcat \patb}}{\tysend{\pata}} = \tyrecv{\patb}
\end{mathpar}
\end{definition}

Following~\citet{CrafaP17}, it is convenient to identify types up to
commutativity and associativity, \eg\ we do not distinguish between
$\retty{\tyrecvp{\msgtag{A} \patconcat \msgtag{B}}}$ and
$\retty{\tyrecvp{\msgtag{B} \patconcat \msgtag{A}}}$.
We may however need to use subtyping to rewrite a type into a form that allows two
mailbox types to be combined (\eg\ to combine $\tysend{\msgtag{A}}$ and
$\tyrecvp{\many{\msgtag{A}}}$, we would need to use subtyping to rewrite
the latter type to $\tyrecvp{\msgtag{A} \patconcat \many{\msgtag{A}}}$).

The following \emph{usage combination} is not commutative as a $\usable$
variable use must occur \emph{before} a $\returnable$ use (ensuring that the
returnable use is the variable's last lexical occurrence). Furthermore, note
that $\scombtwo{\returnable}{\returnable}$ is undefined (ensuring that there is
only one returnable instance of a variable per thread).

\begin{definition}[Usage combination]
The \emph{usage combination} operator is the partial binary
operator defined by the axioms
$\usagecombtwo{\usable}{\usable} = \usable$ and
$\usagecombtwo{\usable}{\returnable} = \returnable$.
\end{definition}

We can now define usage-annotated type and environment combination.

\begin{definition}[Usage-annotated type combination]
The \emph{usage-annotated type combination} operator $\scombtwo{\tya}{B}$ is
the binary operator defined by the axioms
$\scombtwo{\basety}{\basety} = {\basety}$ and
\scombtwo
\end{definition}

\begin{definition}[Environment combination ($\tyenv$)]
Usage-annotated environment combination $\scombtwo{\tyenv_1}{\tyenv_2}$ is the
smallest partial operator on type environments closed under the
following rules:
\vspace{-1em}

\begin{mathpar}
\inferrule
{ }
{ \scombtwo{\cdot}{\cdot} = \cdot}

\inferrule
{ x \not\in \dom{\tyenv_2} \\
\scombtwo{\tyenv_1}{\tyenv_2} = \tyenv
\scombtwo{(\tyenv_1, x : \tya)}{\tyenv_2} = \tyenv,
x : \tya

\inferrule
{ x \not\in \dom{\tyenv_1} \\
\scombtwo{\tyenv_1}{\tyenv_2} = \tyenv
\scombtwo{\tyenv_1}{(\tyenv_2, x : \tya)} =
\tyenv, x : \tya

\inferrule
\scombtwo{\tyenv_1}{\tyenv_2} = \tyenv
\scombtwo{(\tyenv_1, x : \tya)}{(\tyenv_2, x : \tyb)} =
\tyenv, x : (\scombtwo{\tya}{\tyb})
\end{mathpar}
\end{definition}

We use usage-annotated type combination when combining the types of two
variables used in
subsequent evaluation frames (\ie\ in the subject and body of a
$\calcwd{let}$ expression).
We also require \emph{disjoint} combination, where two environments are only
able to share variables of base type:

\begin{definition}[Disjoint environment combination]
Disjoint environment combination $\pluscombtwo{\tyenv_1}{\tyenv_2}$ is the
smallest partial operator on type environments closed under the
following rules:

\begin{mathpar}
\inferrule
{ }
{ \pluscombtwo{\cdot}{\cdot} = \cdot }

\inferrule
{ x \not\in \dom{\tyenv_2} \\
\pluscombtwo{\tyenv_1}{\tyenv_2} = \tyenv
{ \pluscombtwo{\tyenv_1, x : \tya}{\tyenv_2} = \tyenv, x : \tya }

\inferrule
{ x \not\in \dom{\tyenv_1} \\
\pluscombtwo{\tyenv_1}{\tyenv_2} = \tyenv
{ \pluscombtwo{\tyenv_1}{\tyenv_2, x : \tya} = \tyenv, x : \tya }

\inferrule
{ \pluscombtwo{\tyenv_1}{\tyenv_2} = \tyenv }
{ \pluscombtwo{\tyenv_1, x : \basety}{\tyenv_2, x : \basety} = \tyenv, x : \basety }
\end{mathpar}
\end{definition}

\begin{figure}[t]

\headertwo
{Typing rules for programs and definitions}
\begin{mathpar}
\inferrule
\prog = \progdef{\sigs}{\seq{D}}{\tma} \\
(\defseq[\prog]{D_i})_i \\
\tseq[\prog]{\cdot}{\tma}{\tyunit}
{ \progseq{\prog} }

\inferrule
\tseq[\prog]{\seq{x : \tya}}{\tma}{\tyb}
{ \defseq[\prog]{\fndef{f}{\seq{x : \tya}}{\tyb}{\tma}} }
\end{mathpar}

\headersig{Typing rules for terms}{$\tseq[\prog]{\tyenv}{\tma}{\tya}$}
\begin{mathpar}
\inferrule
{ }
{ \vseq{\hastypetwo{x}{\tya}}{x}{\tya}  }

\inferrule
{ c \text{ has base type } \basety }
{ \vseq{\cdot}{c}{\basety} }

\inferrule
\prog(f) = \fndef{f}{\seq{x : \tya}}{\tyb}{\tma} \\
(\vseq{\tyenv_i}{\vala_i}{\tya_i})_{i \in 1..n}
{ \tseq{\tyenv_1 + \cdots + \tyenv_n}{\fnapp{f}{\vala_1, \ldots, \vala_n}}{\tyb} }

\inferrule
\tseq{\tyenv_1}{\tma}{\makereturnable{\pretya}} \\
\tseq{\tyenv_2, x : \makereturnable{\pretya}}{\tmb}{\tyb}
{ \tseq{\scombtwo{\tyenv_1}{\tyenv_2}}{\letin[\pretya]{x}{\tma}{\tmb}}{\tyb} }

\inferrule
\tseq{\tyenv}{\tma}{\one}
\tseq{\makeusable{\tyenv}}{\spawn{\tma}}{\one} }

\inferrule
{ }
{ \tseq{\cdot}{\mbnew}{\retty{\mbrecvone}} }

\inferrule
\proglookup{\algomsg{m}} = \seq{\pretya} \\
\tseq{\tyenv}{\vala}{\usablety{\tysend{\algomsg{m}}}} \\\\
(\tseq{\tyenv'_i}{\valb_i}{\makeusable{\pretya_i}})_{i \in 1..n}
{ \tseq
{\tyenv + \tyenv'_1 + \ldots +  \tyenv'_n }

\inferrule
\tseq{\tyenv_1}{\vala}{\retty{\tyrecv{\patb}}} \\
\gseq{\patb}{\tyenv_2}{\seq{G}}{\tya} \\
\subpat{\pata}{\patb} \\
\pnf{\patb}
{ \tseq{{\tyenv_1} + {\tyenv_2}}{\guardann{\vala}{\pata}{\seq{G}}}{\tya} }

\inferrule
{ \subtypetwo{\tyenv}{\tyenv'} \\
\subtypetwo{\tya}{\tyb} \\
\tseq{\tyenv'}{\tma}{\tya} }
{ \tseq{\tyenv}{\tma}{\tyb}  }
\end{mathpar}

\headertwo
{Typing rules for guards}
\framebox{$\gseq[\prog]{\pata}{\tyenv}{\seq{\gd}}{\tya}$}
\framebox{$\gseq[\prog]{\pata}{\tyenv}{\gd\vphantom{\seq{\gd}}}{\tya}$}
\begin{mathpar}
\inferrule
\gseq
{\pata_1 \patplus \ldots \patplus \pata_n}

\inferrule
{ }
{ \gseq{\mbzero}{\tyenv}{\fail}{\tya} }

\inferrule
\tseq{\tyenv}{\tma}{\tya}
{ \gseq{\mbone}{\tyenv}{\free{\tma}}{\tya} }

\inferrule
\prog(\msgtag{m}) = \seq{\pretya} \\
\base{\seq{\pretya}} \vee \base{\tyenv} \\\\
\tseq
y : \usageann{\returnable}{\tyrecv{E}},
\seq{x} : \seq{\makeusable{\pretya}}}
\gseq{\algomsg{m} \!\patconcat\!
\end{mathpar}

\headersig{Pattern residual}{$\pata \without \msgtag{m}$}
\begin{mathpar}
\inferrule
{ \mbzero \without \defmsg \defeq \mbzero }

\inferrule
{ \mbone \without \defmsg \defeq \mbzero }

\inferrule
{ \msgtag{m} \without \msgtag{m} \defeq \mbone }

\inferrule
{ \msgtag{m} \ne \msgtag{n} }
{ \algomsg{m} \without \algomsg{n} \defeq \mbzero }

\inferrule
{ (\patplustwo{\pata}{\patb}) \without \defmsg
\defeq (\pata \without \defmsg) \patplus (\patb \without \defmsg) }

\inferrule
{ (\pata \patconcat \patb) \without \defmsg \defeq
((\pata \without \defmsg) \patconcat \patb) \patplus
(\pata \patconcat (\patb \without \defmsg))
\end{mathpar}

\headertwo
{Pattern normal form (PNF)}
\begin{mathpar}
\inferrule
{ \pnflittwo{\pata}{\mbzero} }

\inferrule
{ \pnflittwo{\pata}{\mbone} }

\inferrule
{ \patb \tyequiv \pata \without \defmsg }
{ \pnflittwo{\pata}{\defmsg \patconcat \patb} }

\inferrule
{ \pnflittwo{\pata}{\patb_1} \\ \pnflittwo{\pata}{\patb_2} }
{ \pnftwo{\pata}{\patb_1 \patplus \patb_2} }

\inferrule
{ \pnflittwo{\pata}{\patb} }
{ \pnftwo{\pata}{\patb} }
\end{mathpar}
\caption{\langname declarative term typing}
\label{fig:declarative-typing}
\end{figure}

\subsubsection{Typing rules}
Fig.~\ref{fig:declarative-typing} shows the declarative typing rules for
\langname. As the system is declarative it helps to read the rules top-down.

\paragraph*{Programs and definitions.}
A program is typable if all of its definitions are typable, and its body has
unit type. A definition $\fndef{f}{\seq{x : \tya}}{\tyb}{\tma}$ is typable if
$\tma$ has type $\tyb$ under environment $\seq{x : \tya}$.

\paragraph*{Terms.}
Term typing has the judgement $\tseq[\prog]{\tyenv}{\tma}{\tya}$, which states
that when defined in the context of program $\prog$, under environment $\tyenv$,
term $\tma$ has type $\tya$. We omit the $\prog$ parameter in the rules for readability.
Rule \textsc{T-Var} types a variable in a singleton environment; we
account for weakening in \textsc{T-Sub}. Rule \textsc{T-Const}
types a constant under an empty environment; we assume an implicit schema
mapping constants to types, and assume at least the unit value $()$ of type
Rule \textsc{T-App} types function application according to the definition in
$ \prog$. Each argument must be typable under a disjoint type
environment to avoid aliasing mailbox names in the body of the

Rule \textsc{T-Let} types sequential composition. The subject of the
$\calcwd{let}$ expression must be returnable; since
$\scombtwo{\tyenv_1}{\tyenv_2}$ is defined, we know that if the subject
(typable using $\tyenv_1$) contains
a returnable variable, then it cannot appear in $\tyenv_2$.
This avoids aliasing and use-after-free errors.

Rule \textsc{T-Spawn} types spawning a term $M$ of unit type as a new process.
The type environment used to type $M$ can contain any number of returnable, but
the conclusion of the rule  `masks' any returnable types as second-class.
Intuitively, this is because there is no need to impose
an ordering on how a variable is used in a separate process: while
within a single process a \calcwd{guard} on some name $x$ should not precede a
send on $x$, there is no such restriction if the two expressions are executing
in concurrent processes.
Rule \textsc{T-New} creates a fresh mailbox with type $\retty{\mbrecvone}$,
since subsequent sends and receives must ``balance out'' to an empty mailbox.

Rule \textsc{T-Send} types a send expression $\send{V}{m}{\seq{W}}$, where a
message $\msgtag{m}$ with payloads $\seq{W}$ is sent to a mailbox $V$.
Value $\vala$ must be a reference
with type $\usablety{\tysend{\msgtag{m}}}$, meaning that it can be used to send
message $\msgtag{m}$. The mailbox only needs to be \emph{second-class}, but
subtyping means that we can also send to a first-class name. All payloads
$\seq{V}$ must be subtypes of the types defined by the signature for message
$\msgtag{m}$, and payloads must be typable under separate environments
to avoid aliasing when receiving a message.
Unlike in session-typed functional programming languages, sending is a
side-effecting operation of type $\one$, and the behavioural typing is accounted
for in environment composition.

Rule \textsc{T-Guard} types the  expression $\guardann{\vala}{\pata}{\seq{\gd}}$,
that retrieves from mailbox $\vala$ with some pattern $\pata$ using guards $\seq{\gd}$.
The first premise ensures that under a type environment $\tyenv_1$, mailbox $V$
has type $\retty{\tyrecv{\patb}}$: the mailbox should have a receive capability
with pattern $\patb$, and must be returnable. Demanding that the mailbox is
returnable rules out use-after-free errors since we cannot use the mailbox name
in the continuation.
The second premise states that under type environment $\tyenv_2$, guards $\seq{G}$ all return a value of type
$\tya$ and correspond to pattern $\patb$. The third premise requires that the
pattern assertion $\pata$ is
contained within $\patb$.  The final premise, $\pnf{\patb}$, ensures
that $\patb$ is in \emph{pattern normal form}: the pattern should be a
disjunction of pattern literals. That is $\mbzero$, $\mbone$, or
$\patconcattwo{\msgtag{m}}{\patb}$, where $\patb$ is equivalent to $\pata$
without message $\msgtag{m}$.

Finally, rule \textsc{T-Sub} allows the use of
subtyping. Subtyping on type environments is crucial when constructing
derivations, \eg\ two patterns may have the same semantics but differ
syntactically. Applying \textsc{T-Sub} makes it possible to rewrite
mailbox types so that they can be combined by the type combination
operators. We also allow the usual use of subsumption on return types, \eg\
allowing a value with a subtype of a function argument to be used.

\paragraph*{Guards.}

Rule \textsc{TG-GuardSeq} types a sequence of guards, ensuring that each guard is
typable under the same type environment and with the same return type.
\textsc{TG-Fail} types a failure guard: since the type system will ensure that
such a guard is never evaluated, it can have any type environment and any type,
and is typable under pattern literal $\mbzero$. Rule \textsc{TG-Free} types a
guard of the form $\free{M}$, where $M$ has type $\tya$.
Finally, rule \textsc{TG-Recv} types a guard of the form
$\receive{m}{\seq{x}}{y}{\tma}$, that retrieves a message with tag $\msgtag{m}$
from the mailbox, binding its payloads (whose types are retrieved from the
signature for message $\msgtag{m}$) to $\seq{x}$, and re-binding the mailbox to
$y$ with an updated type in continuation $\tma$. The payloads are made
\emph{usable} rather than returnable, as otherwise the payloads could interfere
with the names in the enclosing context.

\paragraph*{Pattern residual.}
The \emph{pattern residual} $\pata \without \msgtag{m}$ calculates the pattern
$\pata$ after $\msgtag{m}$ is consumed, and corresponds to the Brzozowski
derivative~\cite{B64} over a commutative regular expression.
The residual of $\mbzero$, $\mbone$, or $\msgtag{n}$ (where $\msgtag{n} \ne
\msgtag{m}$) with respect to a message tag $\msgtag{m}$ is the unreliable type
The derivative of $\msgtag{m}$ with respect to $\msgtag{m}$ is $\mbone$. The
derivative operator distributes over $\patplus$, and the derivative of
concatenation is the disjunction of the derivative of each subpattern.

\paragraph*{Example.}

We end this section by showing the derivation for the $\mkwd{client}$ definition
from the future example in~\secref{sec:introduction}, which creates a future and
self mailbox, initialises the future with a number, and then requests and prints
the result.  In the following, we abbreviate $\var{future}$ to $\var{f}$,
$\var{self}$ to $s$, and $\var{result}$ to $r$. We assume that the program
includes a signature $\sigs = [\msgtag{Put} \mapsto \tyint, \msgtag{Get} \mapsto
\tysend{\msgtag{Reply}}, \msgtag{Reply} \mapsto \tyint]$, and the
$\mkwd{emptyFuture}$ and $\mkwd{fullFuture}$ definitions
We split the derivation into three subderivations. Since it is easier to read
derivations top-down, we start by typing the $\calcwd{guard}$ expression. In the
following, we refer to the $\calcwd{receive}$ guard as $G$, and name the first derivation $\derivd_1$:

\begin{mathpar}
\inferrule
\inferrule
{ }
\tseq
{ \var{s} : \retty{\tyrecvp{\msgtag{Reply} \patconcat \mbone}}}
{ \var{s} }
{ \retty{\tyrecvp{\msgtag{Reply} \patconcat \mbone}} }
\\
\inferrule
\inferrule
\inferrule
{ \inferrule*
{ }
{ \tseq{\var{s} :
\retty{\tyrecv{\mbone}}}{\var{s}}{\retty{\tyrecv{\mbone}}} }
{ \tseq
{\var{s} : \retty{\tyrecv{\mbone}}}
\\
\tseq
{\var{r} : \tyint}
\tseq
{ \var{s} : \retty{\mbrecvone}, \var{r} : \tyint}
{ \sugarfree{\var{s}}; \mkwd{print}(\mkwd{intToString}(\var{r})) }
{ \one}
{ \gseq
{\msgtag{Reply} \patconcat \mbone}
\cdot
\bl
\receivethree{Reply}{\var{r}}{\var{s}} \\
\quad \sugarfree{\var{s}};
\mkwd{print}(\mkwd{intToString}(\var{r}))
\el
\\
\bl
\msgtag{Reply} \subpatone \msgtag{Reply} \patconcat \mbone
\\
\pnf{\msgtag{Reply} \patconcat \mbone}
\el
\tseq
{\var{s} : \retty{\tyrecvp{\msgtag{Reply} \patconcat \mbone}} }
\guardann{\var{s}}{\msgtag{Reply}}{G}
\end{mathpar}

The type of the $\var{s}$ mailbox in the subject of the $\calcwd{guard}$
expression is $\retty{\tyrecvp{\msgtag{Reply} \patconcat \mbone}}$
denoting that the mailbox can contain a $\msgtag{Reply}$
message and will then be empty. The $\calcwd{receive}$ guard binds $s$
at type $\retty{\mbrecvone}$ and $r$ at $\tyint$, freeing $s$ and using $r$ in
the $\mkwd{print}$ expression.  The $\msgtag{Reply}$ annotation on the guard is
a subpattern of the pattern of $s$.
The above derivation is used within derivation $\deriv{D}_2$:

\begin{mathpar}
\inferrule
\inferrule
\inferrule*
{ }
{ \tseq
{\var{f} : \usablety{\tysend{\msgtag{Put}}}}
\\
\inferrule*
{ }
{ \tseq{\cdot}{5}{\tyint} }
{ \tseq
{\var{f} : \usablety{\tysend{\msgtag{Put}}}}
\\
\inferrule*
\inferrule
\inferrule*
\inferrule*
{ }
\tseq
{\var{f} : \usablety{\tysend{\msgtag{Get}}}}
{ \tseq
{\var{f} : \retty{\tysend{\msgtag{Get}}}}
\\
\inferrule*
{ }
{ \tseq
{\var{s} : \usablety{\tysend{\msgtag{Reply}}}}
{ \tseq
{\var{f} : \retty{\tysend{\msgtag{Get}}}, \var{s} : \usablety{\tysend{\msgtag{Reply}}}}
\\
\deriv{D}_1
\tseq
{ \var{f} : \retty{\tysend{\msgtag{Get}}},
\var{s} : \retty{\mbrecvone}
\bl
\send{\var{f}}{Get}{\var{s}}; \\
\guardann{\var{s}}{\msgtag{Reply}}{G}
\el
{ \one }
{ \tseq
{\var{f} : \retty{\tysendp{\msgtag{Put} \patconcat \msgtag{Get}}},
\var{s} : \retty{\mbrecvone}
\bl
\send{\var{f}}{Put}{5}; \;
\send{\var{f}}{Get}{\var{s}}; \\
\guardann{\var{s}}{\msgtag{Reply}}{\cdots}
\el
\end{mathpar}

Here $\var{f}$ is used to send a \msgtag{Put} and then a \msgtag{Get} with  $\var{s}$ of type
as  payload.
As the two sends to the $\var{f}$ message are sequentially composed, the
type of $\var{f}$ at the root of the subderivation is
$\retty{\tysendp{\patconcattwo{\msgtag{Put}}{\msgtag{Get}}}}$. Since \var{s} is used at type $\retty{\tyrecvp{\msgtag{Reply} \patconcat
\mbone}}$ in $\derivd_1$, the send and receive patterns balance out to the empty
mailbox type $\retty{\tyrecv{\mbone}}$.
Finally, we can construct the derivation for the entire term:

\begin{mathpar}
\inferrule
\inferrule*
{ }
{ \tseq{\cdot}{\mbnew}{\retty{\mbrecvone}} }
\\
\inferrule*
\inferrule*
\inferrule*
\inferrule*
\tseq
{\var{f} : \retty{\tyrecvp{\msgtag{Put} \patconcat \many{\msgtag{Get}}}}}
{ \mkwd{emptyFuture}(\var{f}) }
{ \one }
{ \tseq
{\var{f} : \usablety{\tyrecvp{\msgtag{Put} \patconcat \many{\msgtag{Get}}}}}
\tseq
{\var{f} : \usablety{\tyrecvp{(\msgtag{Put} \patconcat
\msgtag{Get}) \patconcat \mbone}}}
\\
\inferrule*
\inferrule*
{ }
{ \tseq{\cdot}{\mbnew}{\retty{\mbrecvone}}}
\\
\deriv{D}_2
\tseq
{ \var{f} : \retty{\tysendp{\msgtag{Put} \patconcat
\msgtag{Get}} } }
\bl
\letintwo{\var{s}}{\mbnew} \\
\send{\var{f}}{Put}{5}; \cdots
\el
{ \one }
\tseq
{ \var{f} : \retty{\mbrecvone} }
\bl
\spawn{\mkwd{emptyFuture}(\var{f})}; \\
\letintwo{\var{s}}{\mbnew} \\
\send{\var{f}}{Put}{5}; \cdots
\el
{ \one }
\tseq
{ \cdot }
\bl
\letintwo{\var{f}}{\mbnew} \\
\spawn{\mkwd{emptyFuture}(\var{f})}; \\
\letintwo{\var{s}}{\mbnew} \\
\send{\var{f}}{Put}{5}; \;
\send{\var{f}}{Get}{\var{s}}; \\
\guardanntwo{\var{s}}{\msgtag{Reply}} \\
\quad \receivethree{Reply}{\var{r}}{\var{s}} \\
\qquad \sugarfree{\var{s}};\\
\qquad \mkwd{print}(\mkwd{intToString}(\var{r})) \\
\}
\el
{ \one }
\end{mathpar}

Since we let-bind \var{f} to $\mbnew$, $\var{f}$ must have type
$\retty{\mbrecvone}$. Definition $\mkwd{emptyFuture}$ requires an argument of
type $\retty{\tyrecvp{\patconcattwo{\msgtag{Put}}{\many{\msgtag{Get}}}}}$; since
the function application appears in the body of the $\calcwd{spawn}$ we can mask
the usage annotation to $\usable$, and  use environment subtyping to
rewrite the type of \var{f} to $\retty{\tyrecvp{(\msgtag{Put} \patconcat
\msgtag{Get})
\patconcat \mbone}}$.
This then balances out with the use of \var{f} in
$\derivd_2$, completing the derivation.

\begin{figure}
\header{Runtime syntax}

\begin{minipage}{0.3\textwidth}
\[
\begin{array}{lrcl}
\text{Runtime names} & a \\
\text{Names} & \nma, \nmb, \nmc & ::= & x \midspace a \\
\text{Frames} & \sigma & ::= & \fframe{x}{M} \\
\text{Frame stacks} & \framestack & ::= & \emptystack \midspace \frameconcat{\mvframe}{\framestack}\\
\end{array}
\]
\end{minipage}
\hfill
\begin{minipage}{0.6\textwidth}
\[
\begin{array}{lrcl}
\text{Guard contexts} & \ctx{G} & ::= & \seq{G_1} \cdot [~] \cdot \seq{G_2} \\
\text{Configurations} & \config{C}, \config{D} & ::= &
\thread{\tma}{\framestack} \midspace \sentmsg{a}{m}{\seq{V}} \\
& & \midspace & \config{C} \parallel \config{D} \midspace \res{a} \config{C} \\
\text{Runtime type environments} & \plainenv & ::= & \cdot \midspace \plainenv, \nma : \pretya
\end{array}
\]
\end{minipage}

\headersig{Reduction rules}{$\config{C} \cevalp \config{D}$}
\vspace{-1em}

\[
\begin{array}{lrcl}
\textsc{E-Let} &
\thread{\letin[\pretya]{x}{M}{N}}{\framestack} & \ceval &
\thread{M}{\frameconcat{\fframe{x}{N}}{\framestack}}\\
\textsc{E-Return} &
\thread{V}{\frameconcat{\fframe{x}{M}}{\framestack}} &
\ceval & \thread{M \{ V / x \}}{\framestack} \\
\textsc{E-App} & \thread{\fnapp{f}{\seq{V}}}{\framestack} & \ceval &
\thread{\tma \{ \seq{V} / \seq{x} \}}{\framestack} \\
& & &
\quad (\text{if } \prog(f) = \fndef{f}{\seq{x: \tya}}{\tyb}{\tma}) \\
\textsc{E-New} & \thread{\mbnew}{\framestack} & \ceval &
\resconf{a}{\thread{a}{\framestack}} \qquad (a \text{ is fresh}) \\
\textsc{E-Send} & \thread{\send{a}{m}{\seq{V}}}{\framestack} & \ceval &
\thread{()}{\framestack} \parallel \sentmsg{a}{m}{\seq{V}} \\
\textsc{E-Spawn} & \thread{\spawn{M}}{\framestack} & \ceval &
\thread{()}{\framestack} \parallel \thread{M}{\emptystack}
\\
\textsc{E-Free} & (\nu a)(\thread{\guardann{a}{\pata}{\ctx{G}[\free{M}]}}{\framestack}) & \ceval &
\thread{M}{\framestack} \\
\end{array}
\]
\vspace{-0.75em}
\[
\begin{array}{lrcl}
\textsc{E-Recv} &
\thread
\parallel \sentmsg{a}{m}{\seq{V}} & \ceval &
\thread
{M \{ \seq{V} / \seq{x}, a / y \}}
\end{array}
\]
\vspace{-1.5em}

\begin{mathpar}
\inferrule*
\config{C} \ceval \config{D}
\res{a}{\config{C}} \ceval \res{a}{\config{D}}

\inferrule*
\config{C} \ceval \config{C}'
{ \config{C} \parallel \config{D} \ceval \config{C}' \parallel
\config{D} }

\inferrule*
\config{C} \equiv \config{C}' \\
\config{C}' \ceval \config{D}' \\
\config{D}' \equiv \config{D}
{ \config{C} \ceval \config{D} }
\end{mathpar}
\vspace{-1.5em}
\caption{\langname operational semantics}
\label{fig:declarative:semantics}
\end{figure}

\subsection{Operational Semantics}
Figure~\ref{fig:declarative:semantics} shows the runtime syntax and reduction
rules for $\langname$. We extend values $V$ with runtime names $a$.
The concurrent semantics of the language is described as a nondeterministic
reduction relation on a language of \emph{configurations}, which resemble terms
in the $\pi$-calculus. Configuration $\thread{\tma}{\framestack}$ is a thread
evaluating term $\tma$, with frame stack $\framestack$; we will discuss frame
stacks in the next section. Configuration $\sentmsg{a}{m}{\seq{\vala}}$ denotes a
message $\msg{m}{\seq{\vala}}$ in mailbox $a$; name restriction
$\res{a}{\config{C}}$ binds name $a$ in $\config{C}$; and
$\config{C} \parallel \config{D}$ denotes the parallel composition of
$\config{C}$ and $\config{D}$.

\paragraph*{Frame stacks.}
We use frame stacks~\cite{Pitts98, EnnalsSM04} rather than evaluation
contexts for technical convenience.  A frame $\fframe{x}{\tma}$ is a pair of a
variable $x$ and a continuation $M$, where $x$ is free in $M$. A frame stack is
an ordered sequence of frames, where $\emptystack$ denotes the empty stack.

\paragraph*{Initial configuration.}
The semantics envisages a single static term $M$ (\ie, program text) to be
evaluated in the context of an empty frame stack: $\thread{\tma}{\emptystack}$.

\paragraph*{Reduction rules.}
Frame stacks are best demonstrated by the \textsc{E-Let} and \textsc{E-Return}
rules: intuitively, $\letin[\pretya]{x}{\tma}{\tmb}$ evaluates $\tma$, binding
the result to $x$ in $\tmb$. The rule adds a fresh frame $\fframe{x}{\tmb}$ to
the top of a frame stack, and evaluates $\tma$. Conversely, \textsc{E-Return}
returns $\vala$ into the parent frame: if the top frame is $\fframe{x}{\tma}$,
then we can evaluate the continuation $\tma$ with $\vala$ substituted for $x$.
Rule \textsc{E-App} evaluates the body of function $f$ with arguments
$\seq{\vala}$ substituted for the parameters $\seq{x}$.

Rule \textsc{E-New} creates a fresh mailbox name restriction and returns it into the calling context. Rule \textsc{E-Send} sends a message with
tag $\msgtag{m}$ and payloads $\seq{V}$ to a mailbox $a$, returning $()$ to the calling
context and creating a sent message configuration $\sentmsg{a}{m}{\seq{\vala}}$.
Rule \textsc{E-Spawn} spawns a computation as a fresh process, with an empty
frame stack.
Rule \textsc{E-Free} allows a name $a$ to be garbage collected if it is not
contained in any other thread, evaluating the continuation $\tma$ of the
$\calcwd{free}$ guard. Finally, rule \textsc{E-Recv} handles receiving a message
from a mailbox, binding the payload values to $\seq{x}$ and updated mailbox name
to $y$ in continuation $\tma$.
The remaining rules are administrative.

\subsection{Metatheory}

\subsubsection{Runtime typing.}
To prove metatheoretical properties about $\langname$ we introduce
a type system on configurations; this type system is used only for reasoning and
is not required for typechecking.

\paragraph*{Runtime type environments.}
The runtime typing rules make use of a type environment $\plainenv$ that maps
variables to types that \emph{do not} contain usage information. Usage
information is inherently only useful in constraining \emph{sequential} uses of
a mailbox variable, where guards are blocking, whereas it makes little sense to
constrain \emph{concurrent} usages of a variable.
Runtime type environment combination on $\pcombtwo{\plainenv_1}{\plainenv_2}$ is
similar to usage-annotated type environment combination but with two differences: it
is \emph{commutative} to account for the unordered nature of parallel
threads, and type combination does not include usage information.

\begin{definition}[Environment combination ($\plainenv$)]
Environment combination $\pcombtwo{\plainenv_1}{\plainenv_2}$ is the
smallest partial commutative binary operator on type environments closed under
the following rules:
\vspace{-1em}

\begin{mathpar}
\inferrule
{ }
{ \pcombtwo{\cdot}{\cdot} = \cdot }

\inferrule
x \not\in \dom{\plainenv_2} \\\\
\pcombtwo{\plainenv_1}{\plainenv_2} = \plainenv
\pcombtwo{(\plainenv_1, x {:} \pretya)}{\plainenv_2} = \plainenv, x {:} \pretya

\inferrule
x \not\in \dom{\plainenv_1} \\\\
\pcombtwo{\plainenv_1}{\plainenv_2} = \plainenv
\pcombtwo{\plainenv_1}{(\plainenv_2, x {:} \pretya)} =
\plainenv, x {:} \pretya

\inferrule
{ \pcombtwo{\plainenv_1}{\plainenv_2} = \plainenv }
\pcombtwo{(\plainenv_1, x {:} \pretya)}{(\plainenv_2, x {:} \pretyb)}
\plainenv, x {:} (\mbcombtwo{\pretya}{\pretyb})
\end{mathpar}
\end{definition}

\begin{figure}[t]
\headersig{Configuration Typing}{$\cseq{\plainenv}{\config{C}}$}
\begin{mathpar}
\inferrule
{ \cseq{\plainenv, a : \mbrecvone}{ \config{C} } }
{ \cseq{\plainenv}{\res{a} \config{C}} }

\inferrule
\cseq{\plainenv_1}{\config{C}} \\
\cseq{\plainenv_2}{\config{D}}
{ \cseq{\pcombtwo{\plainenv_1}{\plainenv_2}}{\config{C} \parallel \config{D}} }

\inferrule
{ (\vseq{\makeusable{\plainenv_i}}{V_i}{\tya_i})_{i \in 1..n} \\
\seq{\tya} \subtype \makeusable{\siglookup{m}}
{ \cseq{\plainenv_1 + \ldots + \plainenv_n, a : \tysend{\msgtag{m}}}{\sentmsg{a}{m}{\seq{V}} } }

\inferrule
\makereturnable{\plainenv} = \scombtwo{\tyenv_1}{\tyenv_2}  \\
\tseq{\tyenv_1}{\tma}{\tya} \\
\stackseq{\tyenv_2}{\tya}{\framestack}
{ \cseq{\plainenv}{\thread{\tma}{\framestack}} }

\inferrule
{ \plainenv \subtype \plainenv' \\
\cseq{\plainenv'}{\config{C}}
{ \cseq{\plainenv}{\config{C}} }
\end{mathpar}

\headersig{Frame Stack Typing}{$\stackseq{\tyenv}{\tya}{\framestack}$}
\vspace{-0.8em}
\begin{mathpar}
\inferrule
{ \stackseq{\cdot}{\tya}{\emptystack} }

\inferrule
\tseq{\tyenv_1, x : \tya}{M}{\tyb} \\
\returnablepred{\tyb} \\
\stackseq{\tyenv_2}{\tyb}{\framestack}
{ \stackseq
\end{mathpar}
\vspace{-1em}

\caption{\langname runtime typing}
\label{fig:declarative:rt-typing}
\end{figure}

Disjoint combination on runtime type environments $\plainenv_1 + \plainenv_2$
(omitted) is defined analogously to disjoint combination on $\tyenv$.

\paragraph*{Runtime typing rules.}
Figure~\ref{fig:declarative:rt-typing} shows the runtime typing rules.
Rule \textsc{TC-Nu} types a name restriction if the name is of type
$\mbrecvone$; in turn this ensures that sends and receives on the mailbox
``balance out'' across threads. Rule \textsc{TC-Par} allows configurations $\config{C}$ and
$\config{D}$ to be composed in parallel if they are typable under combinable
runtime type environments.
Rule \textsc{TC-Message} types a message configuration
$\sentmsg{a}{m}{\seq{V}}$.  Name $a$ of type $\tysend{\msgtag{m}}$ cannot appear
in any of the values sent as a payload. Each payload value $\vala$ must be a
subtype of the type defined by the message signature, under the second-class
lifting of a disjoint runtime type environment.
Rule \textsc{TC-Subs} allows subtyping on runtime type environments; the
subtyping relation $\plainenv \subtype \plainenv'$ is analogous to subtyping on

\paragraph*{Thread and frame stack typing.}
Rule \textsc{TC-Thread} types a thread, which is a pair of a
currently-evaluating term, typable under an environment $\tyenv_1$, and a stack
frame, typable under an environment $\tyenv_2$. The combination $\tyenv_1 \scomb
\tyenv_2$ should result in the returnable lifting of $\plainenv$: intuitively,
we should be able to use every mailbox variable in $\plainenv$ as returnable in
the thread. \textsc{TC-Thread} makes use of the frame stack typing judgement
$\stackseq{\tyenv}{\tya}{\framestack}$ (inspired by~\cite{EnnalsSM04}), which
can be read ``under type environment $\tyenv$, given a value of type $\tya$,
frame stack $\framestack$ is well-typed''.
The empty frame stack is typable under the empty
environment given any type.
A non-empty frame stack $\frameconcat{\fframe{x}{\tma}}{\framestack}$ is
well-typed if $\tma$ has some returnable type $\tyb$, given a variable $x$ of
type $\tya$. The remainder of the stack must then be well-typed given $\tyb$.
We combine the environments used for typing the head term and the remainder of
the stack using $\scomb$ as we wish to account for sequential uses of a mailbox;
for example, in the term $\send{x}{m}{\vala}; \send{x}{n}{\valb}$, $x$ would
have type $\usablety{\tysendp{\patconcattwo{\msgtag{m}}{\msgtag{n}}}}$.

\subsubsection{Properties.}

We can now state some metatheoretical results.  We relegate proofs to

Typability is preserved by reduction; the proof is nontrivial since we must do
extensive reasoning about environment combination.

\begin{restatable}[Preservation]{theorem}{preservation}
If $\progseq{\prog}$, and
$\cseq[\prog]{\Gamma}{\config{C}}$ with $\tyenv$ reliable, and
$\config{C} \cevalpnopad \config{D}$, then $\cseq[\prog]{\tyenv}{\config{D}}$.
\end{restatable}

Preservation implies mailbox conformance: the property that a configuration will
never evaluate to a singleton failure guard. To
state mailbox conformance, it is useful to define the notion of a
\emph{configuration context} $\config{H} ::= (\nu a)\ctx{H}
\midspace \ctx{H} \parallel \config{C} \midspace \thread{[~]}{\framestack}$, that allows us to focus on a single

\begin{corollary}[Mailbox Conformance]
If $\progseq{\prog}$ and $\cseq[\prog]{\tyenv}{\config{C}}$ with $\tyenv$ reliable, then $\config{C}
\mathop{\not{\cevalnopad^{*}}} \ctx{H}[\sugarfail{\vala}]$.
\end{corollary}

\paragraph*{Progress.}
To prove a progress result for $\langname$, we begin with some auxiliary definitions.

\begin{definition}[Message set]
A \emph{message set} $\mathcal{M}$ is a configuration of the form:
\parallel \cdots \parallel
\sentmsgg{a_n}{\msgtag{m}_n}{\seq{\vala_n}}$.
We say that a message set $\msgset$ \emph{contains a message} $\msgtag{m}$
\emph{for} $a$ if $\msgset \equiv \sentmsg{a}{m}{\seq{\vala}} \parallel \msgset'$.
\end{definition}

Next, we classify \emph{canonical forms}, which give us a global view of a
configuration. Every well typed process is structurally congruent to a
canonical form.

\begin{definition}[Canonical form]
A configuration $\config{C}$ is in \emph{canonical form} if it is of the
form: $(\nu a_1) \cdots (\nu a_l)(\thread{\tma_1}{\framestack_1} \parallel
\cdots \parallel \thread{\tma_m}{\framestack_m} \parallel \msgset)$
\end{definition}

\begin{definition}[Waiting]
We say that a term $\tma$ is \emph{waiting on mailbox
$a$ for a message with tag} $\msgtag{m}$,
written $\waiting{\tma}{a}{\msgtag{m}}$,
$\tma$ can be written $\guardann{a}{\pata}{\mathcal{G}[\receive{m}{x}{y}{\tmb}]}$.
\end{definition}

$\fv{-}$ denote the set of free variables in a term $\tma$ or frame stack
We can then use canonical forms to characterise a progress
result: either each thread can reduce, has reduced to a value, or is waiting for
a message which has not yet been sent by a different thread.
\begin{restatable}[Partial Progress]{theorem}{progress}\label{thm:weak-progress}
Suppose $\progseq{\prog}$ and $\cseq[\prog]{\cdot}{\config{C}}$ where $\config{C}$ is in canonical form:
\[
\config{C} = (\nu a_1) \cdots (\nu a_l)(\thread{\tma_1}{\framestack_1} \parallel
\cdots \thread{\tma_m}{\framestack_m} \parallel \msgset)
\]

Then for each $\tma_i$, either:
\begin{itemize}
\item there exist $\tma'_i, \framestack'_i$ such that
$\thread{\tma_i}{\framestack_i} \ceval
\thread{\tma'_i}{\framestack'_i}$; or
\item $\tma_i$ is a value and $\framestack_i = \epsilon$; or
\item $\waiting{\tma_i}{a_j}{\msgtag{m}_j}$
where $\msgset$ does not contain a message
$\msgtag{m}_j$ for $a_j$
and $a_j \not\in \fv{\seq{\gd_i}} \cup \fv{\framestack_i}$,
where $\seq{\gd_i}$ are the guard clauses of $\tma_i$.
\end{itemize}
\end{restatable}
A key consequence of Theorem~\ref{thm:weak-progress} is the absence of
self-deadlocks: since we can only guard on a returnable mailbox, and a
returnable name must be the last occurrence in the thread, it cannot be that the
$\calcwd{guard}$ expression is blocking a send to the same mailbox in the same thread.
As we cannot use dependency graphs~\secrefp{sec:dgs}, our progress result
does not rule out inter-process deadlocks.
\section{Algorithmic Typing}\label{sec:algorithmic}
Writing a typechecker based on \langname's declarative
typing rules is challenging due to nondeterministic context splits, environment
subtyping, and pattern inclusion. \emph{MC}$^2$~\cite{mc2} is a
typechecker for the mailbox calculus, based on a typechecker for
concurrent object usage protocols~\cite{Padovani18}. The \emph{MC}$^2$ type system has, however, not been formalised. We adopt several ideas from \emph{MC}$^2$, especially algorithmic type combination, and adapt the approach for a programming language.

\begin{figure}[t]

\begin{minipage}{0.43\textwidth}
\[
\begin{array}{lrcl}
\text{Pattern variables} & \patvara, \patvarb \\
\text{Mailbox patterns} & \ppata, \ppatb & ::= & \mbzero \midspace \mbone \midspace
\algomsg{m} \midspace \patplustwo{\ppata}{\ppatb} \\
& & \midspace &
\patconcattwo{\ppata}{\ppatb} \midspace \many{\ppata} \midspace
\patvara \\
\text{Mailbox types} & \pmbty & ::= & \tysend{\ppata}  \midspace \tyrecv{\ppata} \\
\text{Types} & \ppretya, \ppretyb & ::= & \basety \midspace \pmbty \\
\text{Usage-ann.\ types} & \ptya, \ptyb & ::= & \basety \midspace \usagety{\pmbty} \\
\end{array}
\]
\end{minipage}
\hfill
\begin{minipage}{0.55\textwidth}
\[
\begin{array}{lrcl}
\text{Augmented type envs.} & \penv & ::= & \cdot \midspace \penv, x : \ptya \\
\text{Nullable type envs.} & \nullableenv & ::= & \penv \midspace
\noenv \\
\text{Augmented definitions} & \pdef & ::= & \fndef{f}{\seq{x :
\ptya}}{\ptyb}{\tma} \\
\text{Constraints} & \phi & ::= & \subpatconstr{\ppata}{\ppatb} \\
\text{Constraint sets} & \constrs \\
\end{array}
\]
\end{minipage}
\caption{\langname syntax extended for algorithmic typing}
\label{fig:extended-syntax}
\end{figure}
\paragraph*{Type system overview.}
Our algorithmic type system takes a
\emph{co-contextual}~\cite{ErdwegBKKM15} approach: rather than taking a type environment
as an \emph{input} to the type-checking algorithm, we produce a type environment
as an \emph{output}. The intuition is that (read bottom-up),
\emph{splitting} an environment into two sub-environments is more difficult than
\emph{merging} two environments inferred from subexpressions.
We also generate \emph{inclusion constraints} on patterns to be
solved later.

Bidirectional type systems~\cite{PierceT00, DunfieldK21} split typing rules into
two classes: those that \emph{synthesise} a type $\tya$ for a term $\tma$
($\tradsynth{\tyenv}{\tma}{\tya}$), and those that
\emph{check} that a term $\tma$ has type $\tya$
($\tradchk{\tyenv}{\tma}{\tya}$). Bidirectional type systems
are syntax-directed and amenable to implementation.

We use a co-contextual variant of bidirectional typing first introduced
by~\citet{Zeilberger18:bbt}. The main twist is the variable rule, which becomes a
\emph{checking} rule and records the given variable-type mapping in the
inferred environment.

\subsection{Algorithmic Type System}

\paragraph*{Extended syntax and annotation}
A key difference in comparison to the declarative type system is the addition of
\emph{pattern variables} $\patvara$, that act as a placeholder for part of a
pattern and are generated during typechecking.
We can then generate and solve \emph{inclusion constraints} $\constr$
on patterns.  Figure~\ref{fig:extended-syntax} shows the extended syntax used in
the algorithmic system.

\paragraph*{Constraints}
An important challenge for the algorithmic type system is determining whether one
pattern is \emph{included} within another: \eg\ $\msgtag{m} \subpatone
\many{\msgtag{m}}$.
Given that patterns may contain pattern variables, we may need to defer
inclusion checking until more pattern variables are known, so we
introduce inclusion constraints $\subpatconstr{\ppata}{\ppatb}$ which require
that pattern $\ppata$ is included in pattern $\ppatb$.

\begin{figure}[t]
\headersig{Unrestrictedness}{$\unrseq{\ptya}{\constrs}$}
\begin{mathpar}
\inferrule
{ }
{ \unrseq{\basety}{\emptyset} }

\inferrule
{ }
{ \unrseq{\usablety{\tysend{\ppata}}}{\set{\subpatconstr{\mbone}{\ppata}}} }
\end{mathpar}

\headertwo
{\framebox{$\usage_1 \subtype \usage_2$}
\framebox{$\subtyseq{\ptya}{\ptyb}{\constrs}$}
\begin{mathpar}
\inferrule
{ }
{ \subtypetwo{\usage}{\usage} }

\inferrule
{ }
{ \subtypetwo{\bcirc}{\wcirc} }

\inferrule
{ }
{ \subtyseq{\basety}{\basety}{\emptyset} }

\inferrule
\subtypetwo{\usage_1}{\usage_2}
\subtyseq
{\usageann{\usage_1}{\tysend{\ppata}} }
{\usageann{\usage_2}{\tysend{\ppatb}} }
{ \subpatconstr{\ppatb}{\ppata} }

\inferrule
\subtypetwo{\usage_1}{\usage_2}
\subtyseq
{ \subpatconstr{\ppata}{\ppatb} }
\end{mathpar}

\headertwo{Type
\begin{mathpar}
\inferrule
{ }
{ \joinseq

\inferrule
\patvara {\text{ fresh}}
\joinseq
{ \tysend{\ppata} }
{ \tyrecv{\ppatb} }
{ \tyrecv{\patvara} }
{ \{ \subpatconstr{(\patconcattwo{\ppata}{\patvara})}{\ppatb} \} }

\inferrule
\patvara {\text{ fresh}}
\joinseq
{ \{ \subpatconstr{(\patconcattwo{\ppatb}{\patvara})}{\ppata} \} }

\inferrule
\joinseq{\pmbty_1}{\pmbty_2}{\pmbty}{\constrs}
\joinseq
{ \constrs }

\inferrule
{ \joinseq
\end{mathpar}

\headertwo
{Type merge}
\framebox{$\mergeseq{\ptya_1}{\ptya_2}{\ptyb}{\constrs}$}}
\begin{mathpar}
\inferrule
{ }
\mergeseq
{ \tysend{\ppata} }
{ \tysend{\ppatb} }
{ \tysendp{\patplustwo{\ppata}{\ppatb}} }
{ \emptyset}

\inferrule
\patvara \text{ fresh}
\mergeseq
{ \tyrecv{\ppata} }
{ \tyrecv{\ppatb} }
{ \tyrecv{\patvara} }
{ \set
\subpatconstr{\patvara}{\ppata},
\subpatconstr{\patvara}{\ppatb}

\inferrule
\mergeseq{\pmbty_1}{\pmbty_2}{\pmbty}{\constrs}
\mergeseq
{ \usageann{\usage_1}{\pmbty_1} }
{ \usageann{\usage_2}{\pmbty_2}}
{ \usageann{\maxusage{\usage_1}{\usage_2}}{\pmbty}}
{ \constrs }

\inferrule
{ }
{ \mergeseq
\end{mathpar}
\caption{\langname algorithmic type operations}
\label{fig:algo-type-operations}
\end{figure}

\subsubsection{Algorithmic type operations}
Fig.~\ref{fig:algo-type-operations} shows the algorithmic type combination

\paragraph*{Unrestrictedness and subtyping.}
The algorithmic unrestrictedness operation $\unrseq{\ptya}{\constrs}$ states that
$\ptya$ is unrestricted subject to constraints $\constrs$, and the definition
reflects the fact that a type is unrestricted in the declarative system if it is
a base type or a subtype of $\usablety{\mbsendone}$.
Algorithmic subtyping is similar: a base type is a subtype of itself,
and we check that two mailbox types with the same capability are subtypes of
each other by generating a contravariant constraint for a send type,
and a covariant constraint for a receive type.

\paragraph*{Algorithmic type join.}
Declarative mailbox typing relies  on
the subtyping rule  to manipulate types into a form where
they can be combined with the type combination operators, \eg,
$\mbcombtwo{\tysend{\pata}}{\tyrecvp{\pata \patconcat \patb}} =
\tyrecv{\patb}$. The algorithmic type system cannot apply the same technique as it does
not know, \emph{a priori}, the form of each pattern. Instead, the algorithmic
\emph{type join} operation allows the combination of two mailbox types irrespective
of their syntactic form. Combining two send types is the same as in the
declarative system, but combining a send type with a receive type (and vice
versa) is more interesting: say we wish to combine $\tysend{\ppata}$ and
$\tyrecv{\ppatb}$. In this case, we generate a fresh pattern variable
$\patvara$; the result is $\tyrecv{\patvara}$ along with the constraint that
$\subpatconstr{(\ppata \patconcat \patvara)}{\ppatb}$: namely, that the send
pattern concatenated with the fresh pattern variable is included in the pattern

As an example, joining $\tysend{\msgtag{m}}$ and
$\tyrecvp{\patconcattwo{\msgtag{n}}{\msgtag{m}}}$ produces a receive mailbox
type $\tyrecv{\patvara}$ and a constraint $\subpatconstr{(\msgtag{m} \patconcat
\patvara)}{(\patconcattwo{\msgtag{n}}{\msgtag{m}})}$, for which a valid solution
is $\patvara \mapsto \msgtag{n}$, and hence the expected combined type

\paragraph*{Algorithmic type merge.}
In the declarative type system branching control flow requires that each branch
is typable under the same type environment (using the \textsc{T-Subs} rule).
The algorithmic type system instead generates constraints that ensure that each
type is used consistently across branches using the \emph{algorithmic type merge} operation
Two base types are merged if they are identical.
In the case of mailbox types, the function takes the maximum usage annotation, so
$\maxusage{\returnable}{\usable} = \returnable$. It ensures that when
merging two output capabilities the patterns are combined using
pattern disjunction. Conversely merging two input capabilities generates a
new pattern variable that must be included in both merged patterns.

\paragraph*{Algorithmic environment combination.}
We can extend the algorithmic type operations to type environments; the
(omitted, see Appendix~\ref{ap:defs}) rules are adaptations of the corresponding
declarative operations. Notably, when combining two
environments used in branching control flow such as conditionals where an
output mailbox $\tysend{\ppata}$ is used in one environment but not the other, the
resulting type is $\tysendp{\ppata \patplus \mbone}$ to signify the
\emph{choice} of not sending on the mailbox name.

\paragraph*{Nullable type environments.}
Checking a $\fail$ guard produces a \emph{null} environment $\noenv$ which can
be composed with \emph{any other} type environment, as shown by the following

\begin{definition}[Nullable environment combination]
For each combination operator $\combineop \in \set{\envjoin, \envmerge, +}$
we extend environment combination to nullable type environments,
$\opseq{\nullableenv_1}{\nullableenv_2}{\nullableenv}{\constrs}$ by extending
each environment combination operation with the following rules:

\vspace{-1em}
\begin{mathpar}
\inferrule
{ }
{ \opseq{\noenv}{\noenv}{\noenv}{\emptyset} }

\inferrule
{ }
{ \opseq{\noenv}{\penv}{\penv}{\emptyset} }

\inferrule
{ }
{ \opseq{\penv}{\noenv}{\penv}{\emptyset} }
\end{mathpar}
\end{definition}

Nullable type environments are a supertype of every defined
type environment: $\penv \subtype \noenv$.

\begin{figure}[t]
\headertwo
{Constraint generation for programs and definitions}
\framebox{$\algoprogseq{\prog}{\constrs}$}~
\framebox{$\algodefseq{\fndef{f}{\seq{x : \ptya}}{\ptyb}{\tma}}{\constrs}$}
\begin{mathpar}
\inferrule
\prog = \progdef{\sigs}{\seq{D}}{\tma} \\
(\algodefseq{D_i}{\constrs_i})_i \\
\chkseq{\tma}{\one}{\cdot}{\constrs}
{ \algoprogseq{\prog}{\constrs \cup \constrs_1 \cup \cdots \cup \constrs_n} }

\inferrule
\chkseq{\tma}{\ptyb}{\penv}{\constrs_1} \\
\checkenvseq{\seq{x}}{\seq{\ptya}}{\penv}{\constrs_2} \\
\penv \envwithout \seq{x} = \cdot
{ \algodefseq{\fndef{f}{\seq{x : \ptya}}{\ptyb}{\tma}}{ \constrs_1
\cup \constrs_2} }
\end{mathpar}

\headertwo
{Constraint generation (synthesis)}
\framebox{$\synthseq[\prog]{\tma}{\ptya}{\penv}{\constrs}$}

\begin{mathpar}
\inferrule
{ c \text{ has base type } \basety }
{ \synthseq{c}{\basety}{\cdot}{\emptyset} }

\inferrule
{ }
\synthseq{\mbnew}{\retty{\mbrecvone}}{\cdot}{\emptyset}

\inferrule
\chkseq{\tma}{\one}{\penv}{\constrs}
{ \synthseq{\spawn{\tma}}{\one}{\makeusable{\penv}}{\constrs} }

\inferrule
\prog(\msgtag{m}) = \seq{\ppretya} \\
\chkseq{\pvala}{\usablety{\tysend{\algomsg{m}}}}{\penv'}{\constrs} \\\\
\in 1..n} \\
\combineseqmany{\penv' + \penv'_1 + \ldots + \penv'_n}{\penv}{\constrs''}
{ \synthseq
{\constrs \cup \constrs'_1 \cup \ldots \cup \constrs'_n \cup \constrs''}

\inferrule
\prog(f) = {\tyfun{\seq{\ptya}}{\ptyb}} \\\\
(\chkseq{\pvala_i}{\ptya_i}{\penv_i}{\constrs_i})_{i \in 1..n} \\
\combineseqmany{\penv_1 + \ldots + \penv_n}{\penv}{\constrs}
{ \synthseq
{ \fnapp{f}{\pvala_1, \ldots, \pvala_n} }
{\constrs \cup \constrs_1 \cup \ldots \cup \constrs_n}
\end{mathpar}

\headertwo
{Constraint generation (checking)}
\framebox{$\chkseq[\prog]{\tma}{\ptya}{\penv}{\constrs}$}
\begin{mathpar}
\inferrule
{ }
{ \chkseq{x}{\ptya}{x : \ptya}{\emptyset} }

\inferrule
\chkseq{\tma}{\makereturnable{\pretya}}{\penv_1}{\constrs_1} \\
\chkseq{\tmb}{\ptya}{\penv_2}{\constrs_2} \\\\
\checkenvseq{\penv_2}{x}{\makereturnable{\pretya}}{\constrs_3} \\
\joinseq{\penv_1 \envwithout x}{\penv_2}{\penv}{\constrs_4}
\chkseq
{ \ptya }
{ \penv }
{ \constrs_1 \cup \cdots \cup \constrs_4 }

\inferrule
\chkgseq
{\patb} \\
\chkseq{\vala}{\retty{\tyrecv{\patb}}}{\penv'}{\constrs_2} \\
\combineseq{\nullableenv}{\penv'}{\penv}{\constrs_3}
{ \chkseq
{\constrs_1 \cup \constrs_2 \cup \constrs_3 \cup
\set{\subpatconstr{\pata}{\patb} }}

\inferrule
{ \synthseq{\tma}{\ptya}{\penv}{\constrs_1} \\
\subtyseq{\ptya}{\ptyb}{\constrs_2}
{ \chkseq{\tma}{\ptyb}{\penv}{\constrs_1 \cup \constrs_2} }
\end{mathpar}

\headertwo
{Environment lookup}
\framebox{$\checkenvseq{\penv}{\seq{x}}{\seq{\ptya}}{\constrs}$}

\begin{mathpar}
\inferrule
{ x \not\in \dom{\penv} \\ \unrseq{\ptya}{\constrs} }
{ \checkenvseq{\penv}{x}{\ptya}{\constrs} }

\inferrule
{ \subtyseq{\ptyb}{\ptya}{\constrs} }
{ \checkenvseq{(\penv, x : \ptya)}{x}{\ptyb}{\constrs} }

\inferrule
{ \checkenvseq
{\constrs_1 \cup \cdots \cup \constrs_n} }
\end{mathpar}

\caption{\langname algorithmic typing (programs, definitions, and terms)}
\label{fig:algo-typing-terms}
\end{figure}

Figure~\ref{fig:algo-typing-terms} shows the \langname algorithmic
typing of programs, definitions and terms.  The key idea is to remain in
checking mode for as long as possible, in order to propagate type information to
the variable rule and construct a type environment.
We write
$\penv \envwithout \seq{x}$ for $\{ y : \ptya \mathop{\mid} y : \ptya \in \penv
\wedge y \not\in
\seq{x} \}$.

\paragraph*{Synthesis.}
Our synthesis judgement has the form
$\synthseq[\prog]{\tma}{\ptya}{\penv}{\constrs}$, which can be read
``synthesise type $\ptya$ for term $\tma$ under program $\prog$, producing type
environment $\penv$ and constraints $\constrs$''.
Here, $\tma$ and $\prog$ are inputs of the judgement, whereas $\ptya$, $\penv$,
and $\constrs$ are outputs.
The checking judgement $\chkseq[\prog]{\tma}{\ptya}{\penv}{\constrs}$
can be read
``check that term $\tma$ has type $\ptya$ under program $\prog$, producing type
environment $\penv$ and constraints $\constrs$''.
Here, $\tma$, $\prog$, and $\ptya$ are inputs of the judgement, whereas $\penv$
and $\constrs$ are outputs.
As in the declarative system we omit the $\prog$ annotation in the rules for readability.

Rule \textsc{TS-Const} assigns a known base type to a constant, and rule
\textsc{TS-New} synthesises a type $\retty{\tyrecv{\mbone}}$ (analogous to
\textsc{T-New}); both rules produce an empty environment and constraint set.

Rule \textsc{TS-Spawn} checks that the given computation $M$ has the unit type,
synthesises type $\one$, and infers a type environment $\penv$ and constraint
set $\constrs$. Like \textsc{T-Spawn} in the declarative system, the usability
annotations are masked as usable since usability restrictions are process-local.

Message sending $\send{\vala}{m}{\seq{\valb}}$ is a side-effecting
operation, and so we synthesise type $\tyunit$. Rule \textsc{TS-Send}
first looks up the payload types $\seq{\ppretya}$ in the signature,
and \emph{checks} that message target $\vala$ has mailbox type
$\usablety{\tysend{\msgtag{m}}}$. In performing this check, the type
system will produce environment $\penv'$ that contains an entry
mapping the variable in $\vala$ to the desired mailbox type
Next, the algorithm checks each payload value against the
payload type described by the signature. The resulting environment is
the algorithmic disjoint combination of the environments produced by
checking each payload, and the resulting constraint set is the union of all
generated constraints.

Function application is similar: rule \textsc{TS-App} looks up the
type signature for function $f$ and checks that all arguments have the
expected types. The resulting environment is again the disjoint
combination of the environments, and the constraint set is the union
of all generated constraints.

\paragraph*{Checking.}

Rule \textsc{TC-Var} \emph{checks} that a variable $x$ has type $\ptya$,
producing a type environment $x : \ptya$.
The \textsc{TC-Let} rule checks that a let-binding
$\letin[\pretya]{x}{\tma}{\tmb}$ has type $\ptya$: first, we check that $\tma$
has type $\makereturnable{\pretya}$ noting that only values of returnable type
may be returned, producing environment $\penv_1$ and constraints $\constrs_1$.
Next we check that the body $\tmb$ has type $\ptya$, producing environment
$\penv_2$ and $\constrs_2$.
The next step is to check whether the types of the variable inferred in
$\penv_2$ corresponds with the annotation. The $\mkwd{check}$ meta-function
ensures that if $x$ is not contained within $\penv_2$, then the type of $x$ is
unrestricted; and conversely if $x$ \emph{is} contained within $\penv_2$, then the
annotation is a subtype of the inferred type as the annotation is a \emph{lower
bound} on what the body can expect of $x$.

Rule \textsc{TC-Guard} checks that a guard expression
$\guardann{\vala}{\pata}{\seq{\gd}}$ has return type $\ptya$. First, the rule
checks that the guard sequence $\seq{\gd}$ has type $\ptya$, producing nullable
environment $\nullableenv$, constraint set $\constrs_1$, and pattern $\patb$ in
pattern normal form. Next, the rule checks that the mailbox name $\vala$ has
type $\retty{\tyrecv{\patb}}$, producing environment $\penv'$ and constraint
set $\constrs_2$. Finally, the rule calculates the disjoint combination
of $\nullableenv$
and $\penv'$, producing final environment $\penv$ and constraints $\constrs_3$.

Finally, rule \textsc{TC-Sub} states that if a term $\tma$ is synthesisable with
type $\ptya$, where $\ptya$ is a subtype of $\ptyb$, then $\tma$ is checkable
with type $\ptyb$. The resulting environment is that produced by synthesising
the type for $\tma$, and the resulting constraint set is the union of the
synthesis and subtyping constraints.

\paragraph*{Un-annotated $\calcwd{let}$ expressions.}
Although our core calculus assumes an annotation on $\calcwd{let}$
expressions, this is unnecessary if the let-bound variable is
used in the continuation $\tmb$, or $\tma$ has a synthesisable type.
Specifically, \textsc{TC-LetNoAnn1} allows us to check the type of the
continuation and inspect the produced environment for the type of $x$, which
can be used to check $\tma$.
Similarly, \textsc{TC-LetNoAnn2} allows us to type a
$\calcwd{let}$-binding where $x$ is \emph{not} used in the continuation,
as long as the type of $\tma$ is synthesisable and unrestricted.

\begin{mathpar}
\inferrule
\chkseq{\tmb}{\ptyb}{\penv_1, x : \ptya}{\constrs_1} \\
\returnablepred{\ptya} \\\\
\chkseq{\tma}{\ptya}{\penv_2}{\constrs_2} \\
\joinseq{\penv_2}{\penv_1}{\penv}{\constrs_3}
\chkseq
{ \ptyb }
{ \penv }
{ \constrs_1 \cup \constrs_2 \cup \constrs_3 }

\inferrule
\chkseq{\tmb}{\ptyb}{\penv_1}{\constrs_1} \\
x \not\in \dom{\penv_1} \\\\
\synthseq{\tma}{\ptya}{\penv_2}{\constrs_2} \\
\returnablepred{\ptya} \\
\joinseq{\penv_2}{\penv_1}{\penv}{\constrs_3}
\chkseq
{ \ptyb }
{ \penv }
{ \constrs_1 \cup \constrs_2 \cup \constrs_3 }
\end{mathpar}

We use the explicitly-typed representation in the core calculus for
simplicity and uniformity, however the implementation follows the above
approach to avoid needless annotations.

\paragraph*{Guards.}

\begin{figure}
\headertwo{Constraint generation for guards}{
\framebox{$
\chkgseq
\framebox{$
\chkgseq

\begin{mathpar}
\inferrule
{ (\chkgseq
{\patb_i})_{i \in 1..n} \\\\
\patb = {\patb_1 \patplus \cdots \patplus \patb_n}\\
\manymergeseq
{ \chkgseq
{\constrs \cup \constrs_1 \cup \cdots \cup \constrs_n}
{ \patb }

\inferrule
{ }
{ \chkgseq

\inferrule
{ \chkseq{\tma}{\ptya}{\penv}{\constrs} }
{ \chkgseq{\pata}{\free{\tma}}{\ptya}{\penv}{\constrs}{\mbone} }

\inferrule
\chkseq{\tma}{\ptya}{\penv', y : \retty{\tyrecv{\ppata}}}{\constrs_1} \\
\prog(\msgtag{m}) = {\seq{\ppretya}} \\
\penv = \penv' \envwithout \seq{x} \\
\base{\seq{\ppretya}} \vee \base{\penv} \\
\checkenvseq{\penv'}{\seq{x}}{\seq{\makeusable{\ppretya}}}{\constrs_2}
{ \chkgseq
{\constrs_1 \cup \constrs_2 \cup
\set{\subpatconstr{\pata \without \msgtag{m}}{\ppata}}
{\algomsg{m} \patconcat (\pata \without \msgtag{m})}
\end{mathpar}

\vspace{-1em}
\caption{\langname algorithmic typing (guards)}
\label{fig:algo-typing-guards}
\end{figure}

Figure~\ref{fig:algo-typing-guards} shows the typing rules for
guards; the judgement
$\chkgseq{\pata}{\gd}{\ptya}{\nullableenv}{\constrs}{\patb}$ can be read
``Check that guard $\gd$ has type $\ptya$,
producing environment $\nullableenv$, constraints $\constrs$, and
closed pattern literal $\patb$ in pattern normal form with respect to $\pata$''.
Rule \textsc{TCG-Guards} types a
guard sequence, producing the algorithmic merge of all environments and the
sum of all produced patterns. Rule \textsc{TCG-Fail} types the $\kwfail$ guard
with any type and produces a null type environment, empty constraint set, and
pattern $\mbzero$. Rule \textsc{TCG-Free} checks that guard $\free{\tma}$ has
type $\ptya$ by checking that $\tma$ has type $\ptya$; the guard produces
pattern $\mbone$.

Finally, rule \textsc{TCG-Recv} checks that a receive guard
$\receive{m}{\seq{x}}{y}{\tma}$ has type $\ptya$. First, the rule checks that
$\tma$ has type $\ptya$, producing environment $\penv', y :
\retty{\tyrecv{\ppata}}$ and constraint set $\constrs_1$;  since a
mailbox type with input capability is linear, it \emph{must} be present in the
inferred environment. Next, the rule checks that the inferred types for $\seq{x}$
in $\penv'$ are compatible with the payloads for $\msgtag{m}$ declared in the
signature, producing constraint set $\constrs_2$.
As with the declarative rule, to rule out unsafe aliasing either the
payloads or inferred environment must consist only of base types. The resulting
environment is $\penv$ (i.e., the inferred environment without the mailbox
variable or any payloads).
The resulting constraint set is the union of $\constrs_1$ and $\constrs_2$ along
with an additional constraint which ensures that $\pata \without \msgtag{m}$ is
included in  $\ppata$, allowing us to produce the closed PNF literal
$\msgtag{m} \patconcat (\pata \without \msgtag{m})$.

\subsection{Metatheory}

We can now establish that the algorithmic type system is sound and complete with
respect to the declarative type system. We begin by introducing the notion of
pattern substitutions and solutions.

A \emph{pattern substitution} $\patsubst$ is a mapping from type variables $\patvara$ to
(fully-defined) patterns $\pata$; applying $\patsubst$ to a pattern $\ppata$
substitutes all occurrences of a type variable $\patvara$ for $\aps{\patvara}$.
We extend application of pattern substitutions to types and environments.
We write $\pv{\pata}$ for the set of pattern variables in a pattern and extend it to
types and environments.

\begin{definition}[Pattern solution]
A pattern substitution $\patsubst$ is a \emph{pattern solution} for a
constraint set $\constrs$ (or \emph{solves} $\constrs$) if
$\pv{\constrs} \subseteq \dom{\patsubst}$ and
for each $\subpatconstr{\ppata}{\ppatb} \in \patsubst$, we have
that $\subpat{\apppatsubst{\ppata}}{\apppatsubst{\ppatb}}$.
A solution $\patsubst$ is a \emph{usable} solution if its range does not
contain any pattern equivalent to $\mbzero$.
\end{definition}

\subsubsection{Algorithmic soundness}

\begin{definition}[Covering solution]
We say that a pattern substitution $\patsubst$ is a \emph{covering solution} for a
derivation $\synthseq[\prog]{\tma}{\ptya}{\penv}{\constrs}$ or
$\chkseq[\prog]{\tma}{\ptya}{\penv}{\constrs}$ if given
$\algoprogseq{\prog}{\constrs'}$, it is the case that $\patsubst$ is a usable
solution for $\constrs \cup \constrs'$ such that $\pv{\ptya} \cup \pv{\prog}
\subseteq \dom{\patsubst}$.
\end{definition}

If a term is well typed in the algorithmic system then, given a covering
solution, the term is also well typed in the declarative system.

\begin{restatable}[Algorithmic Soundness]{theorem}{algosoundness}\label{thm:algo-soundness}
\hfill
\begin{itemize}
\item If $\patsubst$ is a covering solution for
$\synthseq[\prog]{\tma}{\ptya}{\penv}{\constrs}$, then
\item If $\patsubst$ is a covering solution for
$\chkseq[\prog]{\tma}{\ptya}{\penv}{\constrs}$, then
\end{itemize}
\end{restatable}

\subsubsection{Algorithmic completeness}

We also obtain a completeness result, but only for the checking direction.
This is because the type system \emph{requires} type information to construct a
type environment.
In practice the lack of a completeness result for synthesis is unproblematic
since all functions have return type annotations, and therefore the only terms
typable in the declarative system but unsynthesisable are top-level terms
containing free variables.
In the following we assume that program $\prog$ is \emph{closed}, i.e. no
definitions or message payloads contain type variables.

\begin{restatable}
[Algorithmic Completeness]
\label{thm:algo-completeness}
If $\progseq{\prog}$ where $\prog$ is closed, and
then there exist some $\penv, \constrs$
and usable solution $\patsubst$ of $\constrs$ such that
$\chkseq[\prog]{\tma}{\tya}{\penv}{\constrs}$ where $\tyenv \subtype \aps{\penv}$.
\end{restatable}

An unannotated \calcwd{let} binding $\letin{x}{\tma}{\tmb}$ is also
typable by the algorithmic type system if either $x$ occurs free in $\tmb$, or
the type of $\tma$ is synthesisable; in practice this encompasses both base
types and linear usages of mailbox types, \ie\ the vast majority of use

\subsection{Constraint solving}\label{sec:constraint-solving}
Constraint solving is covered in depth
by~\citet{Padovani18}, so we provide an informal overview:

\begin{description}
\item[Identify and group bounds]
A \emph{pattern bound} is of the form $\subpatconstr{\ppata}{\patvara}$
\ie\ a constraint whose right-hand-side is a pattern variable.
We firstly group all pattern bounds using pattern disjunction,
\eg\ a constraint set $\set{\subpatconstr{\ppata}{\patvara},
\subpatconstr{\ppatb}{\patvara}, \subpatconstr{\mbone}{\mbone}}$ would
result in the constraint
$\subpatconstr{\ppata \patplus \ppatb}{\patvara}$.
\item[Calculate closed-form solutions]
\citet{HopkinsK99} define a closed-form solution for a set of pattern
bounds $(\subpatconstr{\ppata_i}{\patvara_i})_i$:
there exists a solution $\ppatb_i$ for each $\ppata_i$ such that
$\patvara_i \not\in \pv{\ppatb_i}$.
We can then substitute each closed pattern through the system to
eliminate all pattern variables in the remaining constraints and obtain a
system of closed inclusion constraints.
\item[Translate to Presburger formulae and check satisfiability]
Finally, we translate the closed constraints into Presburger formulae.
Commutative regular expressions, and therefore patterns, can be
expressed as semilinear sets~\cite{Parikh66} that describe
Presburger formulae~\cite{Ginsburg66}.
Since checking the satisfiability of a Presburger formula is decidable,
an external solver like Z3~\cite{MouraB08} can be used to
determine whether each constraint holds. In our case, we use Z3's
quantifier elimination pass and its quantifier-free linear
integer arithmetic solver.
\end{description}
\begin{figure}
\centering
\begin{subfigure}[t]{0.3\textwidth}
\[
\bl
\\
\guardanntwo{\var{mb}}{\msgtag{Arg} \patconcat \msgtag{Arg}} \\
\quad \receivethree{Arg}{x}{\var{mb}'} \\
\qquad
\guardanntwo{\var{mb}'}{\msgtag{Arg}} \\
\qquad \quad \receivethree{\msgtag{Arg}}{y}{\var{mb}''} \\
\qquad \qquad \sugarfree{\var{mb}''}; \\
\qquad \qquad x {+} y \\
\qquad \} \\
\} \\
\el
\]
\caption{Nested $\calcwd{guard}$s}
\label{fig:extensions:nested}
\end{subfigure}
\hfill
\begin{subfigure}[t]{0.27\textwidth}
\[
\bl
\letinone{(x, \var{mb}')} \\
\quad \guardanntwo{\var{mb}}{\msgtag{Arg} \patconcat \msgtag{Arg}} \\
\qquad \receivethree{\msgtag{Arg}}{x}{\var{mb}'} \\
\qqquad {(x, \var{mb}')} \\
\quad \} \; \calcwd{in} \\
\guardanntwo{\var{mb}'}{\msgtag{Arg}} \\
\quad \receivethree{\msgtag{Arg}}{y}{\var{mb}''} \\
\qquad {\sugarfree{mb}''; \; x {+} y} \\
\} \\
\el
\]
\caption{Unnesting using products}
\label{fig:extensions:unnested}
\end{subfigure}
\hfill
\begin{subfigure}[t]{0.33\textwidth}
\[
\bl
\guardanntwo{\var{self}}{\msgtag{M1} \patconcat \msgtag{M2}} \\
\quad \receivethree{M1}{\var{x}}{\var{mb}'} \\
\qquad
\bl
\guardanntwo{\var{mb}'}{\msgtag{M2}} \\
\quad \receivethree{M2}{\var{y}}{\var{mb}''} \\
\qquad \send{\var{x}}{Go}{}; \\
\qquad
\send{\var{y}}{Go}{}; \\
\qquad \sugarfree{\var{mb}''} \\
\}
\el
\}
\el
\]
\caption{Term requiring interfaces}
\label{fig:extensions:interfaces}
\end{subfigure}
\caption{Examples motivating extensions}
\label{fig:extensions}
\end{figure}

\section{Extensions}\label{sec:extensions}
It is straightforward to extend \langname\ with product and sum types, and by
using contextual typing information prior to constraint generation, we
can add higher-order functions and \emph{interfaces} that allow finer-grained alias
analysis. The formalisation can be found in Appendix~\ref{ap:extensions}.

\subsection{Product and Sum Types}
Product and sum constructors are checking cases, and must contain only
returnable components since we must be able to safely substitute their contents
in any context. As with $\calcwd{let}$ expressions we can omit annotations on
elimination forms, \ie\ $\letintwo{(x, y)}{\tma}{\tmb}$ or $\caseof{\vala}{x
\mapsto \tma; y \mapsto \tmb}$, provided that $x$ and $y$ are used in their
continuations, or the sum or product consists of base types.

An advantage of adding product types is that we can avoid nested
$\calcwd{guard}$ clauses, as we can return both a received value and an updated
mailbox name. Figure~\ref{fig:extensions:nested} receives two integers and
returns their sum using nested $\calcwd{guard}$ expressions, whereas
Figure~\ref{fig:extensions:unnested} uses products instead.

Since product types can only contain returnable components, they cannot be used
to replace $n$-ary argument sequences in function definitions and
$\calcwd{receive}$ clauses.

\subsection{Using Contextual Type Information}\label{sec:extensions-contextual}
A co-contextual approach is required to generate the  pattern
inclusion constraints. Sometimes, however, it is useful to have
contextual type information \emph{before} the constraint generation pass.
Consider applying a first-class function:
$(\flaglambda[]{x : \tyint}{\tyint}{x})(5)$.
Although the annotated $\lambda$ expression allows us to synthesise a type
and use a rule similar to \textsc{TS-App}, the lack of contextual type
information means that the approach fails as soon as we
stray from applying function literals
as in $\letin{f}{(\flaglambda[]{x : \tyint}{\tyint}{x})}{f(5)}$).
A typical backwards bidirectional typing approach requires
\emph{synthesising} function argument types, but  this is too
inflexible in our setting as each mailbox name argument would need a type

In the base system a global signature maps
message tags to payload types. While technically convenient, this is inflexible.
First, distinct entities may wish to use the same mailbox tags with different
payload types. For example, a client may send a $\msgtag{Login}$ message
containing credentials to a server,
which may then send a $\msgtag{Login}$ message containing the credentials and a
timestamp to a session management server.
Second, we need a syntactic check on a $\calcwd{receive}$ guard
to avoid aliasing, as outlined in~\secref{sec:whatstheissue}: either the
received payloads or free variables in the guard body must be base types.
This conservative check rules out innocuous cases such as in
Figure~\ref{fig:extensions:interfaces}, which waits for messages from two actors
before signalling them to continue.

With contextual information we can associate each mailbox name with an
\emph{interface} $\iface$, which maps tags to payload types,
and allows us to syntactically distinguish different kinds of mailboxes
(\eg\ a future and its client).
Since a name cannot have two interfaces at once, we can loosen our syntactic
check on $\calcwd{receive}$ guards to require only that the \emph{interfaces} of
mailbox names in the payloads and free variables differ, as typing guarantees
that they will refer to different mailboxes.

We implement the above extensions via a contextual type-directed translation:
we annotate function applications with the type of the
function (\ie\ $\appann{\vala}{\tyfun{\seq{\ptya}}{\ptyb}}{\seq{\valb}}$) which
allows us to synthesise the function type.
Users specify an interface when creating a mailbox ($\mbnewiface$);
our pass then annotates sends and guards with interface information (\ie\
$\sendann{\vala}{\iface}{m}{\seq{\valb}}$ and
$\guardifaceann{\vala}{\pata}{\seq{\gd}}$) for use in constraint generation.

\begin{table}[t]
\setlength\tabcolsep{4pt}
\begin{tabular}{ccp{8.8cm}@{}cc}
\toprule
\textbf{\commentpound} & \textbf{Name} & \textbf{Description} &
\textbf{Strict} &\textbf{Time} (ms) \\
\midrule
\multicolumn{5}{l}{\itshape Original mailbox calculus models taken from~\citet{dP18:mbc}}\\
\midrule
1\label[id]{id:lock} & Lock & Concurrent lock modelling mutual exclusion & \yes\ & $28.5$\\
2\label[id]{id:future} & Future & Future variable that is written to once and read multiple times & \yes\ & $22.5$\\
3\label[id]{id:account} & Account & Concurrent accounts exchanging debit and credit instructions & \yes\ & $19.5$\\
4\label[id]{id:accountf} & AccountF & Concurrent accounts where debit instructions are effected via futures & \yes\ & $33.5$\\
5\label[id]{id:master_worker} & Master-Worker & Master-worker parallel network & \yes\ & $29.0$\\
6\label[id]{id:session_types} & Session Types & Session-typed communicating actors using one arbiter & \no\ & $75.5$\\
\midrule
\multicolumn{5}{l}{\itshape Selected micro-benchmarks adapted from~\citet{ImamS14a:savina}, based on~\citet{NeykovaY16}}\\
\midrule
7 & Ping Pong & Process pair exchanging $k$ ping and pong messages & \yes\ & $24.6$\\
8 & Thread Ring & Ring network where actors cyclically relay one token with counter $k$ & \no\ & $37.2$\\
9 & Counter& One actor sending messages to a second that sums the count, $k$ & \no\ & $29.8$\\
10 & K-Fork & Fork-join pattern where a central actor delegates $k$ requests to workers & \yes\ & $7.1$\\
11 & Fibonacci & Fibonacci server delegating terms $(k-1)$ and $(k-2)$ to parallel actors & \yes\ & $27.1$\\
12 & Big & Peer-to-peer network where actors exchange $k$ messages randomly & \no\ & $62.8$\\
13 & Philosopher & Dining philosophers problem & \no\ &$57.1$\\
14 & Smokers & Centralised network where one arbiter allocates $k$ messages to actors & \no\ & $31.3$\\
15 & Log Map & Computes the term $x_{k + 1} = r{\cdot}x_k(1 - x_k)$ by delegating to parallel actors & \no\ & $57.9$\\
16 & Transaction & Request-reply actor communication initiated by a central teller actor & \no\ & $46.7$\\
\bottomrule
\end{tabular}
\smallskip
\caption{Typechecking concurrent actor examples in \langname}
\label{tbl:examples-table}
\vspace{-1.5em}
\end{table}

\section{Implementation and Expressiveness}\label{sec:implementation}

We outline the implementation of a prototype type checker written in OCaml,
and evidence the expressiveness of \langname\ via a selection of example
programs taken from the literature.
We first show that using quasi-linear typing in place  of
dependency graphs (cf.~\secref{sec:quasi-linear-typing}) does not prevent \langname\ from expressing \emph{all} of the examples in~\cite{dP18:mbc}.
The Savina benchmarks~\cite{ImamS14a:savina} capture typical
concurrent communication patterns and are used both to compare actor
languages and to demonstrate expressiveness; we show that \langname\ can express
10 of the 11 Savina expressiveness benchmarks used by~\citet{NeykovaY16}.
Finally, we encode a case study provided by an industrial partner that develops control software for factories.

\subsection{Implementation Overview}\label{sec:implementation_overview}

\noindent
\langname\ programs are type checked in a six-phase pipeline:
lexing and parsing; desugaring, which expands the sugared form of guards (\ie\
rewrites $\sugarfree{\vala}$ as $\guardann{\vala}{\mbone}{\free{()}}$ and
$\sugarfail{\vala}$ as $\guardann{\vala}{\mbzero}{\fail}$) and adds omitted
pattern variables; IR conversion, which transforms the surface language
(supporting nested expressions) to our explicitly-sequenced intermediate
representation; contextual type-checking, which supports the contextual
extensions from~\secref{sec:extensions-contextual}; constraint
generation; and constraint solving.

The \langname\ typechecker operates in two modes that determine how receive guards are type checked.
\emph{Strict} mode uses the lightweight syntactic checks outlined in
\secref{sec:declarative} and \secref{sec:algorithmic}, whereas  \emph{interface} mode uses interface type information (\secref{sec:extensions-contextual}) to relax these checks.
This means that every \langname\ program accepted in strict mode is also
accepted in interface mode.
More details are given in \Cref{ap:evaluation}.

\subsection{Expressiveness and Typechecking Time}\label{sec:implementation:examples}
\Cref{tbl:examples-table} lists the
implemented in \langname. Examples 1-6 are the mailbox calculus
examples from \citep[Ex. 1--3, and Sec. 4.1--4.3]{dP18:mbc}.
Examples 7-16 are the selection of Savina benchmarks~\citep[Table 1, No.
1--4, 6, 7, 12, 14--16]{ImamS14a:savina} used in~\cite{NeykovaY16}.
The table indicates whether a \langname\ program can be checked in strict (denoted by \yes), \emph{in addition} to interface mode (denoted by \no).
We report the mean typechecking time, excluding phases 1--3 of the pipeline. Measurements are made on a MacBook M1 Pro with 16GB of memory, running macOS 13.2 and OCaml 5.0, and averaging over 1000 repetitions.

\begin{wrapfigure}[25]{r}{0.35\textwidth}
\vspace{-1em}
\centering
\includegraphics[scale=0.35, trim={0 1.2cm 0 0},clip]{figs/seqdiag.pdf}
\caption{Factory use case}
\label{fig:factory-seqdiag}
\end{wrapfigure}

\subsubsection{Benchmarks}

\Cref{tbl:examples-table} shows that all but
one of the mailbox calculus examples from~\cite{dP18:mbc}
can be checked in strict mode.
The Savina examples
capture typical concurrent programming patterns, namely, master-worker (K-Fork, Fibonacci, Log Map), client-server (Ping Pong, Counter), and peer-to-peer (Big), and common network topologies such as star (Philosopher, Smokers, Transaction) and ring (Thread Ring).
Most of these programs require contextual type information (8, 9, and 12--16) to type check.
As \langname\ does not yet support recursive types, we instead emulate fixed
collections using definition parameters in examples 8, 10, 12--16.
We could not encode the Sleeping Barber~\cite[Ex. 8]{NeykovaY16} example since
the number of collection elements varies throughout execution.

The examples reveal the benefits of mailbox typing.
Runtime checks, such as
manual error handling
(\secref{sec:mailbox_types}) are unnecessary since errors (\eg\ unexpected
messages) are \emph{statically} ruled out
by the type system.
Mailbox types also have an edge over session typing tools for actor systems, \eg~\cite{NeykovaY16,TaboneF22}
where developers typically specify protocols in external tools and write code to accommodate the session typing framework.
In contrast, mailbox typing \emph{naturally} fits idiomatic actor programming.

This flexibility does not incur high typechecking runtime (see
\Cref{tbl:examples-table}).
The aim of benchmarking typechecking time is to show that mailbox typechecking is not
prohibitively expensive, rather than
to claim comparative results.
Comparisons with other implementations of (non-mailbox-typed versions of) the
benchmarks written in other languages are unlikely to strengthen our results as
the benchmark source code would be different, and we would be measuring \eg\
Java's entire type system implementation rather than the essence of the
typechecking algorithm.

\subsubsection{Case Study}\label{sec:case_study_robots}
Finally we describe a real-world use case written by \emph{Actyx
AG}\footnote{\url{https://www.actyx.com}}, who develop control software for factories.  The use case
captures a scenario where multiple robots on a factory floor acquire parts from
a warehouse that provides access through a single door.
Robots negotiate with the door to gain entry into the warehouse and obtain the part they require.
The behaviour of our three entities, \emph{Robot}, \emph{Door}, and
\emph{Warehouse} is shown in~\Cref{fig:factory-seqdiag}.
Our concrete syntax closely follows the core calculus of
\secref{sec:declarative}, without requiring that pattern variables in mailbox
types are specified explicitly.
Type checking our completed case study given in Appendix~\ref{ap:case_study} relies on contextual type information
(see \secref{sec:extensions}), and takes

We give an excerpt of our Warehouse process (below) that maps the interactions of its
lifeline in \Cref{fig:factory-seqdiag}.
In its initial state, \lstinline+empty+, the Warehouse expects a \lstinline+Prepare+ message (if there are Robots in the system), or none (if \emph{no} Robot requests access), expressed as the guard \lstinline:Prepare + 1: on \cref{ln:warehouse_prepare_or_not_main}.
When a part is requested, the Warehouse transitions to the state \lstinline+engaged+, where it awaits a \lstinline+Deliver+ message from the Door and notifies the Robot via a \lstinline+Delivered+ message (lines \ref{ln:warehouse_collect_part_start_main}\crefrangeconjunction\ref{ln:warehouse_collect_part_end_main}).
Subsequent interactions that the Warehouse undertakes with the Door and Robot
are detailed in Appendix~\ref{ap:case_study}.
Note that our type system enables us to be \emph{precise} with respect to the messages mailboxes receive.
Specifically, the guard on \cref{ln:warehouse_prepare_or_not_main} expects \emph{at most} one \lstinline+Prepare+ message, capturing the mutual exclusion requirement between Robots, whereas the guard on \cref{ln:warehouse_deliver_main} expects \emph{exactly} \lstinline+Deliver+.

\noindent
\begin{minipage}[b]{.47\textwidth}
\begin{lstlisting}[language=Pat, emph={self}, firstnumber=1]
def empty(self: wh?): Unit {
guard self: Prepare + 1 { (*\label[ln]{ln:warehouse_prepare_or_not_main}*)
free (*$\shortrightarrow$*) ()
receive Prepare(partNum, door) from self (*$\shortrightarrow$*)
door ! Prepared(self);
\end{lstlisting}
\end{minipage}
\hfill
\begin{lrbox}{\listingbox}
\begin{minipage}[b]{.47\textwidth}
\begin{lstlisting}[language=Pat, emph={self}, firstnumber=last]
def engaged(self: wh?): Unit { (*\label[ln]{ln:warehouse_collect_part_start_main}*)
guard self: Deliver { (*\label[ln]{ln:warehouse_deliver_main}*)
receive Deliver(robot, door) from self (*$\shortrightarrow$*)
robot ! Delivered(self, door);
given(self, door)
} (*\label[ln]{ln:warehouse_collect_part_end_main}*)    \end{lstlisting}
\end{minipage}
\end{lrbox}
\raisebox{0.5em}{\usebox{\listingbox}}
\vspace{-1em}
\section{Related work}
\label{sec:related}

\paragraph*{Behaviourally-typed actors.}
The asymmetric nature of mailboxes makes developing
behavioural type systems for actor languages challenging.
\citet{MostrousV11} investigate session typing for Core Erlang, using selective
message reception and unique references to encode session-typed channels.
\citet{TaboneF21,TaboneF22} develop a tool that statically checks
Elixir~\citep{Juric19} actors against binary session types to prove session
\citet{NeykovaY16} propose a programming model for dynamically checking actor
communication against multiparty session types~\cite{HondaYC16}, later
implemented in Erlang by~\citet{Fowler16}.
\citet{NeykovaY17} show how causality information in global types
can support efficient recovery strategies.
\citet{HFDG21} use multiparty session types with explicit connection
actions~\cite{HuY17} to give strong guarantees about actors that support runtime
adaptation, but an actor can only participate in one session at a time.
Using session types to structure communication requires specifying
point-to-point interactions, typically using different libraries and formalisms.
In contrast, our mailbox typing approach naturally fits idiomatic actor
programming paradigms.

\citet{BagherzadehR17} define a type system for active objects~\cite{BoerCJ07}
which can rule out data races; this work targets an imperative calculus and is
not validated via an implementation.
\citet{KamburjanDC16} apply session-based reasoning to a core active object
calculus where types encode remote calls and future resolutions;
communication correctness is ensured by static checks against session

Mailbox types are inspired by behavioural type systems~\cite{CrafaP17} for the \emph{objective join calculus}~\cite{FournetG96}.
The technique can be implemented in Java using code generation via
\emph{matching automata}~\cite{GerboP19}, and dependency graphs can rule out
deadlocks~\cite{Padovani18DF}, but the authors do not consider a programming
language design.
\citet{ScalasYB19} define a behavioural type system for Scala actors.  Types
are written in a domain-specific language, and type-level model checking
determines safety and liveness properties.
Their system focuses on the behaviour
of a process, rather than the state of the mailbox.

\paragraph*{Session-typed functional languages.}
Session types~\cite{DBLP:conf/concur/Honda93, HondaVK98} were originally
considered in the setting of process calculi; \citet{GayV10} were first to
integrate session types in a functional language by building on the linear
$\lambda$-calculus, and their approach has been adopted by several other works
(\eg~\cite{LindleyM15, AlmeidaMTV22}).
Linear types are insufficient for mailbox typing since we require
\emph{multiple} uses of a mailbox name as a sender; we believe our
use of quasi-linearity for behavioural typing is novel, and we conjecture that it could
be used to support other paradigms (\eg\ broadcast) that require
non-linear variable use.

\paragraph*{Co-contextual typing.}
Co-contextual typing~\cite{ErdwegBKKM15} was originally introduced to support
efficient incremental type-checking, and has also been used to support
intrinsically-typed compilation~\cite{RouvoetKV21}.
\citet{Padovani14} uses a co-contextual type algorithm for the linear
$\pi$-calculus with sums, products, and recursive types; and~\citet{CicconeP22}
use it when analysing fair termination properties.
\emph{Backwards bidirectional typing}~\cite{Zeilberger18:bbt} is a co-contextual
formulation of bidirectional typing, and we are first to use it in a language
Co-contextual typing has parallels with the co-de Bruijn nameless variable
representation~\cite{McBride18}, where subterms are annotated with the
variables they contain.

\paragraph{Safety via static analysis}
\citet{ChristakisS11} implement a static analyser for Erlang that detects errors
such as receiving from an empty mailbox, payload mismatches, redundant patterns,
and orphan messages.
All of these issues can be detected with mailbox types, which also allow us
to specify the mailbox state.
\citet{Harrison18} implements an approach incorporating both typechecking and
static analysis to detect errors such as orphan messages and redundant patterns.

\section{Conclusion and Future Work}\label{sec:conclusion}
Concurrent and distributed applications can harbour subtle and insidious bugs,
including protocol violations and deadlocks.
Behavioural types ensure \emph{correct-by-construction} communication-centric
software, but are difficult to apply to actor languages.
We have proposed the \emph{first} language design incorporating \emph{mailbox types}
which characterise mailbox communication.
The multiple-writer, single-reader nature of mailbox-oriented messaging makes
the integration of mailbox types in programming languages highly challenging.
We have addressed these challenges through a novel use of quasi-linear types and
have formalised and implemented an algorithmic type system based on backwards
bidirectional typing \secrefp{sec:algorithmic}, proving it to be sound and
complete with respect to the declarative type system \secrefp{sec:declarative}.
Our approach can flexibly express common communication patterns (\eg\
master-worker) and a real-world case study based on factory automation.

\paragraph{Future work.}
We are investigating implementing mailbox types in a tool for mainstream actor
languages, \eg\ Erlang; in parallel, we are investigating how languages with
first-class mailboxes can be compiled to standard actor languages in order to
leverage mature runtimes.
We plan to consider finer-grained inter-process alias control, and
co-contextual typing with \emph{type} constraints (as well
as pattern constraints), enabling us to study more advanced language
features, \eg\ polymorphism.

\begin{acks}
We thank the anonymous ICFP and AEC reviewers for their constructive reviews; our
STARDUST colleagues for their helpful comments; and Roland Kuhn for
discussion of the case study.  This work was supported by EPSRC Grant
EP/T014628/1 (STARDUST).
\end{acks}

\bibliographystyle{ACM-Reference-Format}
%%% -*-BibTeX-*-
%%% Do NOT edit. File created by BibTeX with style
%%% ACM-Reference-Format-Journals [18-Jan-2012].

\begin{thebibliography}{65}

%%% ====================================================================
%%% NOTE TO THE USER: you can override these defaults by providing
%%% customized versions of any of these macros before the \bibliography
%%% command.  Each of them MUST provide its own final punctuation,
%%% except for \shownote{}, \showDOI{}, and \showURL{}.  The latter two
%%% do not use final punctuation, in order to avoid confusing it with
%%% the Web address.
%%% To suppress output of a particular field, define its macro to expand
%%% to an empty string, or better, \unskip, like this:
%%% \newcommand{\showDOI}[1]{\unskip}   % LaTeX syntax
%%% \def \showDOI #1{\unskip}           % plain TeX syntax
%%% ====================================================================

\ifx \showCODEN    \undefined \def \showCODEN     #1{\unskip}     \fi
\ifx \showDOI      \undefined \def \showDOI       #1{#1}\fi
\ifx \showISBNx    \undefined \def \showISBNx     #1{\unskip}     \fi
\ifx \showISBNxiii \undefined \def \showISBNxiii  #1{\unskip}     \fi
\ifx \showISSN     \undefined \def \showISSN      #1{\unskip}     \fi
\ifx \showLCCN     \undefined \def \showLCCN      #1{\unskip}     \fi
\ifx \shownote     \undefined \def \shownote      #1{#1}          \fi
\ifx \showarticletitle \undefined \def \showarticletitle #1{#1}   \fi
\ifx \showURL      \undefined \def \showURL       {\relax}        \fi
% The following commands are used for tagged output and should be
% invisible to TeX
\providecommand\bibfield[2]{#2}
\providecommand\bibinfo[2]{#2}
\providecommand\natexlab[1]{#1}
\providecommand\showeprint[2][]{arXiv:#2}

\bibitem[Ahmed et~al\mbox{.}(2007)]%
\bibfield{author}{\bibinfo{person}{Amal Ahmed}, \bibinfo{person}{Matthew Fluet}, {and} \bibinfo{person}{Greg Morrisett}.} \bibinfo{year}{2007}\natexlab{}.
\newblock \showarticletitle{L\({}^{\mbox{3}}\): {A} Linear Language with Locations}.
\newblock \bibinfo{journal}{\emph{Fundam. Informaticae}} \bibinfo{volume}{77}, \bibinfo{number}{4} (\bibinfo{year}{2007}), \bibinfo{pages}{397--449}.
\newblock

\bibitem[Almeida et~al\mbox{.}(2022)]%
\bibfield{author}{\bibinfo{person}{Bernardo Almeida}, \bibinfo{person}{Andreia Mordido}, \bibinfo{person}{Peter Thiemann}, {and} \bibinfo{person}{Vasco~T. Vasconcelos}.} \bibinfo{year}{2022}\natexlab{}.
\newblock \showarticletitle{Polymorphic lambda calculus with context-free session types}.
\newblock \bibinfo{journal}{\emph{Inf. Comput.}} \bibinfo{volume}{289}, \bibinfo{number}{Part} (\bibinfo{year}{2022}), \bibinfo{pages}{104948}.
\newblock

\bibitem[Amadio et~al\mbox{.}(1998)]%
\bibfield{author}{\bibinfo{person}{Roberto~M. Amadio}, \bibinfo{person}{Ilaria Castellani}, {and} \bibinfo{person}{Davide Sangiorgi}.} \bibinfo{year}{1998}\natexlab{}.
\newblock \showarticletitle{On Bisimulations for the Asynchronous pi-Calculus}.
\newblock \bibinfo{journal}{\emph{Theor. Comput. Sci.}} \bibinfo{volume}{195}, \bibinfo{number}{2} (\bibinfo{year}{1998}), \bibinfo{pages}{291--324}.
\newblock

\bibitem[Ancona et~al\mbox{.}(2016)]%
\bibfield{author}{\bibinfo{person}{Davide Ancona}, \bibinfo{person}{Viviana Bono}, \bibinfo{person}{Mario Bravetti}, \bibinfo{person}{Joana Campos}, \bibinfo{person}{Giuseppe Castagna}, \bibinfo{person}{Pierre{-}Malo Deni{\'{e}}lou}, \bibinfo{person}{Simon~J. Gay}, \bibinfo{person}{Nils Gesbert}, \bibinfo{person}{Elena Giachino}, \bibinfo{person}{Raymond Hu}, \bibinfo{person}{Einar~Broch Johnsen}, \bibinfo{person}{Francisco Martins}, \bibinfo{person}{Viviana Mascardi}, \bibinfo{person}{Fabrizio Montesi}, \bibinfo{person}{Rumyana Neykova}, \bibinfo{person}{Nicholas Ng}, \bibinfo{person}{Luca Padovani}, \bibinfo{person}{Vasco~T. Vasconcelos}, {and} \bibinfo{person}{Nobuko Yoshida}.} \bibinfo{year}{2016}\natexlab{}.
\newblock \showarticletitle{Behavioral Types in Programming Languages}.
\newblock \bibinfo{journal}{\emph{Found. Trends Program. Lang.}} \bibinfo{volume}{3}, \bibinfo{number}{2-3} (\bibinfo{year}{2016}), \bibinfo{pages}{95--230}.
\newblock
\urldef\tempurl%
\url{https://doi.org/10.1561/2500000031}
\showDOI{\tempurl}

\bibitem[Bagherzadeh and Rajan(2017)]%
\bibfield{author}{\bibinfo{person}{Mehdi Bagherzadeh} {and} \bibinfo{person}{Hridesh Rajan}.} \bibinfo{year}{2017}\natexlab{}.