Luca Padovani

A Simple Library Implementation of Binary Sessions

come   L'archive ouverte pluridisciplinaire

Introduction

One major obstacle to the adoption and integration of session type systems into mainstream programming languages is their reliance on sophisticated and peculiar features, whose built-in support would require massive changes in both languages and their development tools. In the case of binary sessions [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF], for example, the compiler would have to integrate features for (F.1) describing structured protocols as sequences of I/O operations and internal/external choices, (F.2) checking the duality of the protocols associated with the endpoints of a session to make sure that they are used in complementary ways, (F.3) tracking the changes in the type of endpoints as these are used for I/O operations, and (F.4) ensuring the linear usage of endpoints.

In this paper we show how to incorporate a form of session type checking into a broad class of conventional programming languages, by recasting these fancy features into ordinary ones. A step in this direction was taken by Gay and Vasconcelos [START_REF] Gay | Linear type theory for asynchronous session types[END_REF], who realized that (F.3) could be achieved by a clever typing of the communication primitives. The technique is illustrated in program P below, written in an ML-like language: let foo x 0 = let n, x 1 = receive x 0 in (* x 0 : ?int.!bool.end *) let x 2 = send x 1 (n = 0) in (* x 1 : !bool.end *) close x 2 (* x 2 : end *) let bar y 0 = let y 1 = send y 0 42 in (* y 0 : !int.?bool.end *) let b, y 2 = receive y 1 in (* y 1 : ?bool.end *) close y 2 ; print b (* y 2 : end *)

According to [START_REF] Gay | Linear type theory for asynchronous session types[END_REF], the primitives send and receive consume a session endpoint and return the same endpoint with a possibly different session type. Take for example the session type !int.?bool.end, which denotes an endpoint for sending an int and receiving a bool, in this order, before being closed. Then send y 0 42 in bar consumes endpoint y 0 of type !int.?bool.end, sends 42 on it, and returns the endpoint with type ?bool.end, which is then bound to y 1 . Similarly, receive y 1 consumes y 1 of type ?bool.end, waits for a message from it, and returns a pair with the received message b of type bool and the endpoint with type end, which is bound to y 2 . As the operational semantics in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF] clearly illustrates, the y i 's all actually refer to the same endpoint; its subsequent rebindings allow the type checker to track the change in its type without using any dedicated mechanism. Observe that foo has a complementary behavior compared to bar. This is witnessed by the session type of x 0 , which is the dual of that of y 0 : inputs have become outputs, and vice versa. If foo and bar are applied to the two endpoints of a session, duality guarantees communication safety.

The given semantics and typing of the communication primitives are not the only possible ones. An alternative semantics and a corresponding typing for the same primitives emerges from the studies of Kobayashi [START_REF] Kobayashi | Type systems for concurrent programs[END_REF], Demangeon and Honda [START_REF] Demangeon | Full abstraction in a subtyped pi-calculus with linear types[END_REF], and Dardha, Giachino and Sangiorgi [START_REF] Dardha | Session types revisited[END_REF]. These works show that an arbitrary sequence of communications in a session can be encoded as a sequence of communications in a chain of linear channels, each channel being used for one communication only. The chain is realized by pairing the payload in each message with a continuation, that is a fresh channel on which the next communication takes place. Let us re-interpret P as the program Q below, which is syntactically the same as P, but uses this alternative semantics and typing of the communication primitives: Here x i and y j are linear channels and the communication primitives explicitly create and exchange continuations. Channel types have the form κ[t], where κ ∈ {?, !, Ø} is a capability denoting an input, an output, or the closing of a channel and t is the type of messages exchanged on the channel. For instance, the type ![int * ![bool * Ø [unit]]] indicates that y 0 is a channel for sending a pair made of an int and another channel of type ![bool * Ø [unit]]. Now the effect of send y 0 42 is to create a fresh channel, to pair 42 with one reference to such channel of type ![bool * Ø[unit]], to send the pair, and to return another reference to the same fresh channel of type ?[bool * Ø [unit]]. Accordingly, the type of the first reference matches that of x 1 in foo and the type of the second reference matches that of y 1 in bar.

Two reasons make the alternative typing of communication primitives in program Q relevant to our aims. First, program Q only uses ordinary types (channel types and products). Even if the exact correspondence between the session types in P and the types in Q is not entirely obvious, it is clear that both describe the same protocol, just written in different ways. Second, the structurally complex duality relation between the session types of x i and y i in P boils down to a much simpler duality relation between the channel types of x i and y i in Q matching input ? with output ! capabilities, but only in the topmost channel type constructor. This relation, as we will see, can be expressed solely in terms of type equality, given an appropriate representation of channel types.

In a nutshell, the communication primitives in program P have a natural semantics (not creating or exchanging continuations) but require fancy types and related notions; the communication primitives in program Q have an impractical semantics (creating and exchanging continuations) but their types look and behave much like ordinary ones.

