Linear Haskell

Practical Linearity in a Higher-Order Polymorphic Language

Jean-Philippe Bernardy

University of Gothenburg
Department of Philosophy, Linguistics and Theory of Science
Olof Wijksgatan 6
Mathieu Boespflug

Tweag I/O

Ryan R. Newton

Indiana University

Simon Peyton Jones

Microsoft Research

Arnaud Spiwack

Tweag I/O

Linear type systems have a long and storied history, but not a clear
path forward to integrate with existing languages such as OCaml or
Haskell. In this paper, we study a linear type system
designed with two crucial properties in mind:
backwards-compatibility and code reuse across linear and non-linear
users of a library. Only then can the benefits of linear types
permeate conventional functional programming.  Rather than bifurcate
types into linear and non-linear counterparts, we instead
attach linearity to function arrows.  Linear functions can
receive inputs from linearly-bound values, but can also operate over
unrestricted, regular values.

To demonstrate the efficacy of our linear type system — both how
easy it can be integrated in an existing language implementation and
how streamlined it makes it to write programs with linear
types — we implemented our type system in
ghc, the leading Haskell compiler, and demonstrate
two kinds of applications of linear types:
mutable data with pure interfaces;
and enforcing protocols in I/O-performing functions.

[B]concept95 id>10011007.10011006. 10011008.10011024</concept95 id>[E]

[B]concept95 desc>Software and its engineering1pt'Language features</concept95 desc>[E]

[B]concept95 significance>500</concept95 significance>[E]

[B]concept95 id>10011007.10011006. 10011008.10011009. 10011012</concept95 id>[E]

[B]concept95 desc>Software and its engineering1pt'Functional languages</concept95 desc>[E]

[B]concept95 significance>300</concept95 significance>[E]

[B]concept95 id>10011007.10011006. 10011039</concept95 id>[E]

[B]concept95 desc>Software and its engineering1pt'Formal language definitions</concept95 desc>[E]

[B]concept95 significance>300</concept95 significance>[E]

[500]Software and its engineering Language features
[300]Software and its engineering Functional languages
[300]Software and its engineering Formal language definitions

This paper appears in the Proceeding of the ACM Conference on Principles of Programming Languages (POPL) 2018.  This version includes an Appendix that gives an operational semantics for the core language, and proofs of the metatheoretical results stated in the paper.

§ INTRODUCTION

Despite their obvious promise, and a huge research literature, linear
type systems have not made it into mainstream programming languages,
even though linearity has inspired uniqueness typing in Clean, and
ownership typing in Rust.  We take up this challenge by extending
Haskell with linear types.

Our design supports many applications for linear types, but we focus on
two particular use-cases.  First, safe
update-in-place for mutable structures, such as arrays; and second,
enforcing access protocols for external apis, such as files,
sockets, channels and other resources.  Our particular contributions
are these:

* We describe an extension to Haskell for linear types, dubbed , using
two extended examples (sec:consumed-sec:io-protocols).
The extension is non-invasive:
existing programs continue to typecheck,
and existing datatypes can be used as-is even in linear parts
of the program.
The key to this non-invasiveness is that, in contrast to most other
approaches, we focus on linearity on the function arrow
rather than linearity in the kinds (sec:lin-arrow).

* Every function arrow can be declared linear, including those of
constructor types. This results in datatypes which can store
both linear values, in addition to unrestricted ones

* A benefit of linearity-on-the-arrow is that it naturally supports
linearity polymorphism (sec:lin-poly).  This contributes
to a smooth extension of Haskell by allowing many existing functions
(map, compose, etc) to be given more general types, so they can
work uniformly in both linear and non-linear code.

* We formalise our system in a small, statically-typed core
calculus that exhibits all these features (sec:calculus).
It enjoys the usual properties of progress and preservation.

* We have implemented a prototype of the system as a modest extension to ghc
(sec:impl), which substantiates our claim of non-invasiveness.
We use this prototype to implement case-study applications (sec:applications).
Our prototype performs linearity inference, but a systematic
treatment of type inference for linearity in our system remains open.

Retrofits often involve compromise and ad-hoc choices, but in fact we
have found that, as well as fitting into Haskell, our design holds
together in its own right.  We hope that it may perhaps serve as a
template for similar work in other languages.  There is a rich
literature on linear type systems, as we discuss in a long related
work section (sec:related).

§ MOTIVATION AND INTUITIONS

Informally, a function is “linear” if it consumes its argument exactly once.
(It is “affine” if it consumes it at most once.)  A linear type system
gives a static guarantee that a claimed linear function really is linear.
There are many motivations for linear type systems, but here we focus on two of them:

* Is it safe to update this value in-place (sec:freezing-arrays)?
That depends on whether there
are aliases to the value; update-in-place is ok if there are no other pointers to it.
Linearity supports a more efficient implementation, by $O(1)$ update rather than $O(n)$ copying.

* Am I obeying the usage protocol of this external resource
For example, an open file should be closed, and should not be used after it it has been closed;
a socket should be opened, then bound, and only then used for reading; a malloc'd memory
block should be freed, and should not be used after that.
Here, linearity does not affect efficiency, but rather eliminates many bugs.

We introduce our extension to Haskell, which we call , by
focusing on these two use-cases.  In doing so, we introduce a number
of ideas that we flesh out in subsequent subsections.

§.§ Operational intuitions

We have said informally that “a linear function consumes its argument
exactly once”. But what exactly does that mean?

Meaning of the linear arrow:
guarantees that if  is consumed exactly once,
then the argument  is consumed exactly once.

To make sense of this statement we need to know what “consumed exactly once” means.
Our definition is based on the type of the value concerned:

* To consume a value of atomic base type (like  or ) exactly once, just evaluate it.

* To consume a function value exactly once, apply it to one argument, and consume its result exactly once.

* To consume a pair exactly once, pattern-match on it, and consume each component exactly once.

* In general, to consume a value of an algebraic datatype exactly once, pattern-match on it,
and consume all its linear components exactly once
(sec:non-linear-constructors)[You may deduce that pairs have linear components,
and indeed they do, as we discuss in sec:non-linear-constructors.].

This definition is enough to allow programmers to reason about the
typing of their functions, and it drives the formal typing judgements in

Note that a linear arrow specifies how the function uses its argument. It does not
restrict the arguments to which the function can be applied.
In particular, a linear function cannot assume that it is given the
unique pointer to its argument.  For example, if , thenthis is fine:

[B]g x=f x[E]
The type of  makes no particular guarantees about the way in which it uses ;
in particular,  can pass that argument to .

§.§ Safe mutable arrays

The Haskell language provides immutable arrays, built with the function [
Haskell actually generalises over the type of array indices, but for this
paper we will assume that the arrays are indexed, from 0, by  indices.]:
[B]array::Int→[1.5mu (Int,a)1.5mu]→Array a[E]

[3]𝐭𝐲𝐩𝐞 MArray s a[E]

[3]𝐭𝐲𝐩𝐞 Array a[E]

[3]newMArray::Int→ST s (MArray s a)[E]

[9]::MArray s a→Int→ST s a[E]

[3]write::MArray s a→(Int,a)→ST s ()[E]

[3]unsafeFreeze::MArray s a→ST s (Array a)[E]

[13]Monad m⇒[E]

[13][1.5mu a1.5mu]→(a→m ())→m ()[E]

[3]runST::(∀s. ST s a)→a[E]

Signatures for array primitives (current ghc)

But how is  implemented? A possible answer is “it is built-in; don't ask”.
But in reality ghc implements  using more primitive pieces, so that library authors
can readily implement more complex variations — and they certainly do: see for example sec:cursors.  Here is the
definition of , using library functions whose types are given
in fig:array-sigs.

[B]array::Int→[1.5mu (Int,a)1.5mu]→Array a[E]

[B]array size pairs=runST[E]

[3](𝐝𝐨 [8]
[8]{1.5mu ma←newMArray size[E]

[8];forM_ pairs (write ma)[E]

[8];unsafeFreeze ma1.5mu})[E]
In the first line we allocate a mutable array, of type .
Then we iterate over the , with , updating the array in place
for each pair.  Finally, we freeze the mutable array, returning an immutable
array as required.  All this is done in the  monad, using  to
securely encapsulate an imperative algorithm in a purely-functional context,
as described in <cit.>.

Why is  unsafe?  The result of  is a new
immutable array, but to avoid an unnecessary copy,
it is actually .  The intention is, of course, that
that  should be the last use of the mutable array; but
nothing stops us continuing to mutate it further, with quite undefined semantics.
The “unsafe” in the function name is a ghc convention meaning “the programmer
has a proof obligation here that the compiler cannot check”.

The other unsatisfactory thing about the monadic approach to array
construction is that it is overly sequential. Suppose you had a pair of
mutable arrays, with some updates to perform to each; these updates could
be done in parallel, but the  monad would serialise them.

Linear types allow a more secure and less sequential interface.
introduces a new kind of function type: the linear arrow . A linear
function  must consume its argument exactly once.  This new
arrow is used in a new array api, given in

[3]𝐭𝐲𝐩𝐞 MArray a[E]

[3]𝐭𝐲𝐩𝐞 Array a[E]

[3]newMArray::Int→(MArray a⊸Unrestricted b)⊸b[E]

[3]write::MArray a⊸(Int,a)→MArray a[E]

[3]read::MArray a⊸Int→(MArray a,Unrestricted a)[E]

[3]freeze::MArray a⊸Unrestricted (Array a)[E]

Type signatures for array primitives (linear version), allowing
in-place update.

Using this api we can define  thus:

[B]array::Int→[1.5mu (Int,a)1.5mu]→Array a[E]

[B]array size pairs=newMArray size (λma→freeze (foldl write ma pairs))[E]

There are several things to note here:

* The function  allocates a fresh, mutable array of the
specified size, and passes it to the function supplied as the second
argument to , as a linear value .

