Using session types as an effect system
Dominic Orchard

Nobuko Yoshida

Imperial College London, UK

Imperial College London, UK

Side effects are a core part of practical programming. However, they are often hard to reason about,
particularly in a concurrent setting. We propose a foundation for reasoning about concurrent side
effects using sessions. Primarily, we show that session types are expressive enough to encode an
effect system for stateful processes. This is formalised via an effect-preserving encoding of a simple
imperative language with an effect system into the π-calculus with session primitives and session
types (into which we encode effect specifications). This result goes towards showing a connection
between the expressivity of session types and effect systems. We briefly discuss how the encoding
could be extended and applied to reason about and control concurrent side effects.

1

Introduction

Side effects such as input-output and mutation of memory are important features of practical programming. However, effects are often difficult to reason about due to their implicit impact. Reasoning about
effects is even more difficult in a concurrent setting, where interference may cause unintended nondeterminism. For example, consider a parallel program: put x ((get x) + 2) | put x ((get x) + 1) where x is
a mutable memory cell. Given an initial assignment x 7→ 0, the final value stored at x may be any of 3, 2,
or 1 since calls to get and put may be interleaved.
Many approaches to reasoning, specifying, and controlling the scope of effects have therefore been
proposed. Seemingly orthogonally, various approaches for specifying and reasoning about concurrent interactions have also been developed. In this paper, we show that two particular approaches for reasoning
about effects and concurrency are in fact non-orthogonal; one can be embedded into the other. We show
that session types [12] for concurrent processes are expressive enough to encode effect systems [3, 11]
for state. We formalise this ability by embedding/encoding a simple imperative language with an effect
system into the π-calculus with session types: sessions simulate state and session types become effect
annotations. Formally, our embedding maps type-and-effect judgements to session type judgements:
Γ ` M : τ, F

embedding

−
−−−−−
→

JΓK; res : !JτK.end, eff : JFK ` JMK

(1)

That is, an expression M of type τ in context Γ performing effects F, is mapped to a process JMK
which sends its result over session channel res and simulates effects by interactions JFK (defined by an
interpretation of the effect annotation) over session channel eff.
We start with the traditional encoding of a mutable store into the π-calculus (Section 2) and show
how its session types provide a kind of effect system. Section 2 introduces a simple imperative language,
which we embed into the π-calculus with sessions (sometimes called the session calculus) (Section 3).
The embedding is shown sound with respect to an equational theory for the imperative language. Section 4 discusses how to extend the encoding to parallel composition in the imperative language and how
the effect information can be used to safely introduce implicit parallelism in the encoding.
Update: since PLACES’15, this work has been greatly expanded upon. Much of the further work suggested in this paper is
covered in our later paper Effects as Sessions, Sessions as Effects (Orchard, Yoshida) appearing in the proceedings of POPL’16.
S. J. Gay and J. Alglave (Eds.): Programming Language Approaches to
Concurrency- and Communication-Centric Software (PLACES 2015).
EPTCS 203, 2016, pp. 1–13, doi:10.4204/EPTCS.203.1

2

Using session types as an effect system

Our embedding has been partly formalised in Agda and is available at https://github.com/dorchard/
effects-as-sessions (Appendix B gives a brief description). This is used to verify the syntactic soundness of the embedding (essentially, that types and effects are correctly translated and preserved).
The main result of this paper is foundational and technical, about the expressive power of the πcalculus with session primitives and session types. This result has a number of possible uses:
• Effects systems for the π-calculus: rather than adding an additional effect system on top of the
π-calculus, we show that existing work on session types can be reused for this purpose.
• Semantics of concurrency and effects: our approach provides an intermediate language for the
semantics of effects in a concurrent setting.
• Compilation: Related to the above, the session calculus can be used as a typed intermediate language for compilation, where our embedding provides the translation. Section 4 demonstrates an
optimisation step where safe implicit parallelism is introduced based on effect information and
soundness results of our embedding.
Effect systems have been used before to reason about effects in concurrent programs. For example,
Deterministic Parallel Java uses an effect system to check that parallel processes can safely commute
without memory races, and otherwise schedules processes to ensure determinism [1]. Our approach
allows state effects to be incorporated directly into concurrent protocol descriptions, reusing session
types, without requiring interaction between two distinct systems.

2

Simulating state with sessions

2.1 State via processes A well-known way to implement state in a process algebra is to represent a
mutable store as a server-like process (often called a variable agent) that offers two modes of interaction
(get and put). In the get mode, the agent waits to receive a value on its channel which is then “stored”; in
the put it sends the stored value. This can be implemented in the π-calculus with branching and recursive
definitions as follows (Figure 1 describes the syntax; the calculus is based on the second system in [12]
using the dual channels from [6] instead of a polarity-based approach):
def Store(x, c) = c B {get : c!hxi.Storehx, ci, put : c?(y).Storehy, ci, stop : 0} in Storehi, eff i

(2)

where Store is parameterised by the stored value x and a session channel c. That is, Store provides a
choice (by B) over channel c between three behaviours labelled get, put, and stop. The get branch sends
the state x on c and then recurses with the same parameters, preserving the stored value. The put branch
receives y which then becomes the new state by continuing with recursive call Storehy, ci. The stop
branch provides finite interaction by terminating the agent. The store agent is initialised with a value i
and channel eff .
The following parameterised operations get and put then provide interaction with the store:
get(c)(x).P = c C get . c?(x).P

put(c)hV i.P = c C put . c!hV i.P

(3)