The key observation is that it is makes sense to consider a third, intermediate configuration in which the communication primitives do not create or exchange continuations (as in program P) but are typed as if they did create and exchange continuations (as in program Q). This mix-up can be justified as an optimized implementation of the communication primitives in program Q: as the authors of [START_REF] Dardha | Session types revisited[END_REF] point out, there is no need to actually create fresh continuations, for the already existing channel can be reused. We take this optimization one step further: not only continuations need not be created, they need not be exchanged either, precisely because the channel being reused is already known by the interacting processes. In the end, we obtain a set of primitives whose semantics matches exactly that for session communications, but whose typing allows us to realize (F. [START_REF] Bartoletti | Compliance and subtyping in timed session types[END_REF][START_REF] Bocchi | Monitoring networks through multiparty session types[END_REF][START_REF] Bono | Typing Copyless Message Passing[END_REF] in terms of standard notions of generic types and type equality. We do not propose or adopt compile-time mechanisms for (F.4). Instead, we rely on the runtime environment for detecting non-linear endpoint usages that may compromise safety. We will see that the type system is nonetheless capable of identifying a fair number of linearity violations, even if it is not intentionally designed to do so (Example 4).

Here is an account of our contributions:

1. We formalize a core functional language, called FuSe, that combines multithreading and session-based communications in the style of [START_REF] Gay | Linear type theory for asynchronous session types[END_REF] with a runtime mechanism that detects endpoint linearity violations (Section 2). 2. We define an ordinary ML-style type language for FuSe and we adapt and extend the encoding of session types [START_REF] Dardha | Session types revisited[END_REF] into FuSe types. A carefully chosen representation of channel types allows us to express (encoded) session type duality solely in terms of type equality and generic types (Section 3). 3. We equip FuSe with a standard ML-style type system and we type FuSe primitives using encoded (as opposed to built-in) session types. Well-typed FuSe programs are shown to enjoy all the usual properties of sessions (safety, fidelity, progress) under the hypothesis that they use session endpoints linearly (Section 4). 4. To demonstrate the effectiveness of the approach, we detail the implementation of FuSe primitives as a simple OCaml module [START_REF] Leroy | The Objective Caml system, release 4.02 -Documentation and user's manual[END_REF]. The implementation integrates well with OCaml, which is capable of inferring possibly recursive, polymorphic session types and of supporting a form of session subtyping as well (Section 5).

We share motivations and objectives with Neubauer and Thiemann [START_REF] Neubauer | An implementation of session types[END_REF] and with Pucella and Tov [START_REF] Pucella | Haskell session types with (almost) no class[END_REF] although we adopt a different approach. In short: [START_REF] Neubauer | An implementation of session types[END_REF][START_REF] Pucella | Haskell session types with (almost) no class[END_REF] hinge on advanced features of the host language (Haskell) to represent and handle conventional session types; we work with a representation of session types that makes them easy to handle in conventional type systems. Compared to [START_REF] Neubauer | An implementation of session types[END_REF][START_REF] Pucella | Haskell session types with (almost) no class[END_REF], our approach realizes (F.1-3) with a substantially simpler machinery that better integrates with the host language and is less onerous on the programmer. A more in-depth discussion is deferred to Section 6.

The OCaml implementation of FuSe communication primitives, described in full in Section 5, can also be downloaded from the author's home page. Proofs and supplementary technical material are in Appendixes A and B, beyond the page limit.

Syntax and Semantics of FuSe

We use infinite sets of variables x, y, . . . and sessions a, b, . . . ; an endpoint or channel is a pair a p made of a session a and a polarity p, q ∈ {+, -, *}. Polarities + anddenote valid endpoints that can be used for I/O operations whereas the polarity * denotes invalid endpoints that are not supposed to be used. We define a partial involution • on polarities such that + = -and -= + and leave * undefined. We say that a p is the peer of a p when p = *. We let u range over names, which are either variables or endpoints. The syntax of expressions e and processes P, Q is given in Table 1. The symbol c ranges over the constants (), fix, fork, create, close, send, receive, left, right, branch, where () is the unitary value, fix the fixpoint combinator, and fork the primitive that creates new threads. The remaining constants represent communication primitives whose semantics will be detailed shortly. Expressions are conventional and include let bindings and introduction and elimination constructs for products and sums. The symbol K ranges over the tags L and R that inject values into disjoint sums. We use expressions to model threads -the sequential parts of programs -and processes to model parallel threads communicating via sessions. A process is either a thread e , or the parallel composition P | Q of two processes P and Q, or a restriction (νa)P modeling a session a with scope P, or a runtime error resulting from an attempt to use an invalid endpoint. The notions of free and bound names are standard. We write fn(e) and fn(P) respectively for the sets of free names of e and P and we identify terms modulo alpha-renaming of bound names.

The operational semantics is defined in terms of a reduction relation for expressions, a structural congruence and a labeled reduction relation for processes. We make use of conventional notions of values v, w and of evaluation contexts E , defined thus:

v, w ::= c | a p | fun x ↓ -e | (v,w) | K v | fork v | send v E ::= [ ] | E e | vE | (E ,e) | (v,E ) | K E | let x = E in e | let x,y = E in e | match E with {i x i ↓ -e i } i=L,R
(fun x ↓ -e)v -→ e{v/x} [R-LET] let x = v in e -→ e{v/x} [R-FIX] fix v -→ v (fix v) [R-SPLIT] let x,y = (v,w) in e -→ e{v, w/x, y} [R-MATCH] match K v with {i x i ↓ -e i } i∈{L,R} -→ e K {v/x K } Reduction of processes P -→ Q [R-THREAD] E [e] τ -→ E [e ] if e -→ e [R-FORK] E [fork v w] τ -→ E [()] | vw [R-CREATE] E [create()] τ -→ (νa) E [(a + ,a -)] a fresh [R-CLOSE] E [close a p ] | E [close a p ] ca -→ E ca [()] | E ca [()] [R-COMM] E [send a p v] | E [receive a p ] map -→ E map [a p ] | E map [(v map ,a p )] [R-LEFT] E [left a p ] | E [branch a p ] map -→ E map [a p ] | E map [L a p ] [R-RIGHT] E [right a p ] | E [branch a p ] map -→ E map [a p ] | E map [R a p ] [R-ERROR] E [c a * ] τ -→ error [R-PAR] P | R -→ Q | R if P -→ Q [R-NEW-1] (νa)P τ -→ (νa)Q if P map -→ Q or P ca -→ Q [R-NEW-2] (νa)P -→ (νa)Q if P -→ Q and a p ∈ fn( ) [R-STRUCT] P -→ Q if P ≡ P -→ Q ≡ Q
Note that fork v and send v are values because fork and send represent curried binary functions. Evaluation contexts are standard for call-by-value; as usual, we write E [e] for the result of replacing the hole [ ] in E with e. We also write X{v/u} for the capture-avoiding substitution of v in place of the free occurrences of u in X, where X stands for an expression, a process, or an evaluation context.

The reduction relations are defined in Table 2. Reduction of expressions, in the upper part of the table, is standard. The lower part of the table defines a labeled reduction for processes where labels are either τ, denoting an internal action, or map, denoting a message exchange from endpoint a p to endpoint a p in session a, or ca, indicating that the session a has been closed. We define fn(τ) def = / 0 and fn(map) = fn(ca) def = {a + , a -}. Labels allow us to observe the behavior of processes on the channels they use. This information is necessary to show that well-typed processes respect protocols and also to invalidate the endpoints that have been used in a reduction.

Notation. For every expression, process, context X, we write X for X{a * /u} u∈fn( ) .

Intuitively, X invalidates all the endpoints a p in X by replacing them with a * , after an -labeled reduction. When = τ, no (observable) endpoint is used so no endpoint is invalidated. When = map or = ca, both a + and a -are invalidated.

We now describe the reduction rules of processes. Rule [R-THREAD] simply lifts the reduction of expressions to processes. Rule [R-FORK] spawns a new thread, represented as a function v that needs an argument w. The thread is started by applying v to w in parallel with the process that forks the thread. Rule [R-CREATE] creates a new session a. The expression create() reduces to a pair containing two valid endpoints of the session with opposite polarities. Rule [R-CLOSE] models the closing of session a. The operation invalidates every occurrence of a + and a -in the program. In the formal development this operation is synchronous for simplicity, but in the implementation each endpoint can be closed independently of the other. Rule [R-COMM] models the communication between two threads connected by a session a. The message v in the sender thread is transferred to the receiving thread. Following the semantics of [START_REF] Gay | Linear type theory for asynchronous session types[END_REF], the output operation reduces to the endpoint a p used by the sender, while the input operation reduces to a pair containing the message and the endpoint a p used by the receiver. All other occurrences of a p and a p , including those in the message v, are invalidated. Next are [R-LEFT] and [R-RIGHT] modeling the selection of a particular branch in a structured conversation. They are akin to [R-COMM], except that the endpoint used by the receiver is injected into a disjoint sum with a tag K that represents the choice taken. Intuitively, the message being communicated in these cases is just the tag K. Note that there is no explicit creation or passing of continuations in [R-COMM], [R-LEFT], [R-RIGHT]: all that is transferred from one thread to another is just the payload. Rule [R-ERROR] generates a runtime error if there is an attempt to use an invalid endpoint, where "using an endpoint" means that the endpoint occurs as the first argument of a primitive c. Rule [R-PAR] closes reductions under parallel compositions. The label that decorates the reduction relation is used to propagate the effects of an invalidation to the entire program. Rules [R-NEW-1] and [R-NEW-2] close reductions under restrictions. The labels map and ca turn into a τ when they cross the restriction on a, as the session becomes unobservable. Finally, [R-STRUCT] closes reductions under the least structural congruence defined by the rules below:

() | P ≡ P P | Q ≡ Q | P P | (Q | R) ≡ (P | Q) | R (νa) () ≡ () (νa)(νb)P ≡ (νb)(νa)P a + , a -, a * ∈ fn(Q) (νa)P | Q ≡ (νa)(P | Q)
Structural congruence is essentially the same of the π-calculus, except that the idle process is written () and the last rule shrinks or extends the scope of a session only when no valid or invalid endpoint is captured.

Example 1 (mathematical server). We write examples in a language slightly richer than FuSe that includes numbers, booleans, if-then-else, and standard syntactic sugar for possibly recursive let-bindings. The examples compile and run using OCaml [START_REF] Leroy | The Objective Caml system, release 4.02 -Documentation and user's manual[END_REF] and our implementation of the FuSe primitives, described in Section 5. Below is a simple server for mathematical operations, similar to that of [START_REF] Gay | Subtyping for Session Types in the π-calculus[END_REF]: The server is modeled as a function operating on an endpoint x. The function is recursive, so that the server is able to process an arbitrary number of requests within a single session. The server first waits for a request from the client, represented as a tag 'L or 'R (this is the OCaml syntax for polymorphic variant tags, see Section 5.3). If the client selects 'L, the session is closed. If the client selects 'R, the server expects to receive two integer numbers, it sends back their sum, and recurs.

let
A possible client, operating on an endpoint y, is shown below: In this case, the client is computing the sum of the first n naturals by repeated invocations of the server. If n is 0, the computation is over, the client closes the session and returns the result. Otherwise, the client invokes the "plus" operation offered by the server to compute a new partial result and recurs. Note how the endpoint y is used differently in the two branches of the if-then-else.

let
The code to fire up client and server is the following where Thread.create, a function provided by the standard OCaml library for multithreading, corresponds to the fork primitive in FuSe.

Types

In this section we define the types for FuSe, we recall the encoding of [START_REF] Dardha | Session types revisited[END_REF] and extend it to an isomorphism between session types and a suitable subset of FuSe types. This gives us the basis for interpreting and understanding the type of FuSe communication primitives.

Types for FuSe. We let α, β , . . . range over type variables. The syntax of (finite) types and of type schemes is given in Table 3. Type schemes σ are conventional; we will often abbreviate ∀α 1 Type equality corresponds to regular tree equality. Recall that each regular tree consists of a finite number of distinct subtrees and admits finite representations as a system of equations or using the traditional µ notation ( [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF] is the standard reference for regular trees and their finite representations). For example, the equation α = int ↓ α is satisfied by the type t of the "ogre" function that eats infinitely many int arguments. The shape of the equation, with α guarded by a type constructor on the right hand side, effectively defines the unique type t such that t = int ↓ -t (see [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF]Theorem 4.3.1]). We can use infinite types for describing arbitrarily long communication protocols, like the one implemented by server and client in Example 1.

Duality relates the types of channels used in complementary ways:

Definition 1 (type duality). Let ⊥ t be the least relation such that

t 1 t 2 [s] ⊥ t t 2 t 1 [s]
. We write t ⊥ for the s such that t ⊥ t s when t is a channel type; t ⊥ is undefined otherwise.

The rationale for type duality is that if a process uses a channel according to some type t, then we expect another process to use the same channel according to the dual type t ⊥ . So for example,

•• [int] ⊥ t •• [int]
since the dual behavior of "send an int" is "receive an int". On the other hand, we have

•• [t] ⊥ t •• [t],
since "do nothing" is dual of itself. Type duality is a partial involution: when t ⊥ is defined, we have t ⊥⊥ = t.

Our representation of channel capabilities is a bit unusual. Most type systems with channel types, from the seminal paper on channel subtyping [START_REF] Pierce | Typing and subtyping for mobile processes[END_REF] to those for the linear π-calculus [START_REF] Kobayashi | Linearity and the pi-calculus[END_REF] and binary sessions [START_REF] Dardha | Session types revisited[END_REF], use types of the form κ[t] or variants of this, where κ ranges over a finite set of capabilities such as {?, !, Ø}. We have used this notation also in Section 1, while discussing program Q. In these cases, capabilities and types belong to different sorts and computing the dual of a channel type essentially means defining a suitable dual operator for capabilities such that, for instance, ? ⊥ = !.

One shortcoming of this representation is that duality is easily defined only when capabilities are known. Dealing with unknown capabilities means introducing (possibly dualized) capability variables, and this machinery quickly taints the whole type system. Our approach departs from the aforementioned ones in two respects. First, we use two slots for representing the absence or presence of a certain I/O capability, instead of just one slot that contains either one or the other. This representation, which is also convenient in type reconstruction algorithms for the π-calculus [START_REF] Igarashi | Type Reconstruction for Linear π-Calculus with I/O Subtyping[END_REF][START_REF] Padovani | Type reconstruction for the linear π-calculus with composite and equirecursive types[END_REF][START_REF] Padovani | Type Reconstruction Algorithms for Deadlock-Free and Lock-Free Linear π-Calculi[END_REF], allows us to dualize a channel type by just swapping the content of the two slots. Second, we use types to represent capabilities so that type variables can stand for unknown capabilities. For example, the type t def = αβ [γ] denotes a channel for which nothing is known. Nonetheless, the dual of t can still be obtained by swapping α and β , that is

t ⊥ = β α [γ].
Overall, the chosen representation makes it easy to relate a channel type and its dual even when capabilities are not known.

In the following we will make extensive use of channel types with unknown capabilities and unknown message types, so we reserve some convenient notation for them: Notation (channel type variable). We say that a type of the form αβ [γ] is a channel type variable. We let A, B, . . . range over channel type variables and we write ∀A.σ instead of ∀αβ γ.σ when

A = αβ [γ].
Note that the dual A ⊥ of a channel type variable A is always defined.

Session types. Even though our type system does not use built-in session types, the typing of FuSe communication primitives follows from the encoding of session types into ordinary types [START_REF] Dardha | Session types revisited[END_REF]. For this reason, in the remainder of this section we formalize the relationship between session types and FuSe types, recalling the encoding and instantiating it to our setting. Compared to [START_REF] Dardha | Session types revisited[END_REF], we use channel types with a slightly different representation of I/O capabilities and we consider possibly infinite (session) types.

