Luca Padovani

Luca Novara

Types for Deadlock-Free Higher-Order Concurrent Programs

Keywords: D.3.3 [Programming Languages]: Language Constructs and Features-Concurrent programming structures; F.3.3 [Logics and Meanings of Programs]: Studies of Program Structures-Type structure Types and effects, linear channels, deadlock freedom

Deadlock freedom is for concurrent programs what progress is for sequential ones: it indicates the absence of stable (i.e., irreducible) states in which some pending operations cannot be completed. In the particular case of communicating processes, operations are inputs and outputs on channels and deadlocks may be caused by mutual dependencies between communications. In this work we define an effect system ensuring deadlock freedom of higher-order programs that communicate over linear channels and study its integration with polymorphic and recursive types.

Introduction

The inherent concurrency and parallelism of many software systems calls for programming abstractions to synchronize and exchange information between system components. There is a consequent demand for methods providing formally verified guarantees about the properties of programs making use of these abstractions. In this work, we are concerned with communication channels as the abstraction that enables synchronizations and interactions, with deadlock (and absence thereof) as the property being considered, and with types as the method for enforcing this property.

The history of types for communication channels spans from Milner's sorts [START_REF] Milner | The polyadic π-calculus: a tutorial[END_REF] to session types [START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF], going through several variations such as Pierce and Sangiorgi's I/O types [START_REF] Pierce | Typing and subtyping for mobile processes[END_REF] (see [START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF] for a survey). In many cases, channel types are meant to guarantee communication safety, namely that only messages of expected type can travel on a given channel. In other cases, such as in [START_REF] Pierce | Typing and subtyping for mobile processes[END_REF], the direction of messages is also specified. Richer types can guarantee even stronger properties: for example, session types enable the description of whole communication protocols made of an arbitrary, sometimes unbounded, number of message exchanges and can guarantee communication fidelity (the assurance that communications occur in the order specified by the protocol) as well as the absence of deadlocks (the assurance that the interacting parties keep communicating until the protocol is terminated).

[Copyright notice will appear here once 'preprint' option is removed.] Deadlocks cannot occur if processes use just one communication channel or, more generally, if they are connected in an acyclic network. When processes simultaneously interact through several distinct channels, however, cycles in the network topology may arise and at that point the relative order of communications becomes relevant. A paradigmatic instance of such configurations that yields a deadlock can be observed in the program below

{ send a (recv b) } | { send b (recv a) } (1)
consisting of two threads (within { • • • }) running in parallel (the operator |). The leftmost thread is trying to send on channel a the message received from channel b; the rightmost thread is trying to do the opposite. This program is in deadlock, for the communications on a and b are mutually dependent. Yet, it is commonly considered well typed, for example if a and b are channels for sending/receiving integer numbers.

In this article we study a typing discipline that flags (1) as ill typed and, more generally, that guarantees well-typed programs to be free from deadlocks. Type systems that ensure this or similar properties have already been defined for process calculi, for example in [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF]. We contribute here in three ways:

1. We work with a core functional language equipped with communication primitives à la Concurrent ML [START_REF] Reppy | CML: A Higher-Order Concurrent Language[END_REF][START_REF] Reppy | Concurrent Programming in ML[END_REF]. As far as we know, we give the first type system ensuring deadlock freedom for a higher-order language. The challenge is to conjugate the locality of the typing rules with the non-locality of the property (absence of deadlocks) they enforce.

2. We study the integration between the features of types concerning deadlock freedom with polymorphism and recursion. We show that these well-established features, which are essential for coping with common program patterns, must be carefully tuned and revisited in our setting.

3. We focus on communications on linear channels, i.e. channels that can be used for exactly one communication. In this way we are able to address non-trivial combinations of recursive programs and cyclic network topologies that are out of reach of existing type systems for deadlock freedom.

Of these contributions, the third one may sound questionable given the important restriction -channel linearity -that it relies on. In practice, linear channels account for large fraction of communication channels in many actual systems [START_REF] Igarashi | Type-based analysis of usage of values for concurrent programming languages[END_REF][START_REF] Kobayashi | Linearity and the picalculus[END_REF] and structured communications can be modeled using linear channels taking advantage of channel mobility, that is sending channels as messages: we can model both buffered and unbuffered communications and, in the former case, with both finite and unbounded size. Finally, binary sessions can be encoded using linear channels [START_REF] Dardha | Session types revisited[END_REF] and a similar encoding is possible for a large fraction of multiparty sessions as well [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF]. The benefits of linearity include an efficient implementation of channels, confluence of (concurrent) computations, and, as we have said, unprecedented accuracy of the typing discipline.

The basic idea for detecting dangerous programs like [START_REF] Amtoft | Type and behaviour reconstruction for higher-order concurrent programs[END_REF] is very simple: we assign each channel a priority, which is just a number, and we verify that sequential input/output operations are performed in an order that is consistent with such numbering: operations on channels with higher priority can only block operations on channels with lower priority (we adopt the convention that "smaller number" means "higher priority"). This mechanism flags [START_REF] Amtoft | Type and behaviour reconstruction for higher-order concurrent programs[END_REF] as being ill typed because the leftmost thread requires b to have a higher priority than a, and the rightmost thread requires a to have a higher priority than b. No priority assignment can simultaneously satisfy both constraints. The question, then, is how to perform these checks compositionally, i.e. using types.

The first obvious step is to attach the priority of channels to their types. For instance, we can assign the types ![int] m and ?[int] n respectively to a and b in the leftmost thread of (1), and ?[int] m and ![int] n to the same channels in the rightmost thread of [START_REF] Amtoft | Type and behaviour reconstruction for higher-order concurrent programs[END_REF]. Crucially, distinct occurrences of the same channel have opposite polarities (input ? and output !) and same priority. We can also reasonably think of the assignments send : ∀ı.![int] ı →int→unit and recv : ∀ı.?[int] ı → int for the communication primitives, where we allow polymorphism on channel priorities. In this case, the application (send a (recv b)) consists of two subexpressions, the partial application (send a) having type int → unit and its argument (recv b) having type int. Neither of these types hints at the I/O operations performed while evaluating the corresponding expressions, let alone at the priorities of the channels involved in these operations. In other words, they are not sufficiently informative for checking whether communication channels are used in an order that is consistent with their priority. A standard solution in these cases is to use effects [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF][START_REF] Nielson | Type and effect systems[END_REF]: each expression has, along with its type, an effect describing what happens when the expression is evaluated. In our case, the effect is the priority of the channels on which I/O operations are performed, or ⊥ in the case of pure expressions that perform no I/O. In particular, the judgment b : ?[int] n ⊢ recv b : int & n states that (recv b) is an expression of type int whose evaluation performs an I/O operation on a channel with priority n. As usual, function types are decorated with a latent effect saying what happens when the function is applied to its argument. So,

a : ![int] m ⊢ send a : int → m unit & ⊥
states that (send a) is a function that, applied to an argument of type int, produces a result of type unit and, in doing so, performs an I/O operation on a channel with priority m. By itself, (send a) is a pure expression whose evaluation performs no I/O operations, hence the effect ⊥. With this information we can detect dangerous expressions: in a call-by-value language an application e1e2 first evaluates e1, then e2, and then the body of the function resulting from e1. These evaluations are deadlock free if e1 does not perform operations on channels with priority lower than those occurring in e2 (⊥ < n, which is trivially satisfied) and the evaluation of e2 does not perform operations on channels with priority lower than those occurring in e1 (m < n). Since the same analysis on (send b (recv a)) requires the symmetric condition (n < m), the parallel composition of the two threads in (1) is ill typed due to unsatisfiable constraints between the priorities of a and b.

It turns out that the information given by latent effects in function types is insufficient for detecting some deadlocks. To see why, consider the function defined by let f = fun x (send a x; send b x) which sends its argument x on both a and b and where ; denotes the standard sequential composition. The priority n of b should be lower than the priority m of a, for b is used only after the communication on a has completed. The point here is how to choose the priority that decorates the type of f , which must have the form int → h unit. Each of the two obvious possibilities is dangerous: if we take h = m, then

{ recv a } | { f 3; recv b } (2)
is well typed because the latent effect m of (f 3) is numerically smaller than the priority of b in (recv b), which agrees with the fact that (f 3) is evaluated before (recv b); if we take h = n, then

{ recv a; f 3 } | { recv b } (3)
is well typed for similar reasons. This is unfortunate because (3) is, and (2) reduces to, a deadlock. To flag both ( 2) and (3) as ill typed, we must refine the type of f to int→ m,n unit where we keep track of the highest priority of the channels that occur free in the body of f (that is m) as well as of the lowest priority of the channels on which an input/output operation is performed by f when f is applied to an argument (that is n). Intuitively, the first decoration is the "priority" of the whole function, which gives information on the free channels that occur within the function, while the second decoration is the latent effect of the function, as before. So ( 2) is ill typed because the latent effect of (f 3) is the same as the priority of b in (recv b) and ( 3) is ill typed because the effect of (recv a) is the same as the priority of f in (f 3).

Outline.

In what follows we turn the technique sketched in here into a full-fledged type and effect system. We proceed defining the language (Section 2), the type system (Section 3) and studying the properties of well-typed programs (Section 3.4). A more comprehensive comparison with related work is postponed to Section 4. Section 5 discusses some limitations of the approach and hints at possible solutions. Appendix A, which is not formally part of the submission, contains proofs and additional technical material.

Language Syntax & Semantics

We use a countable set of variables x, y, . . . , a countable set of channels a, b, . . . , and a set of constants c. Names u, . . . are either variables or channels. We consider a language of expressions e, . . . and processes P , Q, . . . as defined below:

expression e ::= c u (e, e) ee fun x e rec x e let (x, y) = e in e let x = e in e process P ::= {e} P | P new a in P Expressions comprise constants c, names u, abstractions fun x e, applications e1e2, pairs (e1, e2), and recursion rec x e. We also have two let-binding constructs: a classical one let x = e1 in e2 and another let (x, y) = e1 in e2 that is used for decomposing pairs (the presence of this construct in place of the more conventional projections is due to the linear nature of some types). Constants include the unitary value (), the integer numbers m, n, . . . , as well as the primitives fork, open, send, recv whose semantics will be explained shortly. Processes are either sequential threads {e} made of a single expression, or the parallel composition P | Q of processes, or restrictions new a in P denoting a communication channel with scope P . The notions of free and bound names are as expected, given that the binders are abstractions, lets, and news. We identify terms modulo renaming of bound names and we write fn(e) (respectively, fn(P )) for the set of names occurring free in e (respectively, in P ). As usual we assume that application is left associative, hence e1e2e3 stands for (e1e2)e3. We also sugar the syntax with some evocative notation: we write e1!e2 for send e1 e2; we write _ for unused/fresh variables; we write e1; e2 for let _ = e1 in e2; we write let f x1 • • • xn = e1 in e2 as an abbreviation for Reduction of expressions