where c is the opposite endpoint of a channel, and get selects (by the C operator) the get branch then
receives a value which is bound to x in the scope of P. The put operation selects its relevant branch then
sends a value V before continuing as P.
A process can then use get and put for stateful computation by parallel composition with Store, e.g.
get(eff )(x).put(eff )hx + 1i.end | Storehi, eff i increments the initial value.

Dominic Orchard and Nobuko Yoshida

3

(value variables) v ::= x, y, z
(session channel variables) c, d, c, d
(values)
V ::= C | v
constants / variables
(processes) P, Q ::= c?(x).P
| c!hV i.P
receive / send
| c?(d).P
| c!hdi.P
channel receive / send
| c B {l˜ : P̃}
| c C l.P
branching / selection
| def X(x̃, c̃) = P in Q | XhṼ , c̃i
recursive definition / use
| νc.P
channel restriction
| (P | Q)
parallel composition
| 0
nil process
(value-types) τ ::= unit | nat | S
(contexts) Γ ::= 0/ | Γ, x : τ | Γ, X : (τ̃, S̃)
(l ranges over labels, l˜ : P̃ over sequences of label-process pairs, and ẽ over syntax sequences)
Figure 1: Syntax of π-calculus with recursion and sessions
2.2 Session types Session types provide descriptions (and restrictions) of the interactions that take
place over channels [12]. Session types record sequences of typed send (![τ]) and receive (?[τ]) interactions, terminated by the end marker, branched by select (⊕) and choice (&) interactions, with cycles
provided by a fixed point µα and session variables α:
S, T ::= ![τ].S | ?[τ].S | ⊕[l1 : S1 , . . . , ln : Sn ] | &[l1 : S1 , . . . , ln : Sn ] | µα.S | α | end
where τ ranges over value types nat, unit and session channels S, and l ranges over labels.
Figure 2 (p. 4) gives the rules of the session typing system (based on that in [12]). Session typing
judgements for processes have the form Γ; ∆ ` P meaning a process P has value variables Γ = x1 :
τ1 . . . xn : τn and session-typed channels ∆ = c1 : S1 , . . . cn : Sn .
For a session S, its dual S is defined in the usual way [12]:
![τ].S =?[τ].S ?[τ].S =![τ].S µα.S = µα.S α = α end = end
⊕[l1 : S1 , . . . , ln : Sn ] = &[l1 : S1 , . . . , ln : Sn ] &[l1 : S1 , . . . , ln : Sn ] = ⊕[l1 : S1 , . . . , ln : Sn ]
For some state type τ and initial value i : τ, the Store process (2) has session judgement:
Γ; eff : µα. &[get : ![τ].α, put :?[τ].α, stop : end] ` Storehi, eff i
That is, eff is a channel over which there is an sequence of offered choice between the get branch, which
sends a value, put branch which receives a value, and is terminated by the stop branch.
The session judgements for get and put (3) are then:
Γ, x : τ; ∆, eff : S ` P
Γ; ∆, eff : ⊕[get : ?[τ].S] ` get(eff )(x).P

Γ; 0/ ` V : τ Γ; ∆, eff : S ` P
Γ; ∆, eff : ⊕[put : ![τ].S] ` put(eff )hV i.P

(4)

We use a variant of session typing where selection terms B, used by get and put, have a selection session
type ⊕ with only the selected label (seen above), and not the full range of labels offered by its dual
branching process, which would be ⊕[get :?[τ].S, put :![τ].S, stop : end] for both. Duality of select and
branch types is achieved by using session subtyping to extend select types with extra labels [2] (see
Appendix A for details).
Throughout we used the usual convention of eliding a trailing 0, e.g., writing r!hxi instead of r!hxi.0,
and likewise for session types, e.g., ![τ] instead of ![τ].end.

4

Using session types as an effect system

Γ; ∆ ` V : τ (value typing) (const)

v:τ ∈Γ
C : Cτ
Γ; 0/ ` V : nat
(var)
(suc)
Γ; 0/ ` C : Cτ
Γ; 0/ ` v : τ
Γ; 0/ ` sucV : nat

Γ; ∆ ` P
(end) Γ; c̃ : end ` 0

(def)

(par)

(process typing)

Γ; ∆1 ` P Γ; ∆2 ` Q
Γ; ∆1 , ∆2 ` P | Q

Γ, X : (τ̃, S̃), x̃ : τ̃; c̃ : S̃ ` P
Γ, X : (τ̃, S̃); ∆ ` Q
Γ; ∆ ` def X(x̃, c̃) = P in Q

(chan-recv)

Γ; ∆, c : T, d : S ` P
Γ; ∆, c :?[S].T ` c?(d).P

(recv)

(branch)

Γ, x : τ; ∆, c : S ` P
Γ; ∆, c :?[τ].S ` c?(x).P

(dvar)

Γ; ∆, c : Si ` Pi
Γ; ∆, c : &[l˜ : S̃] ` c B {l˜ : P̃}

Γ; ∆, c : S, c : S ` P
Γ; ∆ ` νc.P

Γ; 0/ ` Ṽ : τ̃
Γ, X : (τ̃, S̃); c̃ : S̃, d˜ : end ` XhṼ , c̃i

(chan-send)

(send)

(restrict)

Γ; ∆, c : T ` P
Γ; ∆, c : ![S].T, d : S ` c!hdi.P