The syntax of session types T , S is given in Table 3. The session type end denotes a channel on which no further communication is allowed. The session types ?T .S and !T .S denote channels to be used respectively for one input and one output of a message of type T and according to S afterwards. The session types T & S and T ⊕ S respectively denote external and internal choices in a protocol. A process using a channel of type T ⊕ S decides whether to behave according to the "left" protocol T or the "right" protocol S. A process using a channel of type T &S accepts the decision of the process using the peer endpoint. As we have seen in Table 2, the choice is effectively encoded and transmitted as an appropriate message, hence ⊕ corresponds to an output and & to an input operation. As for types, we do not devise a concrete syntax for recursive session types and use regular trees in this case as well. For example, the (unique) session type T that satisfies the equality T = !T 1 .!T 1 .?T 2 .T denotes a channel for sending two messages of type T 1 , receiving one message of type T 2 , and then according to the same protocol, over and over again. The given syntax of session types disallows the description of polymorphic protocols and protocols for exchanging messages other than channels. These limitations are immaterial for we introduce session types for illustrative purposes only. All the results in this section extend to more general forms of session types.

Just like channel types, session types too support a notion of duality that relates complementary behaviors. It is defined thus: Definition 2 (session type duality). Session type duality is the largest relation ⊥ st between session types that satisfies the rules

end ⊥ st end S 1 ⊥ st S 2 ?T .S 1 ⊥ st !T .S 2 T i ⊥ st S i (i=1,2) T 1 & T 2 ⊥ st S 1 ⊕ S 2
and the symmetric ones, omitted. Observe that ⊥ st is an endofunction on session types. We write T ⊥ for the session type S such that T ⊥ st S and say that S is the dual of T .

Duality relates inputs with outputs carrying the same message type and end with itself. For example, ?T .!S.end ⊥ st !T .?S.end and if T is the session type such that T = !T 1 .!T 1 .?T 2 .T then T ⊥ is the session type S such that S = ?T 1 .?T 1 .!T 2 .S. It is easy to establish that duality is an involution also for session types (T ⊥⊥ = T ).

We now formalize the claim made in Section 1 that "session types and their encoding describe the same protocol, written in different ways" as an isomorphism between the set S of session types and a suitable subset P of FuSe types which we call protocol types (such essentially syntactic isomorphism between types is supported by a semantic correspondence between processes, see [START_REF] Dardha | Session types revisited[END_REF]). The set P is defined thus: Definition 3. We write P for the largest subset of types such that t ∈ P implies either t =

•• [unit] or t = s 1 s 2 [t 1 t 2 ] and ∈ {*, +} and {s 1 , s 2 } = {•, •} and t 1 ,t 2 ∈ P.
The morphism from S to P is given by the encoding of session types into ordinary types [START_REF] Dardha | Session types revisited[END_REF] and rests on the idea that multiple communications on one channel can be modeled as a sequence of one-shot communications on a chain of different channels. The chain is realized by sending, at each communication, a fresh continuation channel along with the communication payload. For example, the session type !T .S describes a channel used for sending a message of type T first and according to S afterwards. It is encoded as the channel type •• [t * s] where t is the encoding of T and s is the encoding of S ⊥ . The reason why the type s of the continuation is the encoding of S ⊥ and not the encoding of S is because the tail S in !T .S describes the behavior of the sender after it has sent a message of type T , while in the encoding the type of the continuation describes the behavior of the receiver of the continuation. Clearly, the sender will also use the same continuation, but according to the type s ⊥ . In general we have: Definition 4 (encoder). The encoder function • : S → P is coinductively defined by:

end = •• [unit] ?T .S = •• [ T * S ] !T .S = •• [ T * S ⊥ ] T & S = •• [ T + S ] T ⊕ S = •• [ T ⊥ + S ⊥ ]
As an example, if we consider again T = !T 1 .!T 1 .?T 2 .T , then we derive:

T = •• [t 1 * ?T 1 .!T 2 .T ⊥ ]
where

t 1 = T 1 = •• [t 1 * •• [t 1 * !T 2 .T ⊥ ]] = •• [t 1 * •• [t 1 * •• [t 2 * T ⊥⊥ ]]]
where

t 2 = T 2 = •• [t 1 * •• [t 1 * •• [t 2 * T ]]]
If we consider instead the session type S such that S = ?T 1 .?T 1 .!T 2 .S, which is in fact

T ⊥ , then S = •• [t 1 * •• [t 1 * •• [t 2 * T ]]]. The choice of •• [unit]
as the encoding of end is almost arbitrary. We could have used any type in place of unit.

The morphism from P to S reconstructs a session type T by interpreting the type of continuation channels as the tail(s) of T : Definition 5 (decoder). The decoder function • : P → S is coinductively defined by:

•• [unit] = end •• [t * s] = ? t . s •• [t * s] = ! t . s ⊥ •• [t + s] = t & s •• [t + s] = t ⊥ ⊕ s ⊥ It is not immediate to see that • = • -1
, because the two morphisms use different notions of duality, for session types and for channel types respectively. However, as observed in [START_REF] Dardha | Session types revisited[END_REF] and formally stated below, • commutes with duality (and so does • ). This property is key to prove that • and • are indeed one the inverse of the other.

Theorem 1 (commuting duality).

⊥ t • • = • • ⊥ st .
The existence of an isomorphism between S and P shows that using protocol types instead of built-in session types results in no loss of expressiveness (there is an encoding for every session type) and no loss in precision (every session type can be reconstructed from its encoding). Most importantly, Theorem 1 combined with our representation of channel types provides a straightforward method for checking whether T ⊥ st S holds. Suppose for example that T = t i t o [t] and S = s i s o [s]. Using Theorem 1 we deduce

T ⊥ st S ⇐⇒ T ⊥ t S ⇐⇒ t i = s o ∧ t o = s i ∧ t = s
thereby turning the verification of a complex relation T ⊥ st S, which implies matching input with output capabilities across the whole structure of T and S, into three plain type equalities. In prospect of integrating a session type system into an existing type system, this is a major advantage of using encoded (as opposed to built-in) session types.

Type System

We present the type system for FuSe and state its properties. The type system is essentially standard for ML-like languages, in particular it has no baked-in features specifically targeted to session type checking. Compared to the type system in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF], the main differences concern the typing of communication primitives and the fact that the type system is not substructural.

Table 4 gives the typing rules. We let Γ range over type environments which are finite maps from names to type schemes written u 1 : σ 1 , . . . , u n : σ n that keep track of the type of the free names of expressions and processes. We write / 0 for the empty type environment, dom(Γ ) for the domain of Γ , and Γ , Γ for the union of Γ and Γ when dom(Γ ) ∩ dom(Γ ) = / 0. The rules for processes derive judgments of the form Γ P, stating that P is well typed in Γ . Rules [T-THREAD] and [T-PAR] are standard. Rule [T-NEW] introduces in the type environment three endpoints of a session: two of them are valid and typed with dual types (the fact that one of them is typed by t ⊥ implicitly means that t is a channel type); the third one is invalid and typed with ∀A.A. This way, distinct occurrences of an invalid endpoint can appear anywhere a channel is expected and need not be typed in the same way (see Remark 1). There is no typing rule for error.

TypeOf(c) t Γ c : t [T-NAME] σ t Γ , u : σ u : t Γ P | Q [T-NEW] Γ , a + : t, a -: t ⊥ , a * : ∀A.A P Γ (νa)P
The rules for expressions derive judgments of the form Γ e : t and are formulated using the same notation of Wright and Felleisen [START_REF] Wright | A syntactic approach to type soundness[END_REF]. Since the rules are mostly standard, we just focus on a few details. Rules [T-CONST] and [T-NAME] respectively type constants and names by instantiating their type scheme. The type scheme of constants is retrieved by a global function TypeOf(•), to be detailed shortly, while that of names is obtained from the type environment. Following [START_REF] Wright | A syntactic approach to type soundness[END_REF], the relation σ t is defined by t t σ t ∀α.σ t{s/α} and instantiates a type scheme into a type. Rule [T-LET] generalizes the type of the letbound variable by means of the function Close(•), which is defined as in [START_REF] Wright | A syntactic approach to type soundness[END_REF] by

Close(t, Γ ) def = ∀α 1 • • • α n .t
where {α 1 , . . . ,

α n } = ftv(t) \ ftv(Γ )
where ftv collects the free type variables of types and type environments. Rule [T-LET] is well known for being unsound in impure languages, the best-known counterexample being that of polymorphic references (again, see [START_REF] Wright | A syntactic approach to type soundness[END_REF]). However, the counterexample relies crucially on the fact that the same reference is used twice, in such a way that its type scheme can be instantiated with incompatible types in different parts of the program.

[T-LET] is sound if we know that x is used linearly. Since the impure fragment

↓ -α) ↓ -α fork : ∀α.(α ↓ -unit) ↓ -α ↓ -unit create : ∀A.unit ↓ -A * A ⊥ close : •• [unit] ↓ -unit send : ∀αA. •• [α * A] ↓ -α ↓ -A ⊥ receive : ∀αA. •• [α * A] ↓ -α * A left : ∀AB. •• [A + B] ↓ -A ⊥ right : ∀AB. •• [A + B] ↓ -B ⊥ branch : ∀AB. •• [A + B] ↓ -A + B
of FuSe concerns only sessions and we are interested in stating the soundness of FuSe type system under the assumption that channels are indeed used linearly, we can live with just one typing rule for let and not impose the value restriction even if e 1 has side effects (Appendix B.1 details why the counterexample in [START_REF] Wright | A syntactic approach to type soundness[END_REF] does not apply). The function TypeOf is given in Table 5 as a set of associations c : TypeOf(c). The types of () and fix are standard. The type of fork has been chosen to match more closely the one of Thread.create in the OCaml multithreading module. According to the operational semantics, fork accepts a function representing the thread to be created and the argument of type α it needs to start executing. The type of create makes it clear that the primitive returns a pair of endpoints with dual types. Recall that a channel type variable like A is just syntactic sugar for a channel type of the form αβ [γ]. Therefore, the desugared type scheme of create is ∀αβ γ.unit

↓ -αβ [γ] * β α [γ].
The ability to express channel types with unknown message types and capabilities gives create the most general type. The type of close is unremarkable. The type of send follows from the encoding of outputs (Definition 4): send takes a channel for sending messages of type α * A, the payload of type α, and returns a channel of type A ⊥ . According to its type, send should in principle communicate both the payload and the continuation. In reality, as the operational semantics illustrates, only the payload is sent. The type A of the continuation is used to correlate the future behaviors of sender and receiver after this interaction. The type of receive follows from the encoding of inputs: in this case the type of the continuation describes how the channel will be used by the receiver process, once the message has arrived. The types of left and right are analogous to that of send, and the type of branch is analogous to that of receive.

Observe that all the types of FuSe primitives can be expressed in any type system with generic types, once channel type variables have been desugared (Notation 3).

Example 2. Below we propose again the code of server in Example 1 in which we have indicated the type s i of the (free) occurrence of x on line i:

let rec server x = match branch x with (* s 2 = •• [s 3 + s 4 ] *) 'L x ↓ -close x (* s 3 = •• [unit] *) | 'R x ↓ -let n, x = receive x in (* s 4 = •• [int * s 5 ] *) let m, x = receive x in (* s 5 = •• [int * s 6 ] *) let x = send x (n + m) in (* s 6 = •• [int * s 7 ] *) server x (* s 7 = s ⊥ 2 *)
The output on line 6 indicates that server sends a payload of type int and a (virtual) continuation of type s 7 to client. Therefore, s 7 describes the behavior of client on the continuation channel, whereas server will use the same channel according to the type s 2 , which is the dual of s 7 . Overall, the argument x of server has type s =

•• [ •• [unit] + •• [int * •• [int * •• [int * s ⊥ ]]]] therefore we have server : s ↓ -unit.
It is then easy to derive client : int ↓ -s ⊥ ↓ -int, confirming that client and server can interact flawlessly.

We now investigate the relationship between well-typed programs and the three standard properties of sessions: every message sent in a session has the expected type (communication safety); the sequence of interactions in a session follows the prescribed protocol (protocol fidelity); if the interaction in a session stops, there are no pending I/O operations (progress). Obviously, well typing alone is not enough to guarantee these properties, for two reasons: first, the FuSe type system does not enforce the linear usage of endpoints, therefore there exist well-typed programs that try to use endpoints non-linearly causing runtime errors; second, the FuSe type system does not prevent deadlocks, which jeopardize progress and may occur even if endpoint linearity is respected. To take these facts into account, we must weaken the statements of our results with additional hypotheses: that endpoints are used linearly, and that no deadlocks occur. Note that these properties are undecidable in general.

The semantics of our communication primitives allows for a simple definition of linear endpoint usage. Recall that each communication primitive applied to an endpoint a p invalidates every other occurrence of a p before (possibly) returning a p itself. Therefore, any attempt to use an invalid endpoint means that another occurrence of the same endpoint has already been used in the past. It is not enough to check endpoint validity at one particular point in time, for instance in the initial program state, for an endpoint might be duplicated as the program executes. We resort to a coinductive definition that requires linear endpoint usage to be preserved across all possible executions of a process. Definition 6 (affine and linear endpoint usage). Let EA and EL be the largest predicates on processes that are closed by reductions and such that:

-If EA(P) or EL(P) and P ≡ (νa

1 ) • • • (νa n )( E [c a p ] | Q), then p ∈ {+, -}.
-If EL(P) and P ≡ (νa)Q and a p ∈ fn(Q) where p ∈ {+, -}, then a p ∈ fn(Q).

In words, EA is the set of endpoint affine processes, which never try to use the same endpoint twice, while EL is the set of endpoint linear processes which, in addition, never discard a valid endpoint if its peer is being used. Note that EL ⊆ EA and that EL is coarser than the property enforced by linear type systems. In particular, duplications of an endpoint are allowed provided that only valid endpoints are actually used. For example, the expression send (let x, y = (a, a) in x) temporarily duplicates the endpoint a but may occur in a process that satisfies EL. The same expression is ill typed according to the type system in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF].

In order to state subject reduction we have to consider that, like in many other behavioral type systems, the type associated with endpoints may change as the result of interactions occurring on such endpoints. To express this change, we define a suitable reduction relation for type environments mimicking that of processes (Table 2). Definition 7. Let -→ be the least relation between type environments such that:

Γ τ -→ Γ Γ , a p : •• [t * s], a p : •• [t * s] map -→ Γ , a p : s ⊥ , a p : s Γ , a p : •• [t 1 + t 2 ], a p : •• [t 1 + t 2 ] map -→ Γ , a p : t ⊥ i , a p : t i i ∈ {1, 2} Γ , a p : •• [unit], a p : •• [unit] ca -→ Γ We write Γ -→ if there exists Γ such that Γ -→ Γ and Γ -→ if not Γ -→. Observe that Γ map -→ implies Γ map -→ and Γ ca -→.
That is, if communication from a p to a p is allowed at some point of an interaction in session a, communication in the opposite direction is forbidden, as is closing a, at the same point. Similarly, Γ ca -→ implies Γ ma+ -→ and Γ ma--→ (in a closing session a no communication is allowed) and Γ ca -→ -→ implies a + , a -∈ fn( ) (once session a has been closed, no more actions are allowed).

The last ingredient we need to state subject reduction is that of balanced type environment: Γ balanced if, whenever there is an association for some valid endpoint a p in Γ , then there are associations also for its peer a p and for a * as well, with the requirement that peer endpoints must have dual types and invalid ones have type ∀A.A. Formally: Definition 8 (balanced type environment). We say that Γ is balanced if:

1. a p ∈ dom(Γ ) with p ∈ {+, -} implies a p , a * ∈ dom(Γ ) and Γ (a p ) ⊥ t Γ (a p ); 2. a * ∈ dom(Γ ) implies Γ (a * ) = ∀A.A.
Remark 1. To appreciate the relevance of condition (2) in Definition 8 consider

P def = close (send a + 42) | let _,x = receive a -in close x | close (send (if true then c + else a + ) 31)
and the environment Γ def = a + , c + : t, a -, c -: t ⊥ , a * , c * : ∀A.A where

t def = •• [int * •• [unit]].
Observe that P is well typed in Γ and that EA(P) holds despite P contains two occurrences of a + , because a + is never actually used twice. We have

P ma+ -→ close a + | let _,x = (42,a -) in close x | close (send (if true then c + else a * ) 31)
where one occurrence of a + has been invalidated and

Γ ma+ -→ a + , a -: •• [unit], c + : t, c -: t ⊥ , a * , c * : ∀A.A def = Γ
Note that a + and c + have the same type in Γ and incompatible types in Γ . If the type of a * could not be instantiated with an arbitrary channel type (t in this case), then the residual process would be ill typed in Γ .

Theorem 2 (subject reduction). If Γ P where Γ is balanced and EA(P) and P -→ Q, then there exists Γ such that Γ -→ Γ and Γ Q.

Protocol fidelity follows immediately from Theorem 2 and the observations below Definition 7: if an -labeled reduction cannot be performed by a type environment Γ , then it cannot be performed by an endpoint affine process that is well-typed in Γ . Communication safety is a straightforward consequence of typing and is formalized below. Note that endpoint affinity suffices for proving both safety and fidelity.

Proposition 1 (safety). Let Γ P and EA(P). Then:

1. if P ≡ E [send u v] | Q, then Γ (u) = •• [t * s] and Γ v : t; 2. if P ≡ E [c u] | Q and c ∈ {left, right}, then Γ (u) = •• [t + s].
Concerning progress, we first give a syntactic characterization of deadlock: Definition 9 (deadlock). We say that P is deadlocked if

P ≡ (νa 1 ) • • • (νa n ) ∏ i∈I E i [c i c p i i ]
where I = / 0 and for every i ∈ I there exists j ∈ I such that c p i i ∈ fn(E j ) and c i ∈ {close, send, receive, left, right, branch}.

Intuitively, in a deadlocked process all threads are blocked on input/output operations and the peer of the (valid) endpoint in each of such operations occurs guarded by another blocked operation. A well-typed, endpoint linear process P enjoys a partial form of progress: if P cannot reduce anymore and is not deadlocked, then P has no pending I/O operations on open sessions.

Theorem 3 (partial progress). If / 0 P and EL(P), then either there exists Q such that P τ -→ Q or P ≡ () or P is deadlocked.

We conclude the section discussing a representative range of errors that go undetected by the type system. In program_A we have two threads connected by two distinct sessions, each thread waits to receive a message from the other one before sending its own. In program_B one thread attempts to use the same session for receiving and sending a message sequentially. Finally, in program_C a thread is sending on channel a its peer b. This example is typeable by giving to b the infinite type t =

•• [t * •• [unit]] and to a its dual t ⊥ .
In all these cases, static detection of the eventual deadlock requires stronger typing disciplines that either prevent the creation of cyclic network topologies [START_REF] Caires | Session types as intuitionistic linear propositions[END_REF][START_REF] Wadler | Propositions as sessions[END_REF][START_REF] Lindley | A semantics for propositions as sessions[END_REF] or rely on non-trivial extensions of session types [START_REF] Bono | Typing Copyless Message Passing[END_REF][START_REF] Bono | Polymorphic Types for Leak Detection in a Session-Oriented Functional Language[END_REF][START_REF] Padovani | Deadlock and Lock Freedom in the Linear π-Calculus[END_REF].

Example 4 (linearity violations). The condition EA(P) ∧ ¬EL(P) indicates that P respects endpoint affinity but discards valid endpoints that may be necessary in order to have progress. For example, the following well-typed program let a, b = create () in close (send a 42) discards b and reduces to a stuck configuration which is not a deadlock. A compiler might give notice of unused value declarations like b in this example, but it would likely stay quiet if b is replaced by an anonymous pattern _ (OCaml behaves like this).

The condition ¬EA(P) indicates that P attempts to use an invalid endpoint. This happens if the endpoint is used more than once, in a way that disrespects the explicit threading of continuations required by the communication primitives. Two instances of this event, which we call overlap, are illustrated below: The function foo can be typed giving

x type •• [int * •• [unit]]
, even though the second send overlaps with the first. A similar problem occurs in bar, where receive overlaps with send. However, the overlap in bar is detected by the type system, because attempting to send and receive a message using the same y requires y to have incompatible capability annotations (•• for send, •• for receive). All the overlaps of send and left/right or of receive and branch are also detected because the * constructor in the types of send and receive is incompatible with the + constructor in the types of left/right. Overall, the only overlaps that can go undetected are those concerning multiple uses of the same communication primitive with the same message types. Undetected overlaps are subtle, though, since their effects are generally unpredictable. In Section 5.2 we will discuss how overlaps can be detected at runtime.

Implementation

We describe the OCaml module that implements the FuSe primitives for session communication. We start with a basic version of the module (Section 5.1) which we then extend with runtime detection of invalid endpoint usage (Section 5.2) and generalized choices (Section 5.3). The extensions are easy for shared-memory processes. We also discuss whether and how they scale to a distributed setting.

The Basics

The OCaml module that realizes the FuSe communication primitives is shown in full in Figure 1. The interface exports the abstract types • and • (lines 1-2) and an abstract channel type (line 3). In OCaml, the channel type t i t o [s] is written (t i ,t o ,s) t and the sum type t + s becomes the polymorphic variant type ['L of t | 'R of s]. We use polymorphic variants [START_REF] Garrigue | Programming with polymorphic variants[END_REF] support a form of subtyping that is consistent with subtyping for session types [START_REF] Gay | Subtyping for Session Types in the π-calculus[END_REF]. We will see these features at work in Section 5.3. The types of the primitives (lines 4-10) are essentially syntactic variations of those shown in Table 5, so we only make a couple of remarks. First, as in FuSe types, we can switch from one channel type to its dual by the mere flipping of its first two type parameters (see e.g. the type of create on line 4). Second, in the type of branch (line 10), the type expression t as ε denotes the same type as t and creates an alias ε that stands for t itself. Such construction has several uses: here, it is handy to refer to the same variant type in the codomain of branch without rewriting the whole type. Since t as ε binds ε also within t, the same construction is also used in OCaml for creating recursive types. We will see an instance of this feature at work in Example 5.