(fun x e)v -→ e{v/x} rec x e -→ e{rec x e/x} let (x, y) = (v, w) in e -→ e{v, w/x, y} let x = v in e -→ e{v/x} E [e] -→ E [e ′ ] if e -→ e ′ Structural congruence P | {()} ≡ P P | Q ≡ Q | P P | (Q | R) ≡ (P | Q) | R new a in P | Q ≡ new a in (P | Q) if a ∈ fn(Q) Reduction of processes {E [a!v]} | {E ′ [recv a]} a --→ {E [()]} | {E ′ [v]} {E [fork v]} τ --→ {E [()]} | {v()} {E [open()]} τ --→ new a in {E [a]} if a ∈ fn(E ) {e} τ --→ {e ′ } if e -→ e ′ P | Q ℓ --→ P ′ | Q if P ℓ --→ P ′ new a in P ℓ --→ new a in Q if P ℓ --→ Q where ℓ = a new a in P τ --→ Q if P a --→ Q P ℓ --→ Q if P ≡ ℓ --→≡ Q Table 1.
Reduction semantics of expressions and processes.

let f = fun x1 • • • fun xn e1 in e2 and let rec f = e1 in e2
as an abbreviation for let f = rec f e1 in e2.

In the examples we often omit the in part of a let, in which cases it is meant to be the rest of the program. The reduction semantics of the language is given by two relations, one for expressions, another for processes (Table 1). We adopt a call-by-value reduction strategy, for which we need to define the reduction contexts E , . . . and the set of values v, w, . . . :

context E ::= [ ] (E , e) (v, E ) E e vE let (x, y) = E in e let x = E in e value v ::= c a (v, v) fun x e send a
Reductions are either the beta rule that applies a function to its argument, the unfolding of a recursion, the splitting of a pair into its components, or the binding of a value to a variable. As usual e{v/x} denotes the expression obtained by replacing the free occurrences of x in e with v and reduction is closed by reduction contexts. Structural congruence rearranges equivalent processes and is directly linked to that of the π-calculus [START_REF] Milner | The polyadic π-calculus: a tutorial[END_REF][START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF]. The reduction relation of processes has labels ℓ, . . . that are either a channel name a, denoting that a message has been exchanged on a, or the special symbol τ denoting any other reduction. There are four base reductions for processes: a synchronization can happen between two threads where one is willing to send a message v on a channel a and the other is waiting for a message from the same channel; a thread that contains a subexpression fork v spawns a new thread that evaluates v(); a thread that contains a subexpression open() causes the creation of a new channel; the reduction of an expression causes a corresponding τ -labeled reduction of the thread in which it occurs. Reduction for processes is then closed by structural congruence, parallel compositions, and restrictions. In the latter case, the restriction of a disappears as soon as a communication on a oc-curs, witnessing the fact that channels are linear in our model and can be used for one communication only.

We conclude this section with a variety of examples whose purpose is threefold: first of all, we show how to model a number of significant communication patterns using linear channels; second, we argue about desirable properties of programs, in particular deadlock and absence thereof; finally, we put together a reasonably complete test bench for the type system that we develop in Section 3.

In the examples we use a slightly more concrete language equipped with conditionals and a few additional operators. These can be easily accommodated without affecting the results in Section 3.

Example 2.1. Linear channels can be used for notifying the completion of independent subcomputations. For example, the fibo function below computes the n-th number in the Fibonacci sequence by spawning each recursive call in a distinct thread: Before the recursive calls, two new channels a and b are created. As soon as each recursive call terminates, the corresponding result is sent on a and b. These values are collected and added in (recv a) + (recv b). Each channel syntactically occurs twice, but is used for exactly one communication. Note that the function is non-deterministic, in the sense that the spawned threads that evaluate recursive calls execute independently at possibly different speeds; also, expressions are intermingled with (blocking) input/output operations. It is therefore relevant to ask whether this version of fibo is equivalent to the sequential one, in the sense that it is able to reduce until a result is computed without blocking indefinitely on an input/output operation, and whether it always produces the same result, when applied to the same argument. that send a message y on channel x along with a fresh continuation c. The continuation is returned so that further messages can be sent in the same conversation. For example, writing e1!!e2 in place of (ssend e1 e2) and taking ! and !! left-associative, the thread