Γ; 0/ ` V : τ Γ; ∆, c : S ` P
Γ; ∆, c : ![τ].S ` c!hV i.P

(select)

Γ; ∆, c : S ` P
Γ; ∆, c : ⊕[l : S] ` c C l.P

where x̃ : τ̃ is shorthand for a sequence of variable-type pairs, and similarly c̃ : S̃ for channels, l˜ : S̃
for labels and sessions, and Ṽ for a sequence of values.
Figure 2: Session typing relation over the π-calculus with recursion and sessions [12].
2.3 Effect systems Effect systems are a class of static analyses for effects, such as state or exceptions [3, 7, 11]. Traditionally, effect systems are described as syntax-directed analyses by augmenting
typing rules with effect judgements, i.e., Γ ` M : τ, F where F describes the effects of M – usually a set
of effect tokens (but often generalised, e.g., in [7], to arbitrary semi-lattices, monoids, or semirings).
We define the effect calculus, a simple imperative language with effectful operations and a typeand-effect system defined in terms of an abstract monoidal effect algebra. Terms comprise variables,
let-binding, operations, and constants, and types comprise value types for natural numbers and unit:
M, N ::= x | let x ← M in N | op M | c

τ, σ ::= unit | nat

where x ranges over variables, op over unary operations, and c over constants. We do not include function
types as there is no abstraction (higher-order calculi are discussed in Section 5). Constants and operations
can be effectful and are instantiated to provide application-specific effectful operations in the calculus.
As defaults, we include zero and unit constants 0, unit ∈ c and a pure successor operation for natural
numbers suc ∈ op.
Definition 1 (Effect system). Let F be a set of effect annotations with a monoid structure (F , •, I)
where • combines effects (corresponding to sequential composition) and I is the trivial effect (for pure
computation). Throughout F, G, H will range over effect annotations.
Figure 3 defines the type-and-effect relation. The (var) rule marks variable use as pure (with I). In
(let), the left-to-right evaluation order of let-binding is exposed by the composition order of the effect

Dominic Orchard and Nobuko Yoshida

(var)

x:τ ∈Γ
Γ ` x : τ, I

(let)

5

Γ ` M : σ , F Γ, x : σ ` N : τ, G
(const)
Γ ` let x ← M in N : τ, F • G
Γ ` c : Cτ ,CF

(op)

Γ ` M : Opσ , I
Γ ` op M : Opτ , OpF

Figure 3: Type-and-effect system for the effect calculus
F of the bound term M followed by effect G of the let-body N. The (const) rule introduces a constant
of type Cτ with effects CF , and (op) applies an operation to its pure argument of type Opσ , returning a
result of type Opτ with effect OpF .
2.4 State effects The effect calculus can be instantiated with different notions of effect. For state, we
use the effect monoid (List {G τ, P τ}, ++, [ ]) of lists of effect tokens, where G and P represent get and
put effects parameterised by a type τ, ++ concatenates lists and [ ] is the empty list. Many early effect
systems annotated terms with sets of effects. Here we use lists to give a more precise account of state
which includes the order in which effects occur. This is often described as a causal effect system.
Terms are extended with constant get and unary operation put where 0/ ` get : τ, [G τ] and Γ ` put M :
unit, [P τ] for Γ ` M : τ, I. For example, the following is a valid judgement:
0/ ` let x ← get in put (suc x) : nat, [G nat, P nat]

(5)

Type safety of the store is enforced by requiring that any get effects must have the same type as their
nearest preceding put effect. We implicitly apply this condition throughout.
2.5 Sessions as effects The session types of processes interacting with Store provide the same information as the state effect system. Indeed, we can define a bijection between state effect annotations and
the session types of get and put (4):
J[ ]K = end

J(G τ) :: FK = ⊕[get :?[τ].JFK]

J(P τ) :: FK = ⊕[put : ![τ].JFK]

(6)

where :: is the cons operator for lists. Thus processes interacting with Store have session types corresponding to effect annotations. For example, the following has the same state semantics as (5) and
isomorphic session types:
0;
/ eff : J[G nat, P nat]K ` get(eff )(x).put(eff )hsuc xi

3

(7)

Embedding the effect calculus into the π-calculus

Our embedding is based on the embedding of the call-by-value λ -calculus (without effects) into the
π-calculus [5, 10] taking let x ← M in N = (λ x.N) M. Since effect calculus terms return a result and
π-calculus processes do not, the embedding is parameterised by a result channel r over which the return
value is sent, written J−Kr . Variables and pure let-binding are embedded:
Jlet x ← M in NKr = νq. (JMKq | q?(x).JNKr )

JxKr = r!hxi

(8)

Variables are simply sent over the result channel. For let, an intermediate channel q is created over which
the result of the bound term M is sent by the left-hand parallel process JMKq and received and bound to

6

Using session types as an effect system

x by the right-hand process before continuing with JNKr . This enforces a left-to-right, CBV evaluation
order (despite the parallel composition).
Pure constants and unary operations can be embedded similarly to variables and let given suitable
value operations in the π-calculus. For example, successor and zero are embedded as:
Jsuc MKr = νq. (JMKq | q?(x).r!hsuc xi)

JzeroKr = r!hzeroi

(9)

Given a mapping J−K from effect calculus types to corresponding value types in the π-calculus, the above
embedding of terms (8),(9) can be extended to typing judgements as follows (where JΓK interprets the
type of each free-variable assumption pointwise, preserving the structure of Γ):
JΓ ` M : τKr = JΓK; r : !JτK.end ` JMKr

(10)

