{'fraction_non_alphanumeric': 0.025895829253965146, 'fraction_numerical': 0.004674955942823576, 'mean_word_length': 4.887175792507205, 'pattern_counts': {'":': 0, '<': 1, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
On the chemistry of typestate-oriented actors

Typestate-oriented programming is an extension of the OO paradigm in which objects are modeled not just in terms of interfaces but also in terms of their usage protocols, describing legal sequences of method calls, possibly depending on the object's internal state. We argue that the Actor Model allows typestate-OOP in an inherently distributed setting, whereby objects/actors can be accessed concurrently by several processes, and local entities cooperate to carry out a communication protocol. In this article we illustrate the approach by means of a number of examples written in Scala Akka. We show that Scala's abstractions support clean and natural typestate-oriented actor programming with the usual asynchronous and non-blocking semantics. We also show that the standard type system of Scala and a typed wrapping of usual (untyped) Akka's ActorRef are enough to provide rich forms of type safety so that well-typed actors respect their intended communication protocols. This approach draws on a solid theoretical background, consisting of a sound behavioral type system for the Join Calculus, that is a foundational calculus of distributed asynchronous processes whose semantics is based on the Chemical Abstract Machine, that unveiled its strong connections with typestate-oriented programming of both concurrent objects and actors.


Introduction
A key issue of distributed systems is the coordination of distributed entities that concurrently run in the system. Very different solutions can be developed to address this problem, but even distributed systems can be very different, hence it is important to carefully choose a solution (or a set of solutions) that is appropriate for the specific distributed system under consideration. A major distinction, indeed, can be made between the systems that adopt the shared memory model and those that rely on message passing. The first kind of systems is often a natural model for data-centric applications, that fit a centralized control of distributed entities that cooperate to fulfill logically centralized algorithms operating on mutable shared data. On the other hand, communication-centric applications are usually built on top of concurrent/distributes entities that take their decisions only based upon local information (locality and isolation principles).
A general approach to structuring distributed systems is Protocol-Oriented Programming, which endorses thinking (hence programming) in terms of communication protocols. In this view, programming a concurrent/distributed system entails the design of a precise communication protocol involving a possibly dynamic set of interacting parties. However, in order for a paradigm to become an effective programming style, it requires high-level support to express coordination protocols in the programming language, and, above all, it requires some support to check protocol compliance. Finding the correct abstractions to express and enforce coordination protocols is very hard, especially because suitable abstractions should also productively interoperate with the other abstractions provided by the language. For instance, systems with centralized control best fit a top-down implementation of a global coordination protocol, e.g. the multiparty session types's methodology that projects a global protocol into the sub-protocols of local parties [17]. On the contrary, distributed systems made of local entities that work with strong isolation and locality principles, require support for consistent bottom-up compositions of local behaviors. Furthermore, real systems usually rely on hybrid architectures and logical models, so it is important to remind that there is no single solution and trade-offs are unavoidable.
In this article we study the application of the Typestate-Oriented Programming discipline to achieve protocol-oriented programming in an Actor System. Typestate-oriented programming (TSOP for short) [9,2,22,13] is an extension of the OO paradigm where objects are modeled not just in terms of interfaces but in terms of their usage protocols, describing legal sequences of method calls, possibly depending on the objects internal state. In [6] we showed how TSOP can be statically enforced in the Objective Join Calculus, that is a calculus of concurrent objects equipped with a semantics based on the chemical abstract machine [12]. More precisely, we introduced a simple behavioral type theory that allows to describe and enforce structured object protocols consisting of possibilities, prohibitions and obligations. According to the chemical metaphor, programs are modeled as chemical soups of molecules (i.e., multisets of messages sent to objects) that encode both the current state of the objects and the (pending) operations on them. Moreover, reaction rules, corresponding to object's method definitions, explicitly specify both the valid combinations of state and operations as well as the state changes engendered by each operation.
In [7] we put forward a couple of examples written with Scala Akka actors, showing that the actor programming model [16,1] bears strong similarities with TSOP we realized in the Objective Join Calculus, at least at the program level. The formal development of a behavioral type system for actors along the lines of [6] is the subject of current work. Instead, in this article we further explore the implementation of TSOP in the context of Scala Akka, and even if a full implementation of the behavioral type discipline of [6] requires a compiler extension, we demonstrate that exploiting the powerful typing support offered by Scala allows us to go a long way into checking protocol compliance solely using off-the-shelf development tools.

Road map and summary of the contributions
The implementation of typestate-oriented actors is entirely illustrated by means of examples. We start by fully studying an object with a very simple usage protocol, but that is enough to display all the issues of the typestate discipline. This main running example is presented in stages so to separate the explanation of different ingredients, more precisely: • in section 2.1 we draw on plain Akka actors, that are essentially untyped, thus in order to address protocol violations they have to resort to defensive programming by explicitly dealing with unintended messages; • in section 2.2 we introduce the use of types to represent actor's interfaces and typed actor references to encapsulate references to stateful actors; • in section 2.3 we resort to the explicit continuation-passing programming style to keep track of the dynamic change of the actors state; • in section 2.4 we refactor the code so to just implicitly deal with continuations. We define a suitable monad that allows (i) to simplify the code of the user of a stateful actor, bringing better to light its logic, (ii) the compiler to check that a stateful actor will only receive intended messages at the intended state, (iii) and usage protocol to be completely encoded in terms of typed expressions; • while in sections 2.3 and 2.4 we considered a stateful actor accessed by a single user, in section 2.5 we show that in order to scale the approach to the case of multiple concurrent users it is sufficient for the stateful actor to mix-in (a trait implementing) the semanticsà la chemical abstract machine.
The final section 3 displays our TSOP approach at work on a more complex scenario. It shows that Scala Akka actors effectively support the definition of stateful actors that can dynamically change both their behavior and their interface. Moreover, the Scala type system is expressive enough to let the compiler check that a stateful actor will only receive intended messages at the intended states. Besides the absence of wrong messages, a full typing support for protocol-oriented programming would also require to detect violations of protocol obligations, that is to ensure that all the intended messages are eventually sent. This property is captured by the behavioral typing studied in [6] but the required linear types are beyond the expressive power of the current Scala type system. All the code shown in the article is compatible with Scala 2.11.6 and Akka 2.3.4.

The 1-place Buffer
In this section we consider as a running example a buffer that can contain at most one value of a generic type T. The buffer provides just two operations: insert(x:T) and remove(), however since the buffer cannot hold more than a value, no two consecutive insert operations can be executed, and similarly no two consecutive remove operations. Such a usage constraint can be rephrased in typestate-oriented terms as the following protocol: Buffer protocol: the buffer has two possible states, EMPTY and FULL. When in state EMPTY its interface only contains the operation insert(x:T), whose execution moves the buffer to state FULL. When the buffer is in state FULL its interface only contains the operation remove(), whose execution moves it to state EMPTY. The initial state of the buffer is EMPTY.

Untyped Buffer Actor
Moving from the buffer's protocol above to the definition of a Buffer actor is straightforward: simply observe that actors can directly implement finite state machines (FSM) and the protocol above can be easily expressed as a FSM with two states EMPTY and FULL and two edges labeled insert(x:T) and remove() connecting one state with the other. We point out that we are not necessarily advocating the use of FSMs to express objects protocols, we use them here just as a mental bridge between protocol declarations and actor implementations.
The following code defines a generic Akka actor Buffer[T] that is intended to handle only the messages insert and remove, implemented as case classes. In particular, the actor defines two possible behaviors that correspond to the two possible buffer's states: EMPTY and FULL. Each behavior is a partial function (of type Receive as expected for Akka actor's behaviors) that only handles the single message that belongs to the interface of the corresponding state. Moreover, the state change engendered by the operations is obtained by using the actor's ability to change its current behavior by means of the become method. Finally, the definition of the receive method corresponds to setting the initial state of the buffer to EMPTY. Even if the code above is typed, there is no type support to guarantee that: 1. no messages other than insert and remove are sent to the buffer.
2. the insert(v) message is sent only to an EMPTY buffer and the remove() message is sent only to a FULL buffer. Therefore, since each message makes the buffer switch state, insert and remove must be alternated.
Indeed, the following user code is well-typed even if it violates the intended buffer protocol: The insert (20) message is indeed received by a buffer whose current behavior is the FULL(10) partial function, which is not defined on the insert case class. The default Akka's policy for actors that receive a message that is not handled by their current behavior is to wrap that message into an UnhandledMessage object and forward it to the actor system's event stream for logging. Therefore the reception of the unintended (logically wrong) messages insert (20) and 4 gets completely unnoticed by the user actor. By adopting a defensive programming strategy, we could enrich the Buffer class with an overriding of the unhandled(msg:Any) method inherited from the Actor class so to explicitly manage unintended messages. However, the aim of the TSOP approach is opposite: instead of protecting the buffer, it checks the user code and statically marks the sending of the wrong messages as untyped actions.

Adding typed references
The first one of the two guarantees formulated above reminds the basic type safety property of OOP: in well-typed programs all the methods invoked on objects belong to the object's interface. In the context of actors there is no method invocation, but a message is passed as a parameter to the dispatching method, that in Akka is the method def !(msg:Any):Unit of the class ActorRef. However, in this scenario there is no way to link (and check) the actor's interface (i.e. the set of allowed incoming messages) with the types of the parameters of the dispatching method.
We then resort to the following solution: first of all we use the nominal type system of Scala to represent actors interfaces, then we wrap actor references of type ActorRef into instances of the TypedRef[T] generic class which provides a typed-version of the dispatching method with signature def tyTell(msg:T):Unit 1 . In other terms, a wrapper of type TypedRef[T] encapsulates a reference to a stateful actor at state T, and provides a method that allows for the static checking of the correctness of the incoming messages. Observe that the TypedRef[-T] class is contravariant in its type parameter: indeed, let S be a sub-interface of T, then an actor of type TypedRef[S] can be safely substituted by an actor of type TypedRef[T] which is able to handle a superset of messages.
The following code applies this approach to the running example: let BufferInterf, ProduceInt and ConsumeInt be a hierarchy of empty traits corresponding to the interfaces assumed by the buffer in different states; their names remind that when in state EMPTY, resp. FULL, the buffer allows the production, resp. consumption, of an item. Accordingly, the case classes extend the suitable trait so that BufferInterf is the (super-)type of the buffer's messages. Let also buffer be a reference of type TypedRef[BufferInterf] built around the ActorRef spawned by the actor system upon creation of the Buffer actor (lines [15][16]. Then the (typed-)invocation buffer tyTell(msg) will only compile if msg is one of the two intended messages insert or remove. In the user code above we see the type checking in action to prevent unintended messages to be sent to a typed actor reference: line 21 does not compile since the invocation of the tyTell method of the TypedRef[BufferInterf] class does not accept the parameter 4 which is not of type BufferInterf. On the other hand, nothing prevents to send the wrong message 4 to the buffer actor by using its untyped reference as in line 22. This kind of errors can be avoided by designing a proper encapsulation of the type ActorRef so that actor users can only handle typed actor references.
More importantly, line 24 above shows that the second guarantee required by the buffer protocol, that is the alternation of insert and remove, eludes the type checking: two consecutive insertions are well typed even if the second one gets silently discarded because it is received by a FULL buffer. This is not surprising since the information encoded in the types just refer to the buffer interfaces, but nothing expresses the state-change (possibly) provoked by the reception of a message. Furthermore, the initial buffer reference in line 16 could be better typed as an empty buffer, i.e. TypedRef[ProduceInt], since it initially accepts only insert messages. However, with such a type, no remove message can ever be passed to the tyTell method, even after an initial insertion that would have moved the buffer to the correct FULL state. What is really missing here is the buffer reference's ability to keep track of the dynamic change of its type/state between TypedRef[ProduceInt] and TypedRef [ConsumeInt]. Notice that statically we can only approximate these changes with a common supertype, i.e. TypedRef[BufferInterf], but we have seen that it is not enough. The alternative is to take a new reference, of the suitable type, each time the state has changed. This is what we will do in the next subsection resorting to the Continuation-Passing programming style.
It is important to observe that the combination of typed actor references and continuationpassing style is exactly (part of) the solution adopted by the Akka Typed [10] experimental library available in the latest Akka release. Further major differences between our approach and that of Akka Typed will be presented in the next sections.

Tracking State Changes with Continuation-Passing Style
In order to keep track of the state changes caused by message reception, we let actors reply by sending to users a continuation reference, that is a reference to themselves typed at the new state that can be used to continue the interaction according to the rest (the continuation) of the protocol. Since in the actor model the communication is asynchronous, messages are enriched with an additional parameter replyTo referring to the actor that expects the corresponding reply message carrying the continuation.
Accordingly, in the code below the insert and remove case classes have the additional parameter replyTo of type ActorRef corresponding to the (not necessarily typed) user actor that is waiting for the continuation. Moreover, the additional case classes defined in lines 6-7 stand for the reply messages sending back to the user the (typed) continuations. More precisely, when the buffer receives an insert message it moves to the state FULL, hence its continuation, carried by the message insertReply, has type TypedRef[ConsumeInt]. Similarly, the reply to a remove request carries both the removed value and a continuation of type TypedRef[ProduceInt] standing for the buffer that moved to the state EMPTY. Compared to the previous implementation of the Buffer actor, the new definition takes care of the reply messages (lines 12 and 16). The user actor undergoes major changes: the initial buffer reference has type TypedRef[ProduceInt] (line 23) and represents an initially empty buffer. This reference is used just once by the user in line 26 to ask for the insertion of the integer 4. Subsequent references to the buffer are those bound by the parameter o of the reply messages (lines 29 and 31). Therefore, by rebinding the buffer object to new references as a result of sending a message, and by typing such new references with a type that describes the newly reached state, we can control that sequences of message invocations conform to the buffer's usage protocol, provided that each reference is used at most once.
For instance, sending in line 29 an insert message to the reference o would not compile since the compiler knows that the type of the variable o is TypedRef[ConsumeInt]. For the same reason also the expression in line 30 would not compile, even if it follows a remove request. On the other hand, two successive calls o tyTell remove(self); o tyTell remove(self) would be well typed even if they do not respect the buffer protocol, and similarly invoking tyTell insert(0,self) on the reference buffer instead of o in line 29 would not be prevented by the compiler. The point is that in order to enforce protocol compliance, it is important to ensure that a reference (to a typestate actor) is used at most once.
The behavioral type system developed in [6] statically checks the linear usage of typed object references, however this is beyond the capabilities of the standard Scala type system. Therefore, in order to enforce an affine usage of typed references, that is at most one call of the tyTell method, we could enrich the TypedRef class with an affine flag and transform an affinity violation, i.e., a logical error, into a runtime error. For the sake of completeness we show below the corresponding definition, but we do not assume it in the rest of the paper. We finally comment on the difference between this approach and that of Akka Typed actors. As we said above, this module provides both typed actor references (which are instances of the ActorRef[-T] class) and a continuation passing programming style. Type safety guarantees [5] that in well typed programs an actor of type ActorRef[T] will only receive messages of type T. However, a key assumption/constraint of Akka Typed actors is that they can dynamically change their behavior only as along as the new behavior still handles all the messages handled by the previous one. For instance, the 1-place buffer should handle both insert and remove messages in both states EMPTY and FULL. In other words, the buffer must be prepared (i.e., programmed) to receive messages that arrive when it is in the wrong state. Here we are instead claiming that it is possible to define typestate-oriented actors whose behaviors are defined only on messages that are meaningful in the corresponding state.
We will further discuss Akka Typed constraint in later sections; we conclude observing that even in the Akka Typed module there is no support to statically check whether the program violates the continuation-passing style by re-using an "out of date" reference. So, like in the code above, it is responsibility of the programmer to use at most once a typed reference that is subject to a state/type change.

Simplifying the Code with the Continuation Monad
Adopting the continuation-passing style allows stateful actors to take advantage of type checking, but it entails a more involved user code. Explicit use of reply messages carrying continuations might be useful to correctly combine the protocols of two (or more) interacting stateful actors. However, in simple cases where a stateful actor is accessed by a single user, it would be useful to simplify the user code and bring to light its logic. Indeed, looking at the user code shown in the previous subsection it is not immediate to understand that the actor is alternating insert and remove requests.
In this section we illustrate how to simplify the code accessing a stateful actor by encapsulating continuations into a monad. We start by showing the refactoring of the code of a user that alternates insert and remove requests to a 1-place buffer: This code is very similar to that in the untyped case, but it heavily builds on typed continuations, which are hidden within the monad but are still enforcing type safety. Messages insertReply and removeReply are not needed anymore, and the code adopts the for-notation offered by Scala to work with monads. The monad we define below makes use of futures so that the code above has the asynchronous and non-blocking semantics that is distinctive of actors, and the code style is reminiscent of Scala concurrent programs that use futures.
First of all, observe that by using the same variable o for each binding in lines 2-7, we reduce the risk (still not checked by the compiler) of using an out-of-date reference. Similarly, it is easier to spot whether the reference buffer is used only once in line 2. On the other hand, as we will explain below, the user code needs explicit type-enforcements, that have been encapsulated in the methods afterInsert and afterRemove. The main ideas of this approach can be summarized as follows: 1. we have already observed in Section 2.2 that it is essential for types to somehow encode information about the state changes (possibly) provoked by the reception of messages. In Section 2.3 such information is encoded by the reply messages, e.g., the definition case class insertReply(o:TypedRef[ConsumeInt]) links the insert message with the ConsumeInt interface assumed by the buffer in the next state FULL. Here we get rid of reply messages, and we rather define a usage protocol expression that directly encodes the state transitions involved by the actor protocol. More precisely, a protocol expression is a function associating the next state, i.e. the typed continuation, to each message in the actor's interface (lines 27-38 below).

Instead of TypedRef[T]
we use a richer actor wrapper ProtRef[T], which encapsulates both a reference to a stateful actor at state T and the usage protocol expression of such actor. The actor's protocol is indeed inspected in the new definition of the tyTell method, that now returns an object of type Continuation which encapsulates the next state that will be assumed by the actor upon reception of the message passed as parameter to tyTell (lines 13 and 15 below).
3. The abstract class Continuation has an abstract type member NextState and encapsulates a promise and a paired future holding a value of type ProtRef[NextState]. The pair (promise, future) allows the usual asynchronous and non-blocking semantics: the user of the actor sends a message and immediately obtains a future (as a continuation reference), that will be asynchronously completed by the actor which fulfills the corresponding promise upon handling the received message.
More precisely, when the user invokes tyTell(msg), the actor protocol is inspected and a pair (promise, future) of the suitable "next type" is created (see line 13 and the definition of the protocol expression in lines 27-38 below). Then the promise is forwarded to the actor to be completed (line 14), while the continuation is returned to the caller, that is to the user (line 15). Since the Continuation class is implemented as a monad on top of the Future[T] monad (lines 6-8), the user can deal with the returned object using the simple for-notation that is common in Scala programming with futures. The definition of the Buffer actor must then be modified so that instead of sending reply messages the message handler completes a promise. Notice also that, because of the new definition of the tyTell method, the buffer's incoming messages are pairs made of a message tag and the specific promise instance to be completed (lines 3 and 8 below). The injection of the explicit type of the promise variable p in lines 3 and 8 is needed to typecheck the promise completion in lines 5 and 10, on the other hand, a warning is produced by the compiler since the type argument of the generic class Promise gets unchecked because it is eliminated by type erasure. Anyway, the correct type parameter to inject in lines 3 and 8 can be automatically deduced from the buffer's protocol definition, i.e. the Buffer.protocol function defined in the companion object (lines 27-38 of the code above). Summary of the TSOP guarantees actually enforced by typing. The advantages of the approach we described in this section can be summarized as follows: • the buffer is truly implemented as a type-stateful object: (i) each state corresponds to an actor behavior that handles only the messages that belong to the interface assumed in that state, and (ii) state transition is achieved by changing the current behavior (by means of become) and using a typed wrapper corresponding to the interface assumed in the new state; • the user code has a clean logic and its compilation guarantees that the buffer will only receive the intended messages at the intended state. For instance, two consecutive remove requests would result in the ill-typed expression Buffer.afterRemove(o) tyTell remove() that is rejected by the compiler.
It is worth observing that the type casts provided by the methods Buffer.afterInsert and Buffer.afterRemove are inevitable because the compiler can only statically assume that the continuation returned by an invocation of the tyTell operator has an abstract type, therefore a type-coercion is needed. The definition of the tyTell method ensures that the actual type of the returned object is correct because it has been deduced from the usage protocol, hence no type-cast error will occur at runtime. Removing these casts requires implementing a specific static analysis; however our solution keeps the code clean by resorting to so-called Phantom Types 2 .
• most of the code of the given program can be automatically generated from the specification of the intended buffer protocol. In our code the protocol is made of (i) a hierarchy of empty traits that encode interfaces, (ii) a set of case classes defining the messages belonging to these interfaces, and (iii) a function expressing the state transitions entailed by message reception. Ideally, TSOP programmers could define object protocols using some other more declarative language, e.g. UML sequence diagrams, FSMs or CFSMs as in [19] or even using a specific type language as in [6], and the translation into typed code analogous to the one above could be automatically generated. We leave this subject for future developments.

A typestate-based buffer with multiple concurrent users
So far we have considered a rather simple scenarion in which a stateful actor is accessed by a single concurrent user. Ensuring that a stateful object only receives the intended messages at the intended states is much more difficult when the object is aliased or shared [4,8]. For instance, if the empty buffer is initially shared by two users and the first user fills it with a value, it causes the buffer to move to the FULL state thus disabling the insertion that could have been concurrently requested by the second user. However, if the first user later on removes the inserted value, the concurrent insertion requested by the second user could be only temporarily disabled, since the buffer eventually gets back to the EMPTY state. In other terms, in a concurrent (and asynchronous) setting, an actor must be prepared to receive messages that correctly belong to its protocol even if the actor is not in the appropriate state yet. Dealing with this scenario is indeed the main reason why the Akka Typed library allows an actor to dynamically change its behavior as long as the new behavior accepts the same set of messages as the original one. Indeed, if the buffer in the FULL state can somehow handle also the insert messages, no requests get lost. Anyway, in this way the stateful object essentially can change its behavior but it always keeps the same interface. We showed in [6] that we can instead keep the TSOP idea of different interfaces in different states even in a concurrent setting by resorting to the Chemical Semantics.
The chemical model of concurrency, due to Berry and Boudol in 1992 [3], interprets the state of an asynchronous concurrent system as a soup of molecules, corresponding to the messages that have been sent to the concurrent entities. The behavior of the system is then described by reaction rules, that specify how (patterns of) molecules/messages can be consumed so to produce new ones. This model of concurrency is the foundation of the Join Calculus [12], a formal language for which there exist a number of both native and library implementations (e.g., [18,20,21,15]). On the other hand, a similar semantic model can be established also in Scala Akka (i) by interpreting molecules as messages sent to actors, (ii) by interpreting actor behaviors as reaction rules, and (iii) by modifying the default management of the actor mailbox so to keep a received message/molecule until it triggers a reaction, i.e. until the current behavior/state of the actor is able to handle it.
A precise formal account of the connection between the actor model and the Join Calculus that allows to scale to actors the type safety properties proved in [6] is subject of current work. Here we illustrate by means of examples that Scala Akka actors can support the chemical semantics, and the Scala type system can already check typestate-oriented code to some extent.
More precisely, we define a Chemical trait that can be used to optionally provide actors with chemical semantics by means of mix-in composition. The trait is defined so that it only keeps the messages of (super)type ProtocolMsg, that will eventually be handled since they actually belong to the actor's protocol, while other messages can be immediately discarded as errors. The chemReact method extends the actor's behavior so to keep protocol messages (i.e. messages of type ProtocolMsg) arriving at the wrong time, while chemBecome is used to change the actor's state and re-check saved messages. In this definition saved messages are simply re-sent to the mailbox, we show in the next section a more realistic implementation that relies on the Akka's Stash trait [11] that allows an actor to temporarily stash away messages and prepend them to the actor's mailbox right before changing the current behavior.
As far as our running example in concerned, we can obtain a 1-place buffer that is robust with respect to multiple concurrent users by mixing-in the Chemical trait to its definition. To illustrate, we consider a buffer that can be accessed by two kinds of user actors: a Producer actor that repeatedly sends insert messages and a Consumer actor that repeatedly sends remove messages. In this scenario the buffer's usage protocol is different from the one we considered in the previous sections: while the buffer still switches between the states EMPTY and FULL, now each user is aware of a single, fixed buffer interface, i.e., the Producer relies just on the ProduceInt interface to send insert messages, while the Consumer is aware just of the ConsumeInt interface. Accordingly, in the typed encoding of the new buffer's protocol, the type of the continuation references must be adapted: after sending an insert message a Producer will get a continuation of type TypedRef[ProduceInt], while the Consumer will obtain a continuation of type TypedRef [ConsumeInt] as a result of a remove message. We show below the code corresponding to the explicit passing of continuations (cf. section 2.3), while the integration of the chemical semantics with the continuation monad is postponed to the next section. The program above spawns one producer and two consumers accessing the same 1-place buffer. Because of nondeterminism it is unreasonable to expect that the buffer receives alternated messages insert and remove. Thanks to its chemical semantics, however, it is guaranteed that the buffer handles the messages in the correct sequence. Interestingly, the definition of the new class Buffer is identical to the previous ones but for the usage of chemReact and chemBecome methods introduced by the Chemical mix-in. Therefore, we have that with a simple mix-in the clean TSOP definition mentioning only the intended messages at the intended states is actually robust in a fully concurrent context.
We finally remark that in lines 41-43 above we relied on the contravariance of the type parameter of the class TypedRef[-T]: indeed, the buffer reference, which is of type TypedRef[BufferInterf], is passed as a parameter to the Producer, resp. Consumer, constructor which instead expects a parameter of super-type TypedRef[ProduceInt], resp. TypedRef[ConsumeInt].

Chemical semantics with the Continuation monad
For the sake of completeness we rephrase the code above to show the integration of the chemical semantics with the Continuation monad. In particular, the Chemical trait is implemented by means of the Stash trait and it is modified (line 5) to keep the specific kind of messages that in this scenario will be sent to an Actor, that is pairs (m,p) where m is the actual message and p is the promise instance to be filled upon message handling.
The rest of the code is straightforward: the buffer protocol is declared in the companion object and the Buffer class mixes-in the Chemical trait and defines the actor in a typestate-oriented style. Finally, the Producer and Consumer classes define user actors by means of the for-notation.

Bookshop Server
In this section we address a more complex example, showing that our solution for typestateoriented actor programming is effective even with more complex protocols. More precisely, we consider an example coming from the literature about session types, i.e. the Bookshop Server (cf. [14]). A client accessing the server initially adds a number of items to the shopping basket, then asks for the checkout and sends information about the credit card and the shipping. The bookshop protocol is defined by the recursive session type Shop = &<add:?Book.Shop, checkout:?Card.?Address.end>, which essentially corresponds to the TSOP protocol defined by the following FSM: In order to define this protocol in terms of Scala types, we first choose the names of the five possible states and the corresponding interfaces (lines 2-6 and 8-12). State transitions are then encoded in the Shop companion object (lines 15-41). Since the bookshop can be accessed by multiple concurrent users, we need to decide a serving policy. Initially we let the bookshop completely serve one user at a time, and we rely on the chemical semantics to keep initial requests that may concurrently arrive from a user while serving another one. Therefore, we tag with type ProtocolMsg only the initial message add (line 8). We will later discuss other choices that allow a greater degree of concurrency. 1   Notice that the Shop actor is defined as a stateful object with four different behaviors, each one handling only the messages expected to be received in the corresponding state. The additional state END appearing in the public protocol is only used by the users: indeed, at the end of the interaction, the users receive a continuation of type ProtRef[EndInterf] (line 82) that ensures that no further message can be sent to the Shop actor since EndInterf corresponds to the shop's empty interface.
Every shop's behavior calls the chemReact method to keep add messages that might arrive at any moment from a user different form the one that is currently served. On the other hand, the chemBecome method is called only in line 83 at the end of the interaction with the current user. Indeed, while context.become simply changes the actor's state/behavior, the chemBecome method also re-sends the saved add messages so that they can be eventually handled.
In order to increase the throughput of the server, we can let the bookshop interleave the shopping phases and the checkout phases of different users. More precisely, each time the shop gets back to state INIT, it can start serving the shopping or the checkout of another actor. To change the policy in this way it is sufficient to (i) collect in the chemical soup both the add and checkout messages, that is to tag with type ProtcolMsg the entire InitInterf interface (line 2), and (ii) allows a recheck of the saved messages each time the shop enters the INIT state, which means using chemBecome instead of context.become in line 67.
We conclude by showing the code of a program that spawns a bookshop and three users that buy a couple of books each: Notice that in this code any attempt at sending an address message just after the message checkout without sending the credit card number, results in a type safety error. Indeed, the reference Shop.afterCo(o) in line 8 has type ProtRef[CInfoInterf], hence it only accepts card messages. On the other hand, this typing can only prevent wrong message sends but cannot guarantee that intended messages will be actually sent. For instance, a user which starts the interaction with the bookshop but never sends the final address message would satisfy the compiler even if it would leave the shop in an intermediate state. The full behavioral typing we studied in [6] captures these issues byt it requires linear types, which are not available in the standard Scala compiler.

Conclusions
The aim of the TSOP approach is opposite to that of defensive programming: instead of adding code to the stateful object to protect it from wrong accesses, it checks the user code and statically marks the wrong accesses as untyped actions. We illustrated by means of examples that Scala Akka effectively supports typestate-oriented actor programming. An actor can be defined as a stateful object by letting states correspond to actor behaviors that possibly handle different sets of messages. Then, a dynamic change of behavior corresponds to a change of actor's interface. Moreover, by fully encoding stateful protocols into typed expressions, we can let the Scala compiler check that the actor will only handle intended messages at the intended times. Nevertheless, a fair amount of defensive programming is still needed since static detection of violations of protocol obligations (e.g., ensuring that an intended message is eventually sent) requires the verification of linear properties that are currenlty beyond the expressive power of the Scala type system. Moreover, the integration of TSOP with the fault tolerance properties required in distributed actor systems is still an open research issue.
We conclude observing that even if TSOP enables the coordination of concurrent entities, it certainly does not solve the general problem. Indeed a protocol-oriented programming paradigm requires more than a single conceptual model and suitable abstractions and programming patterns can only emerge as a productive integration of different techniques, both at the high level (i.e, techniques to express and verify coordination properties) and at the lower level (i.e., language abstractions, performace and scalability issues).