¦ ¥

We have based the implementation of the primitives on the Event module in OCaml's standard library, which provides an API for communication and synchronization in the style of Concurrent ML [START_REF] Reppy | Concurrent Programming in ML[END_REF]. The Event module has been chosen out of mere convenience; our primitives can be built on top of any minimal API for message passing. In the Event module, the type t Event.channel denotes a channel for exchanging messages of type t and the functions Event.send and Event.receive, instead of performing communications directly, construct communication events. In order for com-munication to actually take place, both the sender and the receiver must synchronize by applying Event.sync to such events.

The representation of a channel type (α,β ,ϕ) t is a ϕ Event.channel (line 13), namely channels in FuSe are Event.channels in OCaml. Note that α and β play no role in the representation of channel types; they are meant to be instantiated with • and • which have no data constructors (lines 11-12). Polarities are not represented either, they are an artifact of the formal model so that peer endpoints can be typed differently.

The implementation of create (line 14) and close (line 15) is dull: the first creates an Event channel and returns a pair with two references (with dual types) to it; the second does nothing (OCaml's garbage collector automatically reclaims unused channels).

Concerning the implementation of send (line 16), we have to keep in mind that the Event.channel underlying our endpoints expects messages that, in principle, contain both the payload x as well as the continuation endpoint u, but we only communicate the payload x. For this reason, we cast x using Obj.magic so that x appears to the type checker as having the type of the pair (x, u). This cast cannot compromise the correct functioning of the Event module: since the Event.channel type is parametric in the type of messages, Event functions cannot make any assumption on their concrete representation. The value returned by send is the same reference u used for the communication, except that its type is cast to the dual type of the continuation. The trickery in send forces a corresponding implementation of receive (line 17): OCaml believes that the event created by Event.receive yields a pair consisting of a payload and a continuation, whereas only the former is actually received. We explicitly pair the endpoint u (which is known to the receiver) to the payload, and we perform another cast so that the pair is typed correctly.

The implementation of left, right, and branch (lines 18-20) follows the same lines. In these cases, only a tag 'L or 'R is communicated, instead of the continuation channel u injected through one of such tags as the type of left and right suggests. The injection is performed on the receiver's side and resorts to one last magic: since the internal OCaml representation of 'K u -that is channel u injected through the K tag -is the same as that of the pair ('K, u), we create such a pair and cast its type to that of the injected channel. This trick spares us one pattern matching on the tag and scales to arbitrary tag sets (see Section 5.3).

Example 5 (session type inference and duality). Below are the types of server and client from Example 1 that OCaml infers automatically when these functions are linked against the module that implements FuSe primitives:

val server : (•,•,[ 'R of (•,•,int * (•,•,int * (•,•,int * (•,•,α) t) t) t) t | 'L of (•,•,unit) t ] as α) t ↓ -unit val client : int ↓ - (•,•,[ 'R of (•,•,int * (•,•,int * (•,•,int * (•,•,α) t) t) t) t | 'L of (•,•,unit) t ] as α) t ↓ -int
These two types correspond exactly to those we have guessed in Example 2. Since the channel type in the type of server is dual of the channel type in the type of client, § ¤ where the initial value for the partial result acc is 0.0 instead of 0, therefore turning acc's type from int to float. Taken in isolation, client' is well typed and OCaml infers the following type for it:

val client' : int ↓ - (•,•,[ 'R of (•,•,float * (•,•,int * (•,•,float * (•,•,α) t) t) t) t | 'L of (•,•,unit) t ] as α) t ↓ -float
However, the channel types of client' and server are not dual of each other (the corresponding message types are not unifiable). OCaml detects this problem and fails to compile a program that connects client' and server with a session.

Runtime Detection of Invalid Endpoint Usages

Figure 2 extends our module with the endpoint invalidation semantics of FuSe so that an exception (declared on line 1) is raised whenever an invalid endpoint is used. Note that invalidation in the formal model is a rather powerful mechanism that acts atomically on all the occurrences of an endpoint in a possibly distributed program. The code in Figure 2 implements the invalidation semantics assuming that processes have access to a shared memory. The idea is to represent endpoints as pairs consisting of an Event.channel and a mutable flag indicating whether the endpoint is valid or not (line 4). The flag effectively approximates the endpoint polarity, with the difference that it only distinguishes between valid and invalid endpoints. Whenever a thread attempts to use an endpoint, the flag in the pair is checked first: if the flag is true, then the endpoint is valid and can be used; if the flag is false, then the endpoint has already been used and an exception is raised. The auxiliary function check (lines 5-6) implements this behavior. Checking that the flag is true and setting it to false must be performed atomically, for concurrent threads may attempt to use the same endpoint simultaneously. Therefore, we realize check using a conventional compare_and_swap operation, whose implementation is undetailed.

Ideally, when a communication primitive returns a continuation endpoint, the flag associated with the endpoint should be restored to true, but doing so on the existing pair might induce other users of the endpoint into thinking that the reference they own is valid, while in fact it is not. The idea is that communication primitives return a fresh pair that contains the same Event.channel in the old pair with a fresh flag reset to true. This refreshing of pairs is implemented by the auxiliary function fresh (line 7). In essence, the cost we pay for detecting the usage of invalid endpoints is the allocation of a new pair and a bool reference at each invocation of a communication primitive.

With this setup, the communication primitives can be implemented by prefixing them with a call to check and wrapping the returned Event.channel(s) with fresh (lines 8-14). In Figure 2 we have elided with ... the unchanged code fragments from Figure 1. Observe that check and refresh remain confined within the module, which exports the same interface it had before, plus the InvalidEndpoint exception.

The naive generalization of this mechanism to a distributed setting requires maintining the consistency of the flag associated with each endpoint across different locations and is clearly unfeasible (recall that endpoints can be communicated in messages). Nonetheless, the mechanism can be adapted to a distributed setting if we assume that communicated endpoints are always meant to be used by the receiver. Otherwise, an endpoint could be sent in a message and simultaneously retained and used by the sender, making it unusable by the receiver. The idea is that an endpoint being sent in a message is invalidated in the sender, electing the receiver as the only owner of a valid reference to the endpoint. As a result, across the whole distributed system, there is always at most one location containing valid references to the roaming endpoint, and linearity violations within such location can be efficiently detected using the code shown in Figure 2. This mechanism can be implemented either by runtime inspection of exchanged messages, or by means of a dedicated primitive for sending endpoints (like throw in [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF]). Both possibilities are very reasonable, given that the communication of endpoints in a distributed environment is likely to require some special handling anyway.

Generalized Choices

Although binary choices suffice to model protocols with an arbitrary branching structure, being able to use multiple tags, with possibly meaningful names, is desirable. The main challenge with generalizing choices to arbitrary tags is that the tags appear explicitly in the types of left, right, and branch, whereas we would like the interface of our library to be as general as possible. One solution is to replace left and right with a generic selection primitive select and revise branch so that select and branch have these types:

val select : (•,•,[>] as ϕ) t ↓ -((α,β,ψ) t ↓ -ϕ) ↓ -(β,α,ψ) t val branch : (•,•,[>] as ϕ) t ↓ -ϕ
The semantics of branch is simply to receive a message of type ϕ. The semantics of select is similar to that of send, except that send takes a message ready to be sent, whereas select takes a function of type (α,β ,ψ) t ↓ ϕ which produces the message, of type ϕ, when applied to a continuation endpoint of type (α,β ,ψ) t. Typically, such function will be the η-expansion of a tag

fun x ↓ -'Tag x
that injects a continuation channel into a polymorphic variant type. The type expression [>] as ϕ in the types of select and branch indicates that ϕ can only be instantiated with a polymorphic variant type. This constraint is crucial for the safety of the library: leaving ϕ unconstrained would make the type (α,β ,ϕ) t unifiable with the type (α,β ,ψ * (γ,δ ,ε) t) t and an ordinary message sent with send could be received with branch as if it were a label, or a label selected with select could be received with receive as if it were an ordinary message.

The implementation of select and branch is similar to that of send and receive, with the difference that select transfers the function over the channel, camouflaging the function as if it were the message produced by the function:

let select u f = Event.sync (Event.send u (Obj.magic f)); Obj.magic u let branch u = Obj.magic (Event.sync (Event.receive u)) u
This handling of arbitrary tags does not scale well to a distributed setting, because sending a function over a channel assumes that sender and receiver share the same address space and trust each other. It is not clear, however, if a really general solution exists in this case. After all, the tags occurring in a protocol are domain-specific, and it might be reasonable for applications to provide specialized versions of select and/or branch that involve the transfer of only the tag, as we have done for left and right. Example 6. Below is a revised and extended version of Example 1 where the mathematical server supports three operations identified by the tags 'Quit, 'Plus, and 'Eq and the client uses select to choose the appropriate ones. It is instructive to look at the types inferred by OCaml for these two functions:

val server : (•,•,[< 'Eq of (•,•,β * (•,•,β * (•,•,bool * (•,•,α) t) t) t) t | 'Plus of (•,•,int * (•,•,int * (•,•,int * (•,•,α) t) t) t) t | 'Quit of (•,•,unit) t ] as α) t ↓ -unit val client : int ↓ -((•,•,[> 'Plus of (•,•,int * (•,•,int * (•,•,int * α) t) t) t | 'Quit of (•,•,unit) t ]) t as α) ↓ -int
Notice that server is parametric in the type β of the operands of the 'Eq operation, as a consequence of the fact that equality is polymorphic in OCaml. Also, the type of x is not exactly the dual of the type of y, because the choice in one type has three tags 'Eq, 'Plus, and 'Quit while the other one has only two. The question then is whether OCaml is able to infer that client and server interact successfully, despite this mismatch in the types of the endpoints they use. This is indeed the case, and the reason lies in the < and > symbols that decorate variant types. The < symbol indicates a closed variant type, one for which the set of tags constitutes an upper bound: the match in the server body handles three tags 'Eq, 'Plus, 'Quit, but not others. The > symbol indicates an open variant type, one for which the set of tags constitutes a lower bound: the 'Plus and 'Quit tags may be produced by client, but this variant type is unifiable with others providing a superset of tags, like the one in the type of x. In conclusion, the rules governing variant types allow OCaml to infer that client and server interact successfully because client needs only a subset of the operations provided by server. If client attempted to use a 'Mult operation, OCaml would signal an error at the point where client and server are connected through a session.

The fact that the revised server interacts correctly with client, despite the type of x is not exactly dual to that of y, is formally explained in terms of subtyping for session types [START_REF] Gay | Subtyping for Session Types in the π-calculus[END_REF]: the dual of the type of x is a subtype of the type of y, meaning that client uses fewer features than those offered by server. We exploit once more the encoding of session types into ordinary types to lift OCaml's built-in subtyping of variant types at the level of channel (and therefore protocol) types.

Concluding Remarks

Inspired by the encoding of session types into (linear) channel types [START_REF] Dardha | Session types revisited[END_REF], we have shown how to realize some key features of a session type system in terms of ordinary features of any type system with generic types. The choice of OCaml for our proof-of-concept implementation allowed us to showcase the full potential of the approach in exchange for the least effort. Nonetheless, the approach is applicable to a broad range of programming languages, albeit with varying degrees of integration and/or convenience.

Substructural type systems are becoming increasingly popular in theoretical models of programming languages, but they are (still) rare in practice. This fact motivated our quest for an alternative handling of linearity violations that could be easily implemented as part of our library for session communications. The typing discipline resulting from our approach is nonetheless able to detect a number of linearity violations (Example 4) and, if the host language supports affine/linear types, the typing of the communication primitives can be easily refined to statically enforce affine/linear endpoint usage.

The choice of synchronous communication in both the formal model and the implementation was motivated by convenience. Asynchronous communication can be modeled like in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF] using explicit queues, adjusting the formal semantics so that the peers of a session are invalidated independently, and basing the implementation on a suitable asynchronous API. The use of a single primitive create to open new sessions has been inspired by Singularity OS [START_REF] Hunt | An Overview of the Singularity Project[END_REF][START_REF] Bono | Typing Copyless Message Passing[END_REF]. Most session calculi and languages provide a pair of accept/request primitives to establish sessions via shared channels [START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF][START_REF] Gay | Linear type theory for asynchronous session types[END_REF]. Shared channels, accept, and request do not pose particular challenges and the implementation (available online) features them already.

A more substantial extension concerns multiparty sessions [START_REF] Honda | Multiparty asynchronous session types[END_REF], those involving an arbitrary, possibly fixed number of participants. It has been shown that some classes of multiparty sessions can be realized in terms of binary sessions connecting pairs of participants (see [25, extended version] and [START_REF] Caires | A typeful characterization of multiparty structured conversations based on binary sessions[END_REF]). As it stands, our approach could deal with each binary session in isolation, but would be unable to recognize the sessions as part of a single multiparty session. Whether the approach can be extended to model "true" multiparty sessions remains an open question.

Related work. Our work aims at the same objectives as [START_REF] Neubauer | An implementation of session types[END_REF][START_REF] Pucella | Haskell session types with (almost) no class[END_REF], but follows a substantially different approach. We focus the comparison on linearity and type representation.

The typing disciplines proposed in [START_REF] Neubauer | An implementation of session types[END_REF][START_REF] Pucella | Haskell session types with (almost) no class[END_REF] rely on monads to simultaneously track the changes in the types of endpoints (F.3) and enforce their linear usage (F.4). We realize (F.3) using the same technique as [START_REF] Gay | Linear type theory for asynchronous session types[END_REF] and rely on the runtime system to detect those linearity violations that may compromise safety. The monadic approach gives stronger static guarantees concerning linearity, but has a cost in terms of either expressiveness or usability: in [START_REF] Neubauer | An implementation of session types[END_REF], monadic computations can involve a single channel only; in [START_REF] Pucella | Haskell session types with (almost) no class[END_REF], channels (or, better, their capabilities) are encapsulated and stacked in the monad, and the programmer must write explicit monadic actions that literally dig into the stack to reach the channel/capability to be used. The provided linearity guarantees weaken to affinity in presence of exceptions, which are a known challenge for substructural type systems. We give up on static detection of (all) linearity violations in favor of a lighter and more open-ended API. Not committing to a specific mechanism, our approach can immediately benefit from native support for affine/linear typing from the host language, if available, or can be complemented by a monadic API in the style of [START_REF] Pucella | Haskell session types with (almost) no class[END_REF], if desired.

Both [START_REF] Neubauer | An implementation of session types[END_REF] and [START_REF] Pucella | Haskell session types with (almost) no class[END_REF] propose a faithful modeling of session types as sequences of I/O actions and internal/external choices, whereas we work with session types encoded into ordinary types [START_REF] Dardha | Session types revisited[END_REF]. Our approach improves the results of [START_REF] Neubauer | An implementation of session types[END_REF][START_REF] Pucella | Haskell session types with (almost) no class[END_REF] in various respects. Duality is not addressed in [START_REF] Neubauer | An implementation of session types[END_REF] and is expressed in [START_REF] Pucella | Haskell session types with (almost) no class[END_REF] using rather sophisticated mechanisms, such as multiparameter type classes and functional dependencies or explicitly provided duality proofs. We have shown that none of these mechanisms is necessary: duality for encoded session types can be expressed in terms of type equality in any type system with generic types. In general, the encoding favors a smoother integration of (encoded) session types within built-in features of the host language. This is clear by looking at the handling of choices and recursion. In Section 5 we have used OCaml polymorphic variants to model choices, but we could have used plain algebraic data types as well. In Scala it might be reasonable to use case classes, and in languages like Java or C++ one could rely on specific class hierarchies. In summary, encoded internal/external choices can be modeled using idiomatic features of the host language, favoring the integration with native notions of subtyping when available (Example 6). We can make similar observations concerning recursion. In [START_REF] Pucella | Haskell session types with (almost) no class[END_REF], recursive session types are represented using de Brujin indexes and type-level Peano numerals and require the programmer to write explicit monadic actions for entering/invoking recursions. We have shown that none of these mechanisms is necessary if the host language features recursive types: the encoding lifts native recursive types to recursive session types transparently (Example 5) and allows the programmer to write recursive/iterative code according to the language style (Example 1).

We conclude observing that the runtime detection of linearity violations is somehow related to the runtime monitoring of session communications [START_REF] Tzu-Chun Chen | Asynchronous distributed monitoring for multiparty session enforcement[END_REF][START_REF] Bocchi | Monitoring networks through multiparty session types[END_REF][START_REF] Demangeon | Practical interruptible conversations: distributed dynamic verification with multiparty session types and python[END_REF][START_REF] Bartoletti | Compliance and subtyping in timed session types[END_REF]. Runtime monitoring is achieved either by a service [START_REF] Tzu-Chun Chen | Asynchronous distributed monitoring for multiparty session enforcement[END_REF][START_REF] Bocchi | Monitoring networks through multiparty session types[END_REF][START_REF] Demangeon | Practical interruptible conversations: distributed dynamic verification with multiparty session types and python[END_REF] or by an active communication middleware [START_REF] Bartoletti | Compliance and subtyping in timed session types[END_REF] that compares the observable behavior of processes against the declared contracts/session types and possibly issues notifications when violations are detected. Like monitoring, our runtime mechanism is meant to ensure communication safety and protocol fidelity. Unlike monitoring, our mechanism is internal to processes and only detects linearity violations, which would not necessarily imply corresponding protocol violations in their observable behavior.

analogous. We have to show that there exist S 1 and S 2 such that S = !S 1 .S 2 and S i R T i for every i = 1, 2. We derive:

S = T = !T 1 .T 2 by definition of T = •• [ T 1 * T ⊥ 2 ] by definition of • = ! T 1 . T ⊥ 2 ⊥ by definition of • = ! T 1 . T ⊥ 2 ⊥ by Theorem 1 = ! T 1 . T 2
because duality is an involution and we conclude by taking S i def = T i and observing that S i R T i by definition of R for every i = 1, 2.

Concerning the relation id S ⊆ R, take (S, T ) ∈ id S , meaning S = T . We have to show that S R T . By definition of R we have T R T and from the relation R ⊆ id S we deduce T = T = S. We conclude by definition of R.

B Supplement to Section 4 B.1 Polymorphic References

Here we show why the standard example that motivates the value restriction in the typing rule for let [START_REF] Wright | A syntactic approach to type soundness[END_REF] is not a counterexample for the soundness of our type system, despite our rule for let generalizes type variables even when the bound expression is not a value. To begin with, we define an OCaml module Ref that models mutable references using sessions: The module exports four functions ref, delete, set, and get. The first two functions respectively create and destroy a mutable reference, while set and get respectively set and retrieve the content of a reference. According to ref, a mutable reference is a thread whose body is represented as a recursive function aux parameterized on the current value v0 stored in the reference and an endpoint x on which the reference listens for three kinds of operations, identified by the tags Delete, Set, and Get. The functions delete, set, and get simply select the corresponding operation and possibly perform the required I/O. OCaml infers the following signature for Ref:

module Ref : sig val ref : α ↓ -(•,•,[< 'Delete of (•,•,unit) t | 'Get of (•,•,α * (•,•,β) t) t | 'Set of (•,•,α * (•,•, b) t) t ] as β) t val delete : (•,•,[> 'Delete of (•,•,unit) t ]) t ↓ -unit val set : (•,•,[> 'Set of (•,•,α * (β,γ,δ) t) t ]) t ↓ -α ↓ -(γ,β,δ) t val get : (•,•,[> 'Get of (•,•,α * (β,γ,δ) t) t ]) t ↓ -α * (β,γ,δ) t end
Now we try to use this implementation of mutable references to reproduce the counterexample in [START_REF] Wright | A syntactic approach to type soundness[END_REF]. The first attempt is based on the program below, which respects the threading in the use of r as required by our EL predicate: On each line we show the type of each binding. Note that the type of r is generalized on line 1 according to our rule [T-LET], but it is subsequently instantiated on line 2. Therefore, by the time an attempt is made to apply the function stored in r to true, the type of r correctly records the fact that the type of the function is int ↓ -int (line 3) and its application to true is flagged as ill typed (line 4).

The second attempt is based on a program that disrespects the threading of the use of r, so that its polymorphic type can be instantiated multiple times: This program is well typed thanks to our rule [T-LET], which generalizes the type variables in the type of r (line 1). However, by the time the reference r is accessed for the get operation (line 3), it has been invalidated by the previous set operation (line 2), therefore the program results in a runtime error. In general, all the programs in which rule [T-LET] yields dangerous generalizations either are ill typed or they violate the EA predicate. Therefore, the premises of Theorem 2 suffice to establish subject reduction.

B.2 Subject Reduction for Expressions

We just recall the key type preservation result from [START_REF] Wright | A syntactic approach to type soundness[END_REF], whose proof only requires minor adaptations concerning the set of values in FuSe.

Lemma 1 (subject reduction for expressions). If Γ e : t and e -→ e , then Γ e : t.

Proof. This is a straightforward adaptation of [START_REF] Wright | A syntactic approach to type soundness[END_REF]Lemma 4.3], where the values include a few more cases.

1. If Γ e : t, then Γ , Γ e : t; 2. If Γ P, then Γ , Γ P.

Proof. Standard properties of any non-substructural type system.

Structural congruence alters the basic arrangement of processes without affecting typing.

Lemma 6 (congruence preserves typing). If Γ P and P ≡ Q, then Γ Q.

Below is the statement of subject reduction of processes (Section 4) with its full proof. The result is essentially standard, except for the fact that endpoints may be invalidated in the reduct. The hypothesis EA(P) suffices to exclude the possibility that error occurs in the reduct.

Theorem 2 (subject reduction for processes). If Γ P and Γ is balanced and EA(P) and P -→ Q, then there exist Γ such that Γ -→ Γ and Γ Q.

Proof. By induction on the derivation of P -→ Q and by cases on the last rule applied. [R-RIGHT] Symmetric of the previous case.

[R-ERROR] Then P = E [c a * ] and Q = error and = τ. This case is impossible for it contradicts the hypothesis EA(P). [R-NEW-1] Then P = (νa)P and P -→ Q and Q = (νa)Q and = τ and is either map or ca. From [T-NEW] we deduce Γ , a + : t, a -: t ⊥ , a * : ∀A.A P . Observe that Γ , a + : t, a -: t ⊥ , a * : ∀A.A is balanced if so is Γ . We distinguish two subcases, depending on the shape of .

-If = ca, then by induction hypothesis we deduce Γ , a * : ∀A.A Q . By Lemma 5, we deduce Γ , a + : t, a -: t ⊥ , a * : ∀A.A Q and we conclude by taking Γ = Γ and one application of [R-NEW-2] Then P = (νa)P and P -→ Q and Q = (νa)Q and a p ∈ fn( ). From [T-NEW] we deduce Γ , a + : t, a -: t ⊥ , a * : ∀A.A P . Observe that Γ , a + : t, a -: t ⊥ , a * : ∀A.A is balanced if so is Γ . By induction hypothesis we deduce Γ , a + : t, a -: t ⊥ , a * : ∀A.A Q for some Γ such that Γ -→ Γ . We conclude with an application of [T-NEW].

[R-STRUCT] A simple induction using Lemma 6.

B.4 Soundness

This section contains the proof of partial progress (Theorem 3). The first auxiliary result provides a syntactic characterization of those expressions that are unable to reduce further. These are not necessarily values, for expressions may contain instances of the communication primitives that reduce only at the level of processes. Proof. If e is a value there is nothing left to prove, so we assume that e is not a value and proceed by induction on the structure of e and by cases on its shape, excluding the case when e is a variable. We only discuss the case when e = e 1 e 2 , the others being simpler or similar.

-If e 1 is not a value, then from the hypothesis e -→ we deduce e 1 -→. From the hypothesis Γ e : t we deduce Γ e 1 : s ↓ -t. By induction hypothesis we deduce that there exist E , c, and v such that e 1 = E [c v] where c ∈ {(), fix}. We conclude by taking E = E e 2 .

-If e 1 is a value but e 2 is not, then from the hypothesis e -→ we deduce e 2 -→. From the hypothesis Γ e : t we deduce Γ e 2 : s for some s. By induction hypothesis we deduce that there exist E , c, and v such that e 2 = E [c v] where c ∈ {(), fix}. We conclude by taking E = e 1 E . -If both e 1 and e 2 are values, then from the hypothesis e -→ we can exclude the possibility that e 1 is an abstraction or fix, for in these cases e always reduces. From the hypothesis Γ e : t we deduce that Γ e 1 : s ↓ -t. By inspecting the syntax of values and looking at Table 5, there are two possibile values other than abstractions and fix that can have arrow type. Either e 1 is a constant c ∈ {(), fix}, in which case we conclude by taking E = [ ] and v = e 2 , or e 1 has the form c v where c ∈ {fork, send}, in which case we conclude by taking E = [ ]e 2 .

Theorem 3 (partial progress). If / 0 P and EL(P), then either there exists Q such that P τ -→ Q or P ≡ () or P is deadlocked.

Proof. Observe that P -→ implies = τ, because P is typed in an empty environment and so is a closed process. Suppose that P τ -→ and P ≡ () , for otherwise there is nothing left to prove. Using structural congruence, we can always derive P ≡ (νa 1 ) • • • (νa n ) ∏ i∈I e i where I = / 0. From the hypothesis P τ -→ we deduce e i -→ for every i ∈ I and from the hypothesis / 0 P we know that each e i is well typed and has type unit. Hence, from Lemma 7 we deduce that for every i ∈ I either e i is a value or there exist E i , c i , and v i such that e i = E i [c i v i ] where c i ∈ {(), fix}. Since the only value of type unit is (), we can assume that none of the e i is (), for such threads could be removed by structural congruence. From the hypothesis P τ -→ we also deduce that none of the c i is create or fork, for otherwise P would be able to reduce according to the rules in Table 2. In summary, we can derive

P ≡ (νa 1 ) • • • (νa n ) ∏ i∈I E i [c i v i ]
where c i ∈ {(), fix, fork, create} for every i ∈ I.

From the hypothesis / 0 P we deduce that for all i ∈ I there exist c i and p i such that v i = c p i i . Therefore we derive P ≡ (νa 1 )

• • • (νa n )Q where Q = ∏ i∈I E i [c i c p i i ]
. We observe that if c i = send, then E i = [ ] because the partial application send v i cannot have type unit. Therefore, all the applications of send are saturated and ready to synchronize with the corresponding receive, if this occurred in an evaluation context. From the hypothesis EL(P), we also know that p i ∈ {+, -} for every i ∈ I. Now, from the hypotheses / 0 P and [T-NEW], we know that there exists Γ balanced such that Γ Q. Consider i ∈ I. From the hypothesis EL(P) we deduce that c p i i must occur somewhere in P. We reason by cases on c i , and discuss only one case, when c i = send, the others being analogous. Then, there exist t and s such that Γ c p i i : j for some j ∈ I. It cannot be the case that c j = receive, for otherwise P would be able to reduce, therefore c j ∈ {send, left, right, branch}. But this is impossible too, either because the capability annotation in the type of the endpoint is incompatible with •• (when c j ∈ {send, left, right}, or because the message type has a topmost + type constructor, while it should have a topmost * type constructor (when c j = branch). In conclusion, we deduce that c p i i cannot be any of the c p j j for j ∈ I. Therefore, it must be the case that c p i i ∈ fn(E j ) for some j ∈ I.

  let foo x 0 = let n, x 1 = receive x 0 in (* x 0 : ?[int * ![bool * Ø[unit]]] *) let x 2 = send x 1 (n = 0) in (* x 1 : ![bool * Ø[unit]] *) close x 2 (*x 2 : Ø[unit] *) let bar y 0 = let y 1 = send y 0 42 in (* y 0 : ![int * ![bool * Ø[unit]]] *) let b, y 2 = receive y 1 in (* y 1 : ?[bool * Ø[unit]] *) close y 2 ; print b (* y 2 : Ø[unit] *)

Example 3 (

 3 deadlocks). Below are some typical examples of endpoint linear programs that eventually deadlock. let program_A = let worker x y = let z, x = receive x in let y = send y z in close x; close y in let a, b = create () in let c, d = create () in fork (worker a) d; fork (worker c) b let program_B = let a, b = create () in let n, a = receive a in let b = send n in close a; close b let program_C = let a, b = create () in close (send a b)

  let foo x = let _ = send x 42 in let x = send x 43 in (* *) close x let bar y = let _ = send y 42 in let _, y = receive y in (* *) close y

Fig. 1 .

 1 Fig. 1. Interface and implementation of the OCaml module for session communications.

Fig. 2 .

 2 Fig. 2. Implementation of session communications with invalid endpoint detection.

  x = receive x in let m, x = receive x in let x = send x (n + m) in server s | 'Eq x ↓ let n, x = receive x in let m, x = receive x in let x = send x (n = m) in server s let client n y = let rec aux acc n y = if n = 0 then begin let y = select y (fun x ↓ -'Quit x) in close u; acc end else let y = select y (fun x ↓ -'Plus x) in let y = send y acc in let y = send y n in let res, y = receive y in aux res (n -1) u in aux 0 n u

  , x = receive x in aux v x | 'Get x ↓ -let x = send x v in aux v x in let a, b = create () in let _ = Thread.create (aux v0) a in b let delete r = close (select r (fun x ↓ -'Delete x)) let set r = send (select r (fun x ↓ -'Set x)) let get r = receive (select r (fun x ↓ -'Get x)) end

  let r = Ref.ref (fun x ↓ -x) in (* r : ∀α.(α ↓ α) ref *) let r = Ref.set r (fun x ↓ -x + 1) in (* r : (int ↓ -int) ref *) let f, r = Ref.get r in (* f : int ↓ -int, r : (int ↓ -int) ref *) f true (* type error *)

  [R-FORK] Then P = E [fork v w] and Q = E [()] | vw and = τ. From [T-THREAD] we deduce Γ E [fork v w] : unit. From Lemma 3 and TypeOf(fork) we deduce that Γ fork v w : unit and Γ v : t ↓ -unit and Γ w : t. From Lemma 4 we deduce Γ E [()] : unit. From [T-APP] we deduce Γ vw : unit. We conclude with two applications of [T-THREAD] and one application of [T-PAR] by taking Γ= Γ . [R-CREATE] Then P = E [create()] and Q = (νa) E [(a + ,a -)]where a is fresh and = τ. From [T-THREAD] we deduce Γ E [create()] : unit. From Lemma 3 and TypeOf(create) we deduce Γ create() : t * t ⊥ . Since a is fresh we have a + , a -, a * ∈ dom(Γ ). From Lemma 4 we deduce Γ , a + : t, a -: t ⊥ , a * : ∀A.A E [(a + ,a -)] : unit. We conclude with one application of [T-THREAD] and one application of [T-NEW] by taking Γ = Γ . [R-CLOSE] Then P = E [close a p ] | E [close a p ] ] and Q = E [()] | E [()] and = ca. From [T-PAR] and [T-THREAD] we deduce Γ E [close a p ] : unit and Γ E [close a p ] : unit. From Lemma 3 and TypeOf(close) we deduce Γ (a p ) = Γ (a p ) = •• [unit] and Γ close a p : unit and Γ close a p : unit. Therefore, Γ = Γ , a p : •• [unit], a p : •• [unit] for some Γ such that Γ -→ Γ . From Lemma 4 we deduce Γ E [()] : unit and Γ E [()] : unit. We conclude with two applications of [T-THREAD] and one application of [T-PAR]. [R-COMM] Then P = E [send a p v] | E [receive a p ] and Q = E [a p ] | E [(v,a p )] and = map. From the hypothesis Γ P and rules [T-PAR] and [T-THREAD] we deduce that Γ E [send a p v] : unit and Γ E [receive a p ] : unit. From Lemma 3 and TypeOf(send) and the hypothesis that Γ is balanced we deduce that there exists Γ such that Γ = Γ , a p : •• [t * s], a p : •• [t * s] and Γ send a p v : s ⊥ and Γ v : t. From Lemma 3 and TypeOf(receive) we deduce that and Γ receive a p : t * s. Let Γ def = Γ , a p : s ⊥ , a p : s and observe that Γ -→ Γ . From Lemma 4 we derive Γ E [a p ] : unit. From one application of [T-PAIR] and Lemma 4 we derive Γ E [(v,a p )] : unit. We conclude with two applications of [T-THREAD] and one application of [T-PAR]. [R-LEFT] Then P = E [left a p ] | E [branch a p ] and Q = E [a p ] | E [L a p ] and = map. From the hypothesis Γ P and rules [T-PAR] and [T-THREAD] we deduce that Γ E [left a p ] : unit and Γ E [branch a p ] : unit. From Lemma 3 and TypeOf(left)and the hypothesis that Γ is balanced we deduce that there exists Γ such that Γ = Γ , a p : •• [t + s], a p : •• [t + s] and Γ left a p : t ⊥ . From Lemma 3 and TypeOf(branch) we deduce that Γ branch a p : t + s. Let Γ def = Γ , a p : t ⊥ , a p : t and observe that Γ -→ Γ . From Lemma 4 we derive Γ E [a p ] : unit. From one application of [T-LEFT] and Lemma 4 we derive Γ E [L a p ] : unit. We conclude with two applications of [T-THREAD] and one application of [T-PAR].

  [R-PAR] Then P = P | R and P -→ Q and Q = Q | R . From [T-PAR] we deduce Γ P and Γ R. By induction hypothesis we deduce Γ Q for some Γ such that Γ -→ Γ . From Lemma 2 we deduce that Γ R . We conclude with an application of [T-PAR].

  [T-NEW].-If = map, then by induction hypothesis we deduce that there exists s such that Γ , a + : t, a -: t ⊥ , a * : ∀A.A map -→ Γ , a + : s, a -: s ⊥ , a * : ∀A.A and Γ , a + : s, a -: s ⊥ , a * : ∀A.A Q . We conclude by taking Γ = Γ and one application of [T-NEW].