With effects Our approach to embedding effectful computations is to simulate effects by interacting
with an effect-handling agent over a session channel. The embedding, written J−Keff
r , maps a judgement
Γ ` M : τ, F to a session type judgement with channels ∆ = (r : !JτK.end, eff : JFK), i.e., the effect
annotation F is interpreted as the session type of channel eff . For state, this interpretation is defined as
in eq. (6). The embedding first requires an intermediate step, written L − Mei,eo
r
= ∀g. JΓK; r : !JτK, ei : ?JF • gK, eo :!JgK ` L M Mei,eo
L Γ ` M : τ, F Mei,eo
r
r

(11)

where ei and eo are channels over which channels for simulating effects (which we call effect channels)
are communicated: ei receives an effect channel of session type JF • gK (i.e., capable of carrying out
effects F • g) and eo sends a channel of session type JgK (capable of carrying out effects g). Here the
effect g is universally quantified at the meta level. This provides a way to “thread” a channel for effect
interactions through a computation, such as in the case of let-binding (see below).
The embedding of effect calculus terms is then defined:
)
L let x ← M in N Mei,eo
= νq, ea . (L M Mei,ea
| q?(x).L N Mea,eo
r
r
q
L x Mei,eo
= ei?(c).r!hxi.eo!hci
r

LC Mei,eo
= ei?(c).JCKr .eo!hci
r

L op M Mei,eo
r

= ei?(c).Jop MKr .eo!hci

(when C is pure)
(when op is pure)

(12)

The embedding of variables is straightforward, where an effect channel c is received on ei and then sent
without use on eo. Embedding pure operations and constants is similar, reusing the pure embedding
defined above in equation (9).
The let case resembles the pure embedding of let, but threads through an effect channel to each subexpression. An intermediate channel ea is introduced over which an effect channel is passed from the
embedding of M to N. Let Γ ` M : σ , F and Γ, x : σ ` N : τ, G then in the embedding of let x ← M in N
the universally quantified effect variable ∀g for L M Mei,ea
is instantiated to G • h. The following partial
q
session-type derivation for the let encoding shows the propagation of effects via session types:
,ea
q :!Jσ K, ei :?JF • gK, ea :!JgK ` L M Mei
g 7→ G • h
q

q :!Jσ K, ei :?JF • (G • h)K, ea :!JG • hK ` L M Mqei,ea

,eo
q :?Jσ K, r :!JτK, ea :?JG • hK, eo :!JhK ` q?(x).L N Mea
r

,eo
r :!JτK, ei :?JF • (G • h)K, eo :!JhK, q :!Jσ K, q :?Jσ K, ea :!JG • hK, ea :?JG • hK ` L M Mqei,ea | q?(x).L N Mea
r
,eo
r :!JτK, ei :?J(F • G) • hK, eo :!JhK ` νq, ea. (L M Mqei,ea | q?(x).L N Mea
)
r

Dominic Orchard and Nobuko Yoshida

7

Associativity of • is used in the last rule to give the correct typing for the embedding of let.
The get and put operations of our state effects are embedded similarly to equation (3) (page 2), but
with the receiving and sending of the effect channel which is used to interact with the store:
L get Mei,eo
= ei?(c).c C get . c?(x).r!hxi.eo!hci
r

L put M Mei,eo
= νq. (JMKq | ei?(c).q?(x).c C put . c!hxi.r!huniti.eo!hci)
r

(13)

The embedding of get receives channel c over which it performs its effect by selecting the get branch
and receiving x which is sent as the result on r before sending c on eo. The put embedding is similar to
get and let, but using the pure embedding JMKq since M is pure. Again, the effect channel c is received
on ei and is used to interact with the store (the usual put action) before being sent on eo.
The full embedding is then defined in terms of the intermediate embedding L − M as follows:
ei,eo
JΓ ` M : τ, FKeff
| ei!heff i.eo?(c))
r = JΓK; r : !JτK, eff : JFK ` νei, eo. (L Γ ` M : τ, F Mr

(14)

where eff is the free session channel over which effects are performed. Note that c (received on eo) is
never used and thus has session type end.
Finally, the embedded program is composed in parallel with the variable agent, for example:
def Store(x, c) = . . . (see eq. (2)) in Storeh0, eff i | Jlet x ← get in put (suc x)Keff
r

(15)

3.1 Soundness The effect calculus exhibits the equational theory defined by the relation ≡ in Figure 4,
which enforces monoidal properties on effects and the effect algebra (assoc),(unitL),(unitR), and which
allows pure computations to commute with effectful ones (comm). Our embedding is sound with respect
to these equations up to weak bisimulation of session calculus processes (see, e.g. [4], for more on the
weak bisimulation relation).
Theorem 1 (Soundness). If Γ ` M ≡ N : τ, F then JΓK; (r :!JτK.end, e : JFK) ` JMKer ≈ JNKer
Appendix C gives the proof. Proof of soundness with respect to (comm) requires an additional restriction
on the effect algebra, that:
∀F, G. (F • G) ≡ I ⇒ (F ≡ G ≡ I)
(16)
That is, if the composition of two effects is pure, then both components are themselves pure. This is
equivalent to requiring that there are no inverse elements (with respect to •) in the effect set F . The state
effect system described here satisfies this additional effect-algebra condition since any two lists whose
concatenation is the empty list implies that both lists are themselves empty.
The soundness proof for (comm) is split into an additional lemma that shows the encoding of effectful
terms marked as pure with I can be factored through the encoding of pure terms (shown at the start of
Section 3). That is, in an appropriate session calculus context C, then:
C[L Γ ` M : τ, I Mei,eo
] ≈ C[ei?(c).eo!hci | JMKr ]
r
Thus, the intermediate encoding of a pure term is weakly bisimilar to a pure encoding (without effect
simulation) composed in parallel with a process which receives an effect-simulating channel c on ei and
sends it on eo without any use. Appendix C provides the details and proof.

8

Using session types as an effect system

(assoc)

Γ ` M : σ , F Γ, x : σ ` N : τ 0 , G Γ, y : τ 0 ` P : τ, H x 6∈ FV (P)
(let y ← (let x ← M in N) in P) ≡ (let x ← M in (let y ← N in P)) : τ, F • G • H

(unitL)

Γ ` x : σ , I Γ, y : σ ` M : τ, F
Γ ` (let y ← x in M) ≡ M[x/y] : τ, F

