package sessions

  1. Overview
  2. Docs
Library to provide session types to allow for static verification of protocols between concurrent computations

Install 

dune-project
 Dependency

github.com Edit opam file Versions (1)

Authors

  1. E
    essdotteedot <essdotteedot@gmail.com>

Maintainers

  1. E
    essdotteedot <essdotteedot@gmail.com>

Sources

0.1.0.tar.gz
sha256=7b9693aa4e8571fc7dadeeb971a24e523ad411a6cfd6d2e087aae05cfd3882cc
md5=c2d5f085a0aa0f6b5cf7cac2568560fb

doc/sessions.lwt/Binary_session_lwt/Make/index.html

Module Binary_session_lwt.Make

Functor to create a module of type Binary_session.Binary_process.

type 'a io = 'a Lwt.t

The abstract monadic type representing a computation returning 'a.

The abstract type representing one end of a communication channel.

type ('a, 'b) session constraint 'a = [> ] constraint 'b = [> ]

The type representing a communication protocol made up of a sequence of operations between two processes. The type 'a is the sequence of operations from the point of view from the first process and 'b its dual is the sequence of operations from the point of view of the second process.

type ('a, 'b, 'c) process

The type representing a process returning a value of type 'a. The type 'b represents the next allowed sequnce of operations and 'c represents the sequence of operations after performing the first operation in 'b.

val send : 'a -> (unit, ([ `Send of 'a * 'b ], [ `Recv of 'a * 'c ]) session, ('b, 'c) session) process

send v creates a process which is capable of sending a value of type 'a (v) to the other process.

val recv : unit -> ('a, ([ `Recv of 'a * 'b ], [ `Send of 'a * 'c ]) session, ('b, 'c) session) process

recv () creates a process which is capable of receiving a value of type 'a to the other process.

val offer : ('e, ('a, 'b) session, 'f) process -> ('e, ('c, 'd) session, 'f) process -> ('e, ([ `Offer of ('a, 'b) session * ('c, 'd) session ], [ `Choice of ('b, 'a) session * ('d, 'c) session ]) session, 'f) process

offer left_choice right_choice creates a process which allows the other process to make a choice between two choices left_choice and right_choice.

val choose_left : ('e, ('a, 'b) session, 'f) process -> ('e, ([ `Choice of ('a, 'b) session * ('c, 'd) session ], [ `Offer of ('b, 'a) session * ('d, 'c) session ]) session, 'f) process

choose_left left_choice creates a process which internally chooses left_choice and communicates this choice to the other process.

val choose_right : ('e, ('c, 'd) session, 'f) process -> ('e, ([ `Choice of ('a, 'b) session * ('c, 'd) session ], [ `Offer of ('b, 'a) session * ('d, 'c) session ]) session, 'f) process

choose_right right_choice creates a process which internally chooses rigth_choice and communicates this choice to the other process.

val stop : 'a -> ('a, ([ `Stop ], [ `Stop ]) session, unit) process

stop v creates a process which stops (is not capable of performing any further operations) and returns a value v.

val lift_io : 'a io -> ('a, 'b, 'b) process

lift_io io lifts the io computation into the process. The processes' capabilities are not altered.

val return : 'a -> ('a, 'b, 'b) process

return v creates a process which returns v its capabilities are not altered.

val (>>=) : ('a, 'b, 'c) process -> ('a -> ('d, 'c, 'e) process) -> ('d, 'b, 'e) process

p1 >>= f creates a process which is the composition of running p1 then applying.

val run_processes : ('a, ('b, 'c) session, unit) process -> ('d, ('c, 'b) session, unit) process -> ((unit -> 'a io) * (unit -> 'd io)) io

run_process p1 p2 will run two processes p1 and p2 which have dual session types and which have unit as their end state capabilities (i.e., are complete processes). The result is a Binary_session.IO.t returning a pair of functions which may be invoked to run each process.

Note, the channel that is opened between the two processes is closed when the processes have completed.