Lemma 7 .

 7 Let Γ ground and Γ e : t and e -→. Then either e is a value or there exist E , c, and v such that e = E [c v] where c ∈ {(), fix}.

Table 1 .

 1 Syntax of FuSe expressions and processes.

	Expression	e ::= c		(constant)
		| u		(name)
		| fun x	↓ -e	(abstraction)
		| e 1 e 2		(application)
		| (e 1 ,e 2 )	(pair construction)
		| K e		(sum injection)
		| let x = e 1 in e 2	(let binding)
		| let x,y = e 1 in e 2	(pair splitting)
		| match e with {i x i	↓ -e i } i=L,R (case analysis)
	Process P, Q ::= e		(thread)
		| P | Q		(composition)
		| (νa)P	(session)
		| error	(runtime error)

Table 2 .

 2 Reduction of FuSe expressions and processes.

	Reduction of expressions	e -→ e
	[R-BETA]

  • • • ∀α n .t with ∀α 1 • • • α n .t. Types t, s are the regular trees generated by the type constructors in Table 3 and include the unitary type unit, arrows, products, and disjoint sums. In the examples we occasionally use other base types such as int and bool. The types • and • respectively denote the absence and presence of a certain input/output capability in a channel type. They are not inhabited and are only used as

Table 3 .

 3 Syntax of types, type schemes, and session types.

	Type t, s ::= α	(variable)	Type scheme	σ ::= t	(mono type)
	| •		(no cap.)		| ∀α.σ (poly type)
	| •		(one cap.)
	| unit (unit)	Session type T, S ::= end	(termination)
	| t	↓ -s (arrow)		| ?T .S (input)
	| t * s (product)		| !T .S (output)
	| t + s (sum)		| T & S	(external choice)
	| t t [t] (channel)		| T ⊕ S (internal choice)
	phantom type parameters. A channel type t i t o [s] has three type parameters: t i and t o
	respectively represent the input and output capabilities of the channel and are always
	either a type variable or • or •; s is the type of the messages that can be sent on/received
	from the channel. For example, •• [int] is a channel type without input capability (•)
	and with output capability (•), hence it denotes a channel for sending messages of type
	int; the type

  •• [int * •• [bool]] denotes a channel for receiving a pair whose first component has type int and whose second component is another channel that can be used for sending a bool. A channel with type •• [t] bears no capabilities and cannot be used for I/O operations. Channel types•• [t] have no role in FuSe.