* Even though linearity is a property of function arrows, not of
types (sec:lin-arrow), we still disinguish the type of
mutable arrays  from that of immutable arrays , because in this api
only immutable arrays are allowed to be non-linear (unrestricted).  The
way to say that results can be freely shared is to use
(our version of linear logic's  modality, see sec:datatypes), as in the type of .

* Because  consumes its input, there is no danger of the same
mutable array being subsequently written to, eliminating the problem with

* Since  is linear, we can only use it once. Thus each call to
returns a (logically) new array, so that the array is single-threaded,
by , through the sequence of writes.

* Above,  has the type ,
which expresses that it consumes its second argument linearly
(the mutable array), while the function it is given as
its first argument () must be linear.
As we shall see in sec:lin-poly this is not a new , but
an instance of a more general, multiplicity-polymorphic version of
a single  (where “multiplicity” refers to how many times a function
consumes its input).

Three factors ensure that a unique  is needed
in any given application , and in turn that
update-in-place is safe. First,  introduces only
a linear .  Second, no function that
consumes an  returns more than a single pointer to it;
so  can never obtain two pointers to .  Third,  must wrap its
result in . This third point means that even if  is used in an
unrestricted way, it suffices to call  a single time to obtain the
result, and in turn no mutable pointer to  can escape when
returns ( when the  result of  is

With this mutable array api,
the  monad has disappeared altogether; it is the array itself
that must be single threaded, not the operations of a monad. That removes
the unnecessary sequentialisation we mentioned earlier and opens the
possibility of exploiting more parallelism at runtime.

Compared to the status quo (using  and ), the
other major benefit
is in shrinking the trusted code base, because more library code (and it
can be particularly gnarly code) is statically typechecked.  Clients who
use only immutable arrays do not see the inner workings of the library, and will
be unaffected. Of course, the functions of
fig:linear-array-sigs are still part of the trusted code base,
in particular, they must not lie about linearity. Our second use-case has a much more direct impact on library clients.

§.§ I/O protocols

[3]𝐭𝐲𝐩𝐞 File[E]

[3]openFile::FilePath→IO File[E]

[3]readLine::File→IO ByteString[E]

[3]closeFile::File→IO ()[E]

Types for traditional file IO

[3]𝐭𝐲𝐩𝐞 File[E]

[3]openFile::FilePath→IO_L 1 File[E]

[3]readLine::File⊸IO_L 1 (File,Unrestricted ByteString)[E]

[3]closeFile::File⊸IO_L ω ()[E]

Types for linear file IO

Consider the api for files in fig:io-traditional, where a
is a cursor in a physical file.

Each call
to  returns a  (the line) and moves the cursor one line
forward.  But nothing stops us reading a file after we have closed it,
or forgetting to close it.
An alternative api using linear types is given in fig:io-linear.
Using it we can write a simple file handling program, , shown here.

[B]firstLine::FilePath→IO_L ω Bytestring[E]

[B]firstLine fp=[E]

[3]𝐝𝐨 [7]
[7]{1.5mu f←openFile fp[E]

[7];(f,Unrestricted bs)←readLine f[E]

[7];closeFile f[E]

[7];return bs1.5mu}[E]

Notice several things:

* Operations on files remain monadic, unlike the case with mutable arrays.
I/O operations affect the world, and hence must be sequenced.  It is not enough
to sequence operations on files individually, as it was for arrays.

* We generalise the  monad so that it expresses whether or not the
returned value is linear.  We add an extra multiplicity type parameter  to the monad ,
where  can be  or , indicating a linear or unrestricted result, respectively.

Now  returns ,
the “” indicating that the returned  must be used linearly.
We will return to how  is defined in sec:linear-io.

* As before, operations on linear values must consume their input
and return a new one; here  consumes the  and produces a new one.

* Unlike the , the  returned by  is unrestricted,
and the type of  indicates this.

It may seem tiresome to have to thread the  as well as sequence
operations with the  monad. But in fact it is often useful do
to do so, because we can use types
to witness the state of the resource, , with separate
types for an open or closed . We show applications in sec:cursors and sec:sockets.

§.§ Linear datatypes

With the above intutions in mind, what type should we assign to a data
constructor such as the pairing constructor ?  Here are two possibilities:

[10]a⊸b⊸(a,b) [26]
[26] [41]

Using the definition in sec:consumed, the former is clearly the correct
choice: if the result of  is consumed exactly once,
then (by def:consume),
and  are each consumed exactly once; and hence  is linear it its

[B]f1 x=𝐜𝐚𝐬𝐞 x 𝐨𝐟 (a,b)→(a,a)[E]

[B]f2 x=𝐜𝐚𝐬𝐞 x 𝐨𝐟 (a,b)→(b,a)[E]

So much for construction; what about pattern matching?  Consider
and  defined here;

is an ordinary Haskell function. Even though the data constructor  has
a linear type, that does not imply that the pattern-bound variables  and
must be consumed exactly once; and indeed they are not.
Therefore,  does not have the linear type .
Why not?  If the result of  is consumed once, is  guaranteed to be consumed
once?  No:  is guaranteed to be evaluated once, but its first component is then
consumed twice and its second component not at all, contradicting def:consume.

In contrast,  does have a linear type: if  is consumed exactly once,
then indeed  is consumed exactly once.

The key point here is that the same pair constructor works in both functions;
we do not need a special non-linear pair.

The same idea applies to all existing Haskell datatypes: in
we treat all datatypes defined using legacy Haskell-98
(non-gadt) syntax as defining constructors with linear arrows.
For example here is a declaration of 's list type,
whose constructor  uses linear arrows:

[B]𝐝𝐚𝐭𝐚 [1.5mu a1.5mu]=[1.5mu 1.5mu]|a:[1.5mu a1.5mu][E]
[B]()::[1.5mu a1.5mu]⊸[1.5mu a1.5mu]⊸[1.5mu a1.5mu][E]

[B][1.5mu 1.5mu][9]

Just as with pairs, this is not a new, linear list type: this is
's list type, and all existing Haskell functions will work
over it perfectly well.
Even better, many list-based functions are in fact linear, and
can be given a more precise type. For example we can write  as

This type says that if  is consumed exactly once, then
is consumed exactly once, and so is , and indeed our type
system will accept this definition.

As before, giving a more precise type to  only strengthens the
contract that  offers to its callers; it does not restrict
its usage. For example:
[3]sum::[1.5mu Int1.5mu]⊸Int[E]

[3]f::[1.5mu Int1.5mu]⊸[1.5mu Int1.5mu]→Int[E]

[3]f xs ys=sum (xsys)+sum ys[E]
Here the two arguments to  have different multiplicities, but
the function  guarantees that it will consume  exactly once if
is consumed exactly once.

For an existing language, being able to strengthen , and similar
functions, in a backwards-compatible way is a huge boon.  Of
course, not all functions are linear: a function may legitimately
demand unrestricted input.  For example, the function  above
consumes  twice, and so
needs an unrestricted arrow for that argument.

Finally, we can use the very same pairs and lists
types to contain linear values (such as mutable arrays) without
compromising safety.  For example:
[B]upd::(MArray Char,MArray Char)⊸Int→(MArray Char,MArray Char)[E]

[B]upd (a1,a2) n[17]
[30]=(write a1 n 'x',a2)[E]

[30]=(write a2 n 'o',a1)[E]

§.§ Unrestricted data constructors

Suppose we want to pass a linear  and an unrestricted  to a function .
We could give  the signature .  But suppose
we wanted to uncurry the function; we could then give it the type
[3]f::(MArray Int,Int)⊸[29]
[29]MArray Int[E]
But this is no good: now  is only allowed to use the  linearly, but it
might actually use it many times.  For this reason it is extremely useful to be
able to declare data constructors with non-linear types, like this:
[3]𝐝𝐚𝐭𝐚 PLU a b 𝐰𝐡𝐞𝐫𝐞 {1.5mu PLU::a⊸b→PLU a b1.5mu}[E]

[3]f::PLU (MArray Int) Int⊸[32]
[32]MArray Int[E]
Here we use gadt-style syntax to give an explicit type signature to the data
constructor , with mixed linearity.
Now, when constructing a  pair the type of the constructor means
that we must always supply an unrestricted second argument; and dually
when pattern-matching on  we are therefore free to use the second argument
in an unrestricted way, even if the  value itself is linear.

Instead of defining a pair with mixed linearity, we can also write
[3]𝐝𝐚𝐭𝐚 Unrestricted a 𝐰𝐡𝐞𝐫𝐞 {1.5mu Unrestricted::a→Unrestricted a1.5mu}[E]

[3]f::(MArray Int,Unrestricted Int)⊸[42]
[42]MArray Int[E]
The type  is very much like “” in linear
logic, but in our setting it is just an ordinary user-defined datatype.
We saw it used in fig:linear-array-sigs, where the result of  was
a pair of a linear  and an unrestricted array element:
[3]read::MArray a⊸Int→(MArray a,Unrestricted a)[E]
Note that, according to the definition in sec:consumed,
if a value of type  is consumed exactly once,
that tells us nothing about how the argument of the data constructor is consumed:
it may be consumed many times or not at all.

§.§ Multiplicity polymorphism

A linear function provides more guarantees to its caller than
a non-linear one — it is more general.  But the higher-order
case thickens the plot. Consider the standard  function over
(linear) lists:
[B]map f [1.5mu 1.5mu][15]
[15]=[1.5mu 1.5mu][E]

[B]map f (x:xs)[15]
[15]=f x:map f xs[E]
It can be given the two following incomparable types:

Thus,  features quantification over multiplicities and
parameterised arrows ().  Using these,  can be given
the following more general type: .

Likewise, function composition and  (cf. sec:freezing-arrays)
can be given the following general types:
[B]foldl::∀p q. (a→_p b→_q [40]
[40]a)→a→_p [1.5mu b1.5mu]→_q a[E]

[B](∘)::∀p q. (b→_p c)⊸(a→_q b)→_p a→_p·q c[E]

[B](f∘g) x=f (g x)[E]
The type of  says that two functions that accept arguments of arbitrary
multiplicities ( and  respectively) can be composed to form a
function accepting arguments of multiplicity  (the
product of  and  — see def:equiv-multiplicity).

Finally, from a backwards-compatibility perspective, all of these
subscripts and binders for multiplicity polymorphism can be
ignored. Indeed, in a context where client code does not use
linearity, all inputs will have unlimited multiplicity, $ω$, and transitively all
expressions can be promoted to $ω$. Thus in such a context the
compiler, or indeed documentation tools, can even altogether hide
linearity annotations from the programmer when this language
extension is not turned on.

§.§ Linear input/output

In sec:io-protocols we introduced the
monad.[ is not a monad in the strict sense, because  and
can be different in . However it is a relative
monad <cit.>. The details, involving the
functor  and linear
arrows, are left as an exercise to the reader.]
But how does it work?
is just a generalisation of the  monad, thus:
[3]𝐭𝐲𝐩𝐞 IO_L p a[E]

[3]return_IO_L::a→_p IO_L p a[E]

[13]::IO_L p a⊸(a→_p IO_L q b)⊸IO_L q b[E]
The idea is that if , then  is an input/output
computation that returns a linear value of type .  But what does it mean to
“return a linear value” in a world where linearity applies only to
function arrows?  Fortunately, in the world of monads each computation
has an explicit continuation, so we just need to control the linearity of
the continuation arrow.  More precisely, in an application
where , we need the continuation  to be linear, .
And that is captured by the multiplicity-polymorphic type of .

Even though they have a different type than usual, the bind and return
combinators of  can be used in the familiar way. The difference
with the usual monad is that multiplicities may be mixed, but this
poses no problem in practice.  Consider
[3]printHandle::File⊸IO ω ()[E]

[3]printHandle f=𝐝𝐨[E]

[5]{1.5mu (f,Unrestricted b)←atEOF f[49]

[8]𝐢𝐟 b 𝐭𝐡𝐞𝐧 closeFile f[49]

[8]𝐞𝐥𝐬𝐞 𝐝𝐨 [17]
[17]{1.5mu (f,Unrestricted c)←read f[49]

[17];putChar c[49]

[17];printHandle f1.5mu}1.5mu}[E]
Here  and  return a linear  that should be closed,
but  and  return an ordinary non-linear .  So this
sequence of operations has mixed linearity.  Nevertheless, we can
interpret the -notation with  in the usual way:
[3]read f[14]
[14] `bind_IO_L`  λ(f,Unrestricted c)→[E]

[3]putChar c[14]
[14] `bind_IO_L`  λ_→…[E]
Such an interpretation of the -notation requires Haskell's
extension, but if linear I/O becomes
commonplace it would be worth considering a more robust solution.

Internally, hidden from clients, ghc actually implements  as a function,
and that implementation too is illuminated by linearity, like so:
[B]𝐝𝐚𝐭𝐚 World[E]

[B]𝐧𝐞𝐰𝐭𝐲𝐩𝐞 IO_L p a=IO_L {1.5mu unIO_L::World⊸IORes p a1.5mu}[E]

[B]𝐝𝐚𝐭𝐚 IORes p a 𝐰𝐡𝐞𝐫𝐞[E]

[3]IOR::World⊸a→_p IORes p a[E]

[11]::IO_L p a⊸(a→_p IO_L q b)⊸IO_L q b[E]

[B]bind_IO_L (IO_L m) k=IO_L (λw→[34]
[34]𝐜𝐚𝐬𝐞 m w 𝐨𝐟[E]

[36]IOR w' r→unIO_L (k r) w')[E]
A value of type  represents the state of the world, and is
threaded linearly through I/O computations.  The linearity of the
result of the computation is captured by the  parameter of ,
which is inherited by the specialised form of pair,  that an
computation returns.  All linearity checks are verified by the
compiler, further reducing the size of the trusted code base.

§.§ Linearity and strictness

It is tempting to assume that, since a linear function consumes its
argument exactly once, then it must also be strict.  But not so!
For example

[B]f x=(x,True)[E]
Here  is certainly linear according to sec:consumed, and
given the type of  in sec:linear-constructors. That is, if
is consumed exactly once, then each component of its result pair is
consumed exactly once, and hence  is consumed exactly once.
But  is certainly not strict:  is not .

§ : A CORE CALCULUS FOR

We do not formalise all of , but rather a core calculus,
which exhibits all key features, including datatypes and
multiplicity polymorphism.  This way we make precise much of the
informal discussion above.

§.§ Syntax

0.4  Multiplicities

\begin{align*}
π,μ &::= 1 ~|~ ω ~|~ p ~|~ π+μ ~|~ π·μ
\end{align*}

0.4  Types

\begin{align*}
A,B ::= A →_π B ~|~  ∀p. A ~|~ D~p_1~…~p_n
\end{align*}

0.3  Contexts

\begin{align*}
Γ,Δ & ::=  (x :_{μ} A), Γ ~|~ –
\end{align*}

0.6 Datatype declaration

\begin{align*}
\data D~p_1~…~p_n~\mathsf{where} \left(c_k : A₁ →_{π₁} …    A_{n_k} →_{π_{n_k}} D\right)^m_{k=1}
\end{align*}

\begin{align*}
e,s,t,u & ::= x & \text{variable} \\
& \pip λ_π (x{:}A). t & \text{abstraction} \\
& \pip t s & \text{application} \\
& \pip λp. t & \text{multiplicity abstraction} \\
& \pip t π & \text{multiplicity application} \\
& \pip c t₁ … t_n & \text{data construction} \\
& \pip \case[π] t {c_k  x₁ … x_{n_k} → u_k}  & \text{case} \\
& \pip \flet[π] x_1 : A₁ = t₁ … x_n : A_n = t_n \fin u & \text{let}
\end{align*}

Syntax of

The term syntax of  is that of a type-annotated (à la
Church) simply-typed $λ$-calculus with let-definitions
(fig:syntax).  It includes multiplicity polymorphism, but to avoid clutter
we omit ordinary type polymorphism.

is an explicitly-typed language: each binder is annotated with
its type and multiplicity; and multiplicity abstraction and application
are explicit.   will use type inference to fill in
much of this information, but we do not address the challenges of type
inference here.

The types of  (see fig:syntax) are simple types with
arrows (albeit multiplicity-annotated ones), datatypes, and
multiplicity polymorphism.
We use the following abbreviations:
\(A → B ≝  A →_ω B\) and
\(A ⊸ B ≝ A →_1 B\).

Datatype declarations (see fig:syntax) are of the following form:

\begin{align*}
\data D~p_1~…~p_n~\mathsf{where} \left(c_k : A₁ →_{π₁} ⋯    A_{n_k} →_{π_{n_k}} D\right)^m_{k=1}
\end{align*}

The above declaration means that \(D\) is parameterized over \(n\) multiplicities $p_i$ and has \(m\) constructors \(c_k\),
each with \(n_k\) arguments. Arguments of
constructors have a multiplicity, just like arguments of functions: an
argument of multiplicity $ω$ means that consuming the data constructor once
makes no claim on how often that argument is consumed (def:consume).
All the variables in the multiplicities $π_i$ must be among
$p_1…p_n$; we write $π[π_1…π_n]$ for the substitution of $p_i$ by
$π_i$ in $π$.

§.§ Static semantics

Γ, x :_π A  ⊢   t : B
Γ ⊢ λ_π (x:A). t  :  A  →_q  Babs

Δ_i ⊢ t_i : A_i
$c_k : A_1 →_{μ_1} … →_{μ_{n-1}}
A_n →_{μ_n} D~p_1~…~p_n$ constructor
ωΓ+∑_i μ_i[π₁…π_n]Δ_i ⊢ c_k  t₁ … t_n : D π₁ … π_ncon

Γ_i   ⊢  t_i  : A_i
Δ, x₁:_π A₁ …  x_n:_π A_n ⊢ u : C
Δ+π∑_i Γ_i ⊢ [π] x_1 : A_1 = t₁  …  x_n : A_n = t_n  u : Clet

Γ ⊢  t : A
$p$ fresh for $Γ$
Γ ⊢ λp. t : ∀p. Am.abs

Γ ⊢ t :  ∀p. A
Γ ⊢ t π  :  A[π/p]m.app

Typing rules

The static semantics of  is given in fig:typing.  Each
binding in $Γ$, of form \(x :_π A\), includes a multiplicity $π$
(fig:syntax).  The familiar judgement \(Γ ⊢ t : A\) should
be read as follows

\(Γ ⊢ t : A\) asserts that consuming the term $t : A$ exactly once will
consume each binding $(x :_{π} A)$ in $Γ$ with its multiplicity $π$.

One may want to think of the types in $Γ$ as
inputs of the judgement, and the multiplicities as outputs.

The rule (abs) for lambda abstraction adds $(x :_{π} A)$ to the
environment $Γ$ before checking the body  of the abstraction.
Notice that in , the lambda abstraction  $λ_π(x{:}A). t$
is explicitly annotated with multiplicity $π$.  Remember, this
is an explicitly-typed intermediate language; in
this multiplicity is inferred.

The dual application rule (app) is more interesting:

To consume  once, we consume  once, yielding the
multiplicities in $Γ$, and  once, yielding the multiplicies in
$\Delta$.  But if the multiplicity $π$ on 's function arrow is $ω$,
then the function consumes its argument not once but $ω$ times, so all
's free variables must also be used with multiplicity $ω$. We
express this by scaling the multiplicities in $\Delta$ by $π$.
Finally we need to add together all the
multiplicities in $Γ$ and $π\Delta$; hence the context $Γ+πΔ$ in the
conclusion of the rule.

In writing this rule we needed to “scale” a context by
a multiplicity, and “add” two contexts.  We pause to define these operations.

\begin{align*}
(x :_π A,Γ) + (x :_{μ} A,Δ) &= x :_{π+μ} A, (Γ+Δ)\\
(x :_π A,Γ) + Δ &= x :_π A, Γ+Δ & (x ∉ Δ)\\
() + Δ &= Δ
\end{align*}

Context addition is total: if a variable occurs in both operands the
first rule applies (with possible re-ordering of bindings in $Δ$), if
not the second or third rule applies.

π(x :_μ A, Γ) =  x :_πμ A, πΓ

The following laws hold:

\begin{align*}
Γ + Δ &= Δ + Γ &
π (Γ+Δ) &= π Γ + π Δ\\
(π+μ) Γ &= π Γ+ μ Γ \\
(πμ) Γ &= π (μ Γ) &
1 Γ &= Γ
\end{align*}

These operations depend, in turn, on addition and multiplication of multiplicities.
The syntax of multiplicities is given in fig:syntax.
We need the concrete multiplicities $1$ and $ω$ and, to support polymorphism,
multiplicity variables (ranged over by the metasyntactic
variables \(p\) and \(q\)) as well as formal sums and products of multiplicities.

Multiplicity expressions are quotiented by the following equivalence

The equivalence of multiplicities is the smallest transitive and
reflexive relation, which obeys the following laws:

* $+$ and $·$ are associative and commutative

* $1$ is the unit of $·$

* $·$ distributes over $+$

* $ω · ω = ω$

* $1 + 1 = 1 + ω = ω + ω = ω$

Thus, multiplicities form a semi-ring (without a zero), which extends
to a module structure on typing contexts. We may want to have a
stronger notion of equivalence for multiplicities, as we discuss in

Returning to the typing rules in fig:typing, the rule (let) is like
a combination of (abs) and (app).  Again, each $\flet$ binding is
explicitly annotated with its multiplicity.

The variable rule (var) uses a standard idiom:

This rule allows us to ignore variables with
multiplicity $ω$ (usually called weakening),
so that, for example $x :_1 A, y :_ω B ⊢ x : A$ holds
[Pushing weakening to the variable rule is
classic in many $λ$-calculi, and in the case of linear logic,
dates back at least to Andreoli's work on
focusing <cit.>.]. Note that the judgement
$x :_ω A ⊢ x : A$ is an instance of the variable rule, because
$(x :_ω A)+(x :_1 A) = x:_ω A$.

Finally, abstraction and application for multiplicity polymorphism
are handled straightforwardly by (m.abs) and (m.app).

§.§ Data constructors and case expressions

The handling of data constructors and case expressions is a
distinctive aspect of our design.  For constructor applications, the rule
(con), everything is straightforward: we treat the data constructor in
precisely the same way as an application of a function with that data constructor's type.
This includes weakening via the $ωΓ$ context in the conclusion.
The (case) rule is more interesting:

First, notice that the $\mathsf{case}$ keyword is annotated with a
multiplicity $π$; this is analogous to the explicit
multiplicity on a $\mathsf{let}$ binding.  It says how often the scrutinee (or,
for a $\mathsf{let}$, the right hand side) will be consumed.  Just as
for $\mathsf{let}$, we expect $π$ to be inferred from an un-annotated $\mathsf{case}$ in

The scrutinee $t$ is consumed $π$ times, which accounts for the $πΓ$ in
the conclusion.  Now consider the bindings $(x_i :_{πμ_i[π_1…π_n]} A_i)$ in the
environment for typechecking $u_k$.  That binding will be linear only if
both $π$ and $π_i$ are linear; that is, only if we specify
that the scrutinee is consumed once, and the $i$'th field of the data constructor $c_k$
specifies that is it consumed once if the constructor is (def:consume).

To put it another way, suppose one of the linear
Recall sec:non-linear-constructors, which described
how each constructor can have a mixture of linear and non-linear fields.]
of $c_k$ is used non-linearly in $u_k$.  Then, $μ_i=1$ (it is a linear field),
so $π$ must be $ω$, so that $πμ_i=ω$.  In short, using a linear field non-linearly
forces the scrutinee to be used non-linearly, which is just what we want.
Here are some concrete examples:

[21]a [27]
[27] [39]

[3]fst [12]
[22]a [39]
[39]swap [48]

Recall that both fields of a pair are linear (sec:linear-constructors).
In , the second component of the pair is used non-linearly (by being
discarded) which forces the use of $\mathsf{case}_ω$, and hence a non-linear type
for .  But  uses the components linearly, so we can use $\mathsf{case}_1$, giving
a linear type.

§.§ Metatheory

In order to prove that our type system meets its stated goals, we
introduce an operational semantics.

The details can be found in the extended version of this
article <cit.>.

The details are deferred to appendix:dynamics.

Of consuming exactly once
The operational semantics is a big-step operational semantics for
lazy evaluation in the style of <cit.>.
<cit.>, starting from a big-step evaluation
relation $a⇓b$, we define partial derivations and from there a
partial evaluation relation
$a⇓^*b$ (see sec:partial-derivations).
Progress is expressed as the
fact that a derivation of $a⇓^*b$ can always be extended.

The operational semantics differs from
's in two major respects:

* The reduction states are heavily annotated with type
information. These type annotations are used for the proofs.

* Reduction is indexed by whether we intend to consume the term
under consideration exactly once or an arbitrary number of times

* Variables in the environments are annotated by a multiplicity
($1$ or $ω$), $ω$-variables are ordinary variables. When forced, an
$ω$-variable is replaced by its value (to model lazy sharing), but
$1$-variables must be consumed exactly once: when forced,
they are removed from the environment. Reduction gets stuck if a
1-variable is used more than once.

Because the operational semantics gets stuck if a 1-variable is used
more than once, the progress theorem
(thm:progress-denotational) shows that linear functions do
indeed consume their argument at most once if their result is consumed
exactly once. The 1-variables are in fact used exactly once: it is a
consequence of type preservation that evaluation of a closed term of a
basic type (say ) returns an environment with no 1-variables.

Our preservation and progress theorems

(proved in the extended
version <cit.>)
(proved in sec:denotational)
read as follows:

If $a$ is well typed, and $a⇓b$, or $a⇓^*b$ then $b$ is well-typed.

Evaluation does not block. That is, for any partial evaluation
$a⇓^*b$, where $a$ is well-typed, the derivation can be extended.

In-place update & typestate
Furthermore, linear types can be
used to implement some operations as in-place updates, and
typestates (like whether an array is mutable or frozen) are actually
enforced by the type system.

To prove this, we introduce a second, distinct, semantics. It is also
a Launchbury-style semantics. It differs from <cit.> in the following ways:

* Environments are enriched with mutable references (for the sake
of concreteness, they are all references to arrays but they could be

* Typestates are implemented by mutating the type of such
references, functions can block if the type of the references is not
correct: that is, we track typestates dynamically.

The idea behind the latter is that progress will show that we are
never blocked by typestates. In other words, they are enforced
statically and can be erased at runtime.

It is hard to reason on a lazy language with mutation. But what we
show is that we are using mutation carefully enough so that
they behave as pure data. To formalise this, we relate this
semantics with mutation to our pure semantics above. Specifically, we
show that they are bisimilar.
<cit.> use a similar technique for a language with linear types
and both a pure and imperative semantics.

Bisimilarity allows us to lift the type-preservation and
progress from the pure semantics. That is, writing $σ,τ$ for states of
this evaluation with mutation:

For any well-typed $σ$, if $σ⇓τ$ or $σ⇓^*τ$, then $τ$ is

Evaluation does not block. That is, for any partial evaluation
$σ⇓^*τ$, for $σ$ well-typed, the evaluation can be

In particular, typestates need not be checked dynamically.

Just as importantly, we can prove that, indeed, we cannot observe
mutations. More precisely, we prove that the pure semantics and the
semantics with mutation are observationally equivalent: any observation, which we
reduce to a boolean test, is identical in either semantics.

The semantics with in-place mutation is observationally equivalent
to the pure semantics.

That is, for any closed term of type $\varid{Bool}$, if $e$ evaluates
to the value $z$ with the pure semantics, and to the value $z'$ with
the semantics with mutation, then $z=z'$.

§.§ Design choices & trade-offs

We could as well have picked different points in the design space for
. We review some of the choices we made in this section.

Case rule
Thanks to $\varid{case}_ω$, we can use linear arrows on all data
types. Indeed we can write the following and have  typecheck:
[B]𝐝𝐚𝐭𝐚 Pair a b 𝐰𝐡𝐞𝐫𝐞[E]

[3]Pair::a⊸b⊸Pair a b[E]

[B]fst::Pair a b→a[E]

[B]fst x=𝐜𝐚𝐬𝐞 _ω x 𝐨𝐟 Pair a b→a[E]
It is possible to do without $\varid{case}_ω$, and have only $\varid{case}_1$.
Consider  again.  We could instead have
[B]𝐝𝐚𝐭𝐚 Pair p q a b 𝐰𝐡𝐞𝐫𝐞[E]

[3]Pair::a→_p b→_q Pair p q a b[E]

[B]fst::Pair 1 ω a b⊸a[E]

[B]fst x=𝐜𝐚𝐬𝐞 _1 x 𝐨𝐟 Pair a b→a[E]
But now multiplicity polymorphism infects all basic datatypes (such
as pairs), with knock-on consequences.  Moreover,  is annotated so it seems
reasonable to annotate  in the same way.

To put it another way, $\varid{case}_ω$ allows us to meaningfully inhabit
, while linear logic
does not.

Because the type $A⊸B$ only strengthens the contract of its elements
compared to $A→B$, one might expect the type $A⊸B$ to be a subtype of $A→B$.
But while  has polymorphism, it does not have subtyping.
For example, if

then the call  is ill-typed, even though  provides more
guarantees than  requires.
On the other hand,  might well be multiplicity-polymorphic, with type
; in which case  is, indeed, typeable.

The lack of subtyping is a deliberate choice in our design: it is well
known that Hindley-Milner-style type inference does not mesh well with
subtyping (see, for example, the extensive exposition by
<cit.>, but also <cit.> for
a counterpoint).

However, while  is ill-typed in , it is accepted in .
The reason is that the $η$-expansion  is
typeable, and  perform this expansions during type
inference. Such an $η$-expansion is not completely
semantics-preserving as  is always a well-defined value,
even if  loops: this difference can be observed with Haskell's
operator. Nevertheless, such $η$-expansions are already standard
practice in ghc: a similar situation arises when using rank-2
types. For example, the core language of ghc does not accept
[B]g::(∀a. (Eq a,Show a)⇒a→Int)→Char[E]

[B]f::∀a. (Show a,Eq a)⇒a→Int[E]
The surface language, again, accepts , and elaborates it into . We simply extend this
mechanism to linear types.

Polymorphism & multiplicities Consider the definition: “”.

Our typing rules would validate both  and .
So, since we think of multiplicities ranging over $\{1,ω\}$, surely we should
also have ?  But as it stands, our rules do
not accept it. To do so we would need $x :_p Int ⊢ x : Int$.  Looking
at the (var) rule in fig:typing, we can prove that premise by case analysis,
trying $p=1$ and $p=ω$.
But if we had a domain of multiplicities which includes
$0$ (see sec:extending-multiplicities), we would not be able to prove $x :_p Int ⊢ x : Int$, and rightly
so because it is not the case that .

More generally, we could type more programs if we added more laws
relating variables in def:equiv-multiplicity, such as $p+q=ω$,
but this would prevent potential extensions to the set of
multiplicities. For now, we accept the more conservative rules of

Divergence.  Consider this definition[
returns the infinite list .  The function
appends two lists, and has type ; we have not
given a formal typing rule for recursive definitions, but its form is
entirely standard.]:
[3]f::[1.5mu Int1.5mu]⊸[1.5mu Int1.5mu][E]

[3]f xs=repeat 1xs[E]
But wait!  Does  really consume its argument  exactly
once? After all,  is infinite so  will never evaluate
at all!

In corner cases like this we look to metatheory.  Yes, the typing rules give
the specified types for  and .
Yes, the operational claims guaranteed by the metatheory remain valid.
Intuitively you may imagine it like this: linearity claims that if you were consume
the result of  completely, exactly once, then you would consume its argument once; but
since the result of  is infinite we cannot consume it completely exactly once, so
the claim holds vacuously.

§ IMPLEMENTING

We implement  on top of the leading Haskell compiler,
ghc, version 8.2[https://github.com/tweag/ghc/tree/linear-types].
The implementation modifies type inference and
type-checking in the compiler. Neither the intermediate language <cit.>
nor the run-time system are affected.

Our implementation of multiplicity polymorphism is incomplete, but the current
prototype is sufficient for the examples and case studies presented in
in this paper (see sec:evaluation).

In order to implement the linear arrow, we added a multiplicity
annotation to function arrows as in .
The constructor for arrow types is
constructed and destructed frequently in ghc's type checker, and this
accounts for most of the modifications to existing code.

As suggested in sec:typing-contexts, the multiplicities are an
output of the type inference algorithm. In order to infer the
multiplicities coming out of a  expression we need a way to
aggregate the multiplicities coming out of the individual branches. To
this effect, we compute, for every variable, the join of its
multiplicity in each branch.

affects 1,152 lines of ghc (in subsystems of the compiler
that together amount to more than 100k lines of code), including 444
net extra lines. These figures support our claim that  is
easy to integrate into an existing implementation: despite
ghc being 25 years old, we implement a first version of
with reasonable effort.

§ EVALUATION AND CASE STUDIES

While many linear type systems have been proposed,

a retrofitted linear type system for a mature language like Haskell offers
the opportunity to implement non-trivial applications mixing linear and
non-linear code, I/O, etc., and observe how linear code interacts with existing
libraries and the optimiser of a sophisticated compiler.

Our first method for evaluating the implementation is to simply compile a large
existing code base together with the following changes: (1) all
(non-gadt) data constructors are
linear by default, as implied by the new type system; and (2) we update standard
list functions to have linear types (, , ).

Under these conditions, we verified that the base ghc libraries and the nofib
benchmark suites compile successfully: 195K lines of Haskell, providing
preliminary evidence of backwards compatibility.

In the remainder of section, we describe case-studies implementated with the modified
of sec:implementation.

In sec:industry, we propose further applications for , which we
have not yet implemented, but which motivate this work.

§.§ Computing directly with serialised data

While sec:freezing-arrays covered simple mutable arrays, we now
turn to a related but more complicated application: operating directly on binary,
serialised representations of algebraic datatypes
(like <cit.> do).
The motivation is that programs are increasingly decoupled into separate (cloud)
services that communicate via serialised data in text or binary formats, carried
by remote procedure calls.

The standard approach is to deserialise data into an in-heap, pointer-based representation,

process it, and then serialise the result for transmission.

This process is inefficient, but nevertheless tolerated, because the alternative
— computing directly with serialised data — is far too difficult to program.

Nevertheless, the potential performance gain of working directly with serialised
data has motivated small steps in this direction:

libraries like “Cap'N Proto” [<https://capnproto.org/>] enable unifying
in-memory and on-the-wire formats for simple product types (protobufs).

Here is an unusual case where advanced types can yield performance by
making it practical to code in a previously infeasible style: accessing
serialised data at a fine grain without copying it.

[B]𝐝𝐚𝐭𝐚 Tree=Leaf Int|Branch Tree Tree[E]

[9]::Tree⊸Packed1pt'[1.5mu Tree1.5mu][E]

[9]::Packed1pt'[1.5mu Tree1.5mu]⊸Tree[E]

[14]Packed (Tree1pt':r)→_p[E]

[14](Packed (Int1pt':r)→_p a)→[E]

[14](Packed (Tree1pt':Tree1pt':r)→_p a)→a[E]

The interface on the right gives an example of type-safe, read-only
access to serialised data for a particular datatype[This
interface uses type-level lists as can be found in Haskell's

A  value is a pointer to raw bits (a bytestring), indexed by the
types of the values contained within.  We define a type-safe serialisation
layer as one which reads byte-ranges only at the type and size they were
originally written.  This is a small extension of the memory safety we
already expect of Haskell's heap — extended to include the contents of
bytestrings containing serialised data[The additional safety ensured
here is lower-stakes than typical memory-safety, as, even it is violated, the
serialised values do not contain pointers and cannot segfault the program
reading them.].

To preserve this type safety, the  type must be abstract.

Consequently, a client of the module defining  need not be privy to the
memory layout of its serialisation.

If we cannot muck about with the bits inside a  directly, then we can
still retrieve data with , , the traditional, copying,
approach to deserialisation.  Better still is to read the data without
copying.  We can manage this feat with , which is analogous to the
expression “”.

Lacking built-in syntax,  takes two continuations
corresponding to the two branches of the case expression.

Unlike the case expression,  operates on the packed byte stream, reads
a tag byte, advances the pointer past it, and returns a type-safe pointer to the
fields ( in the case of a leaf).

It is precisely to access multiple, consecutive fields that  is indexed
by a list of types as its phantom type parameter.  Individual atomic
values (, , etc) can be read one at a time with a lower-level
primitive, which can efficiently read out scalars and store them in
[3]read::Storable a⇒Packed (a1pt':r)⊸(a,Packed r)[E]

[B]sumLeaves::Packed1pt'[1.5mu Tree1.5mu]→Int[E]

[B]sumLeaves p=fst (go p)[E]

[3]𝐰𝐡𝐞𝐫𝐞 go [13]
[18]caseTree p[E]

[22]𝐥𝐞𝐭 [27]
[27](n,p3)=go p2[E]

[27](m,p4)=go p3[E]

[22]𝐢𝐧 (n+m,p4))[E]

Putting it together, we can write a function that consumes serialised data, such
as , shown on the right.

Indeed, we can even use  to implement , turning it into safe
“client code” – sitting outside the module that defines  and the
trusted code establishing its memory representation.

In this read-only example, linearity was not essential, only phantom types.
Next we consider an API for writing  values bit by bit, where linearity is key.

In particular, can we also implement  using a public interface?

§.§.§ Writing serialised data

To create a serialised data constructor, we must write a tag, followed by the

A linear write pointer can ensure all fields are initialised, in order.
We use a type “” for write pointers, parameterised by (1) a
list of remaining things to be written, and (2) the type of the final value
which will be initialised once those writes are performed.  For example, after
we write the tag of a  we are left with:

“” —

an obligation to write the  field, and a promise to receive
a  value at the end (albeit a packed one).

To write an individal number, we provide a primitive that shaves one
element off the type-level list of obligations (a counterpart to , above):
As with mutable arrays, this  operates in-place on the buffer, in spite
being a pure function.

[3]write::Storable a⇒a⊸Needs (a1pt':r) t⊸Needs r t[E]

When the list of outstanding writes is empty, we can retrive a readable packed buffer.
Just as when we froze arrays (sec:freezing-arrays), the immutable value
is unrestricted, and can be used multiple times:

[3]finish::Needs1pt'[1.5mu 1.5mu] t⊸Unrestricted (Packed1pt'[1.5mu t1.5mu])[E]

Finalizing written values with  works hand in hand with allocating new
buffers in which to write data (similar to  from sec:freezing-arrays):

[3]newBuffer::(Needs1pt'[1.5mu a1.5mu] a⊸Unrestricted b)⊸b[E]

We also need to explicitly let go of linear input buffers we've exhausted.
[3]done::Packed1pt'[1.5mu 1.5mu]⊸()[E]

The primitives , , , , and  are general
operations for serialised data, whereas  is datatype-specific.
Further, the module that defines  exports a datatype-specific way to
write each serialised data constructor:

[14]::Needs (Tree1pt':r) t⊸Needs (Int1pt':r) t[E]

[14]::Needs (Tree1pt':r) t⊸Needs (Tree1pt':Tree1pt':r) t[E]
Operationally,  functions write only the tag, hiding the exact
tag-encoding from the client, and leaving field-writes as future obligations.

With these building blocks, we can move  and  outside of the
private code that defines s, which has this minimal interface:
[B]𝐦𝐨𝐝𝐮𝐥𝐞 TreePrivate (Tree (),caseTree,startLeaf,startBranch)[E]

[B]𝐦𝐨𝐝𝐮𝐥𝐞 Data.Packed (Packed,Needs,read,write,newBuffer,finish,done)[E]
On top of the safe interface, we can of course define higher-level construction
routines, such as for writing a complete :
[3]writeLeaf n=write n∘startLeaf[E]

Now we can allocate and initialize a complete tree — equivalent to , but without ever creating the non-serialised values — as
[B]newBuffer (finish∘writeLeaf 4∘writeLeaf 3∘startBranch)::Packed1pt'[1.5mu Tree1.5mu][E]

Finally, we have what we need to build a map function that logically operates
on the leaves of a tree, but reads serialised input and writes serialised

Indeed, in our current  implementation “” touches only packed buffers — it performs zero Haskell heap allocation!

We will return to this map example and benchmark it in sec:cursor-benchmark.

With the safe interface to serialised data, functions like  and
are not burdensome to program.  The code for  is shown

[B]mapLeaves::(Int→Int)→Packed1pt'[1.5mu Tree1.5mu]⊸Packed1pt'[1.5mu Tree1.5mu][E]

[B]mapLeaves fn pt=newBuffer (extract∘go pt)[E]

[5]extract (inp,outp)=𝐜𝐚𝐬𝐞 done inp 𝐨𝐟 ()→finish outp[E]

[5]go::Packed (Tree1pt':r)⊸Needs (Tree1pt':r) t⊸(Packed r,Needs r t)[E]

[5]go p=caseTree p [24]
[24](λp o→[34]
[34]𝐥𝐞𝐭 (x,p')=read p [56]
[56]𝐢𝐧 (p',writeLeaf (fn x) o)) [E]

[24](λp o→[34]
[34]𝐥𝐞𝐭 (p',o')=go p (writeBranch o) 𝐢𝐧 go p' o')[E]

§.§.§ A version without linear types

How would we build the same thing in Haskell without linear types?  It may appear
that the ST monad is a suitable choice:

[B]writeST::Storable a⇒a→Needs' s (a1pt':r) t→ST s (Needs' s r t)[E]
Here we use the same typestate associated with a  pointer, while also
associating its mutable state with the  session indexed by .
Unfortunately, not only do we have the same trouble with freezing in the absence
of linearity (, sec:freezing-arrays), we also
have an additional problem not present with arrays:

namely, a non-linear use of a  pointer can ruin our type-safe
deserialisation guarantee!

For example, we can write a  and a  to the same pointer in an
interleaved fashion.  Both will place a tag at byte 0; but the leaf will place
an integer in bytes 1-9, while the branch will place another tag at byte 1.
We can receive a corrupted 8-byte integer, clobbered by a tag from an
interleaved “alternate future”.

Fixing this problem would require switching to an indexed monad with additional
type-indices that model the typestate of all accessible pointers, which would in
turn need to have static, type-level identifiers.  That is, it would require
encoding linearity after all, but in a way which would become very
cumbersome as soon as several buffers are involved.

§.§.§ Benchmarking compiler optimisations

Speedup of operating directly on serialised data, either using
linear-types or the ST monad, as compared to fully unpacking, processing,
and repacking the data.  For reference, a “pointer-based” version is also
included, which doesn't operate on serialised data at all, but instead normal
heap objects — it represents the hypothetical performance of “unpack-repack”
if (de)serialisation were instantaneous.

Finally, as shown in fig:pack-bench, there are some unexpected
performance consequences from using a linear versus a monadic, ST style in

Achieving allocation-free loops in  is always a challenge —
tuple types and numeric types are lazy and “boxed” as heap objects by default.

As we saw in the  and  examples, each recursive call returned a tuple
of a result and a new pointer.  In a monadic formulation, an expression of type
, for , implies that the “result” type , of kind , must be a
lifted type.  Nevertheless, in some situations, for some monads, the
optimiser is able to deforest data constructors returned by monadic actions.

In the particular case of  and  operations over serialised trees,
unfortunately, we are currently unable to eliminate all allocation from
-based implementations of the algorithms.

For the linearly-typed code, however, we have more options.   has the ability to
directly express unboxed values such as a tuple , which
fills two registers and inhabits an unboxed kind distinct from .

In fact, the type of a combinator like  is a good fit for the recent
“levity polymorphism” addition to
Thus we permit the branches of the  to return unlifted, unboxed types, and
give  a more general type:

[B]caseTree::∀(rep::RuntimeRep) (res::TYPE rep) b. [E]

[3]Packed (Tree1pt':b)→_p (Packed (Int1pt':b)→_p res)→(Packed (Tree1pt':Tree1pt':b)→_p res)→res[E]

This works because we do not need to call a function with  as
argument (and thus unknown calling conventions) only return it.

Using this approach, we were able to ensure by construction that the
“linear/packed” implementations in fig:pack-bench were completely
non-allocating, rather than depending on the optimiser.

This results in better performance for the linear, compared to monadic version
of the serialised-data transformations.

The basic premise of fig:pack-bench is that a machine in the network
receives, processes, and transmits serialized data (trees).

We consider two simple benchmarks:  and .
The baseline is the traditional approach: deserialise, transform, and reserialise,
the “unpack-repack” line in the plots.  Compared to this baseline,
processing the data directly in its serialised form results in speedups of over
20$\times$ on large trees.

What linear types makes safe, is also efficient.

The experiment was conducted on a Xeon E5-2699 CPU (2.30GHz, 64GB memory) using
our modified version of  8.2 (sec:impl).  Each
data point was measured by performing many trials and taking a linear regression
of iteration count against time[using the criterion library <cit.>].

This process allows for accurate measurements of both small and large times.  The
baseline unpack-repack tree-summing times vary from 25ns to 1.9 seconds at
depths 1 and 24 respectively.  Likewise, the baseline mapping times vary from
215ns to 2.93 seconds.

We use a simple contiguous implementation of buffers for
serialisation[A full, practical implementation should include growable
or doubling buffers.].

At depth 20, one copy of the tree takes around 10MB, and towards the right half
of the plot we see tree size exceeding cache size.

§.§ Sockets with type-level state

The bsd socket api is a standard, if not the
standard, through which computers connect over networks. It involves a
series of actions which must be performed in order: on the
server-side, a freshly created socket must be bound to an
address, then start listening incoming traffic, then
accept connection requests; said connection is returned as a
new socket, this new socket can now receive traffic. One reason
for having that many steps is that the precise sequence of
actions is protocol-dependent. For tcp traffic you would do as
described, but for udp, which does not need connections, you
would not accept a connection but receive messages directly.

The  library for Haskell, exposes precisely this sequence of

Programming with it is exactly as clumsy as socket libraries for other
languages: after each action, the state of the socket changes, as do the
permissible actions, but these states are invisible in the types.

Better is to track the state of sockets in the type, akin to a typestate
analysis <cit.>.

In the  api of sec:io-protocols, we made files
safer to use at the cost of having to thread a file handle
explicitely: each function consumes a file handle and returns a fresh
one. We can make this cost into an opportunity: we have the option of
returning a handle with a different type from that of the
handle we consumed! So by adjoining a phantom type to sockets to track
their state, we can effectively encode the proper sequencing of socket

As an illustration, we implemented wrapper around the api of the
library. For concision, this wrapper is
specialised for the case of tcp.

[B]𝐝𝐚𝐭𝐚 State=Unbound|Bound|Listening|Connected[E]

[B]𝐝𝐚𝐭𝐚 Socket (s::State)[E]

[B]𝐝𝐚𝐭𝐚 SocketAddress[E]

[12]IO_L 1 (Socket Unbound)[E]

[10]Socket Unbound⊸SocketAddress→IO_L 1 (Socket Bound)[E]

[B]listen::Socket Bound⊸IO_L 1 (Socket Listening)[E]

[12]Socket Listening⊸IO_L 1 (Socket Listening,Socket Connected)[E]

[13]Socket Unbound⊸SocketAddress→IO_L 1 (Socket Connected)[E]

[B]send::Socket Connected⊸ByteString→IO_L 1 (Socket Connected,Unrestricted Int)[E]

[B]receive::Socket Connected⊸IO_L 1 (Socket Connected,Unrestricted ByteString)[E]

[B]close::∀s. Socket s→IO_L ω ()[E]

This linear socket api is very similar to that of files: we use the
monad in order to enforce linear use of sockets. The difference
is the argument to , which represents the current state of the
socket and is used to limit the functions which apply to a socket
at a given time.

Implementing the linear socket api

Our socket api has been tested by writing a small
echo-server. The api is implemented as a wrapper around the
library. Each function wrapped takes half-a-dozen
lines of code, of type annotation and coercions between  and
[Since our implementation of  does not yet
have multiplicity-polymorphism, we had to fake it with type families
and gadts]. There is no computational behaviour besides
error recovery.

It would have been too restrictive to limit the typestate to enforce
the usage protocol of tcp. We do not intend for a new set of
wrapper functions to be implemented for each protocol. Instead the
wrappers are implemented with a generic type-state evolving according
to the rules of a deterministic automaton. Each protocol can define
it's own automaton, which is represented as a set of instances of
a type class.

§.§ Pure bindings to impure apis

In Haskell SpriteKit, <cit.> have a different kind
of problem. They build a pure interface for graphics, in the same style
as the Elm programming language <cit.>, but implement it in terms
of an existing imperative graphical interface engine.

Basically, the pure interface takes an update function  which is
tasked with returning the next state that the screen will display.

The scene is first converted to a
pure tree where each node keeps, along with the pure data, a pointer
to its imperative counterpart when it applies, or  for new
[B]𝐝𝐚𝐭𝐚 Node=Node {1.5mu payload::Int,ref::Maybe (IORef ImperativeNode),children::[1.5mu Node1.5mu]1.5mu}[E]

On each frame, SpriteKit applies  to the current scene, and checks
if a node  was updated. If it was, it applies the update directly
onto  or creates a new imperative node.

Things can go wrong though: if the update function duplicates
any proxy node, one gets the situation where two nodes  and
can point to the same imperative source , but
have different payloads. In this situation the  has become
inconsistent and the behaviour of SpriteKit is unpredictable.

In the api of <cit.>, the burden of checking
non-duplication is on the programmer.  Using linear types, we can
switch that burden to the compiler: we change the update function to
type , and the  field is made linear too.  Thanks
to linearity, no reference can be duplicated: if a node is copied, the
programmer must choose which one will correspond to the old imperative
counterpart and which will be new.

We implemented such an api in our implementation of
. The library-side code does not use any linear code, the
s are actually used unrestrictedly. Linearity is only imposed on
the user of the interface, in order to enforced the above restriction.

§ RELATED WORK

§.§ Linearity via arrows vs. linearity via kinds

There are two possible choices to indicate the distinction between
linear and unrestricted objects.  Our choice is to use the arrow
type. That is, we have both a linear arrow to introduce linear objects
in the environment, and an unrestricted arrow to introduce
unrestricted objects. This choice is featured in the work of
<cit.> and <cit.> and is
ultimately inspired by Girard's presentation of linear logic, which
features only linear arrows, and where the unrestricted arrow $A → B$
is encoded as $!A ⊸ B$.

Another popular choice
is to separate types into two kinds: a linear kind and an unrestricted
kind. Values with a type whose kind is linear are linear, and the
others are unrestricted. (Thus in particular such systems feature
“linear arrows”, but they have a completely different interpretation
from ours.) While this does not match linear logic (there is no such
thing as a linear proposition), it is attractive on the surface
because, intuitively, some types are inherently linear (file handles,
updateable arrays, etc.) and some types are inherently unrestricted
(, , etc.).  However, after scratching the surface we have
discovered that “linearity via arrows” has an edge over “linearity
via kinds”.

Better code reuse  When retrofitting linear types
in an existing language, it is important to share as much code as
possible between linear and non-linear code. In a system with
linearity on arrows, the subsumption relation (linear arrows subsume
unrestricted arrows) and the scaling of context in the application
rule mean that much linear code can be used as-is from unrestricted
code, and be properly promoted. Indeed, assuming lists as defined in
sec:compatibility and:
[5]()::[1.5mu a1.5mu]⊸[1.5mu a1.5mu]⊸[1.5mu a1.5mu][31]

[5]cycle::[1.5mu a1.5mu]→[1.5mu a1.5mu][31]
The following definition type-checks, even though  is applied to
unrestricted values and used in an unrestricted context.
[5]f::[1.5mu a1.5mu]→[1.5mu a1.5mu]→[1.5mu a1.5mu][E]

[5]f xs ys=cycle (xsys)[E]
In contrast, in a two-kind system, a function must declare the
exact linearity of its return value. Consequently, to make a
function promotable from linear to unrestriced, its declaration must
use polymorphism over kinds.

As seen in sec:programming-intro, in  reuse of linear
code extends to datatypes: the usual parametric datatypes (lists,
pairs, etc.) work both with linear and unrestricted values. On the
contrary, if linearity depends on the kind, then if a linear value
is contained in a type, the container type must be linear
too. (Indeed, an unrestricted container could be discarded or
duplicated, and its contents with it.) Consequently, sharing data
types also requires polymorphism.  For example, in a two-kinds
system, the  type may look like so, if one assumes a that
is the kind of linear types and  is the kind of
unrestricted types.
[5]𝐝𝐚𝐭𝐚 List (p::Multiplicity) (a::Type p)::Type p=[1.5mu 1.5mu]|a:(List p m a)[E]
The above declaration ensures that the linearity of the list
inherits the linearity of the contents. A linearity-polymorphic
function could have the definition:
[5]()::List p a→List p a→List p a[E]

[5][1.5mu 1.5mu]xs=xs[E]

Compared to our append function, the type of the above requires
multiplicity polymorphism . Additionnally, the above function
cannot (and should not) mix linear and unrestricted
lists. Indeed because multiplicity is attached to the type of
elements it must be the same for both arguments and the returned

Note that, in the above, we parameterize over multiplicities instead
of parameterizing over kinds directly, as is customary in the
literature. We do so because it fits better , whose kinds are
already parameterized over a so-called
levity <cit.>.

Ats The ats language has a unique take
on linear types <cit.>, which can be
classified as linearity via kinds and does not have
polymorphism.Ats has a notion of stateful views: views are
linear values without run-time representation and are meant to
track the state of pointers (e.g. whether they are
initialised). Pointers themselves remain unrestricted values: only
views are linear.

Dependent types
Linearity on the arrow meshes better with dependent types (see
sec:extending-multiplicities).  Indeed, consider a typical
predicate over files (). It may need to mention its
argument several times to relate several possible sequences of
operations on the file. While this is not a problem in our system,
the function  is not expressible if  is intrinsically
linear. Leaving the door open to dependent types is crucial to us,
as this is currently explored as a possible extension to

Linear values
Yet, an advantage of “linearity via kinds” is the possibility to directly
declare the linearity of values returned by a function – not just that
of the argument of a function. In contrast, in our system if one wants
to indicate that a returned value is linear, we have to
use a double-negation trick. That is, given $f : A → (B ⊸ !r) ⊸ r$,
then $B$ can be used a single time in the (single) continuation, and
effectively $f$ “returns” a single $B$. One can obviously declare a
type for linear values  and chain
-returning functions with appropriate combinators.  In fact,
as explained in sec:linear-io, the cost of the double negation
almost entirely vanishes in the presence of an ambient monad.

§.§ Other variants of “linearity on the arrow”

The  type system is heavily inspired from the work of
<cit.> and <cit.>. Both of them
present a type system where arrows are annotated with the multiplicty
of the the argument that they require, and where the multiplicities
form a semi-ring.

In contrast with ,  uses a
multiplicity-annotated type judgement $Γ ⊢_ρ t : A$, where $ρ$
represents the multiplicity of $t$. So, in
's system, when an unrestricted value is
required, instead of computing $ωΓ$, it is enough to check that
$ρ=ω$. The problem is that this check is arguably too coarse, and
results in the judgement $⊢_ω λx. (x,x) : A ⊸ (A,A)$ being derivable.

This derivation is not desirable: it implies that there cannot be
reusable definitions of linear functions. In terms of linear logic <cit.>,
makes the natural function of type $!(A⊸B) ⟹ !A⊸!B$
into an isomorphism.
In that respect, our system is closer to

The essential differences between our system and that of
is that we support
multiplicity-polymorphism and datatypes. In particular our  rule
is novel.

The literature on so-called
coeffects <cit.>
uses type systems similar to , but
with a linear arrow and multiplicities carried by the exponential
modality instead. , in particular,
develops a Krivine-style realisability model for such a calculus. We are not
aware of an account of Krivine realisability for lazy languages, hence
this work is not directly applicable to .

§.§ Uniqueness and ownership typing

The literature
contains many proposals for uniqueness (or ownership) types (in contrast with
linear types).
Prominent representative languages with uniqueness types include
Clean <cit.> and
Rust <cit.>. , on the other hand, is
designed around linear types based on linear
logic <cit.>.

Idris <cit.> features uniqueness types, which have
been used, in particular, to enforce communication
protocols <cit.>. Uniqueness types, in Idris,
are being replaced by linear types based on
qtt <cit.>, a variant of

Linear types and uniqueness types are, at their core, dual: whereas a linear type is
a contract that a function uses its argument exactly once
even if the call's context can share a linear argument as many times as it
pleases, a uniqueness type ensures that the argument of a function is
not used anywhere else in the expression's context even if the callee
can work with the argument as it pleases.

Seen as a system of constraints, uniqueness typing is a non-aliasing
analysis while linear typing provides a cardinality analysis. The
former aims at in-place updates and related optimisations, the latter
at inlining and fusion. Rust and Clean largely explore the
consequences of uniqueness on in-place update; an in-depth exploration
of linear types in relation with fusion can be found
in <cit.>;
see also the discussion in sec:fusion.

Because of this weak duality, we could have
retrofitted uniqueness types to Haskell. But several points
guided our choice of designing  around linear
logic instead: (a) functional languages have more use
for fusion than in-place update (if the fact that ghc has a cardinality
analysis but no non-aliasing analysis is any indication); (b) there is a
wealth of literature detailing the applications of linear
logic — see sec:applications; (c) and decisively, linear type systems are
conceptually simpler than uniqueness type systems, giving a
clearer path to implementation in ghc.

Rust & Borrowing

In  we need to thread linear variables throughout the
program.  Even
though this burden could be alleviated using syntactic sugar, Rust uses
instead a type-system feature for this purpose: borrowing.
Borrowed values differ from owned values in that they can
be used in an unrestricted fashion, albeit in a delimited

Borrowing does not come without a cost, however: if a
function  borrows a value  of type ,
then the caller of the function must retain  alive
until  has returned; the consequence is that Rust cannot, in
general, perform tail-call elimination, crucial to the operation
behaviour of many functional programs, as some resources must be
released after  has returned.

The reason that Rust programs depend so much on borrowing is that
unique values are the default.  aims to hit a different
point in the design space where regular non-linear expressions are the
norm, yet gracefully scaling up investing extra effort to enforce
linearity invariants is possible.
Nevertheless, we discuss in sec:extending-multiplicities how to
extend  with borrowing.

§.§ Linearity via monads

<cit.> taught us
a conceptually simple approach to lifetimes: the  monad. It has
a phantom type parameter  (the region) that is instantiated once at the
beginning of the computation by a  function of type:
[3]runST::∀a. (∀s. ST s a)→a[E]
This way, resources that are allocated during the computation, such
as mutable cell references, cannot escape the dynamic scope of the call
to  because they are themselves tagged with the same phantom
type parameter.

With region-types such as , we cannot express typestates, but this
is sufficient to offer a safe api for freezing array or
ensuring that files are eventually closed.
This simplicity (one only needs rank-2 polymorphism)
comes at a cost: we've already mentionned in
sec:freezing-arrays that it forces operations to be more
sequentialised than need be, but more importantly, it does not
support prima facie the interaction of nested regions.

<cit.> show that it is possible to promote
resources in parent regions to resources in a subregion. But this is
an explicit and monadic operation, forcing an unnatural imperative
style of programming where order of evaluation is explicit.
The HaskellR project <cit.> uses monadic
regions in the style of  to safely
synchronise values shared between two different garbage collectors for
two different languages.  report
that custom monads make writing code at an interactive prompt
difficult, compromises code reuse, forces otherwise pure functions to
be written monadically and rules out useful syntactic facilities like
view patterns.

In contrast, with linear types, values in two regions hence can safely
be mixed: elements can be moved from one data structure (or heap) to
another, linearly, with responsibility for deallocation transferred

Idris's dependent indexed monad

To go beyond simple regions, Idris <cit.> introduces  a generic way to add typestate on top of a monad, the
indexed monad transformer[See <http://docs.idris-lang.org/en/latest/st/index.html>. Where you
will also discover that  is actually defined in terms of a more
primitive ]. The basic
idea is that everything which must be single-threaded – and that we
would track with linearity – become part of the state of the
monad. For instance, coming back to the sockets of sec:sockets,
the type of  would be as follows:
[3]bind::(sock::Var)→SocketAddress→ST IO () [1.5mu sock:::Socket Unbound:↦Socket Bound1.5mu][E]
Where  is a reference into the monads's state, and  is
the type of  before , and , the type of
after .

Idris uses its dependent types to associate a state to the value of
its first argument. Dependent types are put to even greater use for
error management where the state of the socket depends on whether
succeeded or not:

[12]ST IO (Either () ()) [1.5mu sock:::Socket Unbound:↦(Socket Bound`or`Socket Unbound)1.5mu][E]

[3]bind::Socket Unbound⊸SocketAddress→Either (Socket Bound) (Socket Unbound)[E]

The support for dependent types in ghc is not as
comprehensive as Idris's. But it is conceivable to implement such an
indexed monad transformer in Haskell. However, this is not an easy task,
and we can anticipate that the error messages would be hard to stomach.

§ FUTURE WORK

§.§ Controlling program optimisations

Inlining is a cornerstone of program optimisation, exposing
opportunities for many program transformations. Yet not every function can
be inlined without negative effects on performance: inlining a
function with more than one use sites of the argument may result in
duplicating a computation. For example one should avoid the following
reduction: .

Many compilers can discover safe inlining opportunities by analysing
source code and determine how many times functions use their
arguments.  (In ghc it is called the cardinality
analysis <cit.>). A limitation of such an
analysis is that it is necessarily heuristic (the problem is
undecidable for Haskell). Because inlining is crucial to efficiency, programmers
find themselves in the uncomfortable position of relying on a
heuristic to obtain efficient programs. Consequently, a small, seemingly
innocuous change can prevent a critical inlining opportunity and have
rippling catastrophic effects throughout the program.
Such unpredictable behaviour justifies the folklore that high-level languages should be
abandoned to gain precise control over program efficiency.

A remedy is to use the multiplicity annotations of  as
cardinality declarations. Formalising and implementing the
integration of multiplicities in the cardinality analysis is
left as future work.

§.§ Extending multiplicities

For the sake of this article, we use only multiplicities
$1$ and $ω$.  But in fact  can readily be extended to
more, following <cit.> and
<cit.>. The general setting for  is an
ordered-semiring of multiplicities (with a join operation for type
inference).  In particular, in order to support dependent types,
needs a $0$ multiplicity.   We may also want to add a
multiplicity for affine arguments (arguments which can be
used at most once).

The typing rules are mostly unchanged with the caveat that
$\mathsf{case}_π$ must exclude $π=0$ (in particular we see that we
cannot substitute multiplicity variables by $0$). The variable rule becomes:

\inferrule{ x :_1 A \leqslant Γ }{Γ ⊢ x : A}

Where the order on contexts is the point-wise extension of the order
on multiplicities.

In sec:uniqueness, we have considered the notion of
borrowing: delimiting life-time without restricting to linear
usage. This seems to be a useful pattern, and we believe it can be
encoded as an additional multiplicity as follows: let $β$ be an
additional multiplicity with the following characteristics:

* $1 < β < ω$

* $β+β = 1+β = 0+β = 1+1 = β$

That is, $β$ supports contraction and weakening but is smaller than
$ω$. We can then introduce a value with an explicit lifetime with the
following pattern
[3]borrow::(T→_β Unrestricted a)→_β Unrestricted a[E]
The  function makes the life-time manifest in the structure of
the program. In particular, it is clear that calls within the argument
of  are not tail: a shortcoming of borrowing that we mentioned
in sec:uniqueness.

§.§ Future industrial applications

Our own work in an industrial context triggered our efforts to add
linear types to ghc. We were originally motivated by
precisely typed protocols for complex interactions and by taming
gc latencies in distributed systems. But we have since
noticed other potential applications of linearity in a variety of
other industrial projects.

Streaming I/O Program inputs and outputs are frequently much
larger than the available ram on any single node. Rather than
building complex pipelines with brittle explicit loops copying data
piecemeal to spare our precious ram, one approach is to compose
combinators that transform, split and merge data wholemeal but in
a streaming fashion. These combinators manipulate first-class streams and guarantee bounded memory usage, as in the below
infinitely running echo service:
[5]receive::Socket→IOStream Msg[E]

[5]send::Socket→IOStream Msg→IO ()[E]

[5]echo isock osock=send osock (receive isock)[E]
However, reifying sequences of  actions (socket reads) in this
way runs the risk that effects might be duplicated inadvertently. In
the above example, we wouldn't want to inadvertently hand over the
receive stream to multiple consumers, or the abstraction of
wholemeal I/O programming would be broken (like in <cit.>), because neither consumer would
ultimately see the same values from the stream. If say one consumer
reads in the stream first, the second consumer would see an
empty stream — not what the first consumer saw.

We have seen this very error several times in industrial projects,
where the symptoms are bugs whose root cause are painful to track
down. A linear type discipline would prevent such bugs.

Programming foreign heaps Complex projects with large teams
invariably involve a mix of programming languages. Reusing legacy
code is often much cheaper than reimplementing it. A key to
successful interoperation between languages is performance. If all
code lives in the same address space, then data need not be copied
as it flows from function to function implemented in multiple
programming languages. Trouble is, language A needs to tell language
B what objects in language A's heap still have live references in
the call stack of language B to avoid too eager garbage collection.

For instance, users of  call the jvm
from Haskell via the jni. The jvm implicitly
creates so-called local references any time we request a Java
object from the jvm. The references count as gc
roots that prevent eager garbage collection. For performance, local
references have a restricted scope: they are purely thread-local and
never survive the call frame in which they were created. Both
restrictions to their use can be enforced with linear types.

Remote direct memory access
sec:cursors is an example of an api requiring
destination-passing style. This style often appears
in performance-sensitive contexts. One notable example from our
industrial experience is rdma (Remote Direct Memory Access),
which enables machines in high-performance clusters to copy data
from the address space in one process to that of a remote process
directly, bypassing the kernel and even the
cpu, thereby avoiding any unneeded copy in the process.

One could treat a remote memory location as a low-level resource, to
be accessed using an imperative api. Using linear types, one
can instead treat it as a high-level value which can be written to
directly (but exactly once). Using linear types the compiler can
ensure that, as soon as the writing operation is complete, the
destination computer is notified.

§ CONCLUSION

This article demonstrates how an existing lazy language, such
as Haskell, can be extended with linear types, without compromising
the language, in the sense that:

* existing programs are valid in the extended language
without modification,

* such programs retain the same operational semantics, and in particular

* the performance of existing programs is not affected,

* yet existing library functions can be reused to serve the
objectives of resource-sensitive programs with simple changes to
their types, and no code duplication.

In other words: regular Haskell comes first. Additionally, first-order
linearly typed functions and data structures are usable directly from
regular Haskell code. In such a setting their semantics is that of
the same code with linearity erased.

was engineered as an unintrusive design, making it tractable
to integrate to an existing, mature compiler with a large ecosystem.
We have developed a prototype implementation extending
ghc with multiplicities. As we hoped, this
design integrates well in ghc.

Even though we change only 's type system, we found that the
compiler and runtime already had the features necessary for unboxed,
off-heap, and in-place data structures.  That is,  has the
low-level compiler primitives and ffi support to implement,
for example, mutable arrays, mutable cursors into serialised data, or
off-heap foreign data structures without garbage collection.  These
features could be used before this work, but their correct use
put some burden-of-proof on the programmers. Linearity unlocks these
capabilities for safe, compiler-checked use, within pure code.

This work has received funding from the ERCEuropean
Commissionhttps://erc.europa.eu/ through the sage project
(Grant agreement
no. [http://www.sagestorage.eu]ERC671500), as well as
from VRSwedish Research Councilhttps://www.vr.se/
via the establishment of the Centre for Linguistic Theory and
Studies in Probability (clasp) at the University of Gothenburg.

We thank Manuel Chakravarty, Stephen Dolan and Peter Thiemann for their valuable
feedback on early versions of this paper.

§ SEMANTICS AND SOUNDNESS OF

In accordance with our stated goals in sec:introduction, we are
interested in two key properties of our system: 1. that we can implement
a linear api with mutation under the hood, while exposing a
pure interface, and 2. that typestates are indeed enforced. This
appendix establishes these results in accordance to
sec:metatheory where they were presented.

We introduce two dynamic semantics for : a semantics with
mutation which models the implementation but blocks on incorrect
type-states, and a pure semantics, which we dub denotational as
it represents the intended meaning of the program. We consider here array
primitives in the style of sec:freezing-arrays, but we could extend to
any number of other examples such as the files of

We prove the two semantics bisimilar, so that type-safety and progress
can be transported from the denotational semantics to the ordinary
semantics with mutation. The bisimilarity itself ensures that the
mutations are not observable and that the semantics is correct in exposing
a pure semantics. The progress result proves that typestates need not be
tracked dynamically.

§.§ Preliminaries

Our operational semantics are big-step semantics with laziness in the
style of <cit.>. In such semantics, sharing
is expressed by mutating the environment assigning value to
variables. Terms are transformed ahead of execution in order to
reflect the amount of sharing that a language like Haskell would
offer. In particular the arguments of an application are always

Following <cit.>, however, we consider
not only standard big-step derivations but also partial derivations.
The reason to consider partial derivation is that they make it
possible to express properties such as progress: all partial
derivations can be extended.

Given a number of rules defining $a⇓b$ with ordered premises (we will
use the ordering of premises shortly), we
define a total derivation of $a⇓b$ as a tree in the standard
fashion. As usual $a⇓b$ holds if there is a total derivation for it.
A partial derivation of $a⇓?$ (the question mark is part of the
syntax: the right-hand value is the result of the evaluation, it is
not yet known for a partial derivation!) is either:

* just a root labelled with $a⇓?$,

* or an application of a rule matching $a$ where exactly one of
the premises, $a'⇓?$ has a partial derivation, all the premises to
the left of $a'⇓?$ have a total derivation, and the premises to the
right of $a'⇓?$ are not known yet (since we would need to know the
value $?$ to know what the root of the next premise is).

Remark that, by definition, in a partial derivation, there is exactly one
$b⇓?$ with no sub-derivation. Let us call $b$ the head of the
partial derivation. And let us write $a⇓^*b$ for the relation which
holds when $b$ is the head of some partial derivation with root
$a⇓?$. We call $a⇓^*b$ the partial evaluation relation, and, by
contrast, $a⇓b$ is sometimes referred to as the the complete
evaluation relation.

§.§ Ordinary semantics

Our semantics, which we often call ordinary to constrast it
with the denotational semantics of sec:denotational, follows
closely the semantics of <cit.>. The main
differences are that we keep the type annotation, and that we have
primitives for proper mutation.

Mixing mutation and laziness is not usual, as the unspecified
evaluation order of lazy languages would make mutation order
unpredicable, hence programs non-deterministic. It is our goal to show
that the linear typing discipline ensures that, despite the mutations,
the evaluation is pure.

Just like <cit.> does, we constrain the terms
to be explicit about sharing, before any evaluation takes
place. fig:launchbury:syntax shows the translation of abtrary
term to terms in the explicit-sharing form.

Translation of typed terms

\begin{align*}
(λ_π(x{:}A). t)^* &= λ_π(x{:}A). (t)^* \\
x^*             &= x \\
(t  x )^*     &= (t)^*  x \\
(t  u )^*     &= \flet[π] y : A = (u)^* \fin (t)^*  y &
\text{with $Γ⊢ t : A →_π B$}
\end{align*}

\begin{align*}
c_k  t₁ … t_n   &= \flet x₁ :_{π_1} A_1 = (t₁)^*,…, x_n :_{π_n} A_n = (t_n)^*
\fin c_k x₁ … x_n & \text{with $c_k : A_1
→_{π_1}…A_n →_{π_n}D$}
\end{align*}

\begin{align*}
(\case[π] t {c_k  x₁ … x_{n_k} → u_k})^* &= \case[π] {(t)^*} {c_k  x₁ … x_{n_k} → (u_k)^*} \\
(\flet[π] x_1: A_1= t₁  …  x_n : A_n = t_n \fin u)^* & = \flet[π] x₁:A_1 = (t₁)^*,…, x_n:A_n= (t_n)^* \fin (u)^*
\end{align*}

Syntax for the Launchbury-style semantics

The evaluation relation is of the form $Γ : e ⇓ Δ : z$ where $e$ is an
expression, $z$ a value $Γ$ and $Δ$ are environments with
bindings of the form $x :_ω A = e$ assigning the expression $e$ the the
variable $x$ of type $A$. Compared to the pure semantic of
, we have one additional kind of
values, $l$ for names of arrays. Array names are given semantics by
additional bindings in environments which we write, suggestively, $l
:_1 A = arr$. The $1$ is here to remind us that arrays cannot be used
arbitrarily, however, it does not mean they are always used in a
linear fashion: frozen arrays are not necessarily linear, but they
still appear as array names.

The details of the ordinary evaluation relation are given in
fig:dynamics. Let us describe the noteworthy rules:

mutable cell array names are values, hence are not
reduced. In that they differ from variables.

newMArray allocates a fresh array of the given size (we write
$i$ for an integer value). Note that
the value of $a$ is not evaluated: an array in the environment is
a concrete list of (not necessarily distinct) variables.

writeArray Mutates its array argument

freezeArray Mutates the type of its argument to
before wrapping it in $\varid{Unrestricted}$, so that we cannot call
$\varid{write}$ on it anymore: $\varid{write}$ would block because
the type of $l$ is not . Of course, in an implementation
this would not be checked because progress ensures that the case
never arises.

Γ : λp. t ⇓ Γ : λp. tm.abs

Γ : e ⇓ Δ : λp.e'
Δ : e'[π/q] ⇓ Θ : z Γ :
e π ⇓ Θ : z m.app

Γ : λ_π(x:A). e ⇓ Γ : λ_π(x:A). eabs

Γ : e ⇓ Δ : λ_π(y:A).e'
Δ : e'[x/y] ⇓ Θ : z Γ :
e x ⇓ Θ : z application

Γ : e ⇓ Δ : z(Γ,x :_ω A = e) : x ⇓ (Δ;x :_ω A = z) :

(Γ,l :_1 A = arr) : l ⇓ (Γ, l :_1 A = arr) : lmutable cell

(Γ,x_1 :_ω A_1 = e_1,…,x_n :_ω A_n e_n) : e ⇓ Δ : z
Γ : [π] x₁ : A_1 = e₁ … x_n : A_n = e_n e ⇓ Δ :

Γ : c  x₁ … x_n ⇓ Γ : c  x₁ …

Γ: e ⇓ Δ : c_k  x₁ … x_n
Δ : e_k[x_i/y_i] ⇓ Θ : z
Γ : [π] e c_k  y₁ … y_n ↦ e_k  ⇓ Θ : zcase

Γ:n ⇓ Δ:i
(Δ, l :_1 MArray a = [a,…,a]) : [1] x = l f x ⇓ Θ : Unrestricted x
Γ : newMArray n a f ⇓ Θ : Unrestricted xnewMArray

Δ:arr ⇓ (Θ,l:_1 MArray a = [a_1,…,a_i,…,a_n]):l
Γ : write arr n a ⇓ Θ,l :_1 MArray a =
[a_1,…,a,…,a_n] : lwrite

Γ:arr ⇓ (Δ,l :_1 MArray a = [a_1,…,a_n]):l
Γ : freeze arr ⇓ (Δ,l :_1 Array a = [a_1,…,a_n],
x :_ω Array a = l) :
Unrestricted xfreeze

Γ : n ⇓ Δ : i
Δ:arr ⇓ (Θ,l :_1 Array a =
[a_1,…,a_i,…,a_n]) : l
(Θ,l :_1 Array a =
[a_1,…,a_i,…,a_n]) : a_i ⇓ Λ : z
Γ : index arr n ⇓ Λ : z

Ordinary dynamic semantics

§.§ Denotational semantics

Ξ ⊢ (Γ | λp. t ⇓ Γ | λp. t) :_ρ A, Σm.abs

Ξ ⊢ (Γ | e ⇓ Δ | λp.e') :_ρ A, Σ
Ξ ⊢ (Δ | e'[π/q] ⇓ Θ | z) :_ρ A, Σ (Γ :
e π ⇓ Θ : z) :_ρ A, Σ m.app

Ξ ⊢ (Γ | λ_π(x:A). e ⇓ Γ | λ_π (x:A). e) :_ρ A→_π B, Σabs

Ξ  ⊢  (Γ|e      ⇓ Δ|λ(y:_π A).u):_ρ A →_π B, x:_πρ A, Σ

Ξ  ⊢  (Δ|u[x/y] ⇓ Θ|z)   :_ρ       B,            Σ
Ξ  ⊢  (Γ|e x ⇓ Θ|z) :_ρ B ,Σ

Ξ, x:_ωB ⊢ (Γ|e ⇓ Δ|z) :_ρ A, Σ
Ξ ⊢ (Γ,x :_ω B = e | x  ⇓ Δ, x :_ω B = z | z) :_ρ A, Σ
shared variable

Ξ ⊢ (Γ|e ⇓ Δ|z) :_1 A, Σ
Ξ ⊢ (Γ,x :_1 B = e| x  ⇓  Δ|z) :_1 A,  Σ
linear variable

Ξ ⊢ (Γ,       x_1 :_ρπ A_1 = e_1 … x_n :_ρπ A_n = e_n  |  t ⇓ Δ|z) :_ρ C, Σ
Ξ ⊢ (Γ|[π] x_1 :  A_1 = e_1 … x_n : A_n = e_n t ⇓ Δ|z) :_ρ C, Σ

Ξ ⊢ (Γ | c x_1…x_n  ⇓ Γ | c x_1…x_n) :_ρ A, Σ

Ξ,y_1:_π_1qρ A_1 … ,y_n:_π_nqρ A_n ⊢ (Γ|e ⇓ Δ|c_k x_1…x_n) :_πρ D, u_k:_ρ C, Σ

Ξ ⊢ (Δ|u_k[x_i/y_i] ⇓ Θ|z) :_ρ C, Σ
Ξ ⊢ (Γ|[π] e c_k y_1…y_n ↦ u_k ⇓ Θ|z) :_ρ C, Σ

Ξ ⊢ (Γ|n ⇓ Δ|i), Int, (arr:_ρ MArray a, Σ)
Ξ ⊢
(Δ|[1] x = [a,…,a] f x) ⇓ Θ|Unrestricted x) :_1 Unrestricted B, Σ
Ξ ⊢ (Γ|newMArray n a f ⇓ Θ|Unrestricted x) :_ρ Unrestricted B, ΣnewMArray

Ξ ⊢ (Γ|n⇓Δ|i) :_ρ Int, (arr:_ρ MArray a, Σ)
Ξ ⊢ (Δ|arr⇓Θ|[a_1,…,a_i,…,a_n]) :_ρ
MArray a, Σ
Ξ ⊢ (Γ|write arr n a
⇓ Γ|[a_1,…,a,…,a_n]) :_ρ MArray a, Σwrite

Ξ ⊢ (Γ|arr ⇓ Δ|[a_1,…,a_n]) :_ρ MArray a, Σ
Ξ ⊢ (Γ|freeze arr ⇓ Δ,x :_1 Array a = [a_1,…,a_n]|Unrestricted x
) :_ρ Unrestricted (Array a), Σfreeze

Ξ ⊢ (Γ | n ⇓ Δ | i) :_ρ Int,Σ
Ξ ⊢ (Δ|arr ⇓ Θ |
[a_1,…,a_i,…,a_n])) :_ρ Array a,Σ
Ξ ⊢ (Θ | a_i ⇓ Λ | z)
:_ρ A, Σ
Ξ ⊢ (Γ | index arr n ⇓ Λ | z) :_ρ a, Σ

Denotational dynamic semantics

The ordinary semantics, if a good model of what we are implementing in
practice, is not very convenient to reason about directly. First
mutation is a complication in itself, but it is also difficult to
recover types (or even multiplicity annotations) from a particular
evaluation state.

We address this difficulty by introducing a denotational semantics where the states
are annotated with types and linearity. The denotational semantics
also does not perform mutations: arrays are seen as ordinary values
which we modify by copy.

An annotated state is a tuple $Ξ ⊢ (Γ|t :_ρ A),Σ$ where

* $Ξ$ is a typing context

* $Γ$ is a typed environment, a collection of
bindings of the form $x :_ρ A = e$

* $t$ is a term

* $ρ∈\{1,ω\}$ is a multiplicity

* $A$ is a type

* $Σ$ is a typed stack, a list of triple $e:_ρ A$ of
a term, a multiplicity and an annotation.

Terms are extended with array expressions: $[a_1, …, a_n]$ where the
$a_i$ are variables.

Let us introduce a notation which will be needed in the definition of
well-typed state.

We define a type of left-weighted pairs:

$$\data a~{}_π\!⊗ a = ({}_π\!,) : a →_π b ⊸ a~{}_π\!⊗ b$$

Let us remark that

* We have not introduced type parameters in datatypes, but it
is straightforward to do so

* We annotate the data constructor with the multiplicity $π$,
which is not mandated by the syntax. It will make things simpler.

Weighted pairs are used to internalise a notion of stack that keeps
track of multiplicities in the following definition, which defines
when annotated states are well-typed.

We say that an annotated state is well-typed if the following
typing judgement holds:

Ξ ⊢ \flet Γ \fin (t,\termsOf{Σ}) : (A~{}_ρ\!⊗\multiplicatedTypes{Σ})

Where $\flet Γ \fin e$ stands for the use of $Γ$ as a sequence of
let-bindings with the appropriate multiplicity[We skip over
the case of mutually recursive bindings in our presentation. But
we can easily extend the formalism with then. Recursive bindings
must be of multiplicity $ω$, and mutually recursive definition are
part of a single $\flet$ block. When defining $\flet Γ$ we need to
pull a mutually recursive block as a single $\flet$ block as
well.], $\termsOf{e_1 :_{ρ_1} A_1, … , e_n :_{ρ_n} A_n}$ for
$(e_1~{}_{ρ_1}\!, (…, (e_n~{}_{ρ_n},())))$, and
$\multiplicatedTypes{e_1 :_{ρ_1} A_1, … , e_n :_{ρ_n} A_n}$ for

We define the denotational reduction relation, also written $⇓$, as a
relation on annotated states. Because $Ξ$, $ρ$, $A$ and $Σ$ are
always the same for related states, we abbreviate

(Ξ ⊢ Γ|t :_ρ A,Σ) ⇓ (Ξ ⊢ Δ|z :_ρ A,Σ)

Ξ ⊢ (Γ|t ⇓ Δ|z) :_ρ A, Σ

The denotational reduction relation is defined inductively by the
rules of fig:typed-semop.

A few rules of notice:

linear variable linear variables are removed from the
environment when they are evaluated: they are no longer accessible
(if the state is well-typed)

let even if we are evaluating a $\flet_1$m we may have to
introduce a non-linear binding in the environemnt: if the value we
are currently computing will be used as the argument of a
non-linear function, the newly introduced variables may be forced
several times (or not at all). An example is
$\flet[ω] x = (\flet[1] y = \varid{True}) \fin y \fin (x,x)$: if evaluating
this example yielded the binding $y :_1 Bool = True$, then the
intermediate state would be ill-typed. So for the sake of proofs,
instead we add $y :_ω Bool = True$ to the environment

write No mutation is performed in array write: we just return
a new copy of the array.

The denotation semantics preserves the well-typedness of annotated
states throughout the evaluationthm:type-safety. From then on, we
will only consider the evaluation of well-typed states.

If  $Ξ ⊢ (Γ|t ⇓ Δ|z) :_ρ A, Σ$, or $Ξ ⊢ (Γ|t ⇓^* Δ|z) :_ρ A, Σ$ then

Ξ ⊢ (Γ|t :_ρ A),Σ \text{\quad{}implies\quad{}} Ξ ⊢ (Δ|z :_ρ A),Σ.

By induction on the typed-reduction.

The case of the linear variable rule is interesting, as it uses the
fact that, by the constructor rule, $x :_1 B$ can only be used in
the typing of the variable $x$, it is absent from the context when
type-checking $Σ$. In particular note how the rule must
remove $x$ from the environment in order to preserve typing.

Evaluation does not block. That is, for any partial derivation of
$Ξ ⊢ (Γ'|e ⇓ ?) :_ρ A,Σ$, the derivation can be

The proof of progress, for the denotational semantics, is almost
entirely standard. The only unusual rule is the linear variable
rule, in which there are two things of notice:

* The linear variable rule blocks if $ρ = ω$

* The linear variable rule removes the variable $x$ from the

Therefore it suffices to show that the former case never arises. And
that whenever a variable is evaluated, then it appears in the

* Notice that $Ξ⊢Γ,x:_1 B = e|x :_ω A,Σ$ is not a well-typed
state because it reduces to $x:_1B = x:_{ωπ} B$ for some $π$,
which never holds. By type preservation (thm:type-safety),
$Ξ⊢Γ,x:_1 B = e|x :_ω A,Σ$ cannot be the head of a partial

* Similarly $Ξ⊢Γ|x :_1 A,Σ$ where $x∉Γ$ is not well-typed, and
hence cannot be the head of a partial derivation[Notice
that it is an invariant of the denotational evaluation, that
variables in $Ξ$ are not reachable from $e$. This is only true
because let-bindings are not recursive. In the case that they
are recursive, the shared variable rule make it possible to run
into a situation where $x$ is evaluated and part of $Ξ$, in
which case the reduction blocks: this models so-called
black-holing in which ill-founded recursive lazy
definitions report an error rather than looping. This
presentation follows <cit.>, and in
presence of such recursion, progress must be extended to say
that partial derivation can be either extended or is in a black
hole. An alternative solution is to change the shared variable
rule to loop instead of blocking in case of such ill-founded

§.§ Bisimilarity and all that

The crux of our metatheory is that the two semantics are
bisimilar. Bisimilarity allows to tranport properties from the
denational semantics, on which it is easy to reason, and the ordinary
semantics which is close to the implementation. It also makes it
possible to prove observational equality results. Our first definition
is the relation between the states of the ordinary evaluation and
those of the denotational evaluation which witnesses the bisimulation.

A well-typed state is said to be a denotation assignment for an ordinary
state, written $\ta{Γ:e}{Ξ ⊢ Γ' | e' :_ρ A , Σ}$, if
$e[Γ_1]=e' ∧ Γ' = Γ''[Γ_1] ∧ Γ'' \leqslant Γ_ω$. Where

* $Γ_ω$ is the restriction of $Γ$ (a context of the ordinary
semantics) to the variable bindings $x :_ω A = u$

* $Γ_1$ is the restriction of $Γ$ to the array bindings $l :_1 A
= [a_1, …, a_n]$, seen as a substitution.

That is, $Γ'$ is allowed to strengthen some $ω$ bindings to be
linear, and to drop unnecessary bindings. Array pointers are
substituted with their value (since we have array pointers in the
ordinary semantics but only array values in the denotational
semantics). The substitution is subject to

The substitution must abide by the following restrictions in order
to preserve the invariant that  pointers are not shared:

* An  pointer in $Γ_1$ is substituted either exactly
in one place in $Γ''$ or exactly in one place in $e$.

* If an  pointer is substituted in $Γ''$ then it is
substituded in a linear binding $x :_1 A = u$

* If an  pointer is substituted in $e$ the $ρ=1$

* If an  pointer is substituted in the body $u$ as of
$let_p x = u in v$ (sub)expression, the $p=1$

The denotation assignment relation defines a simulation of the
ordinary evaluation by the denotational evaluation, both in the
complete and partial case.

That is:

* for all $\ta{Γ:e}{Ξ ⊢ (Γ'|e) :_ρ A,Σ}$ such that $Γ:e⇓Δ:z$,
there exists a well-typed state $Ξ ⊢ (Δ'|z) :_ρ A,Σ$ such that
$Ξ ⊢ (Γ|t ⇓ Δ|z) :_ρ A, Σ$ and $\ta{Δ:z}{Ξ ⊢ (Δ'|z) :_ρ A,Σ}$.

* for all $\ta{Γ:e}{Ξ ⊢ (Γ'|e) :_ρ A,Σ}$ such that $Γ:e⇓^*Δ:z$,
there exists a well-typed state $Ξ ⊢ (Δ'|z) :_ρ A,Σ$ such that
$Ξ ⊢ (Γ|t ⇓^* Δ|z) :_ρ A, Σ$ and $\ta{Δ:z}{Ξ ⊢ (Δ'|z) :_ρ A,Σ}$.

Both simulations are proved by a similar induction on the derivation
of $Γ:e⇓Δ:z$ (resp. $Γ:e⇓Δ:z$):

* The properties of the substitution of  in the
definition of denotation assignments are crafted to make the
variable and let rules carry through

* The other rules are straightforward

The refinement relation defines a simulation of the strengthened
reduction by the ordinary reduction, both in the complete and
partial case.

That is:

* for all $\ta{Γ:e}{Ξ ⊢ (Γ'|e) :_ρ A,Σ}$ such that
$Ξ ⊢ (Γ'|e' ⇓ Δ'|z') :_ρ A,Σ$, there exists a state $Δ:z$ such
that $Γ:e'⇓Δ:z'$ and $\ta{Δ:z}{Ξ ⊢ (Δ'|z') :_ρ A,Σ}$.

* for all $\ta{Γ:e}{Ξ ⊢ (Γ'|e) :_ρ A,Σ}$ such that
$Ξ ⊢ (Γ'|e ⇓^* Δ'|t) :_ρ A,Σ$, there exists a state $Δ:t'$ such
that $Γ:e⇓^*Δ:z$ and $\ta{Δ:t}{Ξ ⊢ (Δ'|t') :_ρ A,Σ}$.

Both are proved by a straightforward induction over the derivation of
$Ξ ⊢ (Γ'|e ⇓ Δ'|z) :_ρ A,Σ$ (resp. $Ξ ⊢ (Γ'|e ⇓ Δ'|z) :_ρ A,Σ$).

Equipped with this bisimulation, we are ready to prove the soundness
properties of the ordinary semantics. We say that a state $Γ:e$ is
well-typed if there exists an annotated state $Ξ⊢Γ'|e':_ρ A,Σ$, such
that $\ta{Γ:e}{Ξ⊢Γ'|e':_ρ A,Σ}$.

For any well-typed $Γ:e$, if $Γ:e⇓Δ:t$ or $Γ:e⇓^*Δ:t$, then $Δ:t$ is

This is precisely the same statement as lem:actual_type_safety

Evaluation does not block. That is, for any partial derivation of
$Γ:e⇓?$, for $Γ:e$ well-typed, the derivation can be

In particular, typestates need not be checked dynamically.

By liveness (lem:liveness) it is sufficient to prove the case
of the denotational semantics. Which follows from thm:progress-denotational

Observational equivalence, which means, for , that an
implementation in terms of in-place mutation is indistinguishable from
a pure implementation, is phrased in terms of the : any
distinction which we can make between two evaulations can be
extended so that one evaluates to  and the other to .

The ordinary semantics, with in-place mutation is observationally equivalent
to the pure denotational semantics.

That is, for all $\ta{⋅:e}{⊢ (⋅|e) :_ρ \varid{Bool},⋅}$, if $⋅:e ⇓ Δ:z$ and
$⋅ ⊢ (⋅|e⇓ Δ|z')  :_ρ \varid{Bool}, ⋅ $, then $z=z'$

Because the semantics are deterministic, this is a direct
consequence of bisimilarity.