let rec fibo n = if n ≤ 1 then n else let (
{ a!!1!!2!3 }
sends three subsequent messages 1, 2, and 3 that the target thread can receive with a sequence of recv and pair splittings, thus:

{ let (v1, a ′ ) = recv a in let (v2, a ′′ ) = recv a ′ in let v3 = recv a ′′ in ... }
Note the use of fork in the definition of asend meaning that asend, unlike ssend, realizes a non-blocking output operation: the complete evaluation of (asend a v) does not guarantee that v has been received, but only that v has been sent on a. In other words, asend allows us to model asynchronous communication on unbounded FIFO buffers.

Example 2.3. Many parallel algorithms (Jacobi and Gauss-Seidel, leader election, vertex coloring, just to mention a few) use batteries of threads to elaborate some compound data structure. Each "node" of the structure is assigned a distinct thread which iteratively communicates with its neighbors. To maximize parallelism, communication is full duplex, that is threads simultaneously send messages to each other. We can model full-duplex communication using pairs of linear channels, where one channel is used for sending messages to, and the other channel is used for receiving messages from, the neighbor thread. The node function below models one such thread: The thread is parametric in a state (e.g., the current value of the node assigned to the thread), a function f that computes a new state from the current one and that of the neighbor, and two channels x and y for respectively sending the thread's own state (line 2) and receiving that of the neighbor (line 3). At the end of each iteration a new state (f state state ′ ) is computed (line 4). Lines 5-7 instantiate two nodes that are initialized with unspecified initial states statei and transformation functions fi.

An interesting aspect of the system above is that the two threads communicate in a cyclic network topology (the channel that one thread uses for sending is the same channel that the other thread uses for receiving, and vice versa) and that they both iteratively interleave input (i.e., potentially blocking) actions on different channels. It may not be obvious that a system like this runs without deadlocks. For instance, while this is the case for the particular system above, using ssend instead of asend in line 2 or swapping lines 2 and 3 produces another system that is deadlock.

Example 2.4. In this example we model a stream processing network that computes the series of Fibonacci numbers. The network is taken from [START_REF] Reppy | Concurrent Programming in ML[END_REF] and relies on the small library of stream combinators below (we keep using !! to denote ssend of Example 2.2):

let rec link x y = let (v, x ′ ) = recv x in link x ′ y!!v let delay x y = let (_, x ′ ) = recv x in link x ′ y let rec add x y z = let (v, x ′ ) = recv x in let (w, y ′ ) = recv y in add x ′ y ′ z!!(v + w) let rec copy x y z = let (v, x ′ ) = recv x in copy x ′ y!!v z!!v
Each combinator operates on two or three streams that we model using linear channels as we have already done in Examples 2.2 and 2.3: link x y forwards all messages received from x to y; delay x y does the same except that it discards the first message received from x; add x y z receives integers from x and y and sends their sum to z; finally, copy x y z forwards any message from x to both y and z.

We use these combinators for building the network in Figure 1: each integer sent on c1 is duplicated to c2 and out; pairs of subsequent integers sent on c2 are added together thanks to the copy, delay, and add combinators and the result of the addition is injected back on c1. The integers retrieved from out are the Fibonacci series if the first two messages sent on c1 are both 1. In code: The example is interesting in many ways: in particular, it assembles a network compositionally in terms of simpler building blocks, the realized network contains cyclic dependencies (the messages sent on c1 are necessary for generating further messages on the continuations of c1) and interleaves I/O actions on different channels. Again, the fact that the network works as expected is not obvious. Already in [START_REF] Reppy | Concurrent Programming in ML[END_REF] it is observed that the absence of deadlocks in this program, hence the actual production of an infinite sequence of messages on out, depends on the careful implementation and composition of the combinators. In particular: add must first read the non-delayed message, for otherwise the top copy combinator would block trying to deliver a message on c3 before sending the one on c4; the two outputs on line 5 must be asynchronous, for otherwise the program would block there before spawning the combinator that receives these messages (line 9); forgetting either of the two outputs on line 5 would also cause a deadlock, because delay discards one of them.

Type System

We introduce the features of the type system gradually, in three steps: we start with a monomorphic system (Section 3.1) to get some familiarity with priorities and types, then we add polymorphism (Section 3.2), and finally recursive types (Section 3.3). We conclude with the properties of the type system (Section 3.4). The reader interested in presentation of the full type system in one shot may refer to Appendix A.

Core Types

Let P def = Z ∪ {⊥, ⊤} be the set of priorities ordered in the obvious way (⊥ < n < ⊤ for every n ∈ Z); we use ρ, σ, . . . to range over priorities and we write ρ ∧ σ (respectively, ρ ∨ σ) for the minimum (respectively, the maximum) of ρ and σ. We let p, . . . range over the set {?, !, #} of polarities. Types t, s, . . . are defined by

type t ::= B t × t p[t] n t → ρ,ρ t
where basic types B, . . . include unit and int and t × s is the usual product type. The type p[t] n denotes a channel with priority n that can be used to exchange messages with type t according to p: ? means that the channel can be used once for an input, ! means that it can be used once for an output, and # means that it can be used once for an input and once for an output. The arrow t→ ρ,σ s is the type of a function that accepts an argument of type t and returns a value of type s. The function has priority ρ (its closure contains channels with priority ρ or lower) and, when applied, performs I/O operations on channels with priority σ or higher. We write → as an abbreviation for → ⊤,⊥ , that is a pure function not containing channels and not performing any I/O. It is useful to extend the notion of priority to arbitrary types: basic types have the lowest priority ⊤ because their (lack of) use does not affect deadlock freedom in any way, while the priority of a pair is the highest (numerical minimum) of the priorities of its components. Formally, the priority of t, written |t|, is defined as:

|t| def =      ⊤ if t = B |t1| ∧ |t2| if t = t1 × t2 ρ if t = p[s] ρ or t = t1 → ρ,σ t2
We use priorities to distinguish between linear and unlimited types. Linear types denote values (such as channels) that must be used to guarantee deadlock freedom; unlimited types denote values that have no effect on deadlock freedom and may not be used.

Definition 3.1. We say that t is linear if |t| ∈ Z; we say that t is unlimited, written un(t), if |t| = ⊤.
Below are the types of each constant that we consider. We say "types" instead of "type" because, until the introduction of polymorphism in Section 3.2, the same constant has in general several types, and the right one is "guessed" depending on the context. We write TypeOf(c) for one of the types of c.

() : unit n : int open : unit → #[t] n n < |t| recv : ?[t] n → ⊤,n t n < |t| send : ![t] n → t → n,n unit n < |t| fork : (unit → ρ,σ unit) → unit
The primitive open creates a new channel with the full set # of polarities and arbitrary (but finite) priority n.

The primitive recv takes a channel of type ?[t] n , blocks until a message is received, and returns the message. The primitive itself contains no free channels in its closure (hence the priority ⊤) because the only channel it manipulates is its argument. The latent effect is the priority of the channel, as expected.

The primitive send takes a channel of type ![t] n , a message of type t, and sends the message on the channel. Note that the partial application send a is a function whose priority is the same as that of a, and that the latent effect is again the priority of a. Note also that in open, recv, and send the priority of the message must be lower than the priority of the channel. Since priorities are used to enforce an order on the use of values, this condition makes sense given that a message cannot be used until after it has been received, namely after the channel on which it travels has been used.

Finally, fork accepts a thunk with arbitrary priority ρ and latent effect σ and spawns the thunk into an independent thread (see Table 1). Note that fork is a pure function, with lowest priority and no latent effect, regardless of the priority and latent effect of the thunk. This phenomenon is an instance of effect masking, whereby the effect of evaluating an expression becomes unobservable: in our case, fork discharges effects because deadlocks are caused by sequential (rather than parallel) execution of input/output operations.

We now turn to the core set of typing rules. A type environment Γ , . . . is a finite map from names to types defined by Γ ::= ∅ Γ , u : t and considered modulo commutativity of bindings. We write dom(Γ ) for the domain of Γ , namely the set of names for which there is a binding in Γ , and Γ (u) for the type associated with u in Γ ; we write Γ1, Γ2 for the union of Γ1 and Γ2 when dom(Γ1) ∩ dom(Γ2) = ∅. As usual in substructural type systems, we need a more flexible way of combining type environments. In particular, we want to be sure that every linear name is used linearly and we must be able to distribute the polarities of a channel to different parts of the program. To this aim, and following [START_REF] Kobayashi | Linearity and the picalculus[END_REF][START_REF] Sangiorgi | The Pi-Calculus -a theory of mobile processes[END_REF], we define a partial combination operator + between types:

t + t def = t if un(t) p[t] n + q[t] n def = #[t] n if {p, q} = {?, !} (4)
which we extend to type environments, thus:

Γ + Γ ′ def = Γ , Γ ′ if dom(Γ ) ∩ dom(Γ ′ ) = ∅ (Γ , u : t) + (Γ ′ , u : s) def = (Γ + Γ ′ ), u : t + s
For example, we have (x : int, a :

![int] n ) + (a : ?[int] n ) = x : int, a : #[int] n ,
so we might have some part of the program that (possibly) uses a variable x of type int along with channel a for sending an integer and another part of the program that uses the same channel a but this time for receiving an integer. The first part of the program would be typed in the environment x : int, a : ![int] n and the second one in the environment a : ?[int] n . Overall, the two parts would be typed in the environment x : int, a : #[int] n indicating that a is used for both sending and receiving an integer. It is easy to show that + is commutative and associative.

We We are now ready to discuss the core typing rules, presented in Table 2 and deriving judgments of the form Γ ⊢ e : t & ρ for expressions, denoting that e is well typed in Γ , it has type t and effect ρ and judgments of the form Γ ⊢ P for processes, simply denoting that P is well typed in Γ .

Rules for expressions are quite conventional for a substructural type system: axioms [

T-NAME] and [T-CONST] verify that the unused part of the type environment is unlimited and rules such as [T-APP], [T-PAIR], and [T-SPLIT

] that contain two subexpressions split the type environment using the + operator (we omit the simple let binding operator which, in the monomorphic type system, is just a simpler variant of splitting).

Rule [T-REC] for recursions requires the environment to be unlimited, since a recursive term will unfold an arbitrary number of times and therefore cannot contain channels (but it general it will be a function that may accept channels). The condition prevents the typing of an expression such as rec x .a!x, which has type unit and would otherwise be well typed in the environment a : ![unit] n .

Let us now focus on priorities and effects. Names and constants have no effect (⊥); they denote fully evaluated, pure expressions that do not reduce any further. In rule [T-FUN], the effect ρ caused by evaluating the body of the function becomes the latent effect in the arrow type of the function, and the function itself has no effect (⊥). In addition, the arrow is annotated with the priority of the environment Γ in which the function is typed. Intuitively, the names in Γ are stored in the closure of the function; if any of these names is a channel, then we must be sure that the function is eventually used (i.e., applied) in order to guarantee deadlock freedom. In fact, the priority |Γ | gives a slightly more precise information, since it keeps track of the highest priority of any channel that occurs in the closure of the function. We have seen in Section 1 why this information is useful. Below are a few examples:

• the identity function fun x x has type int → ⊤,⊥ int in any unlimited environment; in particular, it contains no channels in its closure and it performs no I/O, so it is pure;

• the function fun x (x, a) has type int→ n,⊥ (int×![int] n ) in the environment a : ![int] n ; it contains channel a with priority n in its closure (whence the priority n in the arrow),

Typing of expressions

[T-NAME] un(Γ ) Γ , u : t ⊢ u : t & ⊥ [T-CONST] un(Γ ) Γ ⊢ c : TypeOf(c) & ⊥ [T-REC] un(Γ ) Γ , x : t ⊢ e : t & ⊥ Γ ⊢ rec x e : t & ⊥ [T-FUN] Γ , x : t ⊢ e : s & ρ Γ ⊢ fun x e : t → |Γ |,ρ s & ⊥ [T-APP] Γ1 ⊢ e1 : t → ρ,σ s & τ1 Γ2 ⊢ e2 : t & τ2 τ1 < |Γ2| τ2 < ρ Γ1 + Γ2 ⊢ e1e2 : s & σ ∨ τ1 ∨ τ2 [T-PAIR] Γi ⊢ ei : ti & ρi (i=1,2) ρ1 < |Γ2| ρ2 < |t1| Γ1 + Γ2 ⊢ (e1, e2) : t1 × t2 & ρ1 ∨ ρ2 [T-SPLIT] Γ1 ⊢ e1 : t1 × t2 & ρ Γ2, x : t1, y : t2 ⊢ e2 : s & σ ρ < |Γ2| Γ1 + Γ2 ⊢ let (x, y) = e1 in e2 : s & ρ ∨ σ Typing of processes [T-THREAD] Γ ⊢ e : unit & ρ Γ ⊢ {e} [T-PAR] Γ1 ⊢ P Γ2 ⊢ Q Γ1 + Γ2 ⊢ P | Q [T-NEW] Γ , a : #[t] n ⊢ P Γ ⊢ new a in P Table 2.
Core typing rules for expressions and processes. but it does not use a for input/output (whence the latent effect ⊥); it is nonetheless well typed because a, which is a linear value, is returned as result;

• the function fun x x!3 has type ![int] n → ⊤,n unit; it has no channels in its closure (priority ⊤) but it performs an output on the channel it receives as argument (priority n);

• the function fun x (recv a + x) has type int → n,n int in the environment a : ?[int] n ; note that neither the domain nor the codomain of the function mention any channel, so the fact that the function has a channel in its closure (and that it performs some I/O) is only apparent from the priorities on the arrow;

• the function fun x x!(recv a) has type ![int] n+1 → n,n+1 unit in the environment a : ![int] n ; it contains channel a with priority n in its closure and performs input/output operations on channels with priority n + 1 (or higher) when applied.

Rule [T-APP] deals with applications e1e2. In the premises, τi is the effect caused by the evaluation of ei. As expected, e1 must result in a function of type t → ρ,σ s and e2 in a value of type t. The evaluation of e1 and e2 may however involve potentially blocking I/O operations on channels, and the two remaining premises make sure that no deadlock can arise. To better understand them, keep in mind that we work with a call-by-value language and that applications, such as e1e2, are evaluated sequentially from left to right. Now, the premise τ1 < |Γ2| makes sure that any I/O operation performed during the evaluation of e1 involves only channels with higher priority than those occurring free in e2 (the free channels of e2 must necessarily occur in Γ2). This is enough to guarantee that the functional part of the application can be fully evaluated without blocking on operations concerning channels that occur later in the program. In principle, this premise should be paired with the symmetric one τ2 < |Γ1| making sure that any I/O operation performed during the evaluation of the argument does not involve channels that occur in the functional part. However, while the argument is being evaluated, we know that the functional part has already become a value (see the definition of reduction contexts in Section 2). Therefore, the only really critical condition to check is that no channels involved in I/O operations during the evaluation of e2 occur in the value of e1. This is expressed by the condition τ2 < ρ, where ρ is the priority of the functional part. Note that when e1 is an abstraction, by rule [T-FUN] ρ coincides with |Γ1|, but in general ρ may be lower than Γ1, so the premise τ2 < ρ gives better accuracy. The effect of the whole application e1e2 is, as expected, the combination of the effects of evaluating e1, e2, and the latent effect of the function being applied. In our case the "combination" is the lowest priority of any channel involved in the application. Below are some examples:

• the application (fun x x) 3 is well typed, because both fun x x and 3 are pure expressions whose effect is ⊥, hence the two rightmost premises of [T-APP] are trivially satisfied;

• the application (fun x x) a is also well typed in the environment a : p[t] n , because the functional part has no effect (⊥);

• the application (fun x x) (recv a) is well typed in the environment a : ?[int] n : the effect of (recv a) is n (the priority of a) which is higher than the priority ⊤ of the function;

• the application (fun x (x, a)) (recv a) is ill typed because the effect of evaluating the argument is the same as the priority of the function. Indeed, for the evaluation of recv a to complete it is necessary that a with output polarity is owned by a thread running in parallel with respect to the application;

• the application (recv a) (recv b) is well typed in the environment a : ?[int → int] 0 , b : ?[int] 1 . Note in particular that the effect of the argument is 1, which is not higher than the priority of the environment a : ?[int → int] 0 used for typing the function. However, 1 is higher than ⊤, which is the priority of the result of the evaluation of the functional part of the application. Therefore, this application would be rejected had we used the premise

τ2 < |Γ1| in [T-APP].

Rule [T-PAIR] has many similarities with [T-APP]

, so we omit a detailed explanation (we see it at work in Example 3.2 below). Just note the premises making sure that the sequential evaluation of the two components of the pair do not block on channels involved in both of them, and the combination of the effects in the conclusion of the rule. Rule [T-SPLIT] is also a standard pair-splitting rule. There is only one premise ρ < |Γ2| checking that no channels used for evaluating the pair also occur in the body e2 of the let.

The typing rules for processes are unremarkable: [T-PAR] splits contexts for typing the processes in parallel, [T-NEW] introduces a new channel in the environment, and [T-THREAD] types threads. Note that the effect of threads is ignored: effects are meant to capture circular dependencies between communications and the conditions concerning priorities in the typing rules detect dependencies that arise within sequential parts of the program (i.e., within expressions); circular dependencies that arise between parallel threads are indirectly detected by the fact that each occurrence of a channel is typed with the same priority (see the discussion of (1) in Section 1).

Example 3.2. In this example we see the combination of effect masking and the asymmetric conditions on priorities in rule [T-PAIR].

In particular, we can derive

a : ![int] 0 ⊢ fork • • • : unit & ⊥ a : ?[int] 0 ⊢ recv a : int & 0 a : #[int] 0 ⊢ (fork fun _ a!3, recv a) : unit × int & 0
where the same channel a occurs and is used in both components of a pair. The effect of the first component is masked by fork and that of the second component satisfies 0 < |unit| = ⊤. provided that m < n, which is consistent with the fact that the receive operation on a blocks the receive operation on b. In conclusion, fibo is well typed and has type int → ⊤,n int.

Polymorphic Types

In this section we show how to enrich the type system with support for polymorphism. Ideally we would just introduce type variables indicating unknown types so that, for example, the identity function fun x x can be given the familiar polymorphic type ∀α.α→ α. The identity function uses its argument linearly, so the type variable α can be instantiated with any type, be it linear or unlimited. In general, however, one must be more careful. Consider, for example, the first projection function

f def = fun x fun _ x
which discards its second argument. Normally a function like this is assigned the type ∀αβ.α → β → α. In our context, this type is too imprecise, for two reasons. First of all, we would like to specify that β can only be instantiated with unlimited types, for the second argument of the function is discarded and so it cannot be, for instance, a channel. Second, we must be able to say that the priority of the second arrow type is the same as the priority of the first argument. Indeed, the partial application (f a) is a function that contains a channel a. Not only this function is linear, but its priority coincides with that of a. In summary, we must be able to reason on, and impose constraints to, the priority of type variables. To this aim, we introduce a category of priority variables ranging over unknown priorities, and we allow quantification over priority, as well as type, variables, as we have already suggested in Section 1. In both cases quantification is bounded: type variables range over types with a specific priority, and priority variables range over priority intervals. Below is the extension of types to polymorphism:

type t ::= • • • α type scheme T ::= t ∀α ρ .T ∀ı ϕ .T priority ρ ::= ⊥ n ⊤ ı ρ ∧ ρ ρ ∨ ρ interval ϕ ::= [ρ, ρ] (ρ, ρ] [ρ, ρ] (ρ, ρ)
Types are enriched with type variables α, β, . . . ; type schemes are possibly quantified types: quantification over type variables specifies the priority of types that can instantiate the type variable, while quantification over priority variables ı, , . . . specifies an interval ϕ of priorities over which the priority variable can be instantiated. We use established notation for denoting intervals ϕ, . . . of P; for example, the closed interval [⊥, ⊤] denotes the whole P and the open interval (⊥, ⊤) denotes the set of finite priorities Z. Having introduced priority variables, we generalize priorities to priority expressions and we keep using ρ, . . . for ranging over these; the operators ∧ and ∨ now become part of the syntax.

Using polymorphic types we can assign proper type schemes to the four primitives of our language: open : ∀ı.∀α ı .∀ (⊥,ı) .unit → #[α]  recv : ∀ı.∀α ı .∀ (⊥,ı) .?[α]  → ⊤, α send : ∀ı.∀α ı .∀ (⊥,ı) .![α]  → α → , unit fork : ∀ı.∀ [⊥,⊤] .(unit → ı, unit) → unit where we omit (⊥, ⊤] intervals. Note that we can specify the constraint requiring messages to have lower priority with respect to the channel on which they travel.

Since now types may contain type variables and priority expressions may contain priority variables, we must parametrize operations on types and relations between priority expressions by a priority environment that keeps track of the priority of type variables and of the intervals on which priority variables range over. Priority environments Θ, . . . are defined by: Θ ::= ∅ Θ, ı ∈ ϕ Θ, α :: ρ We write dom(Θ) for the domain of Θ, namely the set of type and priority variables for which there is an association in Θ, and Θ(α) for the priority of α as determined by Θ. We also write Θ1, Θ2 for the union of Θ1 and Θ2 when they have disjoint domains. To make sure that the associations in priority environments are not ambiguous, we do not equate Θ1, Θ2 and Θ2, Θ1 and we require two basic well-formedness conditions: Θ, ı ∈ ϕ is well formed if all the priority variables in ϕ are in dom(Θ), and Θ, α :: ρ is well formed if all the priority variables in ρ are in dom(Θ). In the following we implicitly assume to work with wellformed priority environments. We write |t| Θ for the expression that denotes the priority of t in the priority environment Θ. Formally:

|t| Θ def =          ⊤ if t = B Θ(α) if t = α ∈ dom(Θ) ρ if t = p[s] ρ or t = t1 → ρ,σ t2 |t1| Θ ∧ |t2| Θ if t = t1 × t2
When checking a relation between priority expressions ρ R σ or a membership ρ ∈ ϕ, knowing the range of the priority variables occurring in ρ and σ is relevant. For example, the relation ı <  does not hold for arbitrary values of ı and  but it holds, say, under the assumptions given by the priority environment ı ∈ (⊥, ⊤),  ∈ (ı, ⊤]. From now on we will write ρ R Θ σ if the relation R holds under the assumptions Θ; similarly, we will write ρ ∈ Θ ϕ. We do not provide any detail regarding the inference engine that derives judgments ρ R Θ σ or ρ ∈ Θ ϕ, we only assume that the inference engine is closed by substitutions. That is, if ρ R Θ,ı∈ϕ,Θ ′ σ and τ ∈ Θ ϕ, then ρ{τ /ı} R Θ,Θ ′ {τ /ı} σ{τ /ı}.

Following [START_REF] Wright | A syntactic approach to type soundness[END_REF], we define two relations for respectively instantiating a type scheme to a type and generalizing a type to a type scheme. Since our form of quantification is bounded, both relations must be parametric over a priority environment which makes sure that instances of type/priority variables are appropriate (in the case of instantiation) and which keeps track of the type/priority variables that have been generalized (in the case of generalization). We have:

t ≻ Θ t |s| = Θ ρ T {s/α} ≻ Θ t ∀α ρ .T ≻ Θ t ρ ∈ Θ ϕ T {ρ/ı} ≻ Θ t ∀ı ϕ .T ≻ Θ t for instantiation and t ≺ ∅ t |t| = ∅ ⊤ t ≺ Θ T t ≺ α::ρ,Θ ∀α ρ .T |t| = ∅ ⊤ t ≺ Θ T t ≺ ı∈ϕ,Θ ∀ı ϕ .T
for generalization. Note that we allow the generalization of a type t only if it can be established that its priority is ⊤ in the empty priority environment. The motivation for this constraint is to prevent the priority of a quantified type to depend on the type/priority variable being quantified. For example, we forbid the generalization int → ı,⊥ int ≺ ı∈(⊥,⊤] ∀ı.(int → ı,⊥ int) because the priority of int → ı,⊥ int depends on ı. We argue that the impact of such restriction is null: types with a finite (non-⊤) priority are linear and denote values that can be used only once, so there is no much point in making them polymorphic. On the contrary, thanks to this restriction we can easily generalize the computation of the priority of polymorphic types, which is trivially ⊤. Formally:

|∀α ρ .T | Θ = |∀ı ϕ .T | Θ def = ⊤
Now that we have introduced polymorphic and extended the notion of priority to them, the last ingredient we need is a revised combination operator +. In practice the definition is the same as that in equation 4, except that the operator is parametric over a priority environment Θ which is used for establishing whether a type (scheme) T is unlimited or not. More precisely, we revise the first equation in (4) thus:

T + Θ T def = T if |T | Θ = Θ ⊤
The extension of + to type environments is just as before, recalling that type environments now associate type schemes to names. In particular:

(Γ , u : T ) + Θ (Γ ′ , u : S) def = (Γ + Θ Γ ′ ), u : T + Θ S
We are now ready to discuss the typing rules of the polymorphic type system. Most of them have exactly the same structure as in the monomorphic type system, except that now judgments for expressions have the form Γ ⊢ Θ e : t & ρ and the relations concerning priorities are parametric in the Θ environment. The rules affected by polymorphism are shown in Table 3 (and the complete revised type system is in Appendix A). A judgment Γ ⊢ Θ e : t & ρ is well formed if all the free type/priority variables occurring in Γ are in dom(Θ). From now on we implicitly assume well formedness of all judgments. Rules [T-NAME POLY] and [T-CONST POLY] are standard: they instantiate the (polymorphic) types of constants and of names in the type environment. Rule [T-LET POLY] implements letpolymorphism: the type t of the expression being bound to the variable x can be generalized to the type scheme T provided that all quantified type/priority variables (in Θ ′ ) do not occur in the type environment Γ1. This is guaranteed by the fact that Θ ′ is disjoint from Θ and that Γ1 must necessarily contain only type/priority variables in Θ for otherwise the judgment in the conclusion would be ill formed. We also need to revise rule [T-REC] to [T-REC POLY] to support polymorphic recursion. The idea is to generalize the type of a recursion variable x and allow each occurrence of a rec x e to be instantiated to a type s that is appropriate for the context where the recursion variable occurs. Polymorphic recursion is essential for typing most of the examples that follow. we can derive (•) : ∀αβγ.∀ı.∀ [⊥,⊤] .∀κ.∀h [⊥,⊤] .

(β → ı, γ) → (α → κ,h β) → ı,⊥ (α → ı∧κ,∨h γ)
(type variables with no priority bounds are assumed to range over any type). We can now define a polymorphic forwarder as follows let forward x = (send x) • recv for which we have

forward : ∀ı.∀ (ı,⊤) .∀κ (,⊤) .∀α κ .?[α] ı → ![α]  → ı, unit
Note that the priority of the channel on which the message is forwarded must be lower than the priority of the channel from which the message is received, and that the message itself must have lower priority than both channels.

Example 3.5. Considering again the functions ssend and asend from Example 2.2, we derive ssend : ∀ı.∀ (ı,⊤) .∀κ (ı,⊤] .∀h

(,⊤] .∀α κ .∀β h . ![α × ?[β]  ] ı → α → ı,ı ![β]  asend : ∀ı.∀ (ı,⊤) .∀κ (ı,⊤] .∀h (,⊤] .∀α κ .∀β h . ![α × ?[β]  ] ı → α → ı,⊥ ![β] 
The only difference between the two types is that asend has no latent effect, since the output is performed in an independent thread that is spawned from within asend. Note also that there is nothing in the definition of these functions imposing that the returned continuation must have output capability. For instance, ssend has also the type

![α × ![β]  ] ı → α → ı,ı ?[β]  .
As a consequence, some expressions lack a principal typing.

Recursive Types

Let us complete the type system with support for recursive types. This is achieved by adding a conventional µα type constructor, but to make recursive types useful in our setting it is necessary to extend types in a slightly more sophisticated way. To see why, consider for example the link combinator that we have defined in Example 2.4 and that forwards all messages received from a stream x to another stream y. Since both x and y are infinite streams, it is reasonable to expect that their respective types will be recursive. Tentatively, we may think of the assignments

x : t and y : ![int × s] 1
where t and s are recursive types satisfying the equations:

t = ?[int × t] 0 s = ?[int × s] 2 (5)
(for simplicity, while discussing this example we fix both the type int of messages and the priorities in types).

Note that each message sent on the output stream y is a pair made of an integer and a continuation channel with input capability, since that continuation will be used for receiving the next message sent on the stream. Note also that the priority of x must be strictly higher than that of y, since in link there is an input operation on x that blocks an output operation on y. The problem is that, by looking at the type schemes associated with send and recv, we see that any message sent on a channel must have a type with a priority that is strictly lower than that for the message, and this is not true

⊤ ≤ Θ |Γ | T ≻ Θ t Γ , u : T ⊢ Θ u : t & ⊥ [T-LET POLY] Γ1 ⊢ Θ,Θ ′ e1 : t & ⊥ t ≺ Θ ′ T Γ2, x : T ⊢ Θ e2 : s & ρ Γ1 + Θ Γ2 ⊢ Θ let x = e1 in e2 : s & ρ [T-CONST POLY] ⊤ ≤ Θ |Γ | TypeOf(c) ≻ Θ t Γ ⊢ Θ c : t & ⊥ [T-REC POLY] ⊤ ≤ Θ |Γ | Γ , x : T ⊢ Θ,Θ ′ e : t & ⊥ T ≻ Θ s Γ ⊢ Θ rec x e : s & ⊥ Table 3.
Rules for polymorphism and polymorphic recursion. for t and s. For example, a message received from a channel with type t has priority |int × t| = |t| = 0, which is the same priority of x. Overall, in order to satisfy the constraint on the priority of message types in the first and every subsequent iteration of link, we must use the assignments

x : t (0)
and

y : ![int × t (2) ] 1
where t (i) satisfies the equation

t (i) = ?[int × t (i+1) ] i (6)
The problem is that t (i) consists of infinitely many nested channel types with numerically increasing priorities. In other words, t (i) is not a regular type, so it cannot be finitely represented by means of the familiar µ notation [START_REF] Courcelle | Fundamental properties of infinite trees[END_REF].

To recover a finite representation of the types t (i) we resort to a new type constructor $ ρ t which allows us to express the priorities in t as being relative to a finite displacement ρ. The value of a priority σ occurring in t is actually ρ + σ, where + is the extension of integer addition to priorities, so that ⊥ + n = ⊥ and ⊤ + n = ⊤ for every n ∈ Z. In summary, we extend the syntax of types and priorities in this way:

type t ::= • • • µα.t $ ρ t priority ρ ::= • • • ρ + ρ
where µα is the standard binder for recursion type variables. Then, in order to make recursions and displacements transparent constructors, we identify types according to the following set of equations:

µα.t = t{µα.t/α} $ ρ B = B $ ρ (t × s) = ($ ρ t) × ($ ρ s) $ ρ (t → σ,τ s) = ($ ρ t) → ρ+σ,ρ+τ ($ ρ s) $ ρ p[t] σ = p[$ ρ t] ρ+σ
The first equation is the standard identification of types modulo folding/unfolding of recursions. The subsequent equations propagate the $ ρ constructor across compound types and add ρ to every explicit priority annotation. For example, we have 3 . Going back to the equation ( 6), we can now define

$ 1 (int × p[int] 2 ) = ($ 1 int) × ($ 1 p[int] 2 ) = int × p[$ 1 int] 3 = int × p[int]
t def = µα.?[int × $ 1 α] 0
and it is easy to see that

t = ?[int × $ 1 t] 0 = ?[int × $ 1 ?[int × $ 1 t] 0 ] 0 = ?[int × ?[int × $ 2 t] 1 ] 0 = • • •
namely that $ i t is a finite representation for t (i) .

Example 3.6. Let us define the type t p stream ρ,τ for representing infinite p-streams of messages of type t:

t p stream ρ,σ def = p[t × µα.?[t × $ σ α] ρ+σ ] ρ
Each time a message is received from (respectively, sent to) an ?-stream (respectively, a !-stream), the priority σ of the stream is incremented by ρ. In particular, we have t ?stream ρ,σ = ?[t × t ?stream ρ+σ,σ ] ρ and t !stream ρ,σ = ![t × t ?stream ρ+σ,σ ] ρ . The functions ssend and asend can be specialized to sending messages on streams. For example, asend has the type ∀α ⊤ .∀ı (⊥,⊤) .∀κ (0,⊤) .α !stream ı,κ → α → ı,⊥ α !stream ı+κ,κ and ssend has an analogous type with ı in place of ⊥ in the latent effect of the rightmost arrow.

We are now ready to give a type to the node function in Example 2.3. We can derive:

node : ∀α.∀ı (⊥,⊤) .∀κ (0,⊤) .α → (α → α → α) → α !stream ı,κ → α ?stream ı,κ → ı,⊤ unit
There are two important observations regarding the typing of node: first, the local variables x ′ and y ′ in the body of node are assigned the types

x ′ : α !stream ı+κ,κ
and y ′ : α ?stream ı+κ,κ which differ from the corresponding types of x and y because of the priorities of streams change each time a message is sent/received. Then, the recursive call of node is well typed thanks to polymorphic recursion. The second observation concerns the latent effect of node, which cannot be finite (or ⊥) because node performs an unbounded sequence of input operations on channels with (numerically) strictly increasing priorities. Then, the saturated application of node yields an expression that has effect ⊤. Because of the constraints on priorities in the typing rules (Table 2) an expression with effect ⊤ cannot be "followed" by any other expression: it cannot be neither the functional part nor the argument of an application (see with the following assignments for the bound names in the body of mk_fibo_network:

ci : int #stream i-1,5 for 1 ≤ i ≤ 4 c5 : int #stream 9,5
c ′ 1 : int !stream 10,5 out : int #stream 2,5 Note that mk_fibo_network itself is a pure function, since all the computation (and communication) is performed in threads spawned within the body of the function. link : ∀α.∀ı.∀ (ı,⊤) .∀κ (0,⊤) .α ?stream ı,κ → α !stream ,κ → ı,⊤ unit delay : ∀α.∀ı.∀ (ı,⊤) .∀κ (0,⊤) .α ?stream ı,κ → α !stream +κ,κ → ı,⊤ unit copy : ∀α.∀ı.∀ (ı,⊤) .∀h (,⊤) .∀κ (0,⊤) .α ?stream ı,κ → α ?stream ,κ → ı,⊥ α !stream h,κ → ı,⊤ unit add : ∀ı.∀ (ı,⊤) .∀h (,⊤) .∀κ (0,⊤) .int ?stream ı,κ → int ?stream ,κ → ı,⊥ int !stream h,κ → ı,⊤ unit Table 4. Typing of the stream combinators in Example 2.4.

Properties

The type system is a conservative extension of the Hindley-Milner type system: every program that does not make use of the communication primitives and that is well typed in the Hindley-Milner type system is also well typed in our type system. This follows from the observation that the effect of pure expressions is ⊥ and unlimited types have priority ⊤ by definition, therefore all the conditions concerning priorities in the typing rules are trivially satisfied.

Let us now discuss the properties of well-typed programs. The first, expected property is subject reduction, namely the fact that the reduction of expressions/processes preserves well typedness. For expressions, this is the familiar preservation of types. For processes, we must take into account the fact that linear channels are consumed after each synchronization (last but one reduction in Table 1). This means that when a process P performs a communication on some channel a, the channel must disappear from the type environment used for typing the process. To this aim, we define a partial operation Γℓ that removes ℓ from Γ , when ℓ is a channel:

Γ -τ def = Γ (Γ , a : ρ ) -a def = Γ
Now, we can formulate subject reduction:

Theorem 3.8. The following properties hold:

1. If Γ ⊢ Θ e : t & ρ and e -→ e ′ , then Γ ⊢ Θ e ′ : t & ρ.

2. If Γ ⊢ P and P ℓ --→ P ′ , then Γℓ ⊢ P ′ .

The fact that the type environment changes because of reductions is a common trait of behavioral type systems, such as those based on session types [START_REF] Dardha | Session types revisited[END_REF][START_REF] Gay | Linear type theory for asynchronous session types[END_REF][START_REF] Honda | Types for dyadic interaction[END_REF][START_REF] Honda | Language primitives and type disciplines for structured communication-based programming[END_REF]. Linear channel types are a basic form of behavioral types. There are two things to remark regarding Theorem 3.8. The first one is that the effect ρ of an expression e does not change when e reduces. This is expected since the reductions of expressions in Table 1 solely concern the pure fragment of the calculus not involving communication primitives. The second observation is that Γa is not defined if a ∈ dom(Γ ). This means that Theorem 3.8 is slightly more than an auxiliary result for proving the soundness of the type system (Theorem 3.11 below). It means that well-typed programs never attempt at using the same channel twice, namely that channels in well-typed programs are indeed linear channels. This property has important practical consequences, since it allows the efficient implementation (and deallocation) of channels [START_REF] Kobayashi | Linearity and the picalculus[END_REF][START_REF] Turner | Once upon a type[END_REF].

Another property granted by linear communications is that computations are deterministic, despite threads may interleave actions in different ways. We express this property as strong confluence of well-typed programs: Theorem 3.9 (strong confluence). Let Γ ⊢ P and P

ℓ 1 --→ P1 and P ℓ 2 --→ P2. Then either P1 ≡ P2 or there exist Q such that P1 ℓ 2 --→ Q and P2 ℓ 1 --→ Q.
Theorems 3.8 and 3.9 just reformulate expected or known results [START_REF] Kobayashi | Linearity and the picalculus[END_REF] concerning the linear π-calculus in the context of a functional language. We now turn the attention to the deadlock freedom properties granted by our typing discipline. Deadlock freedom roughly corresponds to the property that if the program terminates, then it has no pending I/O operations left. In our case, the only terminated program without pending operations is (structurally equivalent to) {()}. We can therefore define deadlock freedom thus: Definition 3.10 (deadlock freedom [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]). We say that P is dead-

lock free if P τ --→ * Q -→ implies Q ≡ {()}.
The notation Q -→ means, as usual, that Q is unable to reduce further. Now, every well-typed, closed process is free from deadlocks:

Theorem 3.11 (soundness). Let ∅ ⊢ P . Then P is deadlock free.

Theorem 3.11 can be generalized to processes that are well typed in a balanced environment Γ , where Γ is balanced if its domain contains only channels with # polarity. The balancing condition, which is trivially satisfied by the empty context ∅ in the statement of Theorem 3.11, ensures that the program is "complete", in the sense that every linear channel is used for both an input and an output operation. This is essential to guarantee that the program does not get stuck on a pending I/O operation which has no complementary one. Nonetheless, one may think that the statement of Theorem 3.11 is rather weak, considering that every process P (even an ill-typed one) can be "fixed" and become part of a deadlock-free system if composed in parallel with the diverging thread {rec x x}.

It is not easy to state an interesting property of well-typed partial programs -programs that are well-typed in non-balanced environments -or of partial computations -computations that have not reached a stable (i.e., irreducible) state. We might think that welltyped programs eventually use all of their channels. This property is false in general, for two reasons. First, our type system does not guarantee the termination of well-typed expressions, so for example a thread like {a!(rec x x)} never uses channel a, because the evaluation of the message does not terminate. Second, there are threads that repeatedly generate (or receive) new channels, so that the set of channels they own is never empty. This happens for instance in Example 2.3 and Example 2.4. What we can prove is that, assuming that a well-typed program does not internally diverge, then each channel it owns will eventually be used for a communication or it will be sent to the environment in a message. To formalize this property we must generalize reductions to labeled transitions, so that we can reason on the evolution of partial programs. Labels λ, . . . of transitions are defined by λ ::= ℓ a?e a!v and the transition relation λ -→ extends reduction with the rules a ∈ bn(C )

C [a!v] a!v -→ C [()] a ∈ bn(C ) fn(e) ∩ bn(C ) = ∅ C [recv a] a?e -→ C [e]
where C ranges over process contexts

C ::= {E } | (C | P ) | (P | C ) | new a in C .
Messages of input transitions have the form a?e where e is an arbitrary expression instead of a value. This is just to allow a technically convenient formulation of Definition 3.12 below. We formalize the assumption concerning the absence of internal divergences as a property that we call interactivity. Note that interactivity is a property of typed processes, which we write as pairs Γ P , since the messages exchanged between a process and the environment in which it executes are not arbitrary in general.

Definition 3.12 (interactivity). Interactivity is the largest predicate on typed processes such that Γ P interactive implies Γ ⊢ P and:

1. P has no infinite reduction P

ℓ 1 -→ P1 ℓ 2 -→ P2 ℓ 3 -→ • • • , and 2. if P ℓ -→ Q, then Γ -ℓ Q is interactive, and 3. if P a!v -→ Q and Γ = Γ ′ , a : ![t] n , then Γ ′′ Q is interactive for some Γ ′′ ⊆ Γ ′ , and 4. if P a?x -→ Q and Γ = Γ ′ , a : ?[t] n , then Γ ′′ Q{v/x} is interactive for some v and Γ ′′ ⊇ Γ ′ such that n < |Γ ′′ \ Γ ′ |.
Clause [START_REF] Amtoft | Type and behaviour reconstruction for higher-order concurrent programs[END_REF] says that an interactive process does not internally diverge, so it will eventually halt either because it terminates or because it needs interaction with the environment in which it executes. Clause (2) simply states that reductions preserve interactivity. Clause [START_REF] Bird | Nested datatypes[END_REF] states that a process with a pending output on a channel a must reduce to an interactive process after the output is performed. Finally, clause (4) states that a process with a pending input on a channel a may reduce to an interactive process after the input of a particular message v is performed. Note that clauses (2) and ( 3) state provable properties of well-typed processes, and the condition Γ ′′ ⊇ Γ where n < |Γ ′′ \ Γ ′ | in clause (4) follows from the typing of v, which must have priority n + 1 or lower. Therefore, the only additional conditions we are imposing on well-typed programs are convergence of P in clause (1) and the existence of v in clause [START_REF] Bird | De Bruijn Notation as a Nested Datatype[END_REF]. It is now possible to prove that well-typed, interactive processes eventually use their channels. Theorem 3.13 (interactivity). Let Γ P be an interactive typed process such that a ∈ fn(P ). Then P

λ 1 -→ P1 λ 2 -→ • • • λn -→ Pn
for some λ1, . . . , λn such that a ∈ fn(P ).

Related Work

Higher-order concurrent languages. Concurrent ML [START_REF] Reppy | CML: A Higher-Order Concurrent Language[END_REF][START_REF] Reppy | Concurrent Programming in ML[END_REF] is probably the most studied higher-order language with concurrency primitives. In addition to primitives such as send and recv, CML also considers first-class events that can be used for building I/O actions in a compositional way, in the style of monadic IO actions of Haskell. The approach we have described in this paper can be easily extended to CML events, by annotating event types with priorities. Effect systems for higher-order concurrent languages are discussed in [START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF][START_REF] Nielson | Higher-order concurrent programs with finite communication topology[END_REF]. Effects are used for checking that the communication behavior of a program does not deviate from a desired protocol or for establishing properties (such as finiteness) of the communication topology of a concurrent system. Type inference algorithms are presented in [START_REF] Amtoft | Type and behaviour reconstruction for higher-order concurrent programs[END_REF][START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF][START_REF] Nielson | Constraints for Polymorphic Behaviours of Concurrent ML[END_REF]. Apart from the fact that we focus on linear communications, a major difference between these and our work is that in [START_REF] Amtoft | Type and behaviour reconstruction for higher-order concurrent programs[END_REF][START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF][START_REF] Nielson | Constraints for Polymorphic Behaviours of Concurrent ML[END_REF][START_REF] Nielson | Higher-order concurrent programs with finite communication topology[END_REF] the structure of communications is recorded in the effects, while in our case effects simply keep track of the priority of the channels involved in communications and the protocol is encoded in types. More recently, linear typing disciplines not based on effects for higher-order languages equipped with a native notion of sessions have been investigated [START_REF] Bono | Polymorphic Types for Leak Detection in a Session-Oriented Functional Language[END_REF][START_REF] Gay | Linear type theory for asynchronous session types[END_REF][START_REF] Wadler | Propositions as sessions[END_REF]. In addition to safety, types are used in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF] for estimating bounds in the size of message queues, and in [START_REF] Bono | Polymorphic Types for Leak Detection in a Session-Oriented Functional Language[END_REF] for detecting memory leaks occurring when channel pointers become part of unreachable, cyclic memory structures. The type system in the present paper subsumes the one in [START_REF] Bono | Polymorphic Types for Leak Detection in a Session-Oriented Functional Language[END_REF], for the absence of cyclic dependencies between channels is a necessary condition for deadlock freedom. Also, we simultaneously simplify and generalize the language in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF]: since binary sessions can be encoded in the linear π-calculus [START_REF] Dardha | Session types revisited[END_REF], our language subsumes that in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF] and in addition our type system treats polymorphism and guarantees deadlock freedom also in presence of session interleaving. Wadler [START_REF] Wadler | Propositions as sessions[END_REF] presents a session-based functional language such that well-typed programs are deadlock free without requiring any particular type annotations dedicated to this purpose. However, in his case the syntax of (well-typed) programs prevents the modeling of cyclic network topologies so that, for instance, the networks in Examples 2.3 and 2.4 are ill typed.

Deadlock freedom. Our type system has been partly inspired by previous static analysis techniques guaranteeing deadlock freedom for the π-calculus [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF]. There are two main differences between [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] and our own work: first, we work with a higher-order language instead of a process calculus. This requires a richer structure of types, in particular using (latent) effects, since the typing rules do not have visibility of the whole continuation of a program fragment. The second main difference regards the use of polymorphism (and particularly of polymorphic recursion) with respect to channel priorities. This feature has a significant impact on the accuracy of the type system. For example, the suitable encodings of the program in Example 2.3 or the stream network in Example 2.4 are ill typed according to the type system in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF]. In general, the lack of polymorphism in [START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF] prevents any process combining recursion and interleaving actions on two or more channels from being well typed. Properties stronger than deadlock freedom such as lock freedomthe assurance that every pending communication eventually takes place -are considered in [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A hybrid type system for lockfreedom of mobile processes[END_REF][START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF]. Our interactivity property (Theorem 3.13) is similar in spirit to the hybrid type system [START_REF] Kobayashi | A hybrid type system for lockfreedom of mobile processes[END_REF] showing that lock freedom can be characterized as the conjunction of deadlock freedom and termination.

Linearity. Our language makes use of linear channels, whose properties have been previously studied in the setting of the πcalculus [START_REF] Kobayashi | Linearity and the picalculus[END_REF]. Many practical systems make widespread use of linear channels [START_REF] Igarashi | Type-based analysis of usage of values for concurrent programming languages[END_REF][START_REF] Igarashi | Type-based analysis of communication for concurrent programming languages[END_REF]. It has been shown that structured communications such as those in binary sessions can be modeled solely using binary sessions [START_REF] Dardha | Session types revisited[END_REF] and a large fraction of multiparty sessions -those with an arbitrary, although usually fixed, number of participants -can be modeled using linear channels as well [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF]. Concurrency models such as Kahn's process networks [START_REF] Kahn | The semantics of simple language for parallel programming[END_REF] or communicating finite-state machines [START_REF] Brand | On communicating finite-state machines[END_REF] make use of communication channels that are exactly, or very close to, those that can be encoded using linear channels. Incidentally, deadlock detection in these systems has been shown to be undecidable, even without channel mobility and in simple network configurations [START_REF] Brand | On communicating finite-state machines[END_REF][START_REF] Cécé | Verification of programs with half-duplex communication[END_REF].

Various forms of linearity find widespread use also in sequential languages, where they can be used for the improvement of code optimizations [START_REF] Turner | Once upon a type[END_REF], safe access control of shared resources [START_REF] Suenaga | Fractional ownerships for safe memory deallocation[END_REF], and refined analysis of deallocations [START_REF] Kobayashi | Quasi-linear types[END_REF]. The monadic I/O system of Haskell is a way of enforcing the linear usage of global state [START_REF] Wadler | Linear types can change the world! In Programming Concepts and Methods[END_REF].

Non-regular types. Limited forms of non-regular types, sometimes called nested datatypes, have already been considered [START_REF] Bird | Nested datatypes[END_REF][START_REF] Bird | De Bruijn Notation as a Nested Datatype[END_REF] also for processes [START_REF] Puntigam | Non-regular process types[END_REF]. In all these cases, the non-regularity follows from the very structure of types, whereas in our case it is only the priority annotations that change.

Concluding Remarks

Type safety alone is not strong enough to entail deadlock freedom when concurrent threads interleave actions on communication channels. This observation has led to the development of type systems [START_REF] Kobayashi | A type system for lock-free processes[END_REF][START_REF] Kobayashi | A new type system for deadlock-free processes[END_REF][START_REF] Kobayashi | A hybrid type system for lockfreedom of mobile processes[END_REF][START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] specifically aimed at ensuring deadlock freedom. A common trait of all these works is that they are based on the π-calculus [START_REF] Milner | The polyadic π-calculus: a tutorial[END_REF]. While computationally complete, the π-calculus's only focus is on communication, and programs encoded in the πcalculus are flat sequences of I/O actions. The intrinsic structure of high-level (and possibly higher-order) programs, which include procedures, functions, objects, modules, etc., is therefore lost in the encoding, meaning that the type-based techniques devised for the π-calculus may need significant reworking when ported back to concrete languages. Inspired by the type system for deadlock free-

11 2014/3/1
dom in [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF], we have studied this porting to a higher-order language with communication primitives à la Concurrent ML [START_REF] Reppy | CML: A Higher-Order Concurrent Language[END_REF][START_REF] Reppy | Concurrent Programming in ML[END_REF].

Our type system grants a strong form of deadlock freedom (Theorems 3.11 and 3.13) with a relatively minimal machinery, which has nonetheless a non-trivial impact when integrated with the other features of the language, most notably polymorphism and recursion. The presented type system also has some limitations, of which we discuss here the two that we consider most critical. The first obvious issue regards type reconstruction. As clearly witnessed by the examples in Section 3, the detailed nature of types makes type reconstruction almost mandatory if the type system is meant to be practically useful. We have not yet investigated whether a complete type reconstruction algorithm can be developed. We do have a prototypical reconstruction algorithm for a similar (but simpler) type system for the π-calculus [START_REF] Padovani | Deadlock and lock freedom in the linear π-calculus[END_REF] and we are aware of the fact that reconstruction algorithms supporting polymorphic recursion are feasible when this form of polymorphism is restricted to effects [START_REF] Amtoft | Type and behaviour reconstruction for higher-order concurrent programs[END_REF][START_REF] Amtoft | Type and Effect Systems: Behaviours for Concurrency[END_REF], which is precisely the way we use it. More work is necessary to see whether these good-looking premises lead to a concrete reconstruction algorithm.

Another issue is that some natural program patterns are ill typed. An example is given by filter_stream below, which is the stream-oriented counterpart of the well-known filter function:

1 let rec filter_stream f x y = 2 let (v,x ′ ) = recv x in 3 if (f v) then filter_stream f x ′ (asend y v) 4 else filter_stream f x ′ y
The problem of filter_stream is that on line 4 the priority of x ′ is displaced with respect to that of x, while that of y stays obviously the same and we are not able to differentiate the displacements for the priorities of different arguments. In general, the mechanism of priority displacement $ ρ allows us to deal with programs whose communication behavior follows a regular pattern and does not depend on the data being communicated. This is not the case for filter_stream. A solution could be to switch to rational (instead of integer) priorities and using more sophisticated priority mapping functions that allow priority "compression": the priority of x ′ could always be chosen to be half way between that of x and that of y. This extension, however, would invalidate Theorem 3.13, which holds only if the set of priorities is discrete, and would certainly complicate an hypothetical type reconstruction algorithm. A workaround could be the combined use of userspecified recursive types together with iso-recursion, in a way that mimics the usual treatment of recursive algebraic data types.

By induction hypothesis we deduce that red(e1) = red(e2) = ∅, hence we must conclude that e is a redex. By Lemma A.14 we deduce that e1 is either an abstraction or the application send a or one of the constants in the set {fork, open, send, recv}. In each case we are able to conclude that e is a redex, possibly using Lemma A.14 again for deducing that open is applied to () and the arguments of send and recv have the right shape.

Corollary A.17. The only well-typed thread without redexes is {()}.

Proof. Let Γ ⊢ {e} where e has no redex. By Lemma A. [START_REF] Kobayashi | Quasi-linear types[END_REF] we deduce that e is a value. By Lemma A.14, the only value of type unit is ().

Theorem A.18 (Theorem 3.9). Let Γ ⊢ P and P

ℓ 1 --→ P1 and P ℓ 2 --→ P2. Then either P1 ≡ P2 or there exist Q such that P1 ℓ 2 --→ Q and P2 ℓ 1 --→ Q.
Proof. Without loss of generality we may assume that P ≡ i∈I Qi where the Qi are threads different from {()}. Indeed, if there are restrictions these can always be brought up at the top level using structural congruence and the inner process is still well typed. Also, {()} threads can be removed again by structural congruence. Now, from Lemma A.16 we know that each Qi has exactly one redex, so it can reduce in at most one way, either independently of the other threads or in combination with another thread Qj if a communication takes place. In the latter case, Qj is uniquely identified because a linear channel cannot occur in more than two threads. In every case it is easy to see that the statement holds.

A.6 Deadlock Freedom

This section is devoted to the proof of the soundness theorem, namely Theorem 3.11. The first auxiliary result states that the effect of an expression is (numerically) larger than the priority of a channel that is the subject of a communication in a well-typed expression. That is, the effect is a conservative approximation of the priority of all the I/O operations performed during the evaluation of a well-typed expression.

Lemma A.19. Let Γ be ground and either

Γ ⊢ Θ E [recv a] : t & ρ or Γ ⊢ Θ E [a!v] : t & ρ. Then |Γ (a)| ≤ ρ.
Proof. This is a straightforward induction on E , using the fact that the typing rules accumulate effects in the conclusion.

The second auxiliary result states the relationship between the priority of the subject of a communication that is a redex, and the priority of any other channel that may occur in a well-typed expression. In particular, the subject of the communication is the channel with the highest (i.e., numerically smallest) priority occurring free in the expression.

Lemma A.20. Let Γ be ground and either The remaining cases are similar.

• Γ ⊢ Θ E [recv a] : t & ρ and b ∈ fn(E ), or • Γ ⊢ Θ E [a!v] : t & ρ and b ∈ fn(E ) ∪ fn(v).
We are now approaching the core of the proof. Before establishing the crucial lemma, we introduce some convenient terminology regarding type environments.

Definition A.21 (even and odd type environment). We say that Γ is even if for every u ∈ dom(Γ ) we have that Γ (u) is a channel type with # polarity. We say that it is odd if, for every u ∈ dom(Γ ) we have that Γ (u) is a channel type with either ? or ! polarity.

Note that the empty type environment is both even and odd. In the following, we use Γeven (respectively, Γ odd ) to range over even (respectively, odd) type environments. Note that any ground type environment Γ can be split into a pair Γ odd , Γeven. A fundamental property of well-typed, stable processes, those that cannot reduce any further, is that they must be typed in an environment where the odd part contains at least one channel whose priority is higher (i.e., numerically smaller) than the priority of all the channels in the even part. That is, the process cannot be blocked on a I/O operation for a channel that occurs with both polarities in the very same process. Proof. We do an induction on the number of restrictions in P .

In the base case P has no restrictions. Then, from the hypothesis P ) ∪ fn(vj) for every j ∈ J, because c has minimum priority hence it cannot be blocked by other operations on channels with greater or equal priority. Then, since c ∈ dom(Γeven) and all channel types in Γeven have even polarity, it must be the case that c = ai = bj for some i ∈ I and j ∈ J. This contradicts the hypothesis that P τ --→. An easy consequence of Lemma A.22 is that every stable process that is well typed in an even environment must be structurally equivalent to {()}.