(comm)

(unitR)

Γ ` M : τ, F
Γ ` (let x ← M in x) ≡ M : τ, F

Γ ` M : τ1 , I
Γ ` N : τ2 , F
Γ, x : τ1 , y : τ2 ` P : τ, G x 6∈ FV (N) y 6∈ FV (M)
Γ ` let x ← M in (let y ← N in P) ≡ let y ← N in (let x ← M in P) : τ, F • G

Figure 4: Equations of the effect calculus

4

Discussion

Concurrent effects In a concurrent setting, side effects can lead to non-determinism and race conditions. For example, the program put (get + 2) | put (get + 1) has three possible final values for the store
due to arbitrarily interleaved get and put operations.
Consider an extension to the source language which adds an operator for parallel composition | (we
elide details of the type-and-effect rule, but an additional effect operator describing parallel effects can be
included). We might then attempt the following encoding, composing encodings of sub-terms in parallel:
eff
eff
JM | NKeff
r = νq1 , q2 . (JMKq1 | JNKq2 | q1 ?(x).q2 ?(y).r!h(x, y)i)

where q1 and q2 are the result channels for each term, from which the results are paired and sent over
r. This encoding is not well-typed under the session typing scheme: the (par) rule (see Figure 2, p. 4)
requires that the session channel environments of each process be disjoint, but eff appears on both sides.
Thus, session types naturally prevent effect interference.
Concurrent programs with effects can be encoded by extending our session calculus with shared
channels, which can be used in parallel and over which session channels are initiated [12]. Shared channels can be used in the encoding of effectful operations (get/put) to lock the store, providing atomicity
of each effectful interaction via the following redefinitions:
def Store(x, k) = accept k(c).c B {get : c!hxi.Storehx, ki, put : c?(y).Storehy, ki, stop : 0} in Storehi, ki
get(k)(x).P = request k(c).c C get . c?(x).P
put(k)hV i.P = request k(c).c C put . c!hV i.P
where k is a shared channel and request/accept initiate separate binary sessions between the store process and the effectful operations. This ensures atomicity of each side-effect interaction (selecting then
send/receiving). Note however that the type of k will describe the behaviour of all possible initiated
sessions. Via subtyping, this becomes ⊕[get :?[τ], put :![τ]] which conveys no information about which
effect operations occur, nor their ordering. This reflects the non-deterministic behaviour of concurrent
effects, where each effectful operation (as an atom) could be arbitrarily interleaved.
Further work is to study various other kinds of concurrent effect interaction that could be described
using the rich language of the session calculus and variations of our embedding.
Compiling to the session calculus One use for our embedding is as a typed intermediate language for
a compiler since the π-calculus with session primitives provides an expressive language for concurrency.
For example, even without explicit concurrency in the source language our encoding can be used to
introduce implicit parallelism as part of a compilation step via the session calculus. In the case of
compiling a term which matches either side of the (comm) rule above, a pure term M can be computed

Dominic Orchard and Nobuko Yoshida

9

in parallel with N, i.e., given terms Γ ` M : τ1 , I and Γ ` N : τ2 , F and Γ, x : τ1 , y : τ2 ` P : τ, G where
x 6∈ FV (N), y 6∈ FV (M) then the following specialised encoding can be given:
L let y ← N in (let x ← M in P) Mei,eo
=
r
ei,eo
L let x ← M in (let y ← N in P) Mr = ν q, s, ea. (JMKq | L N Mei,ea
| q?(x).s?(y).L P Mea,eo
)
s
r
This alternate encoding introduces the opportunity for parallel evaluation of M and N. It is enabled by
the effect system (which annotates M with I) and it is sound: it is weakly bisimilar to the usual encoding
(which follows from the soundness proof of (comm) in Appendix C).

5

Summary and further work

This paper showed that sessions and session types are expressive enough to encode stateful computations with an effect system. We formalised this via a sound embedding of a simple, and general, effect
calculus into the session calculus. Whilst we have focussed on causal state effects, our effect calculus
and embedding can also be instantiated for I/O effects, where input/output operations and effects have a
similar form to get/put. We considered only state effects on a single store, but traditional effect systems
account for multiple stores via regions and first-class reference values. Our approach could be extended
with a store and session channel per region or reference. This is further work. Other instantiations of our
effect calculus/embedding are further work, for example, for set-based effect systems.
Effect reasoning is more difficult in higher-order settings as the effects of abstracted computations
are locally unknown. Effect systems account for this by annotating function types with the latent effects
of a function which are delayed till application. A potential encoding of such types into session types is:
F

Jσ −
→ τK = !Jσ K . ![?JF • GK] . ![!JGK] . ![!JτK]
i.e., a channel over which four things can be sent: a Jσ K value for the function argument, a channel which
can receive an effect channel capable of simulating effects F • G, a channel over which can be sent an
effect channel capable of simulating effects G, and a channel which can send a JτK for the result. Thus,
the encoding of a function receives effect handling channels which have the same form as the effect
channels for first-order term encodings. A full, formal treatment of effects in a higher-order setting, and
the requirements on the underlying calculi, is forthcoming work.
Effects systems also commonly include a (partial) ordering on effects, which describes how effects
can be overapproximated [3]. For example, causal state effects could be ordered by prefix inclusion,
thus an expression M with judgement Γ ` M : τ, [G τ] might have its effects overapproximated (via
a subsumption rule) to Γ ` M : τ, [G τ, P τ 0 ]. It is possible to account for (some) subeffecting using
subtyping of sessions. Formalising this is further work.
Whilst we have embedded effects into sessions, the converse seems possible: to embed sessions into
effects. Nielson and Nielson previously defined an effect system for higher-order concurrent programs
which resembles some aspects of session types [8]. Future work is to explore mutually inverse embeddings of sessions and effects. Relatedly, further work is to explore whether various kinds of coeffect
system (which dualise effect systems, analysing context and resource use [9]) such as bounded linear
logics, can also be embedded into session types or vice versa.
Acknowledgements Thanks to Tiago Cogumbreiro and the anonymous reviewers for their feedback.
The work has been partially sponsored by EPSRC EP/K011715/1, EP/K034413/1, and EP/L00058X/1,
and EU project FP7-612985 UpScale.

10

Using session types as an effect system

References
[1] Robert L Bocchino Jr, Vikram S Adve, Danny Dig, Sarita V Adve, Stephen Heumann, Rakesh Komuravelli,
Jeffrey Overbey, Patrick Simmons, Hyojin Sung & Mohsen Vakilian (2009): A Type and Effect System for
Deterministic Parallel Java. In Proocedings of OOPSLA 2009, pp. 97–116, doi:10.1145/1640089.1640097.
[2] Tzu-Chun Chen, Mariangiola Dezani-Ciancaglini & Nobuko Yoshida (2014): On the Preciseness of Subtyping in Session Types. In: PPDP 2014, ACM Press, pp. 146–135, doi:10.1145/2643135.2643138.
[3] David K. Gifford & John M. Lucassen (1986): Integrating functional and imperative programming. In:
Proceedings of Conference on LISP and func. prog., LFP ’86, doi:10.1145/319838.319848.
[4] Dimitrios Kouzapas, Nobuko Yoshida, Raymond Hu & Kohei Honda (2014): On asynchronous eventful session semantics. Mathematical Structures in Computer Science, pp. 1–62, doi:10.1017/s096012951400019x.
[5] Robin Milner (1992): Functions as Processes. MSCS 2(2), pp. 119–141, doi:10.1017/s0960129500001407.
[6] Dimitris Mostrous & Nobuko Yoshida (2015): Session typing and asynchronous subtyping for the higherorder π-calculus. Inf. Comput. 241, pp. 227–263, doi:10.1016/j.ic.2015.02.002.
[7] Flemming Nielson & Hanne Riis Nielson (1999): Type and effect systems. In: Correct System Design,
Springer, pp. 114–136, doi:10.1007/3-540-48092-7 6.
[8] Hanne Riis Nielson & Flemming Nielson (1994): Higher-order concurrent programs with finite communication topology. In: Proceedings of the symposium on Principles of programming languages, ACM, pp. 84–97,
doi:10.1145/174675.174538.
[9] Tomas Petricek, Dominic A. Orchard & Alan Mycroft (2014): Coeffects: a calculus of context-dependent
computation. In: Proceedings of ICFP, pp. 123–135, doi:10.1145/2628136.2628160.
[10] Davide Sangiorgi & David Walker (2001): The π-Calculus: a Theory of Mobile Processes. Cambridge
University Press, doi:10.2178/bsl/1182353926.
[11] Jean-Pierre Talpin & Pierre Jouvelot (1992): The type and effect discipline. In: Proc. LICS’92, pp. 162–173,
doi:10.1109/lics.1992.185530.
[12] Nobuko Yoshida & Vasco Thudichum Vasconcelos (2007): Language Primitives and Type Discipline for
Structured Communication-Based Programming Revisited: Two Systems for Higher-Order Session Communication. Electr. Notes Theor. Comput. Sci. 171(4), pp. 73–93, doi:10.1016/j.entcs.2007.02.056.

A

Subtyping and selection

Our session typing system assigns selection types that include only the label l being selected ((select) in
Figure 2). Duality with branch types is provided by subtyping on selection types:
(sel)

⊕[l˜ : S̃] ≺ ⊕[l˜ : S̃, l˜0 : S̃0 ]

(this is a special case of the usual full subtyping rule for selection, see [2, [ SUB - SEL ], Table 5, p. 4]).
Therefore, for example, the get process could be typed:
Γ, x : τ; ∆; c : S ` P
(sel)
Γ; ∆, c : ⊕[get : ?[τ].S] ` get(c)(x).P
⊕[get : ?[τ].S] ≺ ⊕[get : ?[τ].S, put : ![τ].S]
(sub)
Γ; ∆, c : ⊕[get : ?[τ].S, put : ![τ].S] ` get(c)(x).P
However, such subtyping need only be applied when duality is being checked, that is, when opposing
endpoints of a channel are bound by channel restriction, νc.P. We take this approach, thus subtyping is
only used with channel restriction such that, prior to restriction, session types can be interpreted as effect
annotations with selection types identifying effectful operations.

Dominic Orchard and Nobuko Yoshida

B

11

Agda encoding

The Agda formalisation of our embedding defines data types of typed terms for the effect calculus
, ` , and session calculus * ` , indexed by the effects, types, and contexts terms:
data_,_`_,_ (eff : Effect) : (Gam : Context Type) -> Type -> (Carrier eff) -> Set where . . .
data _*_`_: (Γ : Context VType) -> (Σ : Context SType) -> (t : PType) -> Set where . . .

