package sessions

This module provides modules to create binary sessions types for statically verifying protocols between a pair of concurrent processes.

Binary processes which are parametrized by binary session types can be created using Binary_process. A pair of processes can only be run if they have compatible (dual) session types.

• author essdotteedot [<essdotteedot[at]gmail[dot]com>]

• version 0.1.0

A session type ('a,'b) session represents a protocol that a particular process carries out. Here 'a and 'b are duals of each other.

A process ('a,'b,'c) process is parameterized by a starting session type 'b, 'a is it's return value and 'c is it's final session type. Two processes can be run only if they have dual initial session types a final session type of unit.

The following operations are duals of each other :

• [`Stop], [`Stop]
• [`Send of 'a * 'b], [`Recv of 'a * 'b], where 'b is a session type
• [`Offer of ('a, 'b) session * ('c, 'd) session ], [ `Choice of ('b, 'a) session * ('d, 'c) session ], where 'a, 'b, 'c, 'd are session types

Here are some examples of processes which are duals (assume we have an implementation of IO called ExIO) :

module BP = Binary_session.Make (ExIO)            
let send_str_recv_int_stop = BP.(send "hello" >>= fun () -> recv () >>= fun (i : int) -> stop ())      
let recv_str_send_int_stop = BP.(recv () >>= fun (s : string) -> send 1 >>= fun () -> stop ())        
let _ = BP.run_processes send_str_recv_int_stop recv_str_send_int_stop

Note that the session type associated with the process send_str_recv_int_stop was inferred as

([ `Send of string * [ `Recv of int * [ `Stop ] ] ],[ `Recv of string * [ `Send of int * [ `Stop ] ] ]) BP.session

as you can see it provides it's own session type [ `Send of string * [ `Recv of int * [ `Stop ] ] ] as well as it's dual [ `Recv of string * [ `Send of int * [ `Stop ] ] ].

The session type associated with the process recv_str_send_int_stop is ([ `Recv of string * [ `Send of int * [ `Stop ] ] ], [ `Send of string * [ `Recv of int * [ `Stop ] ] ]) BP.session

we see that it indeed has the dual of send_str_recv_int_stop which means that BP.run_processes send_str_recv_int_stop recv_str_send_int_stop can type check.

If these two processes were to differ in such a way that they were not duals then BP.run_processes send_str_recv_int_stop recv_str_send_int_stop would not type check.

Here is another example using `Offer and `Choice as well as recursion.

module BP = Binary_session.Make (ExIO)
let rec print_server () = BP.(
    offer 
        (stop ())
         (recv () >>= fun (s : string) ->
          lift_io (Lwt_io.printlf "print server : %s" s) >>=
          print_server)
)  
let rec print_client (i : int) = BP.(
    lift_io (Lwt_io.read_line Lwt_io.stdin) >>= fun (s : string) ->
    if s = "q"
    then choose_right (send (Printf.sprintf "Total lines printed : %d" (i+1)) >>= fun () -> choose_left (stop ()))
    else choose_right (send s >>= fun () -> print_client (i+1))
) 
let _ = BP.run_processes print_server (print_client 0)