Table 4 .

 4 Typing rules for expressions and processes.

	Expressions	Γ e : t
	[T-CONST]

Table 5 .

 5 Type schemes of FuSe constants.

() : unit fix : ∀α.(α

  because they easily generalize sums to arbitrary tags and

	§			Interface	¤
	type •	(* absent I/O capability *)
	type •	(* present I/O capability *)
	type (α,β,ϕ) t	(* channel type	*)
	val create	: unit	↓ -(α,β,ϕ) t * (β,α,ϕ) t
	val close	: (•,•,unit) t	↓ -unit
	val send	: (•,•,ϕ * (α,β,ψ) t) t	↓ -ϕ	↓ -(β,α,ψ) t
	val receive	: (•,•,ϕ * (α,β,ψ) t) t	↓ -ϕ * (α,β,ψ) t
	val left	: (•,•,['L of (α,β,ϕ) t | 'R of (γ,δ,ψ) t]) t	↓ -(β,α,ϕ) t
	val right	: (•,•,['L of (α,β,ϕ) t | 'R of (γ,δ,ψ) t]) t	↓ -(δ,γ,ψ) t
	val branch ¦	: (•,•,['L of (α,β,ϕ) t | 'R of (γ,δ,ψ) t] as ε) t	↓ -ε	¥
	§			Implementation	¤
	type •	(* no representation *)
	type •	(* no representation *)
	type (α,β,ϕ) t = ϕ Event.channel
	let create () = let u = Event.new_channel () in (u, u)
	let close _	= ()
	let send u x	= Event.sync (Event.send u (Obj.magic x)); Obj.magic u
	let receive u = Obj.magic (Event.sync (Event.receive u), u)
	let left u

= Event.sync (Event.send u (Obj.magic 'L)); Obj.magic u let right u = Event.sync (Event.send u (Obj.magic 'R)); Obj.magic u let branch u = Obj.magic (Event.sync (Event.receive u), u)

  •• [t * s] and Γ c

	p i i : •• [t * s]. Suppose that c	p i i = c	p j

[T-ARROW] Γ , x : t e : s Γ fun x ↓ -e : t ↓ -s [T-LET] Γ e 1 : t 1 Γ , x : Close(t 1 , Γ ) e 2 : t 2 Γ let x = e 1 in e 2 : t 2 [T-APP] Γ e 1 : t ↓ -s Γ e 2 : t Γ e 1 e 2 : s [T-PAIR] Γ e i : t i (i=1,2) Γ (e 1 ,e 2 ) : t 1 * t 2 [T-SPLIT] Γ e 1 : t 1 * t 2 Γ , x : t 1 , y : t 2 e 2 : t Γ let x,y = e 1 in e 2 : t [T-LEFT] Γ e : t Γ L e : t + s [T-RIGHT] Γ e : s Γ R e : t + s [T-MATCH] Γ e : t 1 + t 2 Γ , x i : t i e i : t (i=L,R) Γ match e with {i x i ↓ -e i } i=L,R : t Processes Γ P [T-THREAD] Γ e : unit Γ e [T-PAR] Γ P Γ Q

A Supplement to Section 3 In order to clarify what we mean by "coinductively defined function" we flesh out a more rigorous definition of the encoder function.

Definition 10 (encoder). Let C be the largest relation between session types and types such that T C t implies either:

-T = end and t = •• [unit], or -T = ?T 1 .T 2 and t =

Observe that C is a function from session types to types, for T C t 1 and T C t 2 implies t 1 = t 2 . Let • def = C and observe that • satisfies the relations in Definition 4.

Proof. We show that T ⊥ = T ⊥ by case analysis on the shape of T . We consider two representative cases, the others being similar or trivial. T = ?T 1 .T 2 We derive:

by definition of duality on channel types

by definition of duality on session types

We derive:

by definition of duality on channel types

by definition of duality on session types

Proof. We show that • • • = id S where id S is the identity on S. It suffices to show that R def = {( T , T ) | T ∈ S} coincides with id S . We prove the two inclusions R ⊆ id S and id S ⊆ R in this order.

Concerning the relation R ⊆ id S , take S R T . Then S = T . We proceed reasoning by cases on the shape of T . We consider only the case T = !T 1 .T 2 , the others being

B.3 Subject reduction for processes

The next proposition establishes a few properties of the reduction relation on type environments.

Proposition 2. If Γ -→ Γ , then the following properties hold:

Proof. Straightforward from the definition of type environment reduction.

A reduction may invalidate endpoints occurring in an expression or in a process, even if there is no redex in such terms. The following result shows that typing is preserved when invalidations occur. This is a consequence of the fact that the type ∀A.A of invalid endpoints allows them to be typed with any instance of a channel type.

Lemma 2 (invalidation). Let Γ -→ Γ where Γ is balanced. Then Γ e : t implies Γ e : t, and Γ P implies Γ P .

Proof. A simple induction on the typing derivation.

The following two lemmas allow us to reason on the typing of terms occurring in the hole of an evaluation context. In the statements of these results, by "sub-derivation of D" we mean a sub-tree of D. Note that the replacement lemma differs from the one in [START_REF] Wright | A syntactic approach to type soundness[END_REF] since the expression e is replaced not in the original evaluation context E , but in the context E where some endpoints may have been invalidated. Proof. By induction on E .

The type system is not substructural, so it enjoys a standard form of weakening.

Lemma 5 (weakening). The following properties hold: