A sketchy overview of Session Types

In the last decades a great deal of effort in the type systems community has been devoted to investigate the so called session types.
In such an approach to typing for concurrent systems, any sort of value can be exchanged through a channel. The type of a channel is used to discipline the precise order in which values are exchanged. In a sense, a session type can be looked at as a partial specification of an interaction protocol among processes along a particular channel.

For instance, if a client process is connected by means of a channel k to a server process that performs sums, the type of the channel k will be

![int].![int].?(int).end

meaning that k is a channel through which an integer is sent, then another integer is sent and then an integer (the result produced by the server) is expected.
Of course this is the description of the client-server interaction seen from the point of view of the client.
The type of the very same channel, looked at from the server point of view is instead

 
?(int) ?(int) ![int].end

In order to have the possibility of describing complex protocols, the syntax of session types is enriched with branching and selection.
The type &{sum: ?(int).?(int).![int].end, fact : ?(int).![int].end} is the type of the channel (from the server point of view) through which it is possible to ask a computing server, by selecting the appropriate label, to have a sum or a factorial computed.
In general a type &{...} expresses the fact that someone, at the other end of the channel, can send a label in order to select the appropriate continuation of the interaction.

Here is the syntax of session types:

S::=   end 
     | ?(G).S 
     | ![G].S 
     | &{ l1 : S1,...,ln : Sn }
     | ⊕{ l1 : S1,..., ln : Sn }

Whereas a type &{...} denotes a choice that is influenced by a message we receive from the other end of the channel, the type ⊕{...} denotes a choice that depends entirely on ourselves.
G denotes a ground type, like Int, Bool ...

Example: (by Dezani, de'Liguoro)

To illustrate these concepts and their formal representation, let us consider the following protocol, which describes a simplified interaction between a customer (Client) and an ATM, Automated Teller Machine (Server):

• First the User communicates her/his identifier to the ATM.
  The ATM answers with either success or failure.
• In the first case the User can ask either for doing a deposit or a withdraw.
  • For a deposit the User communicates an amount, and waits for a balance.
  • For a withdraw first the User communicates an amount and then the ATM answers with either dispense or overdraft.
• If the answer is failure, then the interaction terminates.

Here is the server's point of view of the protocol:

   ?(String). ⊕{success : &{deposit : ?(Real). ![Real]. end,

                             withdraw : ? Real. ⊕{dispense : end,

                                                  overdraft : end
                                                   }
                             }               
                failure : end
                }

The client's point of view can be obtained by simply replacing '!' by '?' and vice versa, and by replacing '&' by '⊕' and vice versa:

 
  ![String]. &{success : ⊕{deposit : ![Real]. ?(Real). end,

                            withdraw : ! Real. &{dispense : end,

                                                 overdraft : end
                                                 }
                             }               
               failure : end
               }

     Of course if we intended to introduce channels with session types in PICT, we should extend the language PICT with suitable operations (let us call S-PICT such a possible extension of PICT):

• A (blocking) action of label selection along a session channel

       k << l : P
  

  meaning that the process sends the label l along the session channel k and then continues as P;


• A label reception action enabling the process at the other end of the channel to send a label and hence perform a selection

       k >> {l1:P1,..,ln:Pn}
  

  meaning that the process is waiting for a label through k and then continues as P₁ or .. or P_n according to the label received.

Notice that, differently from PICT (and π-calculus), a session channel can be used only by two processes, so it can never happen, if k is a session channel, something like

        k!v.Q | k!w.R | k?y=P                    (*)

(we consider here, for simplicity, a syncronous version of π-calculus and PICT)

Communications belonging to a session are opened through a public name (a port) and pursued through a private channel, specific to the session, which is created at connection time.

The definition of a port in S-PICT could be

  port a : session S

where S is a session type describing the protocol used in the session from the point of view of the server.

The the request of opening a session, in S-PICT, could be

  request a (k).P

By running such process we request a session on the port a to be opened with anyone willing to do so. The (bound) name k is used to refer to the channel name through which the session will be carried on in P. The request action is blocking.

To accept a session-opening request a process of S-PICT could use

  accept a (k).P

The operational semantics of the request and accept actions is the following one:
in case we have

     request a (k).P | accept a (k).Q

this subprocess reduces (evolves) to

   new k : S

       P | Q

The operational semantics of label exchanging, instead, is the following:
in case we have

         k << lh:P  |  k >> {l1:P1,..,ln:Pn}

this reduces to

         P | Ph

Example (continued):
Let S be the session type of the ATM example. Now, if we had

   port a : session S

the process describing a possible client of the ATM could be

   request a (k). 
   
         k!identifier.

         k >> {success : if · · · 
                         
                             then k << deposit:  k ! amount. k ? x =0

                                          
                             else k << withdraw: k ! amount.

                                                 k >> {dispense: · · 
                                                                  
                                                       overdraft: · ·
                                                       }
               failure : 0
               }

whereas the process ATM could be

  def
  accept a (h). 

     h ? x =  
            
        if · · · 

          then h << success : h >> {deposit : h ? y = · · · h ! balance. 0
           
                                    withdraw : h ? z =
                                                        
                                                   if · · · 

                                                      then h << dispense: · · 
                                                                      
                                                      else h << overdraft: · · 
                                    }

         else h << failure : 0

where def means we are considering a replication version of the ATM process, since it can serve many clients, each with a private session channel.

Now, if the ATM process and the client process are well typed in S-PICT, we are guaranteed that the exchanges through the session channel will always follow the protocol described by the session type associated with the port a.

In general, a type system for processes with session types guarantees that

• values are exchanged through a channel according to the protocol described by the (session) type of the channel;
• situations like the one (*) described above can never occur.

Particular versions of session types can be used to describe also multiparty interactions.

There exist many experimental extensions with session types of actual programmaing languages. For instance Haskell, Scala, Java (SessionJ) and others. Extensions with session types are currently investigated also for Erlang.

In our course we shall introduce Scribble, a language (based on session types) for the description of application-level protocols among communicating systems.