Mixing Metaphors: Actors as Channels and
Channels as Actors (Extended Version)
Simon Fowler, Sam Lindley, and Philip Wadler
University of Edinburgh, Edinburgh, United Kingdom
simon.fowler@ed.ac.uk, sam.lindley@ed.ac.uk, wadler@inf.ed.ac.uk

arXiv:1611.06276v3 [cs.PL] 10 May 2017

Abstract
Channel- and actor-based programming languages are both used in practice, but the two are often
confused. Languages such as Go provide anonymous processes which communicate using buffers
or rendezvous points—known as channels—while languages such as Erlang provide addressable
processes—known as actors—each with a single incoming message queue. The lack of a common
representation makes it difficult to reason about translations that exist in the folklore. We define
a calculus λch for typed asynchronous channels, and a calculus λact for typed actors. We define
translations from λact into λch and λch into λact and prove that both are type- and semanticspreserving. We show that our approach accounts for synchronisation and selective receive in
actor systems and discuss future extensions to support guarded choice and behavioural types.
1998 ACM Subject Classification D.1.3 Concurrent Programming
Keywords and phrases Actors, Channels, Communication-centric Programming Languages
Digital Object Identifier 10.4230/LIPIcs.ECOOP.2017.90

1

Introduction

When comparing channels (as used by Go) and actors (as used by Erlang), one runs into an
immediate mixing of metaphors. The words themselves do not refer to comparable entities!
In languages such as Go, anonymous processes pass messages via named channels, whereas
in languages such as Erlang, named processes accept messages from an associated mailbox.
A channel is either a named rendezvous point or buffer, whereas an actor is a process. We
should really be comparing named processes (actors) with anonymous processes, and buffers
tied to a particular process (mailboxes) with buffers that can link any process to any process
(channels). Nonetheless, we will stick with the popular names, even if it is as inapposite as
comparing TV channels with TV actors.

A

b

a

B

c
C

(a) Asynchronous Channels

(b) Actors

Figure 1 Channels and Actors
© S. Fowler, S. Lindley, and P. Wadler;
licensed under Creative Commons License CC-BY
31st European Conference on Object-Oriented Programming (ECOOP 2017).
Editor: Peter Müller; Article No. 90; pp. 90:1–90:55
Leibniz International Proceedings in Informatics
Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

90:2

Mixing Metaphors

Figure 1 compares asynchronous channels with actors. On the left, three anonymous processes
communicate via channels named a, b, c. On the right, three processes named A, B, C
send messages to each others’ associated mailboxes. Actors are necessarily asynchronous,
allowing non-blocking sends and buffering of received values, whereas channels can either be
asynchronous or synchronous (rendezvous-based). Indeed, Go provides both synchronous
and asynchronous channels, and libraries such as core.async [24] provide library support
for asynchronous channels. However, this is not the only difference: each actor has a single
buffer which only it can read—its mailbox—whereas asynchronous channels are free-floating
buffers that can be read by any process with a reference to the channel.
Channel-based languages such as Go enjoy a firm basis in process calculi such as CSP [25]
and the π-calculus [38]. It is easy to type channels, either with simple types (see [46], p.
231) or more complex systems such as session types [17, 26, 27]. Actor-based languages such
as Erlang are seen by many as the "gold standard" for distributed computing due to their
support for fault tolerance through supervision hierarchies [6, 7].
Both models are popular with developers, with channel-based languages and frameworks
such as Go, Concurrent ML [45], and Hopac [28]; and actor-based languages and frameworks
such as Erlang, Elixir, and Akka.

1.1

Motivation

This paper provides a formal account of actors and channels as implemented in programming
languages. Our motivation for a formal account is threefold: it helps clear up confusion; it
clarifies results that have been described informally by putting practice into theory; and it
provides a foundation for future research.
Confusion. There is often confusion over the differences between channels and actors. For
example, the following questions appear on StackOverflow and Quora respectively:
“If I wanted to port a Go library that uses Goroutines, would Scala be a good choice
because its inbox/[A]kka framework is similar in nature to coroutines?” [31], and
“I don’t know anything about [the] actor pattern however I do know goroutines and
channels in Go. How are [the] two related to each other?” [29]
In academic circles, the term actor is often used imprecisely. For instance, Albert et al. [5]
refer to Go as an actor language. Similarly, Harvey [21] refers to his language Ensemble
as actor-based. Ensemble is a language specialised for writing distributed applications
running on heterogeneous platforms. It is actor-based to the extent that it has lightweight,
addressable, single-threaded processes, and forbids co-ordination via shared memory. However,
Ensemble communicates using channels as opposed to mailboxes so we would argue that it is
channel-based (with actor-like features) rather than actor-based.
Putting practice into theory. The success of actor-based languages is largely due to their
support for supervision. A popular pattern for writing actor-based applications is to arrange
processes in supervision hierarchies [6], where supervisor processes restart child processes
should they fail. Projects such as Proto.Actor [44] emulate actor-style programming in a
channel-based language in an attempt to gain some of the benefits, by associating queues
with processes. Hopac [28] is a channel-based library for F#, based on Concurrent ML [45].
The documentation [1] contains a comparison with actors, including an implementation
of a simple actor-based communication model using Hopac-style channels, as well as an

Fowler, Lindley, and Wadler

90:3

sender

receiver

sender

receiver

P1

P1

P1

P1

P2

P2

P2

P2

P3

P3

P3

P3

(a) Channel

(b) Mailbox

Figure 2 Mailboxes as pinned channels

implementation of Hopac-style channels using an actor-based communication model. By
comparing the two, this paper provides a formal model for the underlying techniques, and
studies properties arising from the translations.
A foundation for future research. Traditionally, actor-based languages have had untyped
mailboxes. More recent advancements such as TAkka [22], Akka Typed [4], and Typed
Actors [47] have added types to mailboxes in order to gain additional safety guarantees. Our
formal model provides a foundation for these innovations, characterises why naïvely adding
types to mailboxes is problematic, and provides a core language for future experimentation.

1.2

Our approach

We define two concurrent λ-calculi, describing asynchronous channels and type-parameterised
actors, define translations between them, and then discuss various extensions.
Why the λ calculus? Our common framework is that of a simply-typed concurrent λcalculus: that is, a λ-calculus equipping a term language with primitives for communication
and concurrency, as well as a language of configurations to model concurrent behaviour.
We work with the λ-calculus rather than a process calculus for two reasons: firstly, the
simply-typed λ-calculus has a well-behaved core with a strong metatheory (for example,
confluent reduction and strong normalisation), as well as a direct propositions-as-types
correspondence with logic. We can therefore modularly extend the language, knowing which
properties remain; typed process calculi typically do not have such a well-behaved core.
Secondly, we are ultimately interested in functional programming languages; the λ calculus
is the canonical choice for studying such extensions.
Why asynchronous channels? While actor-based languages must be asynchronous by
design, channels may be either synchronous (requiring a rendezvous between sender and
receiver) or asynchronous (where sending happens immediately). In this paper, we consider
asynchronous channels since actors must be asynchronous, and it is possible to emulate
asynchronous channels using synchronous channels [45]. We could adopt synchronous channels,
use these to encode asynchronous channels, and then do the translations. We elect not to
since it complicates the translations, and we argue that the distinction between synchronous
and asynchronous communication is not the defining difference between the two models.

ECOOP 2017

90:4

Mixing Metaphors

1.3

Summary of results

We identify four key differences between the models, which are exemplified by the formalisms
and the translations: process addressability, the restrictiveness of communication patterns,
the granularity of typing, and the ability to control the order in which messages are processed.
Process addressability. In channel-based systems, processes are anonymous, whereas channels are named. In contrast, in actor-based systems, processes are named.
Restrictiveness of communication patterns. Communication over full-duplex channels is
more liberal than communication via mailboxes, as shown in Figure 2. Figure 2a shows the
communication patterns allowed by a single channel: each process Pi can use the channel
to communicate with every other process. Conversely, Figure 2b shows the communication
patterns allowed by a mailbox associated with process P2 : while any process can send to
the mailbox, only P2 can read from it. Viewed this way, it is apparent that the restrictions
imposed on the communication behaviour of actors are exactly those captured by Merro and
Sangiorgi’s localised π-calculus [37].
Readers familiar with actor-based programming may be wondering whether such a
characterisation is too crude, as it does not account for processing messages out-of-order.
Fear not—we show in §7 that our minimal actor calculus can simulate this functionality.
Restrictiveness of communication patterns is not necessarily a bad thing; while it is
easy to distribute actors, delegation of asynchronous channels is more involved, requiring a
distributed algorithm [30]. Associating mailboxes with addressable processes also helps with
structuring applications for reliability [7].
Granularity of typing. As a result of the fact that each process has a single incoming
message queue, mailbox types tend to be less precise; in particular, they are most commonly
variant types detailing all of the messages that can be received. Naïvely implemented, this
gives rise to the type pollution problem, which we describe further in §2.
Message ordering. Channels and mailboxes are ordered message queues, but there is no
inherent ordering between messages on two different channels. Channel-based languages
allow a user to specify from which channel a message should be received, whereas processing
messages out-of-order can be achieved in actor languages using selective receive.
The remainder of the paper captures these differences both in the design of the formalisms,
and the techniques used in the encodings and extensions.

1.4

Contributions and paper outline

This paper makes five main contributions:
1. A calculus λch with typed asynchronous channels (§3), and a calculus λact with typeparameterised actors (§4), based on the λ-calculus extended with communication primitives specialised to each model. We give a type system and operational semantics for each
calculus, and precisely characterise the notion of progress that each calculus enjoys.
2. A simple translation from λact into λch (§5), and a more involved translation from λch
into λact (§6), with proofs that both translations are type- and semantics-preserving.
While the former translation is straightforward, it is global, in the sense of Felleisen [12].
While the latter is more involved, it is in fact local. Our initial translation from λch to
λact sidesteps type pollution by assigning the same type to each channel in the system.

Fowler, Lindley, and Wadler

90:5

chanStack(ch) , rec loop(st).
let cmd ⇐ take ch in
case cmd {
Push(v) 7→ loop(v :: st)
Pop(resCh) 7→
case st {
[ ] 7→ give (None) resCh;
loop [ ]
x :: xs 7→ give (Some(x)) resCh;
loop xs }
}

actorStack , rec loop(st).
let cmd ⇐ receive in
case cmd {
Push(v) 7→ loop(v :: st)
Pop(resPid) 7→
case st {
[ ] 7→ send (None) resPid;
loop [ ]
x :: xs 7→ send (Some(x)) resPid;
loop xs }
}

chanClient(stackCh) ,
give (Push(5)) stackCh;
let resCh ⇐ newCh in
give (Pop(resCh)) stackCh;
take resCh

actorClient(stackPid) ,
send (Push(5)) stackPid;
let selfPid ⇐ self in
send (Pop(selfPid)) stackPid;
receive

chanMain ,
let stackCh ⇐ newCh in
fork (chanStack(stackCh) [ ]);
chanClient(stackCh)

actorMain ,
let stackP id ⇐ spawn (actorStack [ ]) in
actorClient(stackPid)

(a) Channel-based stack

(b) Actor-based stack

Figure 3 Concurrent stacks using channels and actors

3. An extension of λact to support synchronous calls, showing how this can alleviate type
pollution and simplify the translation from λch into λact (§7.1).
4. An extension of λact to support Erlang-style selective receive, a translation from λact with
selective receive into plain λact , and proofs that the translation is type- and semanticspreserving (§7.2).
5. An extension of λch with input-guarded choice (§7.3) and an outline of how λact might
be extended with behavioural types (§7.4).
The rest of the paper is organised as follows: §2 displays side-by-side two implementations of
a concurrent stack, one using channels and the other using actors; §3–7 presents the main
technical content; §8 discusses related work; and §9 concludes.

2

Channels and actors side-by-side

Let us consider the example of a concurrent stack. A concurrent stack carrying values of type
A can receive a command to push a value onto the top of the stack, or to pop a value and return
it to the process making the request. Assuming a standard encoding of algebraic datatypes,
we define a type Operation(A) = Push(A) | Pop(B) (where B = ChanRef(A) for channels, and
ActorRef(A) for actors) to describe operations on the stack, and Option(A) = Some(A) | None
to handle the possibility of popping from an empty stack.
Figure 3 shows the stack implemented using channels (Figure 3a) and using actors
(Figure 3b). Each implementation uses a common core language based on the simply-typed
λ-calculus extended with recursion, lists, and sums.
At first glance, the two stack implementations seem remarkably similar. Each:
1. Waits for a command

ECOOP 2017

90:6

Mixing Metaphors

chanClient2(intStackCh, stringStackCh) ,
let intResCh ⇐ newCh in
let strResCh ⇐ newCh in
give (Pop(intResCh)) intStackCh;
let res1 ⇐ take intResCh in
give (Pop(strResCh)) stringStackCh;
let res2 ⇐ take strResCh in
(res1, res2)

actorClient2(intStackPid, stringStackPid) ,
let selfPid ⇐ self in
send (Pop(selfPid)) intStackPid;
let res1 ⇐ receive in
send (Pop(selfPid)) stringStackPid;
let res2 ⇐ receive in
(res1, res2)

Figure 4 Clients interacting with multiple stacks

2. Case splits on the command, and either:
Pushes a value onto the top of the stack, or;
Takes the value from the head of the stack and returns it in a response message
3. Loops with an updated state.
The main difference is that chanStack is parameterised over a channel ch, and retrieves
a value from the channel using take ch. Conversely, actorStack retrieves a value from its
mailbox using the nullary primitive receive.
Let us now consider functions which interact with the stacks. The chanClient function
sends commands over the stackCh channel, and begins by pushing 5 onto the stack. Next, it
creates a channel resCh to be used to receive the result and sends this in a request, before
retrieving the result from the result channel using take. In contrast, actorClient performs
a similar set of steps, but sends its process ID (retrieved using self) in the request instead of
creating a new channel; the result is then retrieved from the mailbox using receive.
Type pollution. The differences become more prominent when considering clients which
interact with multiple stacks of different types, as shown in Figure 4. Here, chanClient2
creates new result channels for integers and strings, sends requests for the results, and creates
a pair of type (Option(Int) × Option(String)). The actorClient2 function attempts to do
something similar, but cannot create separate result channels. Consequently, the actor must
be able to handle messages either of type Option(Int) or type Option(String), meaning that
the final pair has type (Option(Int) + Option(String)) × (Option(Int) + Option(String)).
Additionally, it is necessary to modify actorStack to use the correct injection into the
actor type when sending the result; for example an integer stack would have to send a
value inl (Some(5)) instead of simply Some(5). This type pollution problem can be addressed
through the use of subtyping [22], or synchronisation abstractions such as futures [10].

3

λch : A concurrent λ-calculus for channels

In this section we introduce λch , a concurrent λ-calculus extended with asynchronous channels.
To concentrate on the core differences between channel- and actor-style communication, we
begin with minimal calculi; note that these do not contain all features (such as lists, sums,
and recursion) needed to express the examples in §2.

3.1

Syntax and typing of terms

Figure 5 gives the syntax and typing rules of λch , a λ-calculus based on fine-grain call-byvalue [34]: terms are partitioned into values and computations. Key to this formulation are two
constructs: return V represents a computation that has completed, whereas let x ⇐ M in N

Fowler, Lindley, and Wadler

90:7

Syntax
Types
Variables and names
Values
Computations

A, B ::= 1 | A → B | ChanRef(A)
α ::= x | a
V, W ::= α | λx.M | ()
L, M, N ::= V W
| let x ⇐ M in N | return V
| fork M | give V W | take V | newCh

Γ`V :A

Value typing rules
Abs

Var

Γ, x : A ` M : B
Γ ` λx.M : A → B

α:A∈Γ
Γ`α:A

Unit

Γ ` () : 1

Γ`M :A

Computation typing rules
App

Γ`V :A→B Γ`W :A
Γ`V W :B

EffLet

Γ ` M : A Γ, x : A ` N : B
Γ ` let x ⇐ M in N : B

Return

Γ`V :A
Γ ` return V : A

Give

Γ`V :A
Γ ` W : ChanRef(A)
Γ ` give V W : 1

Take

Γ ` V : ChanRef(A)
Γ ` take V : A

Fork

Γ`M :1
Γ ` fork M : 1

NewCh

Γ ` newCh : ChanRef(A)

Figure 5 Syntax and typing rules for λch terms and values

evaluates M to return V , substituting V for x in M . Fine-grain call-by-value is convenient
since it makes evaluation order explicit and, unlike A-normal form [13], is closed under
reduction.
Types consist of the unit type 1, function types A → B, and channel reference types
ChanRef(A) which can be used to communicate along a channel of type A. We let α range
over variables x and runtime names a. We write let x = V in M for (λx.M ) V and M ; N for
let x ⇐ M in N , where x is fresh.
Communication and concurrency for channels. The give V W operation sends value V
along channel W , while take V retrieves a value from a channel V . Assuming an extension of
the language with integers and arithmetic operators, we can define a function neg(c) which
receives a number n along channel c and replies with the negation of n as follows:
neg(c) , let n ⇐ take c in let negN ⇐ (−n) in give negN c
The fork M operation spawns a new process to evaluate term M . The operation returns
the unit value, and therefore it is not possible to interact with the process directly. The
newCh operation creates a new channel. Note that channel creation is decoupled from process
creation, meaning that a process can have access to multiple channels.

3.2

Operational semantics

Configurations. The concurrent behaviour of λch is given by a nondeterministic reduction
relation on configurations (Figure 6). Configurations consist of parallel composition (C k D),
→
−
→
−
restrictions ((νa)C), computations (M ), and buffers (a( V ), where V = V1 · . . . · Vn ).

ECOOP 2017

90:8

Mixing Metaphors

Syntax of evaluation contexts and configurations
Evaluation contexts
Configurations
Configuration contexts

E ::= [ ] | let x ⇐ E in M
−
→
C, D, E ::= C k D | (νa)C | a( V ) | M
G ::= [ ] | G k C | (νa)G

Γ; ∆ ` C

Typing rules for configurations
Par

Γ; ∆1 ` C1 Γ; ∆2 ` C2
Γ; ∆1 , ∆2 ` C1 k C2

Chan

Γ, a : ChanRef(A); ∆, a:A ` C
Γ; ∆ ` (νa)C

Buf

(Γ ` Vi : A)i
−
→
Γ; a : A ` a( V )

Term

Γ`M :1
Γ; · ` M

Figure 6 λch configurations and evaluation contexts

Evaluation contexts. Reduction is defined in terms of evaluation contexts E, which are
simplified due to fine-grain call-by-value. We also define configuration contexts, allowing
reduction modulo parallel composition and name restriction.
Reduction. Figure 7 shows the reduction rules for λch . Reduction is defined as a deterministic reduction on terms (−→M ) and a nondeterministic reduction relation on configurations
(−→). Reduction on configurations is defined modulo structural congruence rules which
capture scope extrusion and the commutativity and associativity of parallel composition.
Typing of configurations. To ensure that buffers are well-scoped and contain values of the
correct type, we define typing rules on configurations (Figure 6). The judgement Γ; ∆ ` C
states that under environments Γ and ∆, C is well-typed. Γ is a typing environment for
terms, whereas ∆ is a linear typing environment for configurations, mapping names a to
channel types A. Linearity in ∆ ensures that a configuration C under a name restriction
(νa)C contains exactly one buffer with name a. Note that Chan extends both Γ and ∆,
adding an (unrestricted) reference into Γ and the capability to type a buffer into ∆. Par
states that C1 k C2 is typeable if C1 and C2 are typeable under disjoint linear environments,
and Buf states that under a term environment Γ and a singleton linear environment a:A, it
→
−
→
−
→
−
is possible to type a buffer a( V ) if Γ ` Vi :A for all Vi ∈ V . As an example, (νa)(a( V )) is
→
−
−
→
well-typed, but (νa)(a( V ) k a(W )) and (νa)(return ()) are not.
Relation notation. Given a relation R, we write R+ for its transitive closure, and R∗ for
its reflexive, transitive closure.
Properties of the term language. Reduction on terms preserves typing, and pure terms
enjoy progress. We omit most proofs in the body of the paper which are mainly straightforward
inductions; selected full proofs can be found in the extended version [15].
I Lemma 1 (Preservation (λch terms)). If Γ ` M : A and M −→M M 0 , then Γ ` M 0 : A.
I Lemma 2 (Progress (λch terms)). Assume Γ is empty or only contains channel references
ai :ChanRef(Ai ). If Γ ` M :A, then either:
1. M = return V for some value V , or
2. M can be written E[M 0 ], where M 0 is a communication or concurrency primitive (i.e.,
give V W, take V, fork M , or newCh), or
3. There exists some M 0 such that M −→M M 0 .

Fowler, Lindley, and Wadler

90:9

Reduction on terms
(λx.M ) V −→M M {V /x}

let x ⇐ return V in M −→M M {V /x}

E[M1 ] −→M E[M2 ]
(if M1 −→M M2 )

Structural congruence
CkD≡DkC

C k (D k E) ≡ (C k D) k E

C k (νa)D ≡ (νa)(C k D) if a 6∈ fv(C)

G[C] ≡ G[D] if C ≡ D

Reduction on configurations
Give
Take
Fork
NewCh
LiftM
Lift

−
→
E[give W a] k a( V )
−
→
E[take a] k a(W · V )
E[fork M ]
E[newCh]
G[M1 ]
G[C1 ]

−→
−→
−→
−→
−→
−→

−
→
E[return ()] k a( V · W )
−
→
E[return W ] k a( V )
E[return ()] k M
(νa)(E[return a] k a())
(a is a fresh name)
G[M2 ]
(if M1 −→M M2 )
G[C2 ]
(if C1 −→ C2 )

Figure 7 Reduction on λch terms and configurations

Reduction on configurations. Concurrency and communication is captured by reduction
on configurations. Reduction is defined modulo structural congruence rules, which capture
the associativity and commutativity of parallel composition, as well as the usual scope
→
−
extrusion rule. The Give rule reduces give W a in parallel with a buffer a( V ) by adding
the value W onto the end of the buffer. The Take rule reduces take a in parallel with a
non-empty buffer by returning the first value in the buffer. The Fork rule reduces fork M
by spawning a new thread M in parallel with the parent process. The NewCh rule reduces
newCh by creating an empty buffer and returning a fresh name for that buffer.
Structural congruence and reduction preserve the typeability of configurations.
I Lemma 3. If Γ; ∆ ` C and C ≡ D for some configuration D, then Γ; ∆ ` D.
I Theorem 4 (Preservation (λch configurations)). If Γ; ∆ ` C1 and C1 −→ C2 then Γ; ∆ ` C2 .

3.3

Progress and canonical forms

While it is possible to prove deadlock-freedom in systems with more discerning type systems
based on linear logic [35, 48] or those using channel priorities [41], more liberal calculi such
as λch and λact allow deadlocked configurations. We thus define a form of progress which
does not preclude deadlock; to help with proving a progress result, it is useful to consider the
notion of a canonical form in order to allow us to reason about the configuration as a whole.
I Definition 5 (Canonical form (λch )). A configuration C is in canonical form if it can be
−
→
−
→
written (νa1 ) . . . (νan )(M1 k . . . k Mm k a1 (V1 ) k . . . k an (Vn )).
Well-typed open configurations can be written in a form similar to canonical form, but
without bindings for names already in the environment. An immediate corollary is that
well-typed closed configurations can always be written in a canonical form.
I Lemma 6. If Γ; ∆ ` C with ∆ = a1 : A1 , . . . , ak : Ak , then there exists a C 0 ≡ C such that
−
→
−
→
C 0 = (νak+1 ) . . . (νan )(M1 k . . . k Mm k a1 (V1 ) k . . . k an (Vn )).
I Corollary 7. If ·; · ` C, then there exists some C 0 ≡ C such that C 0 is in canonical form.

ECOOP 2017

90:10

Mixing Metaphors

Syntax
Types
Variables and names
Values
Computations

A, B, C ::= 1 | A →C B | ActorRef(A)
α ::= x | a
V, W ::= α | λx.M | ()
L, M, N ::= V W
| let x ⇐ M in N | return V
| spawn M | send V W | receive | self

Γ`V :A

Value typing rules
Abs

Var

Unit

Γ, x : A | C ` M : B

α:A∈Γ
Γ`α:A

C

Γ ` λx.M : A →

Γ ` () : 1

B

Γ|B`M :A

Computation typing rules
App

Γ ` V : A →C B
Γ`W :A
Γ|C`V W :B

EffLet

Γ|C`M :A
Γ, x : A | C ` N : B
Γ | C ` let x ⇐ M in N : B

Recv

Γ | A ` receive : A

Send
EffReturn

Γ`V :A
Γ | C ` return V : A

Spawn

Γ|A`M :1
Γ | C ` spawn M : ActorRef(A)

Γ`V :A
Γ ` W : ActorRef(A)
Γ | C ` send V W : 1

Self

Γ | A ` self : ActorRef(A)

Figure 8 Syntax and typing rules for λact

Armed with a canonical form, we can now state that the only situation in which a well-typed
closed configuration cannot reduce further is if all threads are either blocked or fully evaluated.
Let a leaf configuration be a configuration without subconfigurations, i.e., a term or a buffer.
I Theorem 8 (Weak progress (λch configurations)).
−
→
−
→
Let ·; · ` C, C 6−→, and let C 0 = (νa1 ) . . . (νan )(M1 k . . . k Mm k a1 (V1 ) k . . . an (Vn )) be a
canonical form of C. Then every leaf of C is either:
→
−
1. A buffer ai ( Vi );
2. A fully-reduced term of the form return V , or;
→
−
3. A term of the form E[take ai ], where Vi = .
Proof. By Lemma 2, we know each Mi is either of the form return V , or can be written
E[M 0 ] where M 0 is a communication or concurrency primitive. It cannot be the case that
M 0 = fork N or M 0 = newCh, since both can reduce. Let us now consider give and take,
blocked on a variable α. As we are considering closed configurations, a blocked term must
be blocked on a ν-bound name ai , and as per the canonical form, we have that there exists
→
−
some buffer ai ( Vi ). Consequently, give V ai can always reduce via Give. A term take ai can
−
→
→
−
→
−
reduce by Take if Vi = W · Vi0 ; the only remaining case is where Vi = , satisfying (3). J

4

λact : A concurrent λ-calculus for actors

In this section, we introduce λact , a core language describing actor-based concurrency. There
are many variations of actor-based languages (by the taxonomy of De Koster et al,̇ [11], λact
is process-based), but each have named processes associated with a mailbox.

Fowler, Lindley, and Wadler

90:11

Syntax of evaluation contexts and configurations
Evaluation contexts
Configurations
Configuration contexts

E ::= [ ] | let x ⇐ E in M
−
→
C, D, E ::= C k D | (νa)C | ha, M, V i
G ::= [ ] | G k C | (νa)G

Γ; ∆ ` C

Typing rules for configurations
Actor
Par

Γ; ∆1 ` C1 Γ; ∆2 ` C2
Γ; ∆1 , ∆2 ` C1 k C2

Pid

Γ, a : ActorRef(A); ∆, a : A ` C
Γ; ∆ ` (νa)C

Γ, a : ActorRef(A) | A ` M : 1
(Γ, a : ActorRef(A) ` Vi : A)i
−
→
Γ, a : ActorRef(A); a : A ` ha, M, V i

Figure 9 λact evaluation contexts and configurations

Typed channels are well-established, whereas typed actors are less so, partly due to the
type pollution problem. Nonetheless, Akka Typed [4] aims to replace untyped Akka actors,
so studying a typed actor calculus is of practical relevance.
Following Erlang, we provide an explicit receive operation to allow an actor to retrieve a
message from its mailbox: unlike take in λch , receive takes no arguments, so it is necessary
to use a simple type-and-effect system [18]. We treat mailboxes as a FIFO queues to keep
λact as minimal as possible, as opposed to considering behaviours or selective receive. This
is orthogonal to the core model of communication, as we show in §7.2.

4.1

Syntax and typing of terms

Figure 8 shows the syntax and typing rules for λact . As with λch , α ranges over variables and
names. ActorRef(A) is an actor reference or process ID, and allows messages to be sent to
an actor. As for communication and concurrency primitives, spawn M spawns a new actor to
evaluate a computation M ; send V W sends a value V to an actor referred to by reference W ;
receive receives a value from the actor’s mailbox; and self returns an actor’s own process ID.
Function arrows A →C B are annotated with a type C which denotes the type of the
mailbox of the actor evaluating the term. As an example, consider a function which receives
an integer and converts it to a string (assuming a function intToString):
recvAndShow , λ().let x ⇐ receive in intToString(x)
Such a function would have type 1 →Int String, and as an example would not be typeable
for an actor that could only receive booleans. Again, we work in the setting of fine-grain
call-by-value; the distinction between values and computations is helpful when reasoning
about the metatheory. We have two typing judgements: the standard judgement on values
Γ ` V : A, and a judgement Γ | B ` M : A which states that a term M has type A under
typing context Γ, and can receive values of type B. The typing of receive and self depends
on the type of the actor’s mailbox.

4.2

Operational semantics

Figure 9 shows the syntax of λact evaluation contexts, as well as the syntax and typing rules
of λact configurations. Evaluation contexts for terms and configurations are similar to λch .
→
−
The primary difference from λch is the actor configuration ha, M, V i, which can be read as
→
−
“an actor with name a evaluating term M , with a mailbox consisting of values V ”. Whereas
a term M is itself a configuration in λch , a term in λact must be evaluated as part of an

ECOOP 2017

90:12

Mixing Metaphors

Reduction on terms
(λx.M ) V −→M M {V /x}

let x ⇐ return V in M −→M M {V /x}

E[M ] −→M E[M 0 ]
(if M −→M M 0 )

Structural congruence
CkD≡DkC

C k (D k E) ≡ (C k D) k E

C k (νa)D ≡ (νa)(C k D) if a 6∈ fv(C)

G[C] ≡ G[D] if C ≡ D

Reduction on configurations
Spawn

−
→
ha, E[spawn M ], V i

−→

Send
SendSelf
Self
Receive
Lift
LiftM

−
→
−
→
ha, E[send V 0 b], V i k hb, M, W i
−
→
ha, E[send V 0 a], V i
−
→
ha, E[self], V i
−
→
ha, E[receive], W · V i
G[C1 ]
−
→
ha, M1 , V i

−→
−→
−→
−→
−→
−→

−
→
(νb)(ha, E[return b], V i k hb, M, i)
(b is fresh)
−
→
−
→
ha, E[return ()], V i k hb, M, W · V 0 i
−
→
ha, E[return ()], V · V 0 i
−
→
ha, E[return a], V i
−
→
ha, E[return W ], V i
G[C2 ]
(if C1 −→ C2 )
−
→
ha, M2 , V i
(if M1 −→M M2 )

Figure 10 Reduction on λact terms and configurations

actor configuration in order to support context-sensitive operations such as receiving from
the mailbox. We again stratify the reduction rules into functional reduction on terms, and
reduction on configurations. The typing rules for λact configurations ensure that all values
contained in an actor mailbox are well-typed with respect to the mailbox type, and that a
configuration C under a name restriction (νa)C contains an actor with name a. Figure 10
shows the reduction rules for λact . Again, reduction on terms preserves typing, and the
functional fragment of λact enjoys progress.
I Lemma 9 (Preservation (λact terms)). If Γ ` M : A and M −→M M 0 , then Γ ` M 0 : A.
I Lemma 10 (Progress (λact terms)). Assume Γ is either empty or only contains entries of
the form ai : ActorRef(Ai ). If Γ | B ` M : A, then either:
1. M = return V for some value V , or
2. M can be written as E[M 0 ], where M 0 is a communication or concurrency primitive (i.e.
spawn N , send V W , receive, or self), or
3. There exists some M 0 such that M −→M M 0 .
Reduction on configurations. While λch makes use of separate constructs to create new
processes and channels, λact uses a single construct spawn M to spawn a new actor with
an empty mailbox to evaluate term M . Communication happens directly between actors
instead of through an intermediate entity: as a result of evaluating send V a, the value V
will be appended directly to the end of the mailbox of actor a. SendSelf allows reflexive
sending; an alternative would be to decouple mailboxes from the definition of actors, but this
complicates both the configuration typing rules and the intuition. Self returns the name of
the current process, and Receive retrieves the head value of a non-empty mailbox.
As before, typing is preserved modulo structural congruence and under reduction.
I Lemma 11. If Γ; ∆ ` C and C ≡ D for some D, then Γ; ∆ ` D.

Fowler, Lindley, and Wadler

90:13

I Theorem 12 (Preservation (λact configurations)). If Γ; ∆ ` C1 and C1 −→ C2 , then Γ; ∆ ` C2 .

4.3

Progress and canonical forms

Again, we cannot guarantee deadlock-freedom for λact . Instead, we proceed by defining
a canonical form, and characterising the form of progress that λact enjoys. The technical
development follows that of λch .
I Definition 13 (Canonical form (λact )). A λact configuration C is in canonical form if C can
−
→
−
→
be written (νa1 ) . . . (νan )(ha1 , M1 , V1 i k . . . k han , Mn , Vn i).
I Lemma 14. If Γ; ∆ ` C and ∆ = a1 : A1 , . . . ak : Ak , then there exists C 0 ≡ C such that
−
→
−
→
C 0 = (νak+1 ) . . . (νan )(ha1 , M1 , V1 i k . . . k han , Mn , Vn i).
As before, it follows as a corollary of Lemma 14 that closed configurations can be written in
canonical form. We can therefore classify the notion of progress enjoyed by λact .
I Corollary 15. If ·; · ` C, then there exists some C 0 ≡ C such that C 0 is in canonical form.
I Theorem 16 (Weak progress (λact configurations)).
−
→
−
→
Let ·; · ` C, C 6−→, and let C 0 = (νa1 ) . . . (νan )(ha1 , M1 , V1 i k . . . k han , Mn , Vn i) be a
→
−
canonical form of C. Each actor with name ai is either of the form hai , return W, Vi i for some
value W , or hai , E[receive], i.

5

From λact to λch

With both calculi in place, we can define the translation from λact into λch . The key idea is to
emulate a mailbox using a channel, and to pass the channel as an argument to each function.
The translation on terms is parameterised over the channel name, which is used to implement
context-dependent operations (i.e., receive and self). Consider again recvAndShow.
recvAndShow , λ().let x ⇐ receive in intToString(x)
A possible configuration would be an actor evaluating recvAndShow (), with some name a
→
−
and mailbox with values V , under a name restriction for a.
→
−
(νa)(ha, recvAndShow (), V i)
The translation on terms takes a channel name ch as a parameter. As a result of the
translation, we have that:
J recvAndShow () K ch = let x ⇐ take ch in intToString(x)

→
−
with the corresponding configuration (νa)(a(J V K) k J recvAndShow () K a). The values from
the mailbox are translated pointwise and form the contents of a buffer with name a. The
translation of recvAndShow is provided with the name a which is used to emulate receive.

5.1

Translation (λact to λch )

Figure 11 shows the formal translation from λact into λch . Of particular note is the translation
on terms: J − K ch translates a λact term into a λch term using a channel with name ch
to emulate a mailbox. An actor reference is represented as a channel reference in λch ;
we emulate sending a message to another actor by writing to the channel emulating the

ECOOP 2017

90:14

Mixing Metaphors

Translation on types
J A →C B K = J A K → ChanRef(J C K) → J B K

J ActorRef(A) K = ChanRef(J A K)

J1K = 1

Translation on values
JxK = x

JaK = a

J λx.M K = λx.λch.(J M K ch)

J () K = ()

Translation on computation terms
J let x ⇐ M in N K ch = let x ⇐ (J M K ch) in J N K ch
J V W K ch
J return V K ch
J self K ch
J receive K ch

=
=
=
=

let f ⇐ (J V K J W K) in f ch
return J V K
return ch
take ch

J spawn M K ch

=

J send V W K ch

=

let chMb ⇐ newCh in
fork (J M K chMb);
return chMb
give (J V K) (J W K)

Translation on configurations
J C1 k C2 K = J C1 K k J C2 K

J (νa)C K = (νa) J C K

−
→
−
→
J ha, M, V i K = a(J V K) k (J M K a)

Figure 11 Translation from λact into λch

recipient’s mailbox. Key to translating λact into λch is the translation of function arrows
A →C B; the effect annotation C is replaced by a second parameter ChanRef(C), which is
used to emulate the mailbox of the actor. Values translate to themselves, with the exception
of λ abstractions, whose translation takes an additional parameter denoting the channel used
to emulate operations on a mailbox. Given parameter ch, the translation function for terms
emulates receive by taking a value from ch, and emulates self by returning ch.
Though the translation is straightforward, it is a global translation [12], as all functions
must be modified in order to take the mailbox channel as an additional parameter.

5.2

Properties of the translation

The translation on terms and values preserves typing. We extend the translation function
pointwise to typing environments: J α1 : A1 , . . . , αn : An K = α1 : J A1 K, . . . , αn : J An K.
I Lemma 17 (J − K preserves typing (terms and values)).

1. If Γ ` V : A in λact , then J Γ K ` J V K : J A K in λch .
2. If Γ | B ` M : A in λact , then J Γ K, α : ChanRef(J B K) ` J M K α : J A K in λch .

The proof is by simultaneous induction on the derivations of Γ ` V :A and Γ | B ` M :A.
To state a semantics preservation result, we also define a translation on configurations; the
translations on parallel composition and name restrictions are homomorphic. An actor
→
−
→
−
→
−
configuration ha, M, V i is translated as a buffer a(J V K), (writing J V K = J V0 K·, . . . , ·J Vn K
→
−
for each Vi ∈ V ), composed in parallel with the translation of M , using a as the mailbox
channel. We can now see that the translation preserves typeability of configurations.
I Theorem 18 (J − K preserves typeability (configurations)).
If Γ; ∆ ` C in λact , then J Γ K; J ∆ K ` J C K in λch .
We describe semantics preservation in terms of a simulation theorem: should a configuration C1 reduce to a configuration C2 in λact , then there exists some configuration D in λch
such that J C1 K reduces in zero or more steps to D, with D ≡ J C2 K. To establish the result,
we begin by showing that λact term reduction can be simulated in λch .

Fowler, Lindley, and Wadler

90:15

Syntax
Types
Values
Terms

A, B, C ::= . . . | A × B | A + B | List(A) | µX.A | X
V, W ::= . . . | rec f (x) . M | (V, W ) | inl V | inr W | roll V
L, M, N ::= . . . | let (x, y) = V in M | case V {inl x 7→ M ; inr y 7→ N } | unroll V

Γ`V :A

Additional value typing rules
Rec

Γ, x : A, f : A → B ` M : B
Γ ` rec f (x) . M : A → B

Pair

Γ`V :A Γ`W :B
Γ ` (V, W ) : A × B

Inl

Γ`V :A
Γ ` inl V : A + B

Roll

Γ ` V : A{µX.A/X}
Γ ` roll V : µX.A

Γ`M :A

Additional term typing rules
Let

Γ ` V : A × A0
Γ, x : A, y : A0 ` M : B
Γ ` let (x, y) = V in M : B

Case

Γ ` V : A + A0
Γ, x : A ` M : B Γ, y : A0 ` N : B
Γ ` case V {inl x 7→ M ; inr y 7→ N } : B

Unroll

Γ ` V : µX.A
Γ ` unroll V : A{µX.A/X}

M −→M M 0

Additional term reduction rules
(rec f (x) . M ) V −→M
let (x, y) = (V, W ) in M −→M
case (inl V ) {inl x 7→ M ; inr y 7→ N } −→M
unroll (roll V ) −→M

M {(rec f (x) . M )/f, V /x}
M {V /x, W/y}
M {V /x}
return V

Encoding of lists
List(A) , µX.1 + (A × X)
[ ] , roll (inl ())
V :: W , roll (inr (V, W ))
case V {[ ] 7→ M ; x :: y 7→ N } , let z ⇐ unroll V in case z {inl () 7→ M ; inr (x, y) 7→ N }
Figure 12 Extensions to core languages to allow translation from λch into λact

I Lemma 19 (Simulation of λact term reduction in λch ).
If Γ ` M1 : A and M1 −→M M2 in λact , then given some α, J M1 K α −→∗M J M2 K α in λch .
Finally, we can see that the translation preserves structural congruences, and that λch
configurations can simulate reductions in λact .
I Lemma 20. If Γ; ∆ ` C and C ≡ D, then J C K ≡ J D K.
I Theorem 21 (Simulation of λact configurations in λch ).
If Γ; ∆ ` C1 and C1 −→ C2 , then there exists some D such that J C1 K −→∗ D, with D ≡ J C2 K.

6

From λch to λact

The translation from λact into λch emulates an actor mailbox using a channel to implement
operations which normally rely on the context of the actor. Though global, the translation is
straightforward due to the limited form of communication supported by mailboxes. Translating from λch into λact is more challenging, as would be expected from Figure 2. Each
channel in a system may have a different type; each process may have access to multiple
channels; and (crucially) channels may be freely passed between processes.

6.1

Extensions to the core language

We require several more language constructs: sums, products, recursive functions, and
iso-recursive types. Recursive functions are used to implement an event loop, and recursive
types to maintain a term-level buffer. Products are used to record both a list of values in the

ECOOP 2017

90:16

Mixing Metaphors

d

b

e

b
a

a
a

c

(a) Before Translation

(b) After Translation

Figure 13 Translation strategy: λch into λact

buffer and a list of pending requests. Sum types allow the disambiguation of the two types
of messages sent to an actor: one to queue a value (emulating give) and one to dequeue a
value (emulating take). Sums are also used to encode monomorphic variant types; we write
h`1 : A1 , . . . , `n : An i for variant types and h`i = V i for variant values.
Figure 12 shows the extensions to the core term language and their reduction rules;
we omit the symmetric rules for inr. With products, sums, and recursive types, we can
encode lists. The typing rules are shown for λch but can be easily adapted for λact , and it is
straightforward to verify that the extended languages still enjoy progress and preservation.

6.2

Translation strategy (λch into λact )

To translate typed actors into typed channels (shown in Figure 13), we emulate each channel
using an actor process, which is crucial in retaining the mobility of channel endpoints.
Channel types describe the typing of a communication medium between communicating
processes, where processes are unaware of the identity of other communicating parties, and
the types of messages that another party may receive. Unfortunately, the same does not hold
for mailboxes. Consequently, we require that before translating into actors, every channel has
the same type. Although this may seem restrictive, it is both possible and safe to transform
a λch program with multiple channel types into a λch program with a single channel type.
As an example, suppose we have a program which contains channels carrying values
of types Int, String, and ChanRef(String). It is possible to construct a recursive variant
type µX.h`1 : Int, `2 : String, `3 : ChanRef(X)i which can be assigned to all channels in the
system. Then, supposing we wanted to send a 5 along a channel which previously had type
ChanRef(Int), we would instead send a value roll h`1 = 5i (where roll V is the introduction
rule for an iso-recursive type). Appendix A [15] provides more details.

6.3

Translation

We write λch judgements of the form {B} Γ ` M : A for a term where all channels have type
B, and similarly for value and configuration typing judgements. Under such a judgement,
we can write Chan instead of ChanRef(B).
Meta level definitions. The majority of the translation lies within the translation of newCh,
which makes use of the meta-level definitions body and drain. The body function emulates
a channel. Firstly, the actor receives a message recvVal, which is either of the form inl V to
store a message V , or inr W to request that a value is dequeued and sent to the actor with

Fowler, Lindley, and Wadler

90:17

Translation on types (wrt. a channel type C)
L A → B M = L A M →L C M L B M

L Chan M = ActorRef(L C M + ActorRef(L C M))

Translation on communication and concurrency primitives
L fork M M
L give V W M
L newCh M

=
=
=

let x ⇐ spawn L M M in return ()
send (inl L V M) L W M
spawn (body ([ ], [ ]))

L take V M

=

let selfPid ⇐ self in
send (inr selfPid) L V M;
receive

Translation on configurations
L C1 k C2 M = L C1 M k L C2 M
−
→
L a( V ) M

=

L (νa)C M = (νa)L C M

−
→
ha, body (L V M, [ ]), i

Meta level definitions

L M M = (νa)(ha, L M M, i)
a is a fresh name
−
→
where L V M = L V0 M :: . . . :: L Vn M :: [ ]

body , rec g(state) .
let recvVal ⇐ receive in
let (vals, pids) = state in
case recvVal {
inl v 7→ let vals0 ⇐ vals ++ [v] in
let state0 ⇐ drain (vals0 , pids) in
g (state0 )
inr pid 7→ let pids0 ⇐ pids ++ [pid] in
let state0 ⇐ drain (vals, pids0 ) in
g (state0 ) }

drain , λx.
let (vals, pids) = x in
case vals {
[ ] 7→ return (vals, pids)
v :: vs 7→
case pids {
[ ] 7→ return (vals, pids)
pid :: pids 7→ send v pid;
return (vs, pids)
} }

Figure 14 Translation from λch into λact

ID W . We assume a standard implementation of list concatenation (+
+ ). If the message is
inl V , then V is appended to the tail of the list of values stored in the channel, and the new
state is passed as an argument to drain. If the message is inr W , then the process ID W is
appended to the end of the list of processes waiting for a value. The drain function satisfies
all requests that can be satisfied, returning an updated channel state. Note that drain does
not need to be recursive, since one of the lists will either be empty or a singleton.
Translation on types. Figure 14 shows the translation from λch into λact . The translation
function on types L − M is defined with respect to the type of all channels C and is used
to annotate function arrows and to assign a parameter to ActorRef types. The (omitted)
translations on sums, products, and lists are homomorphic. The translation of Chan is
ActorRef(L C M + ActorRef(L C M)), meaning an actor which can receive a request to either store
a value of type L C M, or to dequeue a value and send it to a process ID of type ActorRef(L C M).
Translation on communication and concurrency primitives. We omit the translation on
values and functional terms, which are homomorphisms. Processes in λch are anonymous,
whereas all actors in λact are addressable; to emulate fork, we therefore discard the reference
returned by spawn. The translation of give wraps the translated value to be sent in the left
injection of a sum type, and sends to the translated channel name L W M. To emulate take,
the process ID (retrieved using self) is wrapped in the right injection and sent to the actor
emulating the channel, and the actor waits for the response message. Finally, the translation
of newCh spawns a new actor to execute body.

ECOOP 2017

90:18

Mixing Metaphors

Translation on configurations. The translation function L − M is homomorphic on parallel
composition and name restriction. Unlike λch , a term cannot exist outwith an enclosing actor
context in λact , so the translation of a process evaluating term M is an actor evaluating L M M
with some fresh name a and an empty mailbox, enclosed in a name restriction. A buffer is
translated to an actor with an empty mailbox, evaluating body with a state containing the
(term-level) list of values previously stored in the buffer.
Although the translation from λch into λact , is much more verbose than the translation
from λact to λch , it is (once all channels have the same type) a local transformation [12].

6.4

Properties of the translation

Since all channels in the source language of the translation have the same type, we can
assume that each entry in the codomain of ∆ is the same type B.
I Definition 22 (Translation of typing environments wrt. a channel type B).
1. If Γ = α1 :A1 , . . . , αn : An , define L Γ M = α1 : L A1 M, . . . , αn : L An M.
2. Given a ∆ = a1 : B, . . . , an : B, define L ∆ M =
a1 : (L B M + ActorRef(L B M)), . . . , an : (L B M + ActorRef(L B M)).
The translation on terms preserves typing.
I Lemma 23 (L − M preserves typing (terms and values)).
1. If {B} Γ ` V :A, then L Γ M ` L V M:L A M.
2. If {B} Γ ` M :A, then L Γ M | L B M ` L M M:L A M.

The translation on configurations also preserves typeability. We write Γ  ∆ if for each
a : A ∈ ∆, we have that a : ChanRef(A) ∈ Γ; for closed configurations this is ensured by
Chan. This is necessary since the typing rules for λact require that the local actor name is
present in the term environment to ensure preservation in the presence of self, but there is
no such restriction in λch .
I Theorem 24 (L − M preserves typeability (configurations)).
If {A} Γ; ∆ ` C with Γ  ∆, then L Γ M; L ∆ M ` L C M.
It is clear that reduction on translated λch terms can simulate reduction in λact .
I Lemma 25. If {B} Γ ` M1 : A and M1 −→M M2 , then L M1 M −→M L M2 M.
Finally, we show that λact can simulate λch .
I Lemma 26. If Γ; ∆ ` C and C ≡ D, then L C M ≡ L D M.
I Theorem 27 (Simulation (λact configurations in λch )).
If {A} Γ; ∆ ` C1 , and C1 −→ C2 , then there exists some D such that L C1 M −→∗ D with
D ≡ L C2 M.
Remark. The translation from λch into λact is more involved than the translation from λact
into λch due to the asymmetry shown in Figure 2. Mailbox types are less precise; generally
taking the form of a large variant type.
Typical implementations of this translation use synchronisation mechanisms such as
futures or shared memory (see §7.1); the implementation shown in the Hopac documentation
uses ML references [1]. Given the ubiquity of these abstractions, we were surprised to discover

Fowler, Lindley, and Wadler

90:19

Additional types, terms, configuration reduction rule, and equivalence
Types ::= ActorRef(A, B) | . . .

Terms ::= wait V | . . .

−
→
−
→
−
→
−
→
ha, E[wait b], V i k hb, return V 0 , W i −→ ha, E[return V 0 ], V i k hb, return V 0 , W i
−
→
(νa)(ha, return V, V i) k C ≡ C

Γ | A, B ` M : A

Modified typing rules for terms
Sync-Spawn

Γ | A, B ` M : B
0
Γ | C, C ` spawn M : ActorRef(A, B)

Sync-Wait

Γ ` V : ActorRef(A, B)
Γ | C, C 0 ` wait V : B

Sync-Self

Γ | A, B ` self : ActorRef(A, B)

Γ; ∆ ` C

Modified typing rules for configurations
Sync-Actor

Γ, a:ActorRef(A, B) ` M :B
(Γ, a:ActorRef(A, B) ` Vi :A)i

Sync-Nu

Γ, a : ActorRef(A, B); ∆, a : (A, B) ` C
Γ; ∆ ` (νa)C

−
→
Γ, a : ActorRef(A, B); a:(A, B) ` ha, M, V i

Modified translation
L ChanRef(A) M =
ActorRef(L A M + ActorRef(L A M, L A M), 1)
L A → B M = L A M →C,1 L B M

L take V M = let requestorPid ⇐ spawn (
let selfPid ⇐ self in
send (inr selfPid) L V M;
receive) in
wait requestorPid

Figure 15 Extensions to add synchronisation to λact

that the additional expressive power of synchronisation is not necessary. Our original attempt
at a synchronisation-free translation was type-directed. We were surprised to discover that
the translation can be described so succinctly after factoring out the coalescing step, which
precisely captures the type pollution problem.

7

Extensions

In this section, we discuss common extensions to channel- and actor-based languages. Firstly,
we discuss synchronisation, which is ubiquitous in practical implementations of actor-inspired
languages. Adding synchronisation simplifies the translation from channels to actors, and
relaxes the restriction that all channels must have the same type. Secondly, we consider an
extension with Erlang-style selective receive, and show how to encode it in λact . Thirdly, we
discuss how to nondeterministically choose a message from a collection of possible sources,
and finally, we discuss what the translations tell us about the nature of behavioural typing
disciplines for actors. Establishing exactly how the latter two extensions fit into our framework
is the subject of ongoing and future work.

7.1

Synchronisation

Although communicating with an actor via asynchronous message passing suffices for many
purposes, implementing “call-response” style interactions can become cumbersome. Practical
implementations such as Erlang and Akka implement some way of synchronising on a result:
Erlang achieves this by generating a unique reference to send along with a request, selectively
receiving from the mailbox to await a response tagged with the same unique reference.

ECOOP 2017

90:20

Mixing Metaphors

Another method of synchronisation embraced by the Active Object community [10, 32, 33]
and Akka is to generate a future variable which is populated with the result of the call.
Figure 15 details an extension of λact with a synchronisation primitive, wait, which encodes
a deliberately restrictive form of synchronisation capable of emulating futures. The key idea
behind wait is it allows some actor a to block until an actor b evaluates to a value; this value
is then returned directly to a, bypassing the mailbox. A variation of the wait primitive is
implemented as part of the Links [9] concurrency model. This is but one of multiple ways of
allowing synchronisation; first-class futures, shared reference cells, or selective receive can
achieve a similar result. We discuss wait as it avoids the need for new configurations.
We replace the unary type constructor for process IDs with a binary type constructor
ActorRef(A, B), where A is the type of messages that the process can receive from its mailbox,
and B is the type of value to which the process will eventually evaluate. We assume that
the remainder of the primitives are modified to take the additional effect type into account.
We can now adapt the previous translation from λch to λact , making use of wait to avoid
the need for the coalescing transformation. Channel references are translated into actor
references which can either receive a value of type A, or the PID of a process which can
receive a value of type A and will eventually evaluate to a value of type A. Note that the
unbound annotation C, 1 on function arrows reflects that the mailboxes can be of any type,
since the mailboxes are unused in the actors emulating threads.
The key idea behind the modified translation is to spawn a fresh actor which makes the
request to the channel and blocks waiting for the response. Once the spawned actor has
received the result, the result can be retrieved synchronously using wait without reading from
the mailbox. The previous soundness theorems adapt to the new setting.
I Theorem 28. If Γ; ∆ ` C with Γ  ∆, then L Γ M; L ∆ M ` L C M.
I Theorem 29. If Γ; ∆ ` C1 and C1 −→ C2 , then there exists some D such that L C M −→∗ D
with D ≡ L C2 M.
The translation in the other direction requires named threads and a join construct in λch .

7.2

Selective receive

The receive construct in λact can only read the first message in the queue, which is cumbersome
as it often only makes sense for an actor to handle a subset of messages at a given time.
In practice, Erlang provides a selective receive construct, matching messages in the mailbox
against multiple pattern clauses. Assume we have a mailbox containing values V1 , . . . Vn
and evaluate receive {c1 , . . . , cm }. The construct first tries to match value V1 against clause
c1 —if it matches, then the body of c1 is evaluated, whereas if it fails, V1 is tested against c2
and so on. Should V1 not match any pattern, then the process is repeated until Vn has been
tested against cm . At this point, the process blocks until a matching message arrives.
More concretely, consider an actor with mailbox type C = hPriorityMessage : Message,
StandardMessage : Message, Timeout : 1i which can receive both high- and low-priority messages. Let getPriority be a function which extracts a priority from a message.

Fowler, Lindley, and Wadler

90:21

Additional syntax
Receive Patterns
Computations

c
M

::=
::=

(h` = xi when M ) 7→ N
→
receive {−
c } | ...

Additional term typing rule
Sel-Recv

−
→
c = {h`i = xi i when Mi 7→ Ni }i i ∈ J
Γ, xi : Ai `P Mi : Bool Γ, xi : Ai | h`j : Aj ij∈J ` Ni : C
→
Γ | h`j : Aj ij∈J ` receive {−
c}:C

Additional configuration reduction rule
→
∃k, l.∀i.i < k ⇒ ¬(matchesAny(−
c , Vi )) ∧ matches(cl , Vk ) ∧ ∀j.j < l ⇒ ¬(matches(cj , Vk ))
−→
−
→
−
→ −→
−
→
ha, E[receive { c }], W · V · W 0 i −→ ha, E[N {V 0 /x }], W · W 0 i
k

l

k

l

where
−
→
c = {h`i = xi i when Mi 7→ Ni }i

−
→
W = V1 · . . . · Vk−1

−→0
W = Vk+1 · . . . · Vn

Vk = h`k = Vk0 i

matches((h` = xi when M ) 7→ N, h`0 = V i) , (` = `0 ) ∧ (M {V /x} −→∗M return true)
→
→
matchesAny(−
c , V ) , ∃c ∈ −
c .matches(c, V )
Figure 16 Additional syntax, typing rules, and reduction rules for λact with selective receive

Now consider the following actor:
receive {
hPriorityMessage = msgi when (getPriority msg) > 5 7→ handleMessage msg
hTimeout = msgi
when true
7→ ()
};
receive {
hPriorityMessage = msgi when true 7→ handleMessage msg
hStandardMessage = msgi when true 7→ handleMessage msg
hTimeout = msgi
when true 7→ ()
}

This actor begins by handling a message only if it has a priority greater than 5. After the
timeout message is received, however, it will handle any message—including lower-priority
messages that were received beforehand.
Figure 16 shows the additional syntax, typing rule, and configuration reduction rule
required to encode selective receive; the type Bool and logical operators are encoded using
sums in the standard way. We write Γ `P M : A to mean that under context Γ, a term M
which does not perform any communication or concurrency actions has type A. Intuitively,
this means that no subterm of M is a communication or concurrency construct.
−c } construct models an ordered sequence of receive pattern clauses c of the
The receive {→
form (h` = xi when M ) 7→ N , which can be read as “If a message with body x has label `
−c } ensures that for
and satisfies predicate M , then evaluate N ”. The typing rule for receive {→
→
−
each pattern h`i = xi i when Mi 7→ Ni in c , we have that there exists some `i : Ai contained
in the mailbox variant type; and when Γ is extended with xi : Ai , that the guard Mi has
type Bool and the body Ni has the same type C for each branch.
The reduction rule for selective receive is inspired by that of Fredlund [16]. Assume that
−→
−
→
the mailbox is of the form V1 · . . . · Vk · . . . Vn , with W = V1 · . . . · Vk−1 and W 0 = Vk+1 · . . . · Vn .

ECOOP 2017

90:22

Mixing Metaphors

Translation on types
bActorRef(h`i : Ai ii )c = ActorRef(h`i : bAi cii )

bA × Bc = bAc × bBc

bA + Bc = bAc + bBc

bA →C Bc = bAc →bCc List(bCc) →bCc (bBc × List(bCc))

bµX.Ac = µX.bAc

where C = h`i : A0i ii , and bCc = h`i : bA0i cii

Translation on values
bλx.M c = λx.λmb.(bM c mb)

brec f (x) . M c = rec f (x) . λmb.(bM c mb)

Translation on computation terms (wrt. a mailbox type h`i : Ai ii )
bV W c mb
breturn V c mb
blet x ⇐ M in N c mb
bselfc mb
bsend V W c mb
bspawn M c mb
→
breceive {−
c }c mb

=
=
=
=
=
=
=

let f ⇐ (bV c bW c) in f mb
return (bV c, mb)
let resPair ⇐ bM c mb in let (x, mb0 ) = resPair in bN c mb0
let selfPid ⇐ self in return (selfPid, mb)
let x ⇐ send (bV c) (bW c) in return (x, mb)
let spawnRes ⇐ spawn(bM c[ ]) in return (spawnRes, mb)
→
find(−
c , mb)

Translation on configurations
b(νa)Cc
bC1 k C2 c
−
→
bha, M, V ic

=
=
=

{(νa)D | D ∈ bCc}
{D1 k D2 | D1 ∈ bC1 c ∧ D2 ∈ bC2 c}
−
→
{ha, bM c [ ], b V c i} ∪
−→ −→
{ha, (bM c Wi1 ), Wi2 i | i ∈ 1..n}

where
−→1
Wi = bV1 c :: . . . :: bVi c :: [ ]
−→2
Wi = bVi+1 c · . . . · bVn c

Figure 17 Translation from λact with selective receive into λact

The matches(c, V ) predicate holds if the label matches, and the branch guard evaluates to
−c , V ) predicate holds if V matches any pattern in →
−c . The key idea
true. The matchesAny(→
is that Vk is the first value to satisfy a pattern. The construct evaluates to the body of the
matched pattern, with the message payload Vk0 substituted for the pattern variable xk ; the
−
→ −→
final mailbox is W · W 0 (that is, the original mailbox without Vk ).
Reduction in the presence of selective receive preserves typing.
I Theorem 30 (Preservation (λact configurations with selective receive)). If Γ; ∆ | h`i : Ai ii ` C1
and C1 −→ C2 , then Γ; ∆ | h`i : Ai ii ` C2 .
Translation to λact . Given the additional constructs used to translate λch into λact , it is
possible to translate λact with selective receive into plain λact . Key to the translation is
reasoning about values in the mailbox at the term level; we maintain a term-level ‘save queue’
of values that have been received but not yet matched, and can loop through the list to find
the first matching value. Our translation is similar in spirit to the “stashing” mechanism
described by Haller [19] to emulate selective receive in Akka, where messages can be moved
to an auxiliary queue for processing at a later time.
Figure 17 shows the translation formally. Except for function types, the translation on
types is homomorphic. Similar to the translation from λact into λch , we add an additional
parameter for the save queue.
The translation on terms bM c mb takes a variable mb representing the save queue as its
parameter, returning a pair of the resulting term and the updated save queue. The majority of
−c }, which relies on the meta-level definition find(→
−c ,
cases are standard, except for receive {→
→
−
mb): c is a sequence of clauses, and mb is the save queue. The constituent findLoop function
takes a pair of lists (mb1 , mb2 ), where mb1 is the list of processed values found not to match,

Fowler, Lindley, and Wadler

→
find(−
c , mb) ,
(rec findLoop(ms) .
let (mb1 , mb2 ) = ms in
case mb2 {
→
[ ] 7→ loop(−
c , mb1 )
x :: mb02 7→
let mb0 ⇐ mb1 ++ mb02 in
→
case x {branches(−
c , mb0 ,
0
λy.(let mb1 ⇐ mb1 ++ [y] in
findLoop (mb01 , mb02 )))}) ([ ], mb)

90:23

ifPats(mb, `, y, , default) = default h` = yi
ifPats(mb, `, y,
(h` = xi when M 7→ N ) · pats, default) =
let resPair ⇐ (bM c mb){y/x} in
let (res, mb0 ) = resPair in
if res then (bN cmb){y/x}
else ifPats(mb, `, y, pats, default)
→
loop(−
c , mb) ,
(rec recvLoop(mb) .
let x ⇐ receive in
→
case x {branches(−
c , mb,
0
λy. let mb ⇐ mb ++ [y] in
recvLoop mb0 )}) mb

label(h` = xi when M 7→ N ) = `
→
→
labels(−
c ) = noDups([label(c) | c ← −
c ])
−
→
−
→
matching(`, c ) = [c | (c ← c ) ∧ label(c) = `]
→
→
unhandled(−
c ) = [` | (h` : Ai ← h`i : Ai ii ) ∧ ` 6∈ labels(−
c )]

→
→
→
branches(−
c , mb, default) = patBranches(−
c , mb, default) · defaultBranches(−
c , mb, default)
−
→
patBranches( c , mb, default) =
→
→
→
→
[h` = xi 7→ ifPats(mb, `, x, −
c` , default) | (` ← labels(−
c )) ∧ −
c` = matching(`, −
c ) ∧ x fresh]
→
→
defaultBranches(−
c , mb, default) = [h` = xi 7→ default h` = xi | (` ← unhandled(−
c )) ∧ x fresh]

Figure 18 Meta level definitions for translation from λact with selective receive to λact (wrt. a
mailbox type h`i : Ai ii )

and mb2 is the list of values still to be processed. The loop inspects the list until one either
matches, or the end of the list is reached. Should no values in the term-level representation
of the mailbox match, then the loop function repeatedly receives from the mailbox, testing
each new message against the patterns.
Note that the case construct in the core λact calculus is more restrictive than selective
receive: given a variant h`i : Ai ii , case requires a single branch for each label. Selective
receive allows multiple branches for each label, each containing a possibly-different predicate,
and does not require pattern matching to be exhaustive.
We therefore need to perform pattern matching elaboration; this is achieved by the
branches meta level definition. We make use of list comprehension notation: for example,
−c ) ∧ label(c) = `] returns the (ordered) list of clauses in a sequence →
−c such that
[c | (c ← →
the label of the receive clause matches a label `. We assume a meta level function noDups
which removes duplicates from a list. Case branches are computed using the branches meta
level definition: patBranches creates a branch for each label present in the selective receive,
creating (via ifPats) a sequence of if-then-else statements to check each predicate in turn;
defaultBranches creates a branch for each label that is present in the mailbox type but
not in any selective receive clauses.
Properties of the translation. The translation preserves typing of terms and values.
I Lemma 31 (Translation preserves typing (values and terms)).
1. If Γ ` V : A, then bΓc ` bV c : bAc.
2. If Γ | h`i : Ai ii ` M : B, then
bΓc, mb : List(h`i : bAi cii ) | h`i : bAi cii ` bM cmb : (bBc × List(h`i : bAi cii )).
Alas, a direct one-to-one translation on configurations is not possible, since a message in a
mailbox in the source language could be either in the mailbox or the save queue in the target

ECOOP 2017

90:24

Mixing Metaphors

Γ ` V : ChanRef(A) Γ ` W : ChanRef(B)
Γ ` choose V W : A + B

−
→
−
→
E[choose a b] k a(W1 · V1 ) k b(V2 )
−
→
−
→
E[choose a b] k a(V1 ) k b(W2 · V2 )

−→
−→

−
→
−
→
E[return (inl W1 )] k a(V1 ) k b(V2 )
−
→
−
→
E[return (inr W2 )] k a(V1 ) k b(V2 )

Figure 19 Additional typing and evaluation rules for λch with choice

language. Consequently, we translate a configuration into a set of possible configurations,
depending on how many messages have been processed. We can show that all configurations
in the resulting set are type-correct, and can simulate the original reduction.
I Theorem 32 (Translation preserves typing). If Γ; ∆ ` C, then ∀D ∈ bCc, it is the case that
bΓc; b∆c ` D.
I Theorem 33 (Simulation (λact with selective receive in λact )). If Γ; ∆ ` C and C −→ C 0 ,
then ∀D ∈ bCc, there exists a D0 such that D −→+ D0 and D0 ∈ bC 0 c.
Remark. Originally we expected to need to add an analogous selective receive construct to
λch in order to be able to translate λact with selective receive into λch . We were surprised (in
part due to the complex reduction rule and the native runtime support in Erlang) when we
discovered that selective receive can be emulated in plain λact . Moreover, we were pleasantly
surprised that types pose no difficulties in the translation.

7.3

Choice

The calculus λch supports only blocking receive on a single channel. A more powerful
mechanism is selective communication, where a value is taken nondeterministically from two
channels. An important use case is receiving a value when either channel could be empty.
Here we have considered only the most basic form of selective choice over two channels.
More generally, it may be extended to arbitrary regular data types [42]. As Concurrent
ML [45] embraces rendezvous-based synchronous communication, it provides generalised
selective communication where a process can synchronise on a mixture of input or output
communication events. Similarly, the join patterns of the join calculus [14] provide a general
abstraction for selective communication over multiple channels.
As we are working in the asynchronous setting where a give operation can reduce
immediately, we consider only input-guarded choice. Input-guarded choice can be added
straightforwardly to λch , as shown in Figure 19. Emulating such a construct satisfactorily in
λact is nontrivial, because messages must be multiplexed through a local queue. One approach
could be to use the work of Chaudhuri [8] which shows how to implement generalised choice
using synchronous message passing, but implementing this in λch may be difficult due to the
asynchrony of give. We leave a more thorough investigation to future work.

7.4

Behavioural types

Behavioural types allow the type of an object (e.g. a channel) to evolve as a program
executes. A widely studied behavioural typing discipline is that of session types [26, 27],
which are channel types sufficiently expressive to describe communication protocols between
participants. For example, the session type for a channel which sends two integers and

Fowler, Lindley, and Wadler

90:25

receives their sum could be defined as !Int.!Int.?Int.end. Session types are suited to channels,
whereas current work on session-typed actors concentrates on runtime monitoring [39].
A natural question to ask is whether one can combine the benefits of actors and of session
types—indeed, this was one of our original motivations for wanting to better understand
the relationship between actors and channels in the first place! A session-typed channel
may support both sending and receiving (at different points in the protocol it encodes), but
communication with another process’ mailbox is one-way. We have studied several variants
of λact with polarised session types [36, 43] which capture such one-way communication, but
they seem too weak to simulate session-typed channels. In future, we would like to find an
extension of λact with behavioural types that admits a similar simulation result to the ones
in this paper.

8

Related work

Our formulation of concurrent λ-calculi is inspired by λ(fut) [40], a concurrent λ-calculus
with threads, futures, reference cells, and an atomic exchange construct. In the presence
of lists, futures are sufficient to encode asynchronous channels. In λch , we concentrate on
asynchronous channels to better understand the correspondence with actors. Channel-based
concurrent λ-calculi form the basis of functional languages with session types [17, 35].
Concurrent ML [45] extends Standard ML with a rich set of combinators for synchronous
channels, which again can emulate asynchronous channels. A core notion in Concurrent ML
is nondeterministically synchronising on multiple synchronous events, such as sending or
receiving messages; relating such a construct to an actor calculus is nontrivial, and remains
an open problem. Hopac [28] is a channel-based concurrency library for F#, based on
Concurrent ML. The Hopac documentation relates synchronous channels and actors [1],
implementing actor-style primitives using channels, and channel-style primitives using actors.
The implementation of channels using actors uses mutable references to emulate the take
function, whereas our translation achieves this using message passing. Additionally, our
translation is formalised and we prove that the translations are type- and semantics-preserving.
Links [9] provides actor-style concurrency, and the paper describes a translation into
λ(fut). Our translation is semantics-preserving and can be done without synchronisation.
The actor model was designed by Hewitt [23] and examined in the context of distributed
systems by Agha [2]. Agha et al. [3] describe a functional actor calculus based on the
λ-calculus augmented by three core constructs: send sends a message; letactor creates a new
actor; and become changes an actor’s behaviour. The operational semantics is defined in
terms of a global actor mapping, a global multiset of messages, a set of receptionists (actors
which are externally visible to other configurations), and a set of external actor names.
Instead of become, we use an explicit receive construct, which more closely resembles Erlang
(referred to by the authors as “essentially an actor language”). Our concurrent semantics,
more in the spirit of process calculi, encodes visibility via name restrictions and structural
congruences. The authors consider a behavioural theory in terms of operational and testing
equivalences—something we have not investigated.
Scala has native support for actor-style concurrency, implemented efficiently without
explicit virtual machine support [20]. The actor model inspires active objects [33]: objects
supporting asynchronous method calls which return responses using futures. De Boer et
al. [10] describe a language for active objects with cooperatively scheduled threads within
each object. Core ABS [32] is a specification language based on active objects. Using futures
for synchronisation sidesteps the type pollution problem inherent in call-response patterns

ECOOP 2017

90:26

Mixing Metaphors

with actors, although our translations work in the absence of synchronisation. By working in
the functional setting, we obtain more compact calculi.

9

Conclusion

Inspired by languages such as Go which take channels as core constructs for communication,
and languages such as Erlang which are based on the actor model of concurrency, we have
presented translations back and forth between a concurrent λ-calculus λch with channel-based
communication constructs and a concurrent λ-calculus λact with actor-based communication
constructs. We have proved that λact can simulate λch and vice-versa.
The translation from λact to λch is straightforward, whereas the translation from λch to
λact requires considerably more effort. Returning to Figure 2, this is unsurprising!
We have also shown how to extend λact with synchronisation, greatly simplifying the
translation from λch into λact , and have shown how Erlang-style selective receive can be
emulated in λact . Additionally, we have discussed input-guarded choice in λch , and how
behavioural types may fit in with λact .
In future, we firstly plan to strengthen our operational correspondence results by considering operational completeness. Secondly, we plan to investigate how to emulate λch with
input-guarded choice in λact . Finally, we intend to use the lessons learnt from studying λch
and λact to inform the design of an actor-inspired language with behavioural types.

Acknowledgements
This work was supported by EPSRC grants EP/L01503X/1 (University of Edinburgh CDT
in Pervasive Parallelism) and EP/K034413/1 (A Basis for Concurrency and Distribution).
Thanks to Philipp Haller, Daniel Hillerström, Ian Stark, and the anonymous reviewers for
detailed comments.

1
2
3
4
5
6
7
8
9

References
Actors and Hopac. https://www.github.com/Hopac/Hopac/blob/master/Docs/Actors.
md, 2016.
Gul Agha. Actors: A Model of Concurrent Computation in Distributed Systems. MIT
Press, Cambridge, MA, USA, 1986.
Gul A Agha, Ian A Mason, Scott F Smith, and Carolyn L Talcott. A foundation for actor
computation. Journal of Functional Programming, 7(01):1–72, 1997.
Akka Typed. http://doc.akka.io/docs/akka/current/scala/typed.html, 2016.
Elvira Albert, Puri Arenas, and Miguel Gómez-Zamalloa. Testing of concurrent and imperative software using clp. In PPDP, pages 1–8. ACM, 2016.
Joe Armstrong. Making reliable distributed systems in the presence of sodware errors. PhD
thesis, The Royal Institute of Technology Stockholm, Sweden, 2003.
Francesco Cesarini and Steve Vinoski. Designing for Scalability with Erlang/OTP. "
O’Reilly Media, Inc.", 2016.
Avik Chaudhuri. A Concurrent ML Library in Concurrent Haskell. In ICFP, pages 269–280,
New York, NY, USA, 2009. ACM.
Ezra Cooper, Sam Lindley, Philip Wadler, and Jeremy Yallop. Links: Web Programming
Without Tiers. In Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf, and WillemPaul de Roever, editors, FMCO, volume 4709, pages 266–296. Springer Berlin Heidelberg,
2007.

Fowler, Lindley, and Wadler

90:27

10

Frank S De Boer, Dave Clarke, and Einar Broch Johnsen. A complete guide to the future.
In ESOP, pages 316–330. Springer, 2007.

11

Joeri De Koster, Tom Van Cutsem, and Wolfgang De Meuter. 43 Years of Actors: A
Taxonomy of Actor Models and Their Key Properties. In AGERE. ACM, 2016.

12

Matthias Felleisen. On the expressive power of programming languages. Science of Computer Programming, 17(1-3):35–75, 1991.

13

Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. The essence of
compiling with continuations. In PLDI, pages 237–247. ACM, 1993.

14

Cédric Fournet and Georges Gonthier. The reflexive CHAM and the join-calculus. In
Hans-Juergen Boehm and Guy L. Steele Jr., editors, POPL, pages 372–385. ACM Press,
1996.

15

Simon Fowler, Sam Lindley, and Philip Wadler. Mixing Metaphors: Actors as Channels
and Channels as Actors (Extended Version). CoRR, abs/1611.06276, 2017. URL: http:
//arxiv.org/abs/1611.06276.

16

Lars-Åke Fredlund. A framework for reasoning about Erlang code. PhD thesis, The Royal
Institute of Technology Stockholm, Sweden, 2001.

17

Simon J. Gay and Vasco T. Vasconcelos. Linear type theory for asynchronous session types.
Journal of Functional Programming, 20:19–50, January 2010.

18

David K. Gifford and John M. Lucassen. Integrating functional and imperative programming. In LFP, pages 28–38. ACM, 1986.

19

Philipp Haller. On the integration of the actor model in mainstream technologies: the
Scala perspective. In AGERE, pages 1–6. ACM, 2012.

20

Philipp Haller and Martin Odersky. Scala actors: Unifying thread-based and event-based
programming. Theoretical Computer Science, 410(2):202–220, 2009.

21

Paul Harvey. A linguistic approach to concurrent, distributed, and adaptive programming
across heterogeneous platforms. PhD thesis, University of Glasgow, 2015.

22

Jiansen He, Philip Wadler, and Philip Trinder. Typecasting actors: From Akka to TAkka.
In SCALA, pages 23–33. ACM, 2014.

23

Carl Hewitt, Peter Bishop, and Richard Steiger. A Universal Modular ACTOR Formalism
for Artificial Intelligence. In IJCAI, pages 235–245, San Francisco, CA, USA, 1973. Morgan
Kaufmann Publishers Inc.

24

Rich Hickey. Clojure core.async Channels.
clojure-core-async-channels.html, 2013.

25

C. A. R. Hoare. Communicating Sequential Processes. Communications of the ACM,
21(8):666–677, August 1978.

26

Kohei Honda. Types for dyadic interaction. In Eike Best, editor, CONCUR’93, volume 715
of Lecture Notes in Computer Science, pages 509–523. Springer Berlin Heidelberg, 1993.

27

Kohei Honda, Vasco T. Vasconcelos, and Makoto Kubo. Language primitives and type discipline for structured communication-based programming. In Chris Hankin, editor, ESOP,
chapter 9, pages 122–138. Springer Berlin Heidelberg, Berlin/Heidelberg, 1998.

28

Hopac. http://www.github.com/Hopac/hopac, 2016.

29

How are Akka actors different from Go channels?
https://www.quora.com/
How-are-Akka-actors-different-from-Go-channels, 2013.

30

Raymond Hu, Nobuko Yoshida, and Kohei Honda. Session-based distributed programming
in java. In ECOOP, pages 516–541. Springer, 2008.

http://clojure.com/blog/2013/06/28/

ECOOP 2017

90:28

Mixing Metaphors

31

Is Scala’s actors similar to Go’s coroutines? http://stackoverflow.com/questions/
22621514/is-scalas-actors-similar-to-gos-coroutines, 2014.

32

Einar Broch Johnsen, Reiner Hähnle, Jan Schäfer, Rudolf Schlatte, and Martin Steffen.
ABS: A core language for abstract behavioral specification. In FMCO, pages 142–164.
Springer, 2010.

33

R. Greg Lavender and Douglas C. Schmidt. Active object: An object behavioral pattern for
concurrent programming. In John M. Vlissides, James O. Coplien, and Norman L. Kerth,
editors, Pattern Languages of Program Design 2, pages 483–499. Addison-Wesley Longman
Publishing Co., Inc., Boston, MA, USA, 1996.

34

Paul B. Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value
programming languages. Information and Computation, 185(2):182–210, 2003.

35

Sam Lindley and J. Garrett Morris. A Semantics for Propositions as Sessions. In ESOP,
pages 560–584. Springer, 2015.

36

Sam Lindley and J. Garrett Morris. Embedding session types in haskell. In Haskell, pages
133–145. ACM, 2016.

37

Massimo Merro and Davide Sangiorgi. On asynchrony in name-passing calculi. Mathematical Structures in Computer Science, 14(5):715–767, 2004.

38

Robin Milner. Communicating and Mobile Systems: The Pi Calculus. Cambridge University Press, 1st edition, June 1999.

39

Rumyana Neykova and Nobuko Yoshida. Multiparty session actors. In COORDINATION,
pages 131–146. Springer, 2014.

40

Joachim Niehren, Jan Schwinghammer, and Gert Smolka. A concurrent lambda calculus
with futures. Theoretical Computer Science, 364(3):338–356, 2006.

41

Luca Padovani and Luca Novara. Types for Deadlock-Free Higher-Order Programs. In
Susanne Graf and Mahesh Viswanathan, editors, FORTE, pages 3–18. Springer International Publishing, 2015.

42

Jennifer Paykin, Antal Spector-Zabusky, and Kenneth Foner. choose your own derivative.
In TyDe, pages 58–59. ACM, 2016.

43

Frank Pfenning and Dennis Griffith. Polarized substructural session types. In FoSSaCS,
volume 9034 of Lecture Notes in Computer Science, pages 3–22. Springer, 2015.

44

Proto.Actor. http://www.proto.actor, 2016.

45

John H. Reppy. Concurrent Programming in ML. Cambridge University Press, 2007.

46

Davide Sangiorgi and David Walker. The π-calculus: a Theory of Mobile Processes. Cambridge University Press, 2003.

47

Typed Actors. https://github.com/knutwalker/typed-actors, 2016.

48

Philip Wadler. Propositions as sessions. Journal of Functional Programming, 24(2-3):384–
418, 2014.

Fowler, Lindley, and Wadler

A

90:29

Coalescing Transformation

Our translation from λch into λact relies on the assumption that all channels have the
same type, which is rarely the case in practice. Here, we sketch a sample type-directed
transformation which we call coalescing, which transforms an arbitrary λch program into an
λch program which has only one type of channel.
The transformation works by encapsulating each type of message in a variant type, and
ensuring that give and take use the correct variant injections. Although the translation
necessarily loses type information, thus introducing partiality, we can show that terms and
configurations that are the result of the coalescing transformation never reduce to an error.
We say that a type A is a base carried type in a configuration Γ; ∆ ` C if there exists
some subterm Γ ` V : ChanRef(A), where A is not of the form ChanRef(B).
In order to perform the coalescing transformation, we require an environment σ which
maps each base carried type A to a unique token `, which we use as an injection into a
variant type.
We write σ ^ Γ; ∆ ` C if σ contains a bijective mapping A 7→ ` for each base carried type
in Γ; ∆ ` C. We extend the relation analogously to judgements on values and computation
terms.
Next, we define the notion of a coalesced channel type, which can be used to ensure that
all channels in the system have the same type.
I Definition 34 (Coalesced channel type).
Given a token environment σ = A0 7→ `0 , . . . An 7→ `n , we define the coalesced channel type
cct(σ) as

cct(σ) = µX.h`0 : A0 , . . . , `n : An , `c : ChanRef(X)i
where
A+B = A+B
List(A) = List(A)
ChanRef(A) = ChanRef(X)
µY.A = µY.A
which is the single channel type which can receive values of all possible types sent in the
system.
1 =
A→B =
A×B =

1
A→B
A×B

Note that the definition of a base carried type excludes the possibility of a type of the
form ChanRef(A) appearing in σ. To handle the case of sending channels, we require cct(σ)
to be a recursive type; a distinguished token `c denotes the variant case for sending a channel
over a channel.
Retrieving a token from the token environment σ is defined by the following inference
rules. Note that ChanRef(A) maps to the distinguished token `c .
(A 7→ `) ∈ σ
σ(A) = `

σ(ChanRef(A)) = `c

With the coalesced channel type defined, we can define a function mapping types to
coalesced types.

ECOOP 2017

90:30

Mixing Metaphors

I Definition 35 (Type coalescing).
σ

σ

|1|
σ
|A → B|
σ
|A × B|

= 1
σ
σ
= |A| → |B|
σ
σ
= |A| ×|B|

|A + B|
σ
List(A)
σ
ChanRef(A)
σ
|µX.A|

σ

σ

= |A| +|B|
σ
= List(|A| )
= ChanRef(cct(σ))
σ
= µX.|A|

σ

We then extend |−| to typing environments Γ, taking into account that we must annotate
channel names.
I Definition 36 (Type coalescing on environments). 1. For Γ:
σ

a. ∅ = ∅
σ
σ
σ
b. |x : A, Γ| = x : |A| ,|Γ| .
σ
σ
c. a : ChanRef(A), Γ = aA : ChanRef(cct(σ)),|Γ| .
2. For ∆:
σ

a. ∅ = ∅
σ
σ
b. |a : A, ∆| = aA : cct(σ),|∆|
Figure 20 describes the coalescing pass from λch with multiple channel types into λch
with a single channel type. Judgements are of the shape {σ} Γ ` V : A
V 0 for values;
0
0
{σ} Γ ` M : A
M for computations; and {σ} Γ ` C
C for configurations, where σ is
an bijective mapping from types to tokens, and primed values are the results of the coalescing
pass. We omit the rules for values and functional terms, which are homomorphisms.
Of particular note are the rules for give and take. The coalesced version of give ensures
that the correct token is used to inject into the variant type. The translation of take retrieves
a value from the channel, and pattern matches to retrieve a value of the correct type from
the variant. As we have less type information, we have to account for the possibility that
pattern matching fails by introducing an error term, which we define at the top-level of the
term:

let error = (rec f (x) . f x) in . . .
The translation on configurations ensures that all existing values contained within a
buffer are wrappen in the appropriate variant injection.
The coalescing step necessarily loses typing information on channel types. To aid us in
stating an error-freedom result, we annotate channel names a with their original type; for
example, a channel with name a carrying values of type A would be translated as aA . It is
important to note that annotations are irrelevant to reduction, i.e.:
→
−
→
−
E[give aA W ] k aB ( V ) −→ E[return ()] k aB ( V · W )
As previously discussed, the coalescing pass means that channel types are less specific,
with the pass introducing partiality in the form of an error term, error. However, since we
began with a type-safe program in λch , we can show that programs that have been coalesced
from well-typed λch configurations never reduce to an error term.
I Definition 37 (Error configuration).
A configuration C is an error configuration if C ≡ G[error] for some configuration context G.

Fowler, Lindley, and Wadler

90:31

Coalescing of channel names

{σ} Γ ` V

V0

{σ} Γ ` M

M0

Ref

a : ChanRef(A) ∈ Γ
{σ} Γ ` a : ChanRef(A)

aA

Coalescing of communication and concurrency primitives
Give

{σ} Γ ` V : A
{σ} Γ ` W : ChanRef(A)
{σ} Γ ` give V W : 1

V0
W0

σ(A) = `

give (roll h` = V 0 i) W 0

Take

V0

{σ} Γ ` V : ChanRef(A)

σ(A) = `j

0

{σ} Γ ` take V : A

let x ⇐ take V in
let y ⇐ unroll x in
case y {
h`0 = yi . . . h`j−1 = yi 7→ error
h`j = yi 7→ y
h`j+1 = yi . . . h`n = yi 7→ error }
Fork

NewCh

{σ} Γ ` M : 1

{σ} Γ ` newCh : ChanRef(A)

{σ} Γ ` fork M : 1

newChA

{σ} Γ; ∆ ` C1

C10

{σ} Γ; ∆ ` C2

{σ} Γ; ∆ ` C1 k C2
Term

{σ} Γ ` M : A
{σ} Γ; · ` M

fork M 0
{σ} Γ ` C

Coalescing of configurations
Par

M0

C10

k

Chan

C20

{σ} Γ, a : ChanRef(A); ∆, a : A ` C

C20

M0
M0

{σ} Γ; ∆ ` (νa)C
Buf

({A, σ} Γ ` Vi : A
→
−
{σ} Γ; a : A ` a( V )

(νaA )C

{σ} Γ ` V : A

V0

{A, σ} Γ ` V : A

C0

0

Vi0 )i
−
→
aA (V 0 )
{A, σ} Γ ` V : A

Coalescing of buffer values

C0

V0

σ(A) = `
h` = V i

Figure 20 Type-directed coalescing pass

ECOOP 2017

90:32

Mixing Metaphors

I Definition 38 (Error-free configuration).
A configuration C is error-free if it is not an error configuration.
We can straightforwardly see that the initial result of a coalescing pass is error-free:
I Lemma 39. If σ ^ Γ ` C

C 0 , then C 0 is error-free.

Proof. By induction on the derivation of Γ ` C

C0.

J

Next, we show that error-freedom is preserved under reduction. To do so, we make
essential use of the fact that the coalescing pass annotates each channel with its original
type.
I Lemma 40 (Error-freedom (coalesced λch )).
If Γ; ∆ ` C
C10 , and C10 −→∗ C20 , then C20 is error free.
Proof. (Sketch.) By preservation in λch , we have that Γ; ∆ ` C20 , and by Lemma 39, we can
assume that C10 is error-free.
We show that an error term can never arise. Suppose that C20 was an error configuration,
meaning that C20 ≡ G[error] for some configuration context G. As we have decreed that the
error term does not appear in user programs, we know that error must have arisen from
the refinement pass. By observation of the refinement rules, we see that error is introduced
only in the refinement rule for Take.
Stepping backwards through the reduction sequence introduced by the Take rule, we
have that:

case h`k = W i {
h`0 = yi . . . h`j−1 = yi 7→ error
h`j = yi 7→ y
h`j+1 = yi . . . h`n = yi 7→ error
}
for some k 6= j.
Stepping back further, we have that:

let x ⇐ take aB in
let y ⇐ unroll (roll x) in
case y {
h`0 = yi . . . h`j−1 = yi 7→ error
h`j = yi 7→ y
h`j+1 = yi . . . h`n = yi 7→ error
}
Now, inspecting the premises of the refinement rule for Take, we have that Γ ` aB :
ChanRef(A)
V 0 and σ(A) = `j . Examining the refinement rule for Ref, we have that
{σ} Γ ` a : ChanRef(A)
aA , thus we have that B = A.
However, we have that σ(A) = `j and σ(A) = `k but we know that k 6= j, thus leading to
a contradiction since σ is bijective.
J
Since annotations are irrelevant to reduction, it follows that C 0 has identical reduction
behaviour with all annotations erased.

Fowler, Lindley, and Wadler

B
B.1

90:33

Selected full proofs
λch Preservation

Lemma 2 (Progress (λch terms))
Assume Γ is either empty or only contains entries of the form ai : ChanRef(Ai ).
If Γ ` M : A, then either:
1. M = return V for some value V
2. M can be written E[M 0 ], where M 0 is a communication or concurrency primitive (i.e.
give V W, take V, fork M , or newCh)
3. There exists some M 0 such that M −→M M 0
Proof. By induction on the derivation of Γ ` M : A. Cases Return, Give, Take, NewCh,
and Fork hold immediately due to 1) and 2). For App, by inversion on the typing relation
we have that V = (λx.M ), and thus can β-reduce. For EffLet, we have that Γ ` let x ⇐
M in N : B, with Γ ` M : A and Γ, x : A ` N : B. We proceed using the inductive
hypothesis. If M = return V , we can take a step let x ⇐ return V in N −→M N {V /x}. If M
is a communication term, then we note that let x ⇐ E in N is an evaluation context and can
write E[fork N 0 ] etc. to satisfy 2). Otherwise, M can take a step and we can take a step by
the lifting rule E[M ] −→M E[M 0 ].
J
Lemma 3 If Γ; ∆ ` C and C ≡ D, then Γ; ∆ ` D.
Proof. By induction on the derivation of Γ; ∆ ` C.
Case C k D ≡ D k C.
We assume that Γ; ∆ ` C k D, so we have that ∆ partitions as ∆1 , ∆2 such that Γ; ∆1 ` C
and Γ, ∆2 ` D. It follows immediately by the symmetry of Par that Γ; ∆2 , ∆1 ` D k C as
required.
Case C k (D k E)
We assume that Γ; ∆ ` C k (D k E). We can show that ∆ partitions as ∆1 , ∆2 such that
Γ; ∆1 ` C and Γ; ∆2 ` D k E. We can then show that ∆2 splits as ∆3 , ∆4 such that
Γ; ∆3 ` D and Γ; ∆4 ` E. It is then possible to show that Γ; ∆1 , ∆3 ` C k D and Γ; ∆4 ` E.
Recomposing, we have that Γ; ∆ ` (C k D) k E as required.
Case C k (νa)D ≡ (νa)(C k D) if a 6∈ fv(C)
We assume that Γ; ∆ ` C k (νa)D. From this, we know that ∆ splits as ∆1 , ∆2 such that
Γ; ∆1 ` C and Γ; ∆2 ` (νa)D. By Chan, we know that Γ, a : ChanRef(A); ∆2 , a : A ` D. By
weakening, we have that Γ, a : ChanRef(A) ` C; we can show that Γ, a : ChanRef(A); ∆1 , ∆2 , a :
A ` C k D. By Chan, we have that Γ; ∆ ` (νa)(C k D) as required.
Case G[C] ≡ G[D] if C ≡ D. Immediate by the inductive hypothesis.
J
I Lemma 41 (Replacement). If Γ ` E[M ] : A, Γ ` M : B, and Γ ` N : B, then Γ ` E[N ] : A.
Proof. By induction on the structure of E.

J

Theorem 4 (Preservation (λch configurations)
If Γ; ∆ ` C1 and C1 −→ C2 , then Γ; ∆ ` C2 .

ECOOP 2017

90:34

Mixing Metaphors

Proof. By induction on the derivation of C −→ C 0 . We use Lemma 41 implicitly throughout.
Case Give
→
−
From the assumption Γ; ∆ ` E[give W a] k a( V ), we have that Γ; · ` E[give W a] and
→
−
Γ; a : A ` a( V ). Consequently, we know that ∆ = a : A.
From this, we know that Γ ` give W a : 1 and thus Γ ` W : A and Γ ` a : ChanRef(A).
→
−
→
−
We also have that Γ; a : A ` a( V ), thus Γ ` Vi : A for all Vi ∈ V . By Unit we can show
→
−
Γ; · ` E[return ()] and by Buf we can show Γ; a : A ` a( V · W ); recomposing, we arrive at
→
−
Γ; ∆ ` E[return ()] k a( V W ) as required.
Case Take
→
−
From the assumption Γ; ∆ ` E[take a] k a(W · V ), we have that Γ; · ` E[take a] and that
→
−
Γ; a : A ` a(W · V ). Consequently, we know that ∆ = a : A.
From this, we know that Γ ` take a : A, and thus Γ ` a : ChanRef(A). Similarly, we have
→
−
that Γ; a : ChanRef(A) ` a(W · V ), and thus Γ ` W : A.
→
−
Consequently, we can show that Γ; · ` E[return W ] and Γ; a : A ` a( V ); recomposing, we
→
−
arrive at Γ; ∆ ` E[return W ] k a( V ) as required.
Case NewCh
By Buf we can type Γ; a : A ` a(), and since Γ ` newCh : ChanRef(A), it is also possible to
show Γ, a : ChanRef(A) ` a : ChanRef(A), thus Γ, a : ChanRef(A) ` E[return a].
Recomposing by Par we have Γ, a : ChanRef(A); a : A ` E[return a] k a(), and by Chan
we have Γ; · ` (νa)(E[return a] k a()) as required.
Case Fork
From the assumption Γ; ∆ ` E[fork M ], we have that ∆ = ∅ and Γ ` M : 1. By Unit we
can show Γ; · ` E[return ()], and by Term we can show Γ; · ` M . Recomposing, we arrive at
Γ; ∆ ` E[return ()] k M as required.
Case Lift Immediate by the inductive hypothesis.
Case LiftV Immediate by Lemma 1.
J

Fowler, Lindley, and Wadler

B.2

90:35

λact Preservation

I Lemma 42 (Replacement). If Γ | C ` E[M ] : A, Γ | C ` M : B, and Γ | C ` N : B, then
Γ | C ` E[N ] : B.
Proof. By induction on the structure of E.

J

Theorem 12 (Preservation (λact configurations))
If Γ; ∆ ` C1 and C1 −→ C2 , then Γ; ∆ ` C2 .
Proof. By induction on the derivation of C1 −→ C2 , making implicit use of Lemma 42.
Case Spawn
→
−
From the assumption that Γ; ∆ ` ha, E[spawn M ], V i, we have that ∆ = a : C, that
Γ | C ` spawn M : ActorRef(A) and Γ | A ` M : 1.
We can show Γ, b : ActorRef(A) ` b : ActorRef(A); and therefore that Γ, b : ActorRef(A) `
→
−
E[return b] : 1. By Actor, it follows that Γ, b : ActorRef(A); a : C ` ha, E[return b], V i.
By Actor, we can show Γ, b : ActorRef(A); b : A ` hb, M, i.
→
−
Finally, by Pid and Par, we have Γ; ∆ ` (νb)(ha, E[return b], V i k hb, M, i) as required.
Case Send
→
−
−
→
From the assumption that Γ; ∆ ` ha, E[send V 0 b], V i k hb, M, W i, we have that Γ; a : A `
→
−
−
→
ha, E[send V 0 b], V i and Γ; b : C ` hb, M, W i. Consequently, we can write ∆ = a : A, b : C.
From this, we know that Γ | A ` send V 0 b : 1, so we can write Γ = Γ0 , b : ActorRef(C), and
−
→
Γ ` V 0 : C. Additionally, we know that Γ; b : C ` hb, M, W i and thus that (Γ ` Wi : C) for
−
→
each entry Wi ∈ W .
−
→
−
→
As Γ ` V 0 : C, it follows that Γ ` W ·V 0 and therefore that Γ; b : C ` hb, M, W ·V i. We can
→
−
also show that Γ | C ` return () : 1, and therefore it follows that Γ; a : A ` ha, E[return ()], V i.
−
→
−
→
Recomposing, we have that Γ; ∆ ` ha, E[return ()], W i k hb, M, W · V 0 i as required.
Case Receive
→
−
By Actor, we have that Γ; ∆ ` ha, E[receive], W · V i. From this, we know that Γ | A `
E[receive] : 1 (and thus Γ | A ` receive : A) and Γ ` W : A.
Consequently, we can show Γ ` E[return W ] : 1. By Actor, we arrive at Γ; ∆ `
→
−
ha, E[return W ], V i as required.
Case Self
→
−
By Actor, we have that Γ; ∆ ` ha, E[self], V i, and thus that Γ | A ` E[self] : 1 and
Γ | A ` self : ActorRef(A). We also know that Γ = Γ0 , a : ActorRef(A), and that ∆ = a : A.
Trivially, we can show Γ0 , a : ActorRef(A) ` a : ActorRef(A). Thus it follows that
→
−
Γ0 , a : ActorRef(A) ` E[return a] : 1 and thus it follows that Γ; ∆ ` ha, E[return a], V i as
required.
Case Lift Immediate by the inductive hypothesis.
Case LiftV Immediate by Lemma 9.
J
Proofs for the progress results for λact follow the same structure as their λch counterparts.

ECOOP 2017

90:36

Mixing Metaphors

B.3

Translation: λact into λch

Lemma 23
1. If Γ ` V : A in λact , then J Γ K ` J V K : J A K in λch .
2. If Γ | B ` M : A in λact , then J Γ K, α : ChanRef(J B K) ` J M K α : J A K in λch .
Proof. By simultaneous induction on the derivations of Γ ` V : A and Γ | B ` M : A.
Premise 1
Case Γ ` α : A
By the definition of J − K, we have that J α K = α. By the definition of J Γ K, we have that
α : J A K ∈ J Γ K. Consequently, it follows that J Γ K ` α : J A K.
Case Γ ` λx.M : A → B
From the assumption that Γ ` λx.M : A →C B, we have that Γ, x : A | C ` M : B. By the
inductive hypothesis (premise 2), we have that J Γ K, x : J A K, ch : ChanRef(J C K) ` J M K ch :
J B K.
By two applications of Abs, we have J Γ K ` λx.λch.J M K ch : J A K → ChanRef(J C K) →
J B K as required.
Case Γ ` () : 1 Immediate.
Case Γ ` (V, W ) : (A × B)
From the assumption that Γ ` (V, W ) : (A, B) we have that Γ ` V : A and Γ ` W : B. By the
inductive hypothesis (premise 1) and Pair, we can show J Γ K ` (J V K, J W K) : (J A K × J B K)
as required.
Premise 2
Case Γ | C ` V W : B
From the assumption that Γ | C ` V W : B, we have that Γ ` V : A →C B and Γ ` W : B.
By the inductive hypothesis (premise 1), we have that J Γ K ` J V K : J A K → ChanRef(J C K) →
J B K, and J Γ K ` J W K : J B K.
By extending the context Γ with a ch : ChanRef(J C K), we can show that J Γ K, ch :
ChanRef(J C K) ` J V K J W K ch : J B K as required.
Case Γ | C ` let x ⇐ M in N : B
From the assumption that Γ | C ` let x ⇐ M in N : B, we have that Γ | C ` M : A and that
Γ, x : A | C ` N : B.
By the inductive hypothesis (premise 2), we have that J Γ K, ch : ChanRef(J C K) ` J M K ch :
J A K and J Γ K, x : J A K, ch : ChanRef(J C K) ` J N K ch : J B K.
By EffLet, it follows that J Γ K, ch : ChanRef(J C K) ` let x ⇐ J M K ch in J N K ch : J B K
as required.
Case Γ | C ` return V : A
From the assumption that Γ | C ` return V : A, we have that Γ ` V : A.
By the inductive hypothesis (premise 1), we have that J Γ K ` J V K : J A K.
By weakening (as we do not use the mailbox channel), we can show that J Γ K, y :
ChanRef(J C K) ` return J V K : J A K as required.
Case Γ | C ` send V W : 1
From the assumption that Γ | C ` send V W : 1, we have that Γ ` V : A and Γ ` W :
ChanRef(A).
By the inductive hypothesis (premise 1) we have that J Γ K ` J V K : J A K and J Γ K ` J W K :
ChanRef(J A K).
By Give, we can show that J Γ K ` give J V K J W K : 1, and by weakening we have that
J Γ K, ch : ChanRef(J C K) ` give J V K J W K : 1 as required.

Fowler, Lindley, and Wadler

90:37

Case Γ | C ` receive : C
Given a ch : ChanRef(J C K), we can show that J Γ K, ch : ChanRef(J C K) ` ch : ChanRef(J C K)
and therefore that J Γ K, ch : ChanRef(J C K) ` take ch : J C K as required.
Case Γ | C ` spawn M : ActorRef(A)
From the assumption that Γ | C ` spawn M : ActorRef(A), we have that Γ | A ` M : A.
By the inductive hypothesis (premise 2), we have that J Γ K, chMb : ChanRef(J A K) `
J M K chM b : J A K. By Fork and Return, we can show that J Γ K, chM b : ChanRef(J A K) `
fork (J M K chM b); return chM b : ChanRef(J A K).
By NewCh and EffLet, we can show that J Γ K ` let chM b ⇐ newCh in fork (J M K chM b); return chM b :
ChanRef(J A K).
Finally, by weakening, we have that
J Γ K, ch : ChanRef(J C K) ` let chMb ⇐ newCh in (fork J M K chMb); return chMb : ChanRef(J A K)
as required.
Case Γ | C ` self : ActorRef(C)
Given a ch : ChanRef(J C K), we can show that J Γ K, ch : ChanRef(J C K) ` return ch :
ChanRef(J C K) as required.
J
Theorem 18 If Γ; ∆ ` C, then J Γ K; J ∆ K ` J C K.
Proof. By induction on the derivation of Γ; ∆ ` C.
Case Par
From the assumption that Γ; ∆ ` C1 k C2 , we have that ∆ splits as ∆1 , ∆2 such that
Γ; ∆1 ` C1 and Γ; ∆2 ` C2 . By the inductive hypothesis, we have that J Γ K; J ∆1 K ` J C1 K and
J Γ K; J ∆2 K ` J C2 K. Recomposing by Par, we have that J Γ K; J ∆1 K, J ∆2 K ` J C1 K k J C2 K as
required.
Case Pid
From the assumption that Γ; ∆ ` (νa)C, we have that Γ, a : ActorRef(A); ∆, a : A ` C.
By the inductive hypothesis, we have that J Γ K, a : ChanRef(J A K); J ∆ K, a : J A K ` J C K.
Recomposing by Pid, we have that J Γ K; J ∆ K ` (νa)J C K as required.
Case Actor
→
−
From the assumption that Γ, a : ActorRef(A); a : A ` ha, M, V i, we have that Γ, a :
ActorRef(A) | A ` M : 1. By Lemma 17, we have that J Γ K, a : ChanRef(J A K) ` J M K a : 1.
It follows straightforwardly that J Γ K, a : ChanRef(J A K); · ` J M K a.
→
−
→
−
We can also show that J Γ K, a : ChanRef(J A K); a : J A K ` a(J V K) (where J V K =
J V1 K · . . . · J Vn K), by repeated applications of Lemma 17.
→
−
By Term and Par, we have that J Γ K, a : ChanRef(J A K); a : J A K ` a(J V K) k J M K a as
required.
J
Lemma 20 If Γ; ∆ ` C and C ≡ D, then J C K ≡ J D K.
Proof. By induction on the derivation of Γ; ∆ ` C, examining each possible equivalence. The
result follows easily from the homomorphic nature of the translation on name restrictions
and parallel composition.
J
Theorem 21
If Γ ` C1 and C1 −→ C2 , then there exists some D such that J C1 K −→∗ D, with D ≡ J C2 K.

ECOOP 2017

90:38

Mixing Metaphors

Proof. By induction on the derivation of C −→ C 0 .
Case Spawn

Assumption
Definition of J − K
newCh reduction
Let reduction
Fork reduction
Let reduction
≡
=

−
→
J ha, E[spawn M ], V i K
−
→
a(J V K) k (J E K[let c ⇐ newCh in fork (J M K c); return c] a)
−
→
a(J V K) k (νb)((J E K[let c ⇐ return b in fork (J M K c); return c] a) k b())
−
→
a(J V K) k (νb)((J E K[fork (J M K b); return b] a) k b())
−
→
a(J V K) k (νb)((J E K[return (); return b] a) k (J M K b) k b())
−
→
a(J V K) k (νb)((J E K[return b] a) k (J M K b) k b())
−
→
(νb)(a(J V K) k (J E K[return b] a) k b() k (J M K b))
−
→
J (νb)(ha, E[return b], V i k hb, M, i) K

(1)
(2)
(3)
(4)
(5)
(6)
(7)
(8)

Case Self

Assumption
Definition of J − K
=

−
→
J ha, E[self], V i K
−
→
a((J V K)) k (J E K[return a] a)
−
→
J ha, E[return a], V i K

(1)
(2)

Case Send

Assumption
Definition of J − K
Give reduction
=

−
→
−
→
J ha, E[send V 0 b], V i k hb, M, W i K
−
→
−
→
0
a(J V K) k (J E K[give J V K b] a) k b(J W K) k (J M K b)
−
→
−
→
a(J V K) k (J E K[return ()] a) k b(J W K · J V 0 K) k (J M K b)
−
→
−
→
J ha, E[return ()], V i k hb, M, W · V 0 i K

(1)
(2)
(3)
(4)

Case Receive

Assumption
Definition of J − K
Take reduction
=

−
→
J ha, E[receive], W · V i K
−
→
a(J W K · J V K) k (J E K[take a] a)
−
→
a(J V K) k (J E K[return J W K] a)
−
→
J ha, E[return W ], V i K

(1)
(2)
(3)
(4)

Lift is immediate from the inductive hypothesis, and LiftV is immediate from Lemma 19.
J

Fowler, Lindley, and Wadler

B.4

90:39

Translation: λch into λact

Lemma 23
1. If {B} Γ ` V : A, then L Γ M ` L V M : L A M.
2. If {B} Γ ` M : A, then L Γ M | L B M ` L M M : L A M.
Proof. By simultaneous induction on the derivations of {B} Γ ` V : A and {B} Γ ` M : A.
Premise 1
Case Var
From the assumption that {B} Γ ` α : A, we know that α : A ∈ Γ. By the definition of L Γ M,
we have that α : L A M ∈ L Γ M. Since L α M = α, it follows that L Γ M ` α : L A M as required.
Case Abs
From the assumption that {C} Γ ` λx.M : A → B, we have that {C} Γ, x : A ` M : B. By
the inductive hypothesis (Premise 2), we have that L Γ M, x : L A M | L C M ` L M M : L A M. By
Abs, we can show that L Γ M | L C M ` λx.L M M : L A M →L C M L B M as required.
Case Rec Similar to Abs.
Case Unit Immediate.
Case Pair
From the assumption that {C} Γ ` (V, W ) : A × B, we have that {C} Γ ` V : A and that
{C} Γ ` W : B.
By the inductive hypothesis (premise 1), we have that L Γ M ` L V M : L A M and that
L Γ M ` L W M : L B M.
It follows by Pair that L Γ M ` (L V M, L W M) : (L A M × L B M) as required.
Cases Inl, Inr Similar to Pair.
Case Roll Immediate.
Premise 2
Case App
From the assumption that {C} Γ ` V W : B, we have that {C} Γ ` V : A → B and {C} Γ `
W : A. By the inductive hypothesis (premise 1), we have that L Γ M ` L V M : L A M →L C M L B M
and that L Γ M ` L W M : L A M.
By App, it follows that L Γ M | L C M ` L V M L W M : L B M as required.
Case Return
From the assumption that {C} Γ ` return V : A, we have that {C} Γ ` V : A. By the
inductive hypothesis we have that L Γ M ` L V M : L A M and thus by Return we can show that
L Γ M | L C M ` return L V M : L A M as required.
Case EffLet
From the assumption that {C} Γ ` let x ⇐ M in N : B, we have that {C} Γ ` M : A and
{C} Γ, x : A ` N : B.
By the inductive hypothesis (premise 2), we have that L Γ M | L C M ` L M M : L A M and
L Γ M, x : L A M | L C M ` L N M : L B M. Thus by EffLet it follows that L Γ M | L C M ` let x ⇐
L M M in L N M : L B M.
Case LetPair Similar to EffLet.
Case Case
From the assumption that {C} Γ ` case V {inl x 7→ M ; inr y 7→ N } : B, we have that
{C} Γ ` V : A + A0 , that {C} Γ, x : A ` M : B, and that {C} Γ, y : A0 ` N : B.

ECOOP 2017

90:40

Mixing Metaphors

By the inductive hypothesis (premise 1) we have that L Γ M ` L V M : L A M + L A0 M, and by
premise 2 we have that L Γ M, x : L A M | L C M ` L M M : L B M and L Γ M, y : L A0 M | L C M ` L M M :
L B M.
By Case, it follows that L Γ M | L C M ` case L V M {inl x 7→ L M M; inr y 7→ L N M} : L B M.
Case Unroll Immediate.
Case Fork
From the assumption that {A} Γ ` fork M : 1, we have that {A} Γ ` M : 1. By the
inductive hypothesis, we have that L Γ M | L A M ` L M M : 1.
We can show that L Γ M | L A M ` spawn L M M : ActorRef(1) and also show that L Γ M, x :
ActorRef(1) ` return () : 1.
Thus by EffLet, it follows that L Γ M | L A M ` let x ⇐ spawn L M M in return () : 1 as
required.
Case Give
From the assumption that {A} Γ ` give V W : 1, we have that {A} Γ ` V : A and
{A} Γ ` W : Chan. By the inductive hypothesis, we have that L Γ M ` L V M : L A M and
L Γ M ` L W M : ActorRef(L A M + ActorRef(L A M)). We can show that L Γ M ` inl L V M : L A M +
ActorRef(L A M), and thus it follows that L Γ M | L A M ` send inl V L W M : 1 as required.
Case Take
From the assumption that {A} Γ ` take V : A, we have that {A} Γ ` V : Chan.
By the inductive hypothesis (premise 1), we have that L Γ M ` L V M : ActorRef(L A M +
ActorRef(L A M)).
We can show that:
L Γ M | L A M ` self : ActorRef(L A M)
L Γ M | L A M ` inr self : L A M + ActorRef(L A M)
L Γ M, selfPid : ActorRef(L A M) | L A M ` send inr selfPid L V M : 1
L Γ M, selfPid : ActorRef(L A M), z : 1 | L A M ` receive : L A M
Thus by two applications of EffLet (noting that we desugar M ; N into let z ⇐ M in N ,
where z is fresh), we arrive at:

L Γ M | L A M ` let selfPid ⇐ self in send (inr selfPid) L V M; receive : L A M
as required.
Case NewCh
We have that {A} Γ; ∆ ` newCh : Chan.
Our goal is to show that L Γ M | L A M ` spawn body ([ ], [ ]) : ActorRef(L A M+ActorRef(L A M)).
To do so amounts to showing that L Γ M | L A M + ActorRef(L A M) ` body ([ ], [ ]) : 1.
We sketch the proof as follows. Firstly, by the typing of receive, recvVal must have type
L A M + ActorRef(L A M). By inspection of both case branches and LetPair, we have that state
must have type List(L A M) × List(ActorRef(L A M)).
We expect drain to have type
List(L A M) × List(ActorRef(L A M)) →L A M List(L A M) × List(ActorRef(L A M))
since we use the returned value as a recursive call to g, which must have the same type of
state. Inspecting the case split in drain, we have that the empty list case for values returns
the input state, which of course has the same type. The same can be said for the empty list
case of the readers case split.

Fowler, Lindley, and Wadler

90:41

In the case where both the values and readers lists are non-empty, we have that v has
type L A M and pid has type ActorRef(L A M). Additionally, we have that vs has type List(L A M)
and pids has type List(ActorRef(L A M)). We can show via send that send v pid has type 1.
After desugaring M ; N into an EffLet, we can show that the returned value is of the correct
type.
J
Theorem 24 If {A} Γ; ∆ ` C with Γ  ∆, then L Γ M; L ∆ M ` L C M.
Proof. By induction on the derivation of {A} Γ; ∆ ` C.
Case Par
From the assumption that {A} Γ; ∆ ` C1 k C2 , we have that ∆ splits as ∆1 , ∆2 such that
{A} Γ; ∆1 ` C1 and {A} Γ; ∆2 ` C2 .
By the inductive hypothesis, we have that L Γ M; L ∆1 M ` L C1 M and L Γ M; L ∆2 M ` L C2 M. By
the definition of L − M on linear configuration environments, it follows that L ∆1 M, L ∆2 M = L ∆ M.
Consequently, by Par, we can show that L Γ M; L ∆ M ` L C M1 k L C M2 as required.
Case Chan
From the assumption that {A} Γ; ∆ ` (νa)C, we have that {A} Γ, a : ChanRef(A); ∆, a : A `
C. By the inductive hypothesis, we have that L Γ M, a : ActorRef(L A M+ActorRef(L A M)); L ∆ M, a :
L A M + ActorRef(L A M) ` L C M.
By Pid, it follows that L Γ M; L ∆ M ` (νa)L C M as required.
Case Term
From the assumption that {A} Γ; · ` M , we have that {A} Γ ` M : 1.
By Lemma 23, we have that L Γ M | L A M ` L M M : 1. By weakening, we can show that
L Γ M, a : ActorRef(L A M) | L A M ` L M M : 1.
It follows that, by Actor, we can construct a configuration of the form L Γ M, a :
ActorRef(L A M); a : L A M ` ha, L M M, i, and by Pid, we arrive at
L Γ M; · ` (νa)(ha, L M M, i)
as required.
Case Buf
→
−
We assume that {A} Γ; a : A ` a( V ), and since Γ  ∆, we have that we can write
Γ = Γ0 , a : ChanRef(A).
→
−
From the assumption that {A} Γ0 , a : ChanRef(A); a : A ` a( V ), we have that {A} Γ0 , a :
→
−
ChanRef(A) ` Vi : A for each Vi ∈ V .
By repeated application of Lemma 23, we have that {A} L Γ0 M, a : ActorRef(L A M +
→
−
ActorRef(L A M)) ` L Vi M : L A M for each Vi ∈ V , and by ListCons and EmptyList we can
construct a list L V1 M :: . . . :: L Vn M :: [ ] with type List(L A M).
Relying on our previous analysis of the typing of body, we have that L body M has type:
(List(L A M) × List(ActorRef(L A M))) →L A M+ActorRef(L A M) 1
Thus it follows that

L Γ0 M, a : ActorRef(L A M + ActorRef(L A M)) | L A M + ActorRef(L A M) `
→
−
body (L V M, [ ]) : 1

ECOOP 2017

90:42

Mixing Metaphors

By Actor, we can see that
L Γ0 M, a : ActorRef(L A M + ActorRef(L A M)); a : L A M + ActorRef(L A M) `
→
−
ha, body (L V M, [ ]), i
as required.
J
Theorem 27
If {A} Γ; ∆ ` C1 , and C1 −→ C2 , then there exists some D such that L C1 M −→∗ D with
D ≡ L C2 M.
Proof.
By induction on the derivation of C1 −→ C2 .
Case Give

Assumption
Definition of L − M
≡
−→ (Send)

→
−
E[give W a] k a( V )
→
−
(νb)(hb, L E M[send (inl L W M) a], i) k ha, body ([L V M], [ ]), i
→
−
(νb)(hb, L E M[send (inl L W M) a], i k ha, body ([L V M], [ ]), i)
→
−
(νb)(hb, L E M[return ()], i k ha, body ([L V M], [ ]), inl L W Mi)

Now, let G[−] = (νb)hb, L E M[return ()], i k [−]).
We now have
→
−
G[ha, body ([L V M], [ ]), (inl L W M)i]
which we can expand to

G[ha,

(rec g(state) .
, inl L W Mi]
let recvV al ⇐ receive in
let (vals, readers) = state in
case recvVal {
inl v 7→ let newVals ⇐ vals ++ [v] in
let state0 ⇐ drain (newVals, readers) in
body (state0 )
inr pid 7→ let newReaders ⇐ readers ++ [pid] in
let state0 ⇐ drain (vals, newReaders) in
→
−
body (state’)}) (L V M, [ ])

Applying the arguments to the recursive function g; performing the receive, and the let
and case reductions, we have:
→
−
G[ha, let newVals ⇐ L V M ++ [L W M] in , i]
0
let state ⇐ drain (newVals, [ ]) in
body (state0 )

Fowler, Lindley, and Wadler

90:43

Next, we reduce the append operation, and note that since we pass a state without
pending readers into drain, that the argument is returned unchanged:
→
−
G[ha, let state0 ⇐ return (L V M :: L W M :: [ ]) in body state0 , i]

Next, we apply the let-reduction and expand the evaluation context:
→
−
(νb)(hb, L E M[return ()], i k ha, body (L V M :: L W M :: [ ]), i)

which is structurally congruent to

→
−
(νb)(hb, L E M[return ()], i) k ha, body (L V M :: L W M :: [ ]), i
which is equal to

→
−
L E[return ()] k a(L V · W M) M

as required.
Case Take

→
−
Assumption E[take a] k a(W · V )
→
−
Definition of L − M (νb)(hb, L E M[ let selfPid ⇐ self in, i) k hb, body (L W M :: L V M, [ ]), i
send (inr selfPid) a;
receive]
→
−
≡ (νb)(hb, L E M[ let selfPid ⇐ self in, i k hb, body (L W M :: L V M, [ ]), i)
send (inr selfPid) a;
receive]
→
−
−→ (Self) (νb)(hb, L E M[ let selfPid ⇐ return b in, i k hb, body (L W M :: L V M, [ ]), i)
send (inr selfPid) a;
receive]
→
−
−→M (Let) (νb)(hb, L E M[ send (inr b) a;, i k hb, body (L W M :: L V M, [ ]), i)
receive]
→
−
−→ (Send) (νb)(hb, L E M[return (); receive], i k hb, body (L W M :: L V M, [ ]), (inr b)i)
→
−
−→M (Let) (νb)(hb, L E M[receive], i k hb, body (L W M :: L V M, [ ]), (inr b)i)
Now, let G[−] = (νb)(hb, L E M[receive], i k [−]).
Expanding, we begin with:
G[ha,

(rec g(state) .
, (inr b)i]
let recvV al ⇐ receive in
let (vals, readers) = state in
case recvVal {
inl v 7→ let newVals ⇐ vals ++ [v] in
let state0 ⇐ drain (newVals, readers) in
g (state0 )
inr pid 7→ let newReaders ⇐ readers ++ [pid] in
let state0 ⇐ drain (vals, newReaders) in
→
−
g (state’)}) (L W M :: L V M, [ ])

ECOOP 2017

90:44

Mixing Metaphors

Reducing the recursive function, receiving from the mailbox, splitting the pair, and then
taking the second branch on the case statement, we have:

G[ha,

let newReaders ⇐ [ ] ++ [b] in
, i]
let state0 ⇐ drain (vals, newReaders) in
body state0

Reducing the list append operation, expanding drain, and re-expanding G, we have:
(νb)(hb, E[receive], i k ha, let state0 ⇐ (λx.
let (vals, readers) = x in
case vals {
[ ] 7→ return (vals, readers)
v :: vs 7→
case readers {
[ ] 7→ return (vals, readers)
pid :: pids 7→ send v pid;
body state0

→
−
return (vs, pids)}}) (L W M :: L V M, [b]) in

Next, we reduce the function application, pair split, and the case statements:
(νb)(hb, E[receive], i k ha, let state0 ⇐ send L W M b;
, i
→
−
return (L V M, [ ]))
body state0
We next perform the send operation, and thus we have:
→
−
(νb)(hb, E[receive], L W Mi k ha, body ((L V M, [ ])), i
Finally, we perform the receive and apply a structural congruence to arrive at
→
−
(νb)(hb, E[L W M], i) k ha, body ((L V M, [ ])), i
which is equal to
→
−
L E[return W ] k a( V ) M
as required.
Case NewCh

Assumption
Definition of L − M
−→
≡
=

E[newCh]
(νa)(ha, L E M[spawn (body ([ ], [ ]))], i)
(νa)(νb)(ha, L E M[return b], i k hb, body ([ ], [ ]), i)
(νb)(νa)(ha, L E M[return b], i) k hb, body ([ ], [ ]), i)
L (νb)(E[return b] k b()) M

, i

Fowler, Lindley, and Wadler

90:45

as required.
Case Fork

Assumption
Definition of L − M
−→
−→M
≡
=

E[fork M ]
(νa)(ha, L E M[let x ⇐ spawn L M M in return ()], i)
(νa)(νb)(ha, L E M[let x ⇐ return b in return ()], i k ha, L M M, i)
(νa)(νb)(ha, L E M[return ()], i k hb, L M M, i)
(νa)(ha, L E M[return ()], i) k (νb)(hb, L M M, i)
L E[return ()] k M M

as required.
Case Lift Immediate by the inductive hypothesis.
Case LiftV Immediate by Lemma 25.
J

ECOOP 2017

90:46

Mixing Metaphors

B.5

Correctness of Selective Receive Translation

B.5.1

Translation preserves typing

Theorem 32 (Type Soundness (Translation from λact with selective receive into
λact )) If Γ; ∆ ` C, then it is the case that for all D ∈ bCc, then bΓc; b∆c ` bDc.
Proof. By induction on the typing derivation of Γ; ∆ ` C.
Case Γ; ∆ ` C1 k C2
From the assumption that
Γ ` ∆ ` C1 k C2
we have that ∆ splits as ∆1 , ∆2 and we have that Γ; ∆1 ` C1 and Γ; ∆2 ` C2 .
By the inductive hypothesis, we have that all C10 ∈ bC1 c are well-typed under bΓc; b∆1 c,
and similarly for C 0 2 under bΓc and b∆2 c.
Thus we can conclude (since b∆1 c and b∆2 c remain disjoint) that
bΓc; b∆c ` C10 k C20
for all C10 ∈ bC1 c and C20 ∈ bC2 c.
Case Γ; ∆ ` (νa)C
From the assumption that Γ; ∆ ` (νa)C, we have that
Γ, a : ActorRef(h`i : Ai ii ); a : h`i : Ai ii ` C
By the inductive hypothesis, we have that for all D ∈ bCc, it is the case that
bΓc, a : ActorRef(h`i : bAi cii ); b∆c, a : h`i : bAi cii ` D
It follows by Pid that for all D ∈ bCc, that bΓc; b∆c ` (νa)D as required.
→
−
Case Γ, a : ActorRef(h`i : Ai ii ); a : h`i : Ai ii ` ha, M, V i
From the assumption
→
−
Γ, a : ActorRef(h`i : Ai ii ); a : h`i : Ai ii ` ha, M, V i
we have that
Γ, a : ActorRef(h`i : Ai ii ) | h`i : Ai ii ` M : 1
and that
Γ, a : ActorRef(h`i : Ai ii ) ` Vk : h`i : Ai ii
→
−
for all Vk ∈ V .
By Lemma 31, we have that
bΓc, a : ActorRef(h`i : bAi cii ), mb : List(h`i : bAi ci i) ` bM c mb : 1
Again by Lemma 31, we have that
bΓc, a : ActorRef(h`i : bAi cii ) ` bVi c

Fowler, Lindley, and Wadler

90:47

→
−
for each Vi ∈ V .
We need to show that regardless of the position of the partition between the save queue
and mailbox, the resulting configuration is well typed.
→
−
Subcase D = ha, bM c [ ], b V ci,
By the substitution lemma it follows that
bΓc, a : ActorRef(h`i : bAi cii ) | List(h`i : bAi ci i) ` bM c [ ] : 1
→
−
By Actor, we can show bΓc; a : ActorRef(h`i : bAi cii ); a : h`i : bAi cii ` ha, bM c [ ], V i
as required.
For the remainder of the cases, we establish our result by induction on i.
Base case i = 1:
We can show that
bΓc, a : ActorRef(h`i : bAi cii ) ` bV1 c : h`i : bAi ci i
and thus that
bΓc, a : ActorRef(h`i : bAi cii ) ` [bV1 c] : List(h`i : bAi cii )
Similarly, we have that
(Γ, a : ActorRef(h`i : bAi cii ) ` bVj c : h`i : bAi cii )j∈2..n
−
→
Let us refer to this sequence as V 0 . Thus we can show:
−
→
bΓc, a : ActorRef(h`i : bAi cii ); a : h`i : bAi ci i ` ha, bM c [bV1 c], V 0 i
as required.
Inductive case i = j + 1:
By the inductive hypothesis, we have that
−→ −→
bΓc, a : h`i : bAi cii ; a : h`i : bAi cii ` ha, bM c Wj , Wj0 i
where:
−→
Wj = bV1 c :: . . . :: bVj c :: [ ]
−→0
Wj = bVj+1 c · . . . · bVn c
By Actor, we have that
−→
bΓc; a : h`i : bAi cii | h`i : bAi cii ` bM c Wj : 1
and thus that
−→
bΓc, a : ActorRef(h`i : bAi cii ) ` Wj : List(h`i : bAi cii )
We also have that
(bΓc, a : ActorRef(h`i : bAi cii ) ` bVk c : h`i : bAi ci i)k∈j+1..n
Thus we can show that
bΓc, a : ActorRef(h`i : bAi cii ) ` bV1 c :: . . . :: bVj c :: bVj+1 c :: [ ] : List(h`i : bAi cii )

ECOOP 2017

90:48

Mixing Metaphors

It also remains the case that
(bΓc, a : ActorRef(h`i : bAi ci i) ` bVk c)k∈j+2..n
Therefore we can show that
bΓc, a : ActorRef(h`i : bAi cii ); a : h`i : bAi cii ` ha, bM c bV1 c :: . . . :: bVj c :: bVj+1 c :: [ ], bVj+2 c·. . .·bVn ci
completing the induction.

J

Fowler, Lindley, and Wadler

B.5.2

90:49

Simulation of selective receive

I Lemma 43. Simulation (λact with selective receive in λact —terms) If Γ ` M : A and
0
M −→M M 0 , then given some α, it is the case that bM cα −→+
M bM cα.
Proof. A straightforward induction on M −→M M 0 .

J

I Lemma 44. If Γ `P M : A and M −→∗M return V , then bM c mb −→∗M return (bV c, mb) for
any mb.
Proof. By the definition of −→∗M , we have that there exists some reduction sequence M −→M
M1 −→M · · · −→M Mn −→M return V .
The result follows by repeated application of Lemma 43.
J
I Lemma 45. Suppose V = h` = V 0 i.
−c , V )), then
If Γ ` V : A and ¬(matchesAny(→
−c , mb, default)} −→+ default h` = bV 0 ci.
case h` = bV 0 ci {branches(→
M
−c , V )), we must have that for all
Proof. (Sketch.) For it to be the case that ¬(matchesAny(→
−c where c = h` = x i when M 7→ N :
ci ∈ →
i
i
i
i
i
`i =
6 `, or
`i = `, but Mi {V 0 /xi } −→+
M false.
Recall that
−c , mb, default) , patBranches(→
−c , mb, default)·defaultBranches(→
−c , mb, default)
branches(→
−c , then there will be no corresponding branch in patBranches,
If ` =
6 `i for any pattern in →
but there will be a branch h` = xi 7→ default (` = x) in defaultBranches, reducing to the
required result default h` = bV ci.
→
−
−c such that for each
On the other hand, suppose we have a set of clauses c0 ⊆ →
→
−
(h`0 = xj i when Mj 7→ Nj )j ∈ c0 , it is the case that `0 = `. Then, it must be the case that
for all Mj , that Mj {V 0 /xj } −→+
M false.
→
−
The result can now be established by induction on the length of c0 , by the definition
of ifPats. For the base case, we have default h` = V 0 i immediately, as required. For the
inductive cases, we note that by Lemma 44, each guard bMj c mb −→∗M return (false, mb), and
thus that each ifPats clause will proceed inductively (taking the “else” branch) until the
base case is reached.
J
I Lemma 46. Suppose:
−c = {(h` = x when M i) 7→ N }
We have a consistent set of patterns →
a
a
a
a a
→
−
∃k, l.∀i.i < k.¬(matchesAny( c , Vi )) ∧ matches(cl , Vk ) ∧ ∀j.j < l ⇒ ¬(matches(cj , Vk )).
Γ ` Vk : A
Vk = h` = Vk0 i
Then:
−c , mb, default}) −→+ (bN c mb){bV 0 c/x }
case h`k = Vk0 i {branches(→
l
l
k
M

ECOOP 2017

90:50

Mixing Metaphors

Proof. (Sketch.) Recall that
−c , mb, default) , patBranches(→
−c , mb, default)·defaultBranches(→
−c , mb, default)
branches(→
If matches(cl , Vk ), then it must be the case that cl is of the form {h`k = xl i when Ml 7→ Nl },
with Ml {Vk0 /xl } −→∗M true.
−
c` where
By the definition of patBranches, we know that there exists an ordered list →
→
−
→
−
→
−
c` ⊆ c , and label(c) = `k ; therefore we have that cl ∈ c` .
−
Again, we proceed by induction on the length of →
c` . We know that ∀j.j < l ⇒
−
∗
¬(matches(cj , Vk )), and therefore that Mj −→M return false. Since →
c` is ordered, by Lemma 44,
∗
we have that bM c mb{bVk c/xj } −→M return (false, mb), and proceed inductively. For
ifPats(mb, `, y, cl · pats, default), it will be the case (again by Lemma 44) that bMl cmb −→M
return (true, mb). Reducing, we take the true branch of the if-statement, and arrive at
(bNl cmb){bVk c/xl } as required.
J
Theorem 33 (Simulation (λact with selective receive in λact )) If Γ; ∆ ` C and
C −→ C 0 , then ∀D ∈ bCc, there exists a D0 such that D −→+ D0 .

Proof. By induction on the derivation of C −→ C 0 .
The configuration of the save queue and mailbox are irrelevant to all reductions except
Receive, so we will show the case where the save queue is empty; the other cases follow
exactly the same pattern.
Case Spawn
→
−
We assume that Γ; ∆ ` ha, E[spawn M ], V i.

Assumption
Def. b−c
−→
−→M
=

→
−
ha, E[spawn M ], V i
→
−
ha, bEc[let spawnRes ⇐ spawn (bM c [ ]) in return (spawnRes, [ ])], V i
→
−
(νb)ha, bEc[let spawnRes ⇐ return b in return (spawnRes, [ ])], V i
k hb, bM c[ ], i
→
−
(νb)ha, bEc[return (b, [ ])], V i k hb, bM c[ ], i
→
−
(νb)ha, E[return b], V i k hb, M, i

(1)
(2)
(3)
(4)
(5)

Case Send
→
−
−
→
We assume that Γ; ∆ ` ha, E[send V 0 b], V i k hb, M, W i.

Assumption
Def. b−c
−→
−→M
=

→
−
−
→
ha, E[send V 0 b], V i k hb, M, W i
→
−
−
→
ha, bEc[let x ⇐ send bV 0 c b in (x, [ ])], b V ci k hb, bM c [ ], bW ci
→
−
−
→
ha, bEc[let x ⇐ return () in (x, [ ])], b V ci k hb, bM c [ ], bW c · bV 0 ci
→
−
−
→
ha, bEc[return ((), [ ])], b V ci k hb, bM c [ ], bW c · bV 0 ci
→
−
−
→
ha, E[return ()], V i k hb, M, W · V 0 i

Case SendSelf
→
−
We assume that Γ; ∆ ` ha, E[send V a], V i.

(1)
(2)
(3)
(4)

Fowler, Lindley, and Wadler

Assumption
Def. b−c
−→
−→M
=

→
−
ha, E[send W a], V i
→
−
ha, bEc[let x ⇐ send bW c a in return (x, [ ]), b V ci
→
−
ha, bEc[let x ⇐ return () in return (x, [ ])], b V c · bW ci
→
−
ha, bEc[return ((), [ ])], b V c · bW ci
→
−
ha, E[return ()], V · W i

90:51

(1)
(2)
(3)
(4)
(5)

Case Self
→
−
We assume that Γ; ∆ ` ha, E[self], V i.

Assumption
Def. b−c
−→
−→M
=

→
−
ha, E[self], V i
→
−
ha, (bEc[let selfPid ⇐ self in return (selfPid, [ ])]), b V ci
→
−
ha, (bEc[let selfPid ⇐ return a in return (selfPid, [ ])]), b V ci
→
−
ha, (bEc[return (a, [ ])]), b V ci
→
−
ha, E[return a], V i

(1)
(2)
(3)
(4)
(5)

Case Lift
Immediate by the inductive hypothesis.
Case LiftM
Immediate by Lemma 43.
Case Receive
The interesting case is the translation of selective receive. We sketch the proof as follows.
−
−c }], →
We assume that Γ; ∆ ` ha, E[receive {→
V i, where:
→
−
V = V1 · . . . · Vn
→
−c = {h` = x i when M −→∗ N }
i
i
i
i i
M
By the assumptions of the reduction rule, we also have that there exists some Vk and cl
such that:
−c .
For all i < k, Vi does not match any pattern in →
Vk matches cl .
For all j < l, it is the case that Vk does not match ck .
Thus intuitively, Vk is the first value in the mailbox to match any of the patterns.
By the definition of b−c, we have several possible configurations of the save queue and
the mailbox to consider. More specifically:
−
−c , [ ]), b→
ha, find(→
V ci
→
−→
−
→
−
−c , W 1 ), W→2 i | 1..n}, where −
{ha, find(→
Wi1 = bV1 c :: . . . :: bVi c :: [ ], and Wi2 =
i
i
bVi+1 c · . . . · bVn c,
→
−
→
−c , [ ]), b−
Subcase 1 We have ha, find(→
V1 c · . . . · Vk · . . . · V2 i. Expanding find, we have:

ECOOP 2017

90:52

Mixing Metaphors

−
→
−
→
ha, E[ (rec findLoop(ms) .
], bV1 c · . . . · bVk c · . . . · bV2 ci
let (mb1 , mb2 ) = ms in
case mb2 {
−c , mb )
[ ] 7→ loop(→
1
0
x :: mb2 7→
let mb0 ⇐ mb1 ++ mb02 in
−c , mb0 ,
case x {branches(→
λy.(let mb01 ⇐ mb1 ++ [y] in
findLoop (mb01 , mb02 )))}) ([ ], [ ])
After reducing the application of the recursive function, the pair deconstruction, and the
case split, we have:
→
−
→
−c , [ ])], b−
ha, E[loop(→
V1 c · . . . · bVk c · . . . · bV2 ci
Expanding loop and branches, we have:

ha, E[

−
→
−
→
(rec recvLoop(mb) .
], bV1 c · . . . · bVk c · bV2 ci
let x ⇐ receive in
case x {
−c , mb, default) ·
patBranches(→
−c , mb, default)
defaultBranches(→
}) [ ]

where default = λy.let mb’ ⇐ mb ++ [y] in recvLoop mb0 .
−
→
−c , V ) for all i < k.
Recall that bV1 c = bV1 c · . . . · bVk−1 c, and we have that ¬(matchesAny(→
i
By Lemma 45, we have that
−c , mb)} −→∗ default V
case Vi {branches(→
i
M
In this case, default appends the current value onto the end of the save queue, and calls
recvLoop recursively. Thus, proceeding inductively, we can show that we arrive at
−
→
−c , bV c :: . . . :: bV
ha, E[loop(→
1
k−1 c :: [ ])], bVk c · bV2 ci
Expanding, we see

ha, E[

−
→
(rec recvLoop(mb) .
], bVk c · bV2 ci
let x ⇐ receive in
case x {
−c , mb, default) ·
patBranches(→
−c , mb, default)
defaultBranches(→
}) (bV1 c :: . . . :: bVk−1 c :: [ ])

Reducing the function application and the receive from the mailbox:
−
→
−c , (bV c :: . . . :: bV
ha, E[case bVk c {branches(→
1
k−1 c :: [ ]), default)}], bV2 ci

Fowler, Lindley, and Wadler

90:53

Now, by Lemma 46, we have that
−
→
ha, E[(bNl c bV1 c :: . . . :: bVk−1 c){bVk0 c/xl }], bV2 ci
where bVk c = h`k = bVk0 ci.
−
→
−
→
It follows that this is in bha, E[Nl {bVk0 c/xl }], bV1 c · bV2 cic, concluding this subcase.
Subcase 2: In this subcase, we examine the case where the save queue is initially nonempty. Pick some arbitrary j ∈ 1 . . . n. Let:
−→
bW1 c = bV1 c :: . . . :: bVj c :: [ ]
−→
bW2 c = bVj+1 c · . . . · bVn c
→
−→
−c , [b−
W1 c])], bW2 ci. We now have two possible scenarios: k ≤ j, or
We have ha, E[find(→
k > j.
Expanding find, we have:

ha, E[ (rec findLoop(ms) .
let (mb1 , mb2 ) = ms in
case mb2 {
−c , mb )
[ ] 7→ loop(→
1
0
x :: mb2 7→
let mb0 ⇐ mb1 ++ mb02 in
−c , mb0 ,
case x {branches(→
0
λy.(let mb1 ⇐ mb1 ++ [y] in

−→
], bW2 ci

−→
findLoop (mb01 , mb02 )))}) ([ ], bW1 c)

Define fLoop as follows:
fLoop(mb1 , mb2 ) , (rec findLoop(ms) .
let (mb1 , mb2 ) = ms in
case mb2 {
−c , mb )
[ ] 7→ loop(→
1
0
x :: mb2 7→
let mb0 ⇐ mb1 ++ mb02 in
−c , mb0 ,
case x {branches(→
0
λy.(let mb1 ⇐ mb1 ++ [y] in
fLoop (mb01 , mb02 )))}) (mb1 , mb2 )
After reducing the application of the recursive function and the pair deconstruction we
have:
Subsubcase k ≤ j:
Our reasoning is similar to in the first subcase. We appeal to repeated applications of
Lemma 45 and arrive at
−→
−−→
−−−→
ha, bEc[fLoop(bW10 c, bVk c :: bW100 c)], bW2 ci
−−→
−→
where bW10 c = bV1 c :: . . . :: bVk−1 c and bW200 c = bVk+1 c :: . . . :: bVj c.

ECOOP 2017

90:54

Mixing Metaphors

Expanding, we have
−→
], bW2 ci

ha, E[ (rec findLoop(ms) .
let (mb1 , mb2 ) = ms in
case mb2 {
−c , mb )
[ ] 7→ loop(→
1
0
x :: mb2 7→
let mb0 ⇐ mb1 ++ mb02 in
−c , mb0 ,
case x {branches(→
0
λy.(let mb1 ⇐ mb1 ++ [y] in

−→
−−→
findLoop (mb01 , mb02 )))}) (bW10 c, bVk c :: bW100 c)

Reducing the recursive function application, pair split, and case expression, we have:
→
−−→
−→
−c , b−
ha, E[case bVk c {branches(→
W10 c ++ bW100 c, default}], bW2 ci
where
−→
default = λy.(let mb01 ⇐ bW10 c ++ [y] in
−−→
fLoop (mb01 , bW100 c))})
Now, by Lemma 46, we have
−→
−−→
−→
ha, bEc[(bNl c (bW10 c ++ bW100 c)){bVk0 c/xl }], bW2 ci
which is in
−
→ −
→
bha, E[Nl {Vk0 /xl }], V1 · V2 ic
as required.
Subsubcase k > j:
As before, we appeal to repeated applications of Lemma 45, this time arriving at:
−−−→
−→
ha, bEc[fLoop(bW1 c, [ ])], bW2 ci
Expanding, we have:

ha, E[ (rec findLoop(ms) .
let (mb1 , mb2 ) = ms in
case mb2 {
−c , mb )
[ ] 7→ loop(→
1
0
x :: mb2 7→
let mb0 ⇐ mb1 ++ mb02 in
−c , mb0 ,
case x {branches(→
0
λy.(let mb1 ⇐ mb1 ++ [y] in

−→
], bW2 ci

−→
findLoop (mb01 , mb02 )))}) (bW1 c, [ ])

Evaluating the application of the recursive function, the pair split, and the case statement,
we have:

Fowler, Lindley, and Wadler

90:55

→
−→
−c , b−
ha, E[loop(→
W1 ]c]), bW2 ci
Expanding loop, we have:

ha, bEc[

−→
(rec recvLoop(mb) .
], bW2 ci
let x ⇐ receive in
case x {
−c , mb, default) ·
patBranches(→
−c , mb, default)
defaultBranches(→
−→
}) bW1 c

with
default = λy.let mb0 ⇐ mb ++ [y] in recvLoop mb0
Again by repeated applications of Lemma 45, we arrive at
−→
−−→
→
−c , b−
ha, bEc[loop(→
W1 c ++ bW20 c)], bVk c · bW200 ci
−→
−−→
where bW20 c = bVj+1 c :: . . . :: bVk−1 c, and bW200 c = bVk+1 c · . . . · bVn c.
Now, expanding again, we have:

ha, bEc[

−−→
], bVk c · bW200 ci
(rec recvLoop(mb) .
let x ⇐ receive in
case x {
−c , mb, default) ·
patBranches(→
−c , mb, default)
defaultBranches(→
−→0
−→
}) (bW1 c ++ bW2 c)

reducing the recursive function, receive, and case expression, we have:
−→
−−→
→
−c , (b−
ha, bEc[case bVk c {branches(→
W1 c ++ bW20 c), default)}], bW200 ci
Now, by Lemma 46, we have
−→
−−→
−→
ha, bEc[(bNl c (bW1 c ++ bW10 c)){bVk0 c/xl }], bW200 ci
which is in
−
→ −
→
bha, E[Nl {Vk0 /xl }], V1 · V2 ic
as required.

J

ECOOP 2017