These type constructors are multi-arity infix operators. For the effect calculus type, the first index eff :
Effect is a record providing the effect algebra, operations, and constants, of which the Carrier field
holds the type for effect annotations. The embedding is then a function:
embed : forall {Γ τ F} -> (e : stEff , Γ ` τ , F)
-> (map interpT Γ) * ((Em , [ interpT τ ]!· end) , interpEff F) ` proc

where interpT : Type -> VType maps types of the effect calculus to value types for sessions, and
interpEff : List StateEff -> SType maps state effect annotations to session types SType. Here the
constructor [ ]!· is a binary data constructor representing the session type for send. The intermediate
embedding has the type (which also uses the receive session type [ ]?· ):
embedInterm : forall {Γ τ F G}
-> (M : stEff , Γ ` τ , F)
-> (map interpT Γ * (((Em , [ interpT τ ]!· end) , [ sess (interpEff (F ++ G)) ]?· end)
, [ sess (interpEff G) ]!· end) ` proc

C

Soundness proof of embedding, wrt. Figure 4 equations

Theorem (Soundness). If Γ ` M ≡ N : τ, F then JΓK; (r : !JτK.end, e : JFK) ` JMKer ≈ JNKer
Proof We make use of an intermediate lemma, which we call forwarding, where for all M:
|P
νea.(L M Mei,ea
| ea?(c).eo!hci.P) ≈ L M Mei,eo
r
r

∧

νea.(L M Mea,eo
| ei?(c).ea!hci.P) ≈ L M Mei,eo
|P
r
r

where c is not free in P. This follows by induction on the definition of the intermediate embedding.
Since JMKer = νei, eo. (L M Mrei,eo | ei!hei.eo?(c)) and JNKer = νei, eo. (L N Mei,eo
| ei!hei.eo?(c)) (eq. 14)
r
ei,eo
we need only consider L M Mei,eo
≈
L
N
M
i.e.,
weak
bisimilarity
of
the
intermediate
embeddings. We
r
r
def

address each equation in turn. The relation = denotes definitional equality based on L − Mei,eo
.
r
(unitR)
def

L let x ← M in x Mrei,eo

= ν q, ea. (L M Mqei,ea | q?(x).ea?(c).r!hxi.eo!hci)

≈ ν ea. (L M Mrei,ea | ea?(c).eo!hci)

≈

L M Mei,eo
r



{forwarding q → r}
{forwarding ea → eo}

(unitL)
def

L let y ← x in M Mei,eo
r

= ν q, ea.(L x Mei,ea
| q?(y).L M Mea,eo
)
q
r

def

= ν q, ea.(ei?(c).q!hxi.ea!hci | q?(y).L M Mea,eo
)
r

≈ ν ea.(ei?(c).ea!hci | L M Mea,eo
[x/y])
r

≈
≈

L M Mrei,eo [x/y]
L M[x/y] Mei,eo
r



{β , structural congruence}
{forwarding ei → ea}
{var substitution preserved by L − M}

12

Using session types as an effect system

(assoc)
def

L let y ← (let x ← M in N) in P Mei,eo
r

)
= ν q, ea. (L let x ← M in N Mei,ea
| q?(y).L P Mea,eo
r
q

def

ei,eb
= ν q, ea. (ν q1, eb. (L M Mq1
) | q?(y).L P Mea,eo
)
| q1?(x).L N Meb,ea
q
r

ei,eb
(∗) ≈ ν q, ea, q1, eb. (L M Mq1
| q?(y).L P Mea,eo
)
| q1?(x).L N Meb,ea
q
r
def

{structural congruence}

L let x ← M in (let y ← N in P) Mei,eo
r

)
= ν q, ea. (L M Mqei,ea | q?(x).L let y ← N in P Mea,eo
r

def

= ν q, ea. (L M Mqei,ea | q?(x).ν q1, eb. (L N Mea,eb
| q1?(y).L P Meb,eo
))
r
q1

≈ ν q, ea, q1, eb. (L M Mqei,ea | q?(x).L N Mea,eb
)
| q1?(y).L P Meb,eo
r
q1
≈

ei,eb
ν q, ea, q1, eb. (L M Mq1

≈ (∗) 

|

q1?(x).L N Meb,ea
q

|

q?(y).L P Mea,eo
)
r

{sequentiality, x 6∈ f v(P)}
{α, ea ↔ eb, q ↔ q1}

The proof of the commutativity axiom (comm) relies on an additional equation of the effect algebra,
that for all F, G then F • G ≡ I ⇒ (F ≡ G ≡ I). The proof below is factored into an additional lemma
about encodings of pure computations, given after in Lemma 1. Essentially, given the right session
calculus context C, then C[L Γ ` M : τ, I Mei,eo
] ≈ C[ei?(c).eo!hci | JMKr ]. That is, a pure computation can
r
be factored into a pure encoding and a forwarding from the input effect-channel-carrying channel to the
output channel.
(comm) where Γ ` M : τ1 , I
def

L let x ← M in (let y ← N in P) Mei,eo
r

= ν q, ea. (L M Mqei,ea | q?(x).L let y ← N in P Mea,eo
)
r

def

| q1?(y).L P Meb,eo
= ν q, ea. (L M Mqei,ea | q?(x).ν q1, eb. (L N Mea,eb
))
r
q1

)
≈ ν q, ea, q1, eb. (L M Mqei,ea | L N Mea,eb
| q?(x).q1?(y).L P Meb,eo
r
q1

≈
(∗) ≈

def

L N Mea,eb
q1

{sequentiality, x 6∈ f v(N)}

| q?(x).q1?(y).L P Meb,eo
)
ν q, ea, q1, eb. (ei?(c).ea!hci | JMKq |
r
ei,eb
eb,eo
ν q, q1, eb. (JMKq | L N Mq1 | q?(x).q1?(y).L P Mr )

{purity lemma 1 on M}
{forwarding ei → ea}

L let y ← N in (let x ← M in P) Mei,eo
r

= ν q, ea. (L N Mei,ea
| q?(y).L let x ← M in P Mea,eo
)
q
r

def

= ν q, ea. (L N Mei,ea
| q?(y).ν q1, eb. (L M Mea,eb
| q1?(x).L P Meb,eo
))
q
r
q1

| L M Mea,eb
| q?(y).q1?(x).L P Meb,eo
≈ ν q, ea, q1, eb. (L N Mei,ea
)
q
r
q1

{sequentiality, y 6∈ f v(M)}

≈ ν q, ea, q1, eb. (L N Mei,ea
| ea?(c).eb!hci | JMKq1 | q?(y).q1?(x).L P Meb,eo
) {purity lemma 1 on M}
q
r
ei,ea
ea,eo
≈ ν q, q1, ea. (L N Mq | JMKq1 | q?(y).q1?(x).L P Mr )
{forwarding ea → eb}
≡ ν q, q1, ea. (JMKq1 | L N Mei,ea
| q?(y).q1?(x).L P Mea,eo
)
{structural congruence}
q
r
α
ei,eb
eb,eo
≡ ν q, q1, eb. (JMKq | L N Mq1 | q1?(y).q?(x).L P Mr )
{α, q ↔ q1, ea ↔ eb}
ei,eb
eb,eo
≈ ν q, q1, eb. (JMKq | L N Mq1 | q?(x).q1?(y).L P Mr )
{reorder recv.}
≈ (∗) 

Dominic Orchard and Nobuko Yoshida

13

Lemma 1 (Pure encodings, in context). If an effect system has the property that ∀F, G.(F • G ≡ I) ⇒
(F ≡ G ≡ I) then, for all M, Γ, τ, P, Q it follows that:
L Γ ` M : τ, I Mrei,eo | eo?(c).P | r?(x).Q ≈ ei?(c).eo!hci | JMKr | eo?(c).P | r?(x).Q
Proof. By induction over type-and-effect derivations with a pure effect in the conclusion.
• (var)
L Γ ` x : I Mei,eo | eo?(c).P | r?(x).Q
ei?(c).eo!hci | JxK | eo?(c).P | r?(x).Q
r

= ei?(c).r!hxi.eo!hci | eo?(c).P | r?(x).Q

ei(c)

−−→ r!hxi.eo!hci | eo?(c).P | r?(x).Q

r

= ei?(c).eo!hci | r!hxi | eo?(c).P | r?(x).Q

ei(c)

−−→ eo!hci | r!hxi | eo?(c).P | r?(x).Q

τ

→
− r!hxi | P | r?(x).Q

τ

→
− P|Q

→
− eo!hci | eo?(c).P | Q
→
− P|Q

τ

τ

• (const) Similar to (var), where L Γ ` C : Cτ , I Mei,eo
= ei?(c).JCKr .eo!hci which has the same shape
r
as the (var) encoding and thus follows a similar proof to the above.
• (op) Similar to the above, where L Γ ` op M : Opτ , I Mei,eo
= ei?(c).Jop MKr .eo!hci which has the
r
same shape as (var) and (const) encodings.
• (let) By the additional requirement that ∀F, G.(F • G ≡ I) ⇒ (F ≡ G ≡ I) then the encoding of a
type-and-effect derivation rooted in the (let) rule (with pure effect) is necessarily of the form:
)
L Γ ` let x ← M in N : τ, I Mrei,eo = νq, ea.(L Γ ` M : σ , I Mei,ea
| q?(x).L Γ, x : σ ` N : τ, I Mea,eo
r
q

From the premises, the inductive hypothesis are:

| ea?(c).P | q?(x).Q ≈ ei?(c).ea!hci | JMKq | ea?(c).P | q?(x).Q
(A) L Γ ` M : σ , I Mei,ea
q

(B) L Γ, x : σ ` N : τ, I Mea,eo
| eo?(c).P0 | r?(x).Q0 ≈ ea?(c).eo!hci | JNKr | eo?(c).P0 | r?(x).Q0
r

From these the following weak bisimilarity holds:
(B)

≈

f wd

≈

f wd

≈

(A)

≈

ei(c)

νq, ea.(L Γ ` M : σ , I Mei,ea
) | eo?(c).P | r?(x).Q
| q?(x).L Γ, x : σ ` N : τ, I Mea,eo
r
q
νq, ea.(L Γ ` M : σ , I Mei,ea
| q?(x).(ea?(c).eo!hci | JNKr | eo?(c).P | r?(x).Q)
q

νq.(L Γ ` M : σ , I Mei,eo
| q?(x).(JNKr | eo?(c).P | r?(x).Q)
q

νq, ea.(L Γ ` M : σ , I Mei,ea
| ea?(c).eo!hci | q?(x).(JNKr | eo?(c).P | r?(x).Q))
q

νq, ea.(ei?(c).ea!hci | JMKq | ea?(c).eo!hci | q?(x).(JNKr | eo?(c).P | r?(x).Q))

−−→ νq, ea.(ea!hci | JMKq | ea?(c).eo!hci | q?(x).(JNKr | eo?(c).P | r?(x).Q))
τ

→
− νq.(JMKq | eo!hci | q?(x).(JNKr | eo?(c).P | r?(x).Q))
≈ νq.(JMKq | q?(x).(JNKr | P | r?(x).Q))
≡ νq.(JMKq | q?(x).JNKr ) | P | r?(x).Q
≡ Jlet x ← M in NKr | P | r?(x).Q

ei(c)

ei?(c).eo!hci | Jlet x ← M in NKr | eo?(c).P | r?(x).Q

−−→ eo!hci | Jlet x ← M in NKr | eo?(c).P | r?(x).Q
τ

→
− Jlet x ← M in NKr | P | r?(x).Q