Lemma A.23. Let Γeven be ground and Γeven ⊢ P and P τ --→. Then P ≡ {()}.

Proof. We do an induction on the number of restrictions in P . If P has no restrictions, then from Lemma A.22 we deduce that Γeven = ∅, namely that P is a closed process. We conclude observing that every well-typed, closed process is structurally congruent to {()}. If P ≡ new a in Q, then there exists Γ ′ even such that Γ ′ even ⊢ Q. By induction hypothesis we deduce Q ≡ {()}. This contradicts the hypothesis that P is well typed, since a must occur free in Q, hence this case is impossible. Soundness of the type system is then an easy corollary of the previous Lemmas.

Theorem A.24 (Theorem 3.11). Let ∅ ⊢ P . Then P is deadlock free.

Proof. Straightforward consequence of Theorem A.13 and of Lemma A.23.

A.7 Interactivity

The first auxiliary result we need states that reductions can only decrease the priority of a type environment. Then, we show that every interactive typed process has a sequence of transitions (possibly involving channels with odd type) that leads to a new state in which the priority of channels is strictly lower than in the original process.

Ri

where each Ri is blocked on ai, because no ai can be blocked by another channel with lower (or equal) priority. Using the hypothesis that Γ ′′ Pm we know that there exists a Γ ′ and k labels λi each of the form ai?vi or ai!vi such that

Pm λ 1 -→ • • • λ k -→ P ′
and Γ ′ P ′ is an interactive typed process where none of the ai occurs in Γ ′ . Also, by Definition 3.12 we know that every output action can only remove channels from processes, and every input action can only add channels with priority strictly lower than |Γ odd |. Since the ai were all the channels with priority |Γ odd |, we conclude

|Γ ′′ | < |Γ ′ |.
Interactivity is then a consequence of the fact that the priority of any given channel is at finite distance from that of the whole type environment used for typing a process.

Theorem A.27 (Theorem 3.13). Let Γ P be an interactive typed process such that Γ ⊢ P and a ∈ fn(P ). Then

  a, b) = (open(), open()) in fork fun _ (send a (fibo (n -1))); fork fun _ (send b (fibo (n -2))); (recv a) + (recv b)

Example 2 . 2 .

 22 Structured communications involving the exchange of several messages can be modeled using continuations. To this aim, it is convenient to define two functions let ssend x y = let c = open() in x!(y, c); c let asend x y = let c = open() in fork fun _ x!(y, c); c

1 let rec node state f x y = 2 let

 12 x ′ = asend x state in 3 let (state ′ , y ′ ) = recv y in 4 node f (f state state ′ ) x ′ y ′ 5 in let (a, b) = (open(), open()) in 6 fork fun _ (node state0 f0 a b); fork fun _ (node state1 f1 b a)

1 letFigure 1 .

 11 Figure1. The Fibonacci stream network[START_REF] Reppy | Concurrent Programming in ML[END_REF].

  extend the function | • | to type environments so that |Γ | def = u∈dom(Γ ) |Γ (u)| with the convention that |∅| = ⊤; we write un(Γ ) if |Γ | = ⊤, namely if every type in the range of Γ is unlimited.

Example 3 . 3 .

 33 Considering again fibo in Example 2.1, and assuming that the infix operator + is just the application of the constant + with TypeOf(+) = int → int → int, we derive ⊢ + : TypeOf(+) & ⊥ . . . a : ?[int] m ⊢ recv a : int & m a : ?[int] m ⊢ + (recv a) : int → int & m for the left operand and . . . b : ?[int] n ⊢ recv b : int & n for the right operant, therefore we conclude a : ?[int] m , b : ?[int] n ⊢ + (recv a) (recv b) : int & n

Example 3 . 4 .

 34 Given the usual definition of function composition let (•) f g = fun x (f (g x))

  Then |Γ (a)| < |Γ (b)|.Proof. We prove the result assuming Γ ⊢ Θ E [a!v] : t & ρ and b ∈ fn(E )∪fn(v). With the other hypothesis the proof is analogous. We proceed by induction on E and by cases on its shape.Suppose E = [ ]. Then it must be the case that b ∈ fn(v). From [T-APP] and the type of send we deduce that there exist Γ1 and Γ2 such that Γ1 + Θ Γ2 = Γ and Γ1 ⊢ Θ send a : s → n,n unit and Γ2 ⊢ Θ v : s and Γ (a) = ![s] n and n < |Γ2|. We conclude|Γ (a)| = n < |Γ2| ≤ |Γ2(b)| = |Γ (b)|. Suppose E = (E ′ , e).From [T-PAIR] we deduce that there exist Γ1 and Γ2 and t1 and t2 such that Γ1 + Θ Γ2 = Γ and Γ1 ⊢ Θ E ′ [recv a] : t1 & ρ1 and Γ2 ⊢ Θ e : t2 & ρ2 and ρ1 < |Γ2|. We distinguish two subcases. If b ∈ fn(E ′ ), then by induction hypothesis we deduce |Γ1(a)| < |Γ1(b)| and we conclude by observing that |Γ (a)| = |Γ1(a)| and |Γ (b)| = |Γ1(b)|. If b ∈ fn(e), then we conclude |Γ (a)| = |Γ1(a)| by definition of + Θ ≤ ρ1 by Lemma A.19 < |Γ2| from [T-PAIR] ≤ |Γ2(b)| by definition of |Γ2| = |Γ (b)| by definition of + Θ Suppose E = (v ′ , E ′ ). From [T-PAIR] we deduce that there exist Γ1 and Γ2 such that Γ1 + Θ Γ2 = Γ and Γ1 ⊢ Θ v ′ : t1 and Γ2 ⊢ Θ E ′ [a!v] : t2 & ρ and ρ < |t1|. We distinguish two subcases. If b ∈ fn(v ′ ), then we conclude |Γ (a)| = |Γ2(a)| by definition of + Θ ≤ ρ by Lemma A.19 < |t1| from [T-PAIR] = |Γ1| by Lemma A.5 ≤ |Γ1(b)| by definition of |Γ1| = |Γ (b)| by definition of + Θ If b ∈ fn(E ′ ), then we conclude |Γ (a)| = |Γ2(a)| < |Γ2(b)| = |Γ (b)| using the definition of + Θ and the induction hypothesis.

Lemma A. 22 .

 22 Let Γ odd , Γeven ⊢ P and P τ --→ and Γ odd , Γeven is ground and all channels in Γ odd have odd polarity and all channels in Γeven have even polarity. Then |Γ odd | ≤ |Γeven|.

τ

  --→ it must be the case thatP ≡ i∈I {Ei[recv ai]} | j∈J {E ′ j [bj!vj]} Suppose,by contradiction, that |Γeven| < |Γ odd | and let c ∈ dom(Γeven) such that |Γeven(c)| = |Γeven|. By Lemma A.20 we deduce that c ∈ fn(Ei) for every i ∈ I and c ∈ fn(E ′ j

Lemma A. 25 .

 25 If Γℓ is defined, then |Γ | ≤ |Γ -ℓ|.Proof. Immediate consequence of the definition of Γℓ.

Lemma A. 26 . 1 - 1 -

 2611 Let Γ P be an interactive typed process such that |Γ | < ⊤. Then there exist λ1, . . . , λn and Γ ′ such thatP λ → • • • λn -→ P ′ and Γ ′ P ′ is an interactive typed process and |Γ | < |Γ ′ |.Proof. Consider a maximal reductionP ℓWe know that such reduction exists and is finite becauseΓ P is interactive. Let Γ ′′ = (• • • ((Γ -ℓ1) -ℓ2) -• • •ℓm). From Theorem A.13 we know that Γ ′′ ⊢ Pm and from Lemma A.25 we also know |Γ | ≤ |Γ ′′ |. If |Γ | < |Γ ′′ | there is nothing left to prove, so suppose |Γ | = |Γ ′′ | and let Γ ′′ = Γ odd , Γeven where Γ odd contains only channel with odd polarity and Γeven contains only channels with even polarity. From the hypothesis Pm τ --→ and Γ ′′ ⊢ Pm and Lemma A.22 we deduce that |Γ odd | ≤ |Γeven|. From the hypothesis |Γ | < ⊤ we also know that dom(Γ odd ) contains at least one channel. Let a1, . . . , a k be the channels in dom(Γ odd ) such that |Γ odd (ai)| = |Γ odd |, that is the ai are the channels with highest priority in Γ ′′ . Then it must be the case Pm ≡ new ã in Q | i=1..k

λ 2 -

 2 → • • • λn -→ Pnfor some λ1, . . . , λn such that a ∈ fn(Pn).

Proof. 1 -

 1 We proceed by induction on |Γ (a)| -|Γ |. By Lemma A.26, we know that there exist λ1, . . . , λm and Γ ′′ such that P λ → • • • λm -→ P ′ and Γ ′′ P ′ is an interactive typed process and |Γ | < |Γ ′′ |. We have two possibilities. If |Γ (a)| < |Γ ′′ |, then we conclude a ∈ fn(P ′ ). If |Γ ′′ | ≤ |Γ (a)|, then |Γ (a)| -|Γ ′′ | < |Γ (a)| -|Γ | and we conclude by induction hypothesis.

  Example 3.7. Table4presents the types of the stream combinators used in Example 2.4. All of them take advantage of polymorphic recursion and are non-terminating, tail-recursive functions with latent effect ⊤ just like node discussed in Example 3.6. Now we can derive, for example mk_fibo_network : unit → int ?stream2,5

[T-APP]), it cannot occur within pairs (see [T-PAIR]), nor can it occur in the left part of a let (see [T-SPLIT] and [T-LET]). In other words, it can only occur in tail position. This is precisely what happens with node in Example 2.3.

  We conclude that the assumption |Γeven| < |Γ odd | is absurd, hence |Γ odd | ≤ |Γeven|. In the inductive case, we have P ≡ new a in Q where Q has fewer restrictions than P . From the hypothesis Γ odd , Γeven ⊢ P and [T-NEW] we deduce Γ odd , Γeven, a : #[t] n ⊢ Q. By induction hypothesis we have |Γ odd | ≤ |Γeven, a : #[t] n |. We conclude by observing that |Γeven, a : #[t] n | = |Γeven| ∧ n ≤ |Γeven|.

	16	2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

2014/3/1

A. Supplement to Section 3

Type (scheme) combination

A.2 Restriction of priority environments

We write Θ| {ı 1 ,...,ın,α 1 ,...,αm} for the smallest well-formed priority environment Θ ′ included in Θ such that ıi ∈ dom(Θ ′ ) for every 1 ≤ i ≤ n and αj ∈ dom(Θ ′ ) for every 1 ≤ j ≤ m. Note that Θ {ı} may include priority variables other than ı because the interval of ı may contain other priority variables. For example, if Θ = ı ∈ P,  ∈ (ı, ⊤], then Θ| {} = Θ.

A.3 Basic properties

The following are standard properties of well-typed expressions and values. In all cases the proofs are simple inductions on the derivation of well typedness.

Lemma A.1. Let Γ ⊢ Θ e : t & ρ. Then fn(e) ⊆ dom(Γ ) and ftv(t) ∪ fpv(t) ∪ pv(ρ) ⊆ dom(Θ).

The following Lemma shows that a value has no effects, which is a common feature of effect systems. We implicitly use this property in the rest of the appendix and omit the priority from the judgments that regard values. Therefore, we will often write

For values it is possible to establish an important relationship between the priority of their type and that of the type environments in which they are typed:

TypeOf(c) ≻ Θ t and we conclude by analyzing the priority of constants. If v = a, then t = p[s] ρ and Γ = Γ ′ , a : t and

The case for v = send a is similar to that for a.

We introduce the category of quasi values v, . . . , namely of expressions that are substituted. These include the values, as expected, but also recursive terms, which are substituted when unfolded:

v ::= v | rec x e For quasi values, we have a weaker property than that of Lemma A.5 because a recursive term may, in principle, have a linear type.

Proof. When v is a value the result follows from Lemma A.5. When v is a recursion, we conclude using the hypothesis in rule [T-REC POLY] that the environment is unlimited.

Note that Lemma A.6 does not hold for generic expressions. For example, we have that a!3 has type unit in the type environment

A.4 Subject Reduction

This section is dedicated to the proof of Theorem 3.8 (subject reduction). The result is key for proving the soundness of the type system. The sequence of auxiliary results follows the same pattern as in [START_REF] Gay | Linear type theory for asynchronous session types[END_REF], with the necessary adjustments due to the differences between the type systems.

Typing of expressions

. Complete typing rules for expressions and processes.

Proof. By induction on E .

Proof. By induction on E .

Proof. The proof is almost entirely conventional. The only critical aspect is the fact that x may occur non linearly within e, hence multiple copies of v may be necessary. In these cases, however, the type scheme T of x must be unlimited, as by definition of type combination, and from Lemma A.6 one deduces that Γ1 is also unlimited, meaning that Γ1+Γ1 is defined and equal to Γ1 itself.

we deduce that there exist Γ1 and Γ2 such that Γ = Γ1 + Γ2 and Γi ⊢ Pi for every i = 1, 2. By induction hypothesis we have Γ1ℓ ⊢ P ′ 1 and we conclude Γℓ ⊢ P ′ with one application of [T-PAR] and observing that Γℓ = (Γ1ℓ) + Γ2.

By induction hypothesis and using the fact that ℓ = a we deduce (Γℓ), a :

application of Lemma A.12 and the induction hypothesis.

A.5 Confluence

This section is devoted to the proof of Theorem 3.9. The first auxiliary result is a conventional lemma about canonical forms, inferring the shape of a value having a given type.

Lemma A.14 (canonical forms). Let Γ ⊢ Θ v : t. Then: Proof. By a trivial case analysis on the typing rules of Table 5.

Next, we define the notion of reducible expression, namely of an expression that, when occurring within an evaluation context, it may potentially trigger a reduction of the thread in which it occurs, possibly in combination with another thread in case of a synchronization.

Definition A.15 (redex). A redex r is an expression having one of the following forms:

Note that we consider a!v and recv v to be redexes, even though they are not able to reduce independently, but only if they occur within two parallel threads. The next result shows that each well-typed expression has at most one redex. 1. if e is a value, then red(e) = ∅; 2. if e is not a value, then red(e) is a singleton.

Proof. We prove both properties simultaneously, by induction on e and by cases on its structure.

If e is a constant, a channel, or an abstraction then it is a value and we conclude by observing that red(e) = ∅. Note that e cannot be a variable, because Γ is assumed to be ground. Suppose e = rec x e ′ . Then e is not a value and we conclude by observing that red(e) = {[ ]}.

Suppose e = let x = e1 in e2. Then e is not a value and we must show that red(e) is a singleton. From [T-LET] we deduce that there exist Γ1 and Γ2 such that Γ = Γ1 + Θ Γ2 and Γ1 ⊢ Θ,Θ ′ e1 : s & σ. We distinguish two subcases: if e1 is a value, then by induction hypothesis red(e1) = ∅ and we conclude by observing that red(e) = {[ ]}; if e1 is not a value, then by induction hypothesis red(e1) is a singleton and we conclude by observing that red(e) = {let x = E in e2 | E ∈ red(e1)}.

Suppose e = let (x, y) = e1 in e2. Then e is not a value and from [T-SPLIT] we deduce that there exist Γ1 and Γ2 such that Γ = Γ1 + Θ Γ2 and Γ1 ⊢ Θ e1 : t1 × t2 & σ. We distinguish two subcases: if e1 is a value, then by induction hypothesis we have red(e1) = ∅ and by Lemma A.14 we deduce that it must have the form (v, w), so we conclude by observing that red(e) = {[ ]}; if e1 is not a value, then by induction hypothesis we have that red(e1) is a singleton and we conclude by observing that red(e) = {let (x, y) = E in e2 | E ∈ red(e1)}.

Suppose e = (e1, e2). From [T-PAIR] we deduce that there exist Γ1 and Γ2 such that Γi ⊢ Θ ei : ti & ρi for i = 1, 2. We distinguish three subcases: if both e1 and e2 are values, then by induction hypothesis red(e1) = red(e2) = ∅ and we conclude by ovserving that e is also a value and red(e) = ∅; if e1 is a value but e2 is not, then by induction hypothesis we deduce that red(e1) = ∅ and red(e2) is a singleton and we conclude by observing that red(e) = {(e1, E ) | E ∈ red(e2)}; if e1 is not a value, then by induction hypothesis we deduce that red(e1) is a singleton and we conclude by observing that red(e) = {(E , e2) | E ∈ red(e1)}.

Suppose e = e1e2. Then e is not a value and from [T-APP] we deduce that there exist Γ1 and Γ2 such that Γ1 ⊢ Θ e1 : s → σ,τ t & ρ1 and Γ2 ⊢ Θ e2 : s & ρ2. We distinguish three subcases but we only discuss the subcase in which e1 and e2 are both values, since the other subcases are similar to those already discussed for pairs.