Session type implementation using Janestreet Async

.depend

session.cmi :
example.cmo : session.cmi
example.cmx : session.cmx
session.cmo : session.cmi
session.cmx : session.cmi

.gitignore

*.cm[ioxat]
*.cmxa
*.cmti
*.o
*.annot
test.*

README.md

Session type implementation with Janestreet Async. https://github.com/janestreet/async/

example.ml

include Session;;

let p () = 
  send _0 1234 >>
  recv _0 >>= fun str ->
  print_endline str;
  close _0 >>
  ret ()
      
      (*
val p :
    unit ->
      ((('a, 'b, ('a, int, ('b, string, finish) shot) shot) chan, 'c) cons,
          (empty, 'c) cons, unit)
          monad = <fun>
       *)
(*
val p :
  unit ->
  (((int, (string, 'a) recv) send, 'b) cons, ('a, 'b) cons, unit) monad
*)

let q () =
  recv _0 >>= fun i ->
  send _0 (string_of_int (i*2)) >>
  close _0 >>
  ret ()
(*
val q :
    unit ->
      ((('a, 'b, ('b, int, ('a, string, finish) shot) shot) chan, 'c) cons,
          (empty, 'c) cons, unit)
          monad
*)

let r () = 
  fork _0 (q ()) >>
  p ()
(*
val r :
    unit ->
      ((empty, (empty, 'a) cons) cons, (empty, (empty, 'a) cons) cons, unit)
          monad
*)

(* output:

2468

 *)

            
let p2 () = 
  send _0 7777 >>
  recv_slot _0 _1 >>
  recv _1 >>= fun str ->
  print_endline str;
  close _0 >>
  close _1

let q2 () =
  recv _0 >>= fun v ->
  send_new_chan _0 _1 >>
  send _1 (string_of_int (v - 1111)) >>
  close _0 >>
  close _1

let r2 () =
  fork _0 (q2 ()) >>
  p2 ()

(* output:

6666

 *)

let rec p3 n =
    if n>10 then 
      select_right _0 >> close _0
    else
      select_left _0 >>
        send _0 n >>
        recv _0 >>= fun str ->
        print_endline str;
        p3 (n+1)

let rec q3 () = 
  branch _0
    (_0,fun _ ->
        recv _0 >>= fun x ->
        send _0 (string_of_int x) >>
        q3 ())
    (_0,fun _ ->
        close _0)

let r3 () =
  fork _0 (q3 ()) >>
  p3 1

(* output:

1
2
3
4
5
6
7
8
9
10

 *)

let r4 () =
  run_routine
    _0
    Routine.(send "Hello, " >> recv >>= fun x -> print_endline x; close) >>
  recv _0 >>= fun x ->
  send _0 (x ^ "World!") >>
  close _0

(* output:

Hello, World!

 *)        

let r5 () =
  let proc =
    recv _0 >>= fun i ->
    Printf.printf "My no. is %d.\n" i;
    flush_all();
    close _0
  in
  let rec duplicate = function
    | 0 -> ret ()
    | n ->
       fork _1 proc >>
       LinList.put _0 _1 >>
       duplicate (n-1)
  in
  let rec send_repeat cnt =
    LinList.take
      (_0, _1, fun _ ->
               send _1 cnt >>
               close _1 >>
               send_repeat (cnt+1))
      (_0, fun _ ->
           ret ())
  in
  LinList.nil _0 >>
  duplicate 10 >>
  send_repeat 0
  

let _ = run (r () >> r2 () >> r3 () >> r4 () >> r5 ())

let _ = Async.Std.Scheduler.go()

Makefile

OCAMLC=ocamlfind ocamlc -g -rectypes -thread -package async
OCAMLOPT=ocamlfind ocamlopt -g -rectypes -thread -package async
OCAMLMKTOP=ocamlfind ocamlmktop -g -rectypes -thread -package async
OCAMLDEP=ocamlfind ocamldep
INCLUDES=                 # all relevant -I options here
OCAMLFLAGS=$(INCLUDES)    # add other options for ocamlc here
OCAMLOPTFLAGS=$(INCLUDES) # add other options for ocamlopt here

CMI=session.cmi
BYTE_OBJS=session.cmo example.cmo
NATIVE_OBJS=$(BYTE_OBJS:%.cmo=%.cmx)

all: test.byte

test.native: $(NATIVE_OBJS) $(CMI)
	$(OCAMLOPT) -linkpkg -o test.native $(OCAMLFLAGS) $(NATIVE_OBJS)

test.byte: $(BYTE_OBJS) $(CMI)
	$(OCAMLC) -linkpkg -o test.byte $(OCAMLFLAGS) $(BYTE_OBJS)

test.top: $(BYTE_OBJS) $(CMI)
	$(OCAMLMKTOP) -linkpkg -o test.top $(OCAMLFLAGS) $(BYTE_OBJS)


# Common rules
.SUFFIXES: .ml .mli .cmo .cmi .cmx

.ml.cmo:
	$(OCAMLC) $(OCAMLFLAGS) -c $<

.mli.cmi:
	$(OCAMLC) $(OCAMLFLAGS) -c $<

.ml.cmx:
	$(OCAMLOPT) $(OCAMLOPTFLAGS) -c $<

# Clean up
clean:
	rm -f test.byte test.native
	rm -f *.cm[ioaxt] *.cmax *.cmti *.o *.annot

# Dependencies
depend:
	$(OCAMLDEP) $(INCLUDES) *.mli *.ml > .depend

include .depend

session.ml

module Ivar = Async_core.Raw_ivar
module Scheduler = Async.Std.Scheduler                

type ('a,'b,'p,'q) idx = ('p -> 'a) * ('p -> 'b -> 'q)
type ('hd, 'tl) cons = 'hd * 'tl
type empty = Empty
type all_empty = empty * all_empty

let _0 = (fun (a0,_) -> a0), (fun (_,a) b0 -> (b0,a))
let _1 = (fun (_,(a1,_)) -> a1), (fun (a0,(_,a)) b1 -> (a0,(b1,a)))
let _2 = (fun (_,(_,(a2,_))) -> a2), (fun (a0,(a1,(_,a))) b2 -> (a0,(a1,(b2,a))))
let _3 = (fun (_,(_,(_,(a3,_)))) -> a3), (fun (a0,(a1,(a2,(_,a)))) b3 -> (a0,(a1,(a2,(b3,a)))))
let succ (get,set) = (fun (_,a) -> get a), (fun (a0,a) bn -> (a0,set a bn))

type ('p,'q,'a) monad = 'p -> ('q * 'a) Ivar.t
let ret a p = Ivar.create_full (p, a)
let (>>=) m f p =
  let ret = Ivar.create () in
  Ivar.upon (m p) (fun (q, x) -> Ivar.connect ~bind_rhs:(f x q) ~bind_result:ret);
  ret
let (>>) m n = m >>= (fun _ -> n)
let slide m (p0,p) =
  let ret = Ivar.create () in
  Ivar.upon (m p) (fun (q, x) -> Ivar.fill ret ((p0,q),x));
  ret


let rec all_empty = Empty, all_empty
let run m =
  Async.Std.Deferred.create
    (fun iv -> Ivar.upon (m all_empty) (fun (_, x) -> Async.Std.Ivar.fill iv x))

type pos = Pos and neg = Neg

type ('s,'v,'k) shot = Shot of 's * 'v * 'k Ivar.t
type ('s,'c,'k) pass = Pass of 's * 'c * 'k Ivar.t
type ('s,'k1,'k2) branch = BranchLeft of 's * 'k1 Ivar.t | BranchRight of 's * 'k2 Ivar.t
type finish = unit
type ('s,'t,'v,'w,'k) yield = ('s,'v,('t,'w,'k)shot)shot

type ('s,'t,'k) channel = Chan of 's * 't * 'k Ivar.t

let send (get,set) v p =
  let Chan(s,t,c) = get p in
  let c' = Ivar.create () in
  Ivar.fill c (Shot(s,v,c'));
  Ivar.create_full (set p (Chan(s,t,c')), ())
                                   
let recv (get,set) p =
  let Chan(s,t,c) = get p in
  let ret = Ivar.create () in
  Ivar.upon c (fun (Shot(_, v, c')) -> Ivar.fill ret (set p (Chan(s,t,c')), v));
  ret

let close (get,set) p =
  Ivar.create_full (set p Empty, ())

let send_slot (get0,set0) (get1,set1) p =
  let e, q = get1 p, set1 p Empty in
  let Chan(s,t,c) = get0 q in
  let c' = Ivar.create () in
  Ivar.fill c (Pass(s,e,c'));
  Ivar.create_full (set0 q (Chan(s,t,c')), ())

let send_chan = send_slot
                 
let recv_slot (get0,set0) (get1,set1) p =
  let Chan(s,t,c) = get0 p in
  let ret = Ivar.create () in
  Ivar.upon c (fun (Pass(_,e,c')) -> Ivar.fill ret (set1 (set0 p (Chan(s,t,c'))) e, ()));
  ret

let recv_chan = recv_slot

let send_new_chan (get0,set0) (get1,set1) p =
  let Chan(s,t,c) = get0 p in
  let c' = Ivar.create () in
  let cc = Ivar.create () in
  let e = Pass(s,Chan(t,s,cc),c') in
  Ivar.fill c e;
  Ivar.create_full (set1 (set0 p (Chan(s,t,c'))) (Chan(s,t,cc)), ())

let select_left (get,set) p =
  let Chan(s,t,c) = get p in
  let c' = Ivar.create () in
  Ivar.fill c (BranchLeft(s,c'));
  Ivar.create_full (set p (Chan(s,t,c')), ())
                       
let select_right (get,set) p =
  let Chan(s,t,c) = get p in
  let c' = Ivar.create () in
  Ivar.fill c (BranchRight(s,c'));
  Ivar.create_full (set p (Chan(s,t,c')), ())

let branch (get0,set0) ((get1,set1),f1) ((get2,set2),f2) p =
  let Chan(s,t,c), q = get0 p, set0 p Empty in
  let ret = Ivar.create () in
  Ivar.upon c
            (function
              | BranchLeft(_,c') ->
                 Ivar.connect ~bind_rhs:(f1 () (set1 q (Chan(s,t,c')))) ~bind_result:ret
              | BranchRight(_,c') ->
                 Ivar.connect ~bind_rhs:(f2 () (set2 q (Chan(s,t,c')))) ~bind_result:ret
            );
  ret


let fork (get,set) m p =
  let ivar = Ivar.create () in
  Scheduler.within (fun _ -> ignore (m (Chan(Neg,Pos,ivar),all_empty)));
  Ivar.create_full (set p (Chan(Pos,Neg,ivar)), ())

module LinList = struct                   
  let nil (_,set) p = Ivar.create_full (set p [], ())
  let put (get0,set0) (get1,set1) p =
    let q = set1 p Empty in
    Ivar.create_full (set0 q (get1 p::get0 q), ())
  let take ((get0,set0),(get1,set1),f0) ((_,set2),f2) p =
    match get0 p with
    | x::xs ->
       let ret = Ivar.create () in
       Ivar.upon (f0 () (set1 (set0 p xs) x)) (Ivar.fill ret);
       ret
    | [] -> f2 () (set2 p Empty)
end

module Routine = struct
  let send v (Chan(s,t,c)) =
    let c' = Ivar.create () in
    Ivar.fill c (Shot(s,v,c'));
    Ivar.create_full (Chan(s,t,c'),())
  
  let recv (Chan(s,t,c)) =
    let ret = Ivar.create () in
    Ivar.upon c (fun (Shot(_,v,c')) -> Ivar.fill ret (Chan(s,t,c'),v));
    ret
  
  let close (Chan(_,_,_)) =
    Ivar.create_full (Empty, ())

  let yield v = send v >> recv
end

let run_routine (get,set) m p =
  let c = Ivar.create () in
  m (Chan(Neg,Pos,c));
  Ivar.create_full (set p (Chan(Pos,Neg,c)), ())
                 

session.mli

type ('an,'bn,'a,'b) idx
type (+'hd, +'tl) cons

type empty
type all_empty = (empty, 'a) cons as 'a

val _0 : ('a0, 'b0, ('a0,'a) cons, ('b0,'a) cons) idx
val _1 : ('a1, 'b1, ('a0,('a1,'a) cons) cons, ('a0,('b1,'a) cons) cons) idx
val _2 : ('a2, 'b2, ('a0,('a1,('a2,'a) cons) cons) cons, ('a0,('a1,('b2,'a) cons) cons) cons) idx
val _3 : ('a3, 'b3, ('a0,('a1,('a2,('a3,'a) cons) cons) cons) cons, ('a0,('a1,('a2,('b3,'a) cons) cons) cons) cons) idx
val succ : ('an, 'bn, 'a, 'b) idx -> ('an, 'bn, ('a0,'a) cons, ('a0,'b) cons) idx

type ('p,'q,'a) monad
val ret : 'a -> ('p, 'p, 'a) monad
val (>>=) : ('p,'q,'a) monad -> ('a -> ('q,'r,'b) monad) -> ('p,'r,'b) monad
val (>>) : ('p,'q,'a) monad -> ('q,'r,'b) monad -> ('p,'r,'b) monad
val slide : ('p,'q,'a) monad -> (('p0,'p)cons,('p0,'q)cons,'a) monad

val run : (all_empty,all_empty,'a) monad -> 'a Async.Std.Deferred.t

type ('s, 'v, 'k) shot
type ('s, 'c, 'k) pass
type ('s, 'k1, 'k2) branch
type finish
type ('s,'t,'v,'w,'k) yield = ('s,'v,('t,'w,'k)shot)shot
       
type pos and neg

type ('s, 't, 'k) channel
                  
val send : (('s,'t,('s,'a,'k)shot)channel , ('s,'t,'k) channel, 'p, 'q) idx -> 'a -> ('p,'q,unit) monad
val recv : (('s,'t,('t,'a,'k)shot)channel, ('s,'t,'k) channel, 'p, 'q) idx -> ('p,'q,'a) monad
val close : (('s,'t,finish)channel, empty, 'p, 'q) idx -> ('p, 'q, unit) monad

val send_slot : 
  (('s,'t,('s,'c,'k) pass) channel, ('s,'t,'k) channel, 'q, 'r) idx -> 
  ('c, empty, 'p, 'q) idx ->
  ('p,'r,unit) monad

val recv_slot :
  (('s,'t,('t,'c,'k) pass) channel, ('s,'t,'k) channel, 'p, 'q) idx -> 
  (empty, 'c, 'q, 'r) idx ->
  ('p,'r,unit) monad

val send_chan : 
  (('s,'t,('s,('ss,'tt,'kk)channel,'k) pass) channel, ('s,'t,'k) channel, 'q, 'r) idx -> 
  (('ss,'tt,'kk)channel, empty, 'p, 'q) idx ->
  ('p,'r,unit) monad

val recv_chan :
  (('s,'t,('t,('ss,'tt,'kk)channel,'k) pass) channel, ('s,'t,'k) channel, 'p, 'q) idx -> 
  (empty, ('ss,'tt,'kk)channel, 'q, 'r) idx ->
  ('p,'r,unit) monad

val send_new_chan : 
  (('s,'t,('s,('t,'s,'kk)channel,'k) pass) channel, ('s,'t,'k) channel, 'p, 'q) idx -> 
  (empty,('s,'t,'kk)channel, 'q, 'r) idx ->
  ('p,'r,unit) monad
               
val select_left :
  (('s,'t,('s,'k1,'k2)branch)channel, ('s,'t,'k1)channel, 'p, 'q) idx ->
  ('p,'q,unit) monad
val select_right :
  (('s,'t,('s,'k1,'k2)branch)channel, ('s,'t,'k2)channel, 'p, 'q) idx ->
  ('p,'q,unit) monad
val branch : 
  (('s,'t,('t,'k1,'k2)branch)channel, empty, 'p, 'q) idx ->
  (empty,('s,'t,'k1)channel, 'q,'q1) idx * (unit -> ('q1,'r,'a) monad) ->
  (empty,('s,'t,'k2)channel, 'q,'q2) idx * (unit -> ('q2,'r,'a) monad) ->
  ('p,'r,'a) monad

val fork : 
  (empty, (pos,neg,'k)channel, 'p, 'q) idx -> 
  (((neg,pos,'k)channel, all_empty) cons, all_empty, unit) monad -> 
  ('p,'q,unit) monad

module LinList : sig
  val nil : (empty,'a list,'p,'q) idx -> ('p,'q,unit) monad
  val put : ('a list,'a list,'q,'r) idx -> ('a,empty,'p,'q) idx -> ('p,'r,unit)monad
  val take : ('a list,'a list,'p,'p) idx * (empty,'a,'p,'q1) idx * (unit -> ('q1,'r,'b) monad) ->
             ('a list,empty,'p,'q2) idx * (unit -> ('q2,'r,'b) monad) ->
             ('p,'r,'b) monad
  (*val map : ('a list,'b list,'p,'q) idx -> ('c -> (('a,all_empty)cons,('b,all_empty)cons,'c)monad) -> 'c -> ('p,'q,'c) monad*)
end
               
module Routine : sig
  val send : 'v -> (('s,'t,('s,'v,'k)shot)channel, ('s,'t,'k) channel, unit) monad
  val recv : (('s,'t,('t,'v,'k)shot)channel, ('s,'t,'k) channel, 'v) monad
  val close : (('s,'t,finish)channel, empty, unit) monad
  val yield : 'v -> (('s,'t,('s,'t,'v,'w,'k)yield)channel, ('s,'t,'k)channel, 'w) monad
end

val run_routine :
  (empty, (pos,neg,'k)channel, 'p, 'q) idx ->
  ((neg,pos,'k)channel, empty, unit) monad ->
  ('p,'q,unit) monad

varunion_session.ml

(* compile with OCaml 3.10.0+varunion *)

module type SESSION = sig
  (* slots *)                     
  type (+'hd, +'tl) cons

  (* empty slot(s) *)
  type empty
  type all_empty = (empty, 'a) cons as 'a

  
  (*
   * index to specify usage-tracked `slots'.
   * the type is to read
   *   "in the slot a, replace the n-th content of type an with that of type bn.
   *    the resulting slot is b."
   *)
  type ('an,'bn,'a,'b) idx
  
                       
  val _0 : ('a0, 'b0, ('a0,'a) cons, ('b0,'a) cons) idx
  val _1 : ('a1, 'b1, ('a0,('a1,'a) cons) cons, ('a0,('b1,'a) cons) cons) idx
  val _2 : ('a2, 'b2, ('a0,('a1,('a2,'a) cons) cons) cons, ('a0,('a1,('b2,'a) cons) cons) cons) idx
  val _3 : ('a3, 'b3, ('a0,('a1,('a2,('a3,'a) cons) cons) cons) cons, ('a0,('a1,('a2,('b3,'a) cons) cons) cons) cons) idx
  val succ : ('an, 'bn, 'a, 'b) idx -> ('an, 'bn, ('a0,'a) cons, ('a0,'b) cons) idx
  
  (* variable-type-state monad *)
  type ('p,'q,'a) monad
  val ret : 'a -> ('p, 'p, 'a) monad
  val (>>=) : ('p,'q,'a) monad -> ('a -> ('q,'r,'b) monad) -> ('p,'r,'b) monad
  val (>>) : ('p,'q,'a) monad -> ('q,'r,'b) monad -> ('p,'r,'b) monad

  (* these tags are used to express 'polarity' (indicating an endpoint of a channel) *)
  type pos and neg

  (*
   * the type of channels, which are embedded in slots and not escaped outside the monad.
   * pair of 's and 't shows polarity ('s != 't).
   * every channels have type of either:
   *     (pos, neg, 'k) channel (i.e. 'positive'-side)
   *  or
   *     (neg, pos, 'k) channel (i.e. 'negative'-side)
   *)
  type ('s, 't, 'k) channel
  type 'k cont
          
  (*
   * a session type associated to a channel is represented in a symmetric manner.
   * the type of sending an integer twice has either:
   * <for positive side>
   *   (pos, neg, [`Shot of pos * int * 'k cont]) channel
   * or
   * <for negative side>
   *   (neg, pos, [`Shot of neg * int * 'k cont]) channel
   *
   * symmetrically, channel receiving of an int has the type of either
   *   (pos, neg, [`Shot of neg * int * 'k cont]) channel
   * or
   *   (neg, pos, [`Shot of pos * int * 'k cont]) channel
   *)
                    
  val send : (('s,'t,[>`Shot of 's * 'a * 'k cont])channel , ('s,'t,'k) channel, 'p, 'q) idx -> 'a -> ('p,'q,unit) monad
  val recv : (('s,'t,[`Shot of 't * 'a * 'k cont])channel, ('s,'t,'k) channel, 'p, 'q) idx -> ('p,'q,'a) monad
  val close : (('s,'t,[>`Finish])channel, empty, 'p, 'q) idx -> ('p, 'q, unit) monad
  
  val send_slot : 
    (('s,'t,[>`Pass of 's * 'c * 'k cont]) channel, ('s,'t,'k) channel, 'q, 'r) idx -> 
    ('c, empty, 'p, 'q) idx ->
    ('p,'r,unit) monad
  
  val recv_slot :
    (('s,'t,[`Pass of 't * 'c * 'k cont]) channel, ('s,'t,'k) channel, 'p, 'q) idx -> 
    (empty, 'c, 'q, 'r) idx ->
    ('p,'r,unit) monad
  
  val send_chan : 
    (('s,'t,[>`Pass of 's * ('ss,'tt,'kk)channel * 'k cont]) channel, ('s,'t,'k) channel, 'q, 'r) idx -> 
    (('ss,'tt,'kk)channel, empty, 'p, 'q) idx ->
    ('p,'r,unit) monad
  
  val recv_chan :
    (('s,'t,[`Pass of 't * ('ss,'tt,'kk)channel * 'k cont]) channel, ('s,'t,'k) channel, 'p, 'q) idx -> 
    (empty, ('ss,'tt,'kk)channel, 'q, 'r) idx ->
    ('p,'r,unit) monad
  
  val send_new_chan : 
    (('s,'t,[>`Pass of 's * ('t,'s,'kk)channel * 'k cont]) channel, ('s,'t,'k) channel, 'p, 'q) idx -> 
    (empty,('s,'t,'kk)channel, 'q, 'r) idx ->
    ('p,'r,unit) monad
  
  val fork : 
    (empty, (pos,neg,'k)channel, 'p, 'q) idx -> 
    (((neg,pos,'k)channel, all_empty) cons, all_empty, unit) monad -> 
    ('p,'q,unit) monad

  (*
   * synthesize branching on arbitrary-many `tags
   * here after we need union of abstract poly-variants
   *)

  (*
   * Basic signature of the synthesis
   *)
  module type BRANCH = sig
    (* session  *)
    type 't from = private [> ]
    (* type of the branch *)
    type ('s,'t,'q,'r,'a) branch

    (* used internally *)
    val cont_ : 's -> 'q -> ('r * 'a) cont -> ('s,'t,'q,'r,'a) branch -> 't from -> unit

    (* synthesized branch *)
    val branch : (('s,'t,'t from)channel,empty,'p,'q) idx ->
                  ('s,'t,'q,'r,'a) branch ->
                  ('p,'r,'a) monad
  end

  (* branch `Finish *)
  module BranchFinish :
      BRANCH with
           type 't from = [`Finish] and
           type ('s,'t,'q,'r,'a) branch = unit -> ('q,'r,'a) monad

  type ('s,'t,'v,'k,'q,'r,'a) on_receive =
      {on_receive:'q1. (empty,('s,'t,'k)channel, 'q,'q1) idx * ('v -> ('q1,'r,'a) monad)}
  (* FAIL: we need 'q1 to be existential, not universal. *)

  module type SHOT = sig
      type 'a polyvar = private [> ]
      type v
      type k
      val ext : 'a polyvar -> 'a
    end

  (* Receiving (`SomeTag of 't * 'v * 'k) *)
  module BranchRecv :
    functor (X:SHOT) ->
      BRANCH with
           type 't from = [< ('t * X.v * X.k cont) X.polyvar] and (* '<' is strange but compiles for now *)
           type ('s,'t,'q,'r,'a) branch = ('s, 't,X.v,X.k,'q,'r,'a) on_receive

  (* adding another tag. HERE WE USE UNION OF ABSTRACT VARIANTS *)
  module BranchAddRecv :
    functor (M:BRANCH) -> functor (X:SHOT with type 'a polyvar = private [> ]~[M.from]) ->
      BRANCH with
           type 't from = ['t M.from | ('t * X.v * X.k cont) X.polyvar] and (* HERE *)
           type ('s,'t,'q,'r,'a) branch = ('s,'t,'q,'r,'a) M.branch * ('s,'t,X.v,X.k,'q,'r,'a) on_receive
end

(* signature of Ivar in Janestreet Async *)
module type IVAR = sig
    type 'a t

    val create : unit -> _ t
    val create_full : 'a -> 'a t

    val peek     : 'a t -> 'a option
    val is_empty : _ t -> bool
    val is_full  : _ t -> bool

    val equal : 'a t -> 'a t -> bool

    val connect : bind_result:'a t -> bind_rhs:'a t -> unit
    val fill : 'a t -> 'a  -> unit


    val upon  : 'a t -> ('a -> unit) -> unit

  end
                     
module Session(Ivar:IVAR) : SESSION = struct
    
  type ('a,'b,'p,'q) idx = ('p -> 'a) * ('p -> 'b -> 'q)
  type ('hd, 'tl) cons = 'hd * 'tl
  type empty = Empty
  type all_empty = empty * all_empty
  
  let _0 = (fun (a0,_) -> a0), (fun (_,a) b0 -> (b0,a))
  let _1 = (fun (_,(a1,_)) -> a1), (fun (a0,(_,a)) b1 -> (a0,(b1,a)))
  let _2 = (fun (_,(_,(a2,_))) -> a2), (fun (a0,(a1,(_,a))) b2 -> (a0,(a1,(b2,a))))
  let _3 = (fun (_,(_,(_,(a3,_)))) -> a3), (fun (a0,(a1,(a2,(_,a)))) b3 -> (a0,(a1,(a2,(b3,a)))))
  let succ (get,set) = (fun (_,a) -> get a), (fun (a0,a) bn -> (a0,set a bn))
  
  type ('p,'q,'a) monad = 'p -> ('q * 'a) Ivar.t
  let ret a p = Ivar.create_full (p, a)
  let (>>=) m f p =
    let ret = Ivar.create () in
    Ivar.upon (m p) (fun (q, x) -> Ivar.connect ~bind_rhs:(f x q) ~bind_result:ret);
    ret
  let (>>) m n = m >>= (fun _ -> n)
  
  
  let rec all_empty = Empty, all_empty
  
  type pos = Pos and neg = Neg
  
  type ('s,'v,'k) shot = Shot of 's * 'v * 'k Ivar.t
  type ('s,'c,'k) pass = Pass of 's * 'c * 'k Ivar.t
  type ('s,'k1,'k2) branch = BranchLeft of 's * 'k1 Ivar.t | BranchRight of 's * 'k2 Ivar.t
  type finish = unit
  type ('s,'t,'v,'w,'k) yield = ('s,'v,('t,'w,'k)shot)shot
  
  type ('s,'t,'k) channel = Chan of 's * 't * 'k Ivar.t
  type 'k cont = 'k Ivar.t
  
  let send (get,set) v p =
    let Chan(s,t,c) = get p in
    let c' = Ivar.create () in
    Ivar.fill c (`Shot(s,v,c'));
    Ivar.create_full (set p (Chan(s,t,c')), ())
                                     
  let recv (get,set) p =
    let Chan(s,t,c) = get p in
    let ret = Ivar.create () in
    Ivar.upon c (fun (`Shot(_, v, c')) -> Ivar.fill ret (set p (Chan(s,t,c')), v));
    ret
  
  let close (get,set) p =
    Ivar.create_full (set p Empty, ())
  
  let send_slot (get0,set0) (get1,set1) p =
    let e, q = get1 p, set1 p Empty in
    let Chan(s,t,c) = get0 q in
    let c' = Ivar.create () in
    Ivar.fill c (`Pass(s,e,c'));
    Ivar.create_full (set0 q (Chan(s,t,c')), ())
  
  let send_chan = send_slot
                   
  let recv_slot (get0,set0) (get1,set1) p =
    let Chan(s,t,c) = get0 p in
    let ret = Ivar.create () in
    Ivar.upon c (fun (`Pass(_,e,c')) -> Ivar.fill ret (set1 (set0 p (Chan(s,t,c'))) e, ()));
    ret
  
  let recv_chan = recv_slot
  
  let send_new_chan (get0,set0) (get1,set1) p =
    let Chan(s,t,c) = get0 p in
    let c' = Ivar.create () in
    let cc = Ivar.create () in
    let e = `Pass(s,Chan(t,s,cc),c') in
    Ivar.fill c e;
    Ivar.create_full (set1 (set0 p (Chan(s,t,c'))) (Chan(s,t,cc)), ())
  
  let branch (get0,set0) ((get1,set1),f1) ((get2,set2),f2) p =
    let Chan(s,t,c), q = get0 p, set0 p Empty in
    let ret = Ivar.create () in
    Ivar.upon c
              (function
                | BranchLeft(_,c') ->
                   Ivar.connect ~bind_rhs:(f1 () (set1 q (Chan(s,t,c')))) ~bind_result:ret
                | BranchRight(_,c') ->
                   Ivar.connect ~bind_rhs:(f2 () (set2 q (Chan(s,t,c')))) ~bind_result:ret
              );
    ret
  
  
  let fork (get,set) m p =
    let ivar = Ivar.create () in
    ignore (m (Chan(Neg,Pos,ivar),all_empty));
    Ivar.create_full (set p (Chan(Pos,Neg,ivar)), ())

  module type BRANCH = sig
    type 't from = private [> ]
    type ('s,'t,'q,'r,'a) branch
    val cont_ : 's -> 'q -> ('r * 'a) cont -> ('s,'t,'q,'r,'a) branch -> 't from -> unit
    val branch : (('s,'t,'t from)channel,empty,'p,'q) idx ->
                  ('s,'t,'q,'r,'a) branch ->
                  ('p,'r,'a) monad
  end

  module BranchFinish = struct
    type 't from = [`Finish]
    type ('s,'t,'q,'r,'a) branch = unit -> ('q,'r,'a) monad
    let cont_ s q ret on_close `Finish =
      Ivar.connect ~bind_rhs:(on_close () q) ~bind_result:ret
    let branch (get0,set0) go p =
      let Chan(s,t,c), q = get0 p, set0 p Empty
      and ret = Ivar.create ()
      in
      Ivar.upon c (cont_ s q ret go);
      ret
  end

  module type SHOT = sig
      type 'a polyvar = private [> ]
      type v
      type k
      val ext : 'a polyvar -> 'a
    end
                     
  type ('s,'t,'v,'k,'q,'r,'a) on_receive =
      {on_receive:'q1. (empty,('s,'t,'k)channel, 'q,'q1) idx * ('v -> ('q1,'r,'a) monad)}
      
  module BranchRecv = functor (X:SHOT) -> struct
    type 't from = [< ('t * X.v * X.k cont) X.polyvar]
    type ('s,'t,'q,'r,'a) branch = ('s, 't, X.v, X.k, 'q, 'r, 'a) on_receive

    let cont_ s q ret go (#X.polyvar as x) =
      let (t,v,c') = X.ext x
      and (get1,set1), go = go.on_receive
      in
      Ivar.connect ~bind_rhs:(go v (set1 q (Chan(s,t,c')))) ~bind_result:ret

    let branch (get0,set0) go p =
      let Chan(s,t,c), q = get0 p, set0 p Empty
      and ret = Ivar.create ()
      in
      Ivar.upon c (cont_ s q ret go);
      ret
  end

  module BranchAddRecv(M:BRANCH)(X:SHOT with type 'a polyvar = private [> ]~[M.from]) = struct
    type 't from = ['t M.from | ('t * X.v * X.k cont) X.polyvar]
    type ('s,'t,'q,'r,'a) branch = ('s,'t,'q,'r,'a) M.branch * ('s,'t,X.v,X.k,'q,'r,'a) on_receive

    let cont_ s q ret (go1,go2) = function
      | #M.from as x ->
        M.cont_ s q ret go1 x
      | #X.polyvar as x ->
        let (t,v,c') = X.ext x
        and (get1,set1), go2 = go2.on_receive
        in
        Ivar.connect ~bind_rhs:(go2 v (set1 q (Chan(s,t,c')))) ~bind_result:ret
    let branch (get0,set0) go p =
      let Chan(s,t,c), q = get0 p, set0 p Empty
      and ret = Ivar.create ()
      in
      Ivar.upon c (cont_ s q ret go);
      ret
  end
end

module BranchSynthesisExample(Ivar:IVAR) = struct
  module S = Session(Ivar)
  open S
         
  let branch_close_or_shot1 () =
    let module Shot1 = struct
      type 'a polyvar = [`Shot1 of 'a]
      type v = int
      type k = [`Finish]
      let ext (`Shot1(x)) = x
    end in
    let module M =
      BranchAddRecv(BranchFinish)(Shot1)
    in M.branch
         
  let branch_shot1_or_shot2 () =
    let module Shot1 = struct
      type 'a polyvar = [`Shot1 of 'a]
      type v = int
      type k = [`Finish]
      let ext (`Shot1(x)) = x
    end in
    let module Shot2 = struct
      type 'a polyvar = [`Shot2 of 'a]
      type v = string
      type k = [`Finish]
      let ext (`Shot2(x)) = x
    end in
    let module M = BranchAddRecv(BranchRecv(Shot1))(Shot2)
    in M.branch
end