type epsilon
type ('r, 'a) send
type ('r, 'a) recv
type ('r, 's) choose
type ('r, 's) offer

type ('r, 's) dual

module ModuleLevelProofs : sig
  module type TYPE = sig
    type t
  end

  module type DUAL = sig
    type client
    type server

    val witness : (client, server) dual
  end

  module Epsilon : DUAL
    with type client = epsilon
     and type server = epsilon

  module Send (T : TYPE) (R : DUAL) : DUAL
    with type client = (R.client, T.t) send
     and type server = (R.server, T.t) recv

  module Recv (T : TYPE) (R : DUAL) : DUAL
    with type client = (R.client, T.t) recv
     and type server = (R.server, T.t) send

  module Offer (R : DUAL) (S : DUAL) : DUAL
    with type client = (R.client, S.client) offer
     and type server = (R.server, S.server) choose

  module Choose (R : DUAL) (S : DUAL) : DUAL
    with type client = (R.client, S.client) choose
     and type server = (R.server, S.server) offer

  module Flip (R : DUAL) : DUAL
    with type client = R.server
     and type server = R.client
end

module ValueLevelProofs : sig
  val epsilon : (epsilon, epsilon) dual
  val send   : ('b, 'c) dual -> ((('b, 'a) send, ('c, 'a) recv) dual)
  val recv   : ('b, 'c) dual -> ((('b, 'a) recv, ('c, 'a) send) dual)
  val send'  : 'a -> ('b, 'c) dual -> ((('b, 'a) send, ('c, 'a) recv) dual)
  val recv'  : 'a -> ('b, 'c) dual -> ((('b, 'a) recv, ('c, 'a) send) dual)
  val offer  : ('a, 'b) dual -> ('c, 'd) dual ->
                (('a, 'c) offer, ('b, 'd) choose) dual
  val choose : ('a, 'b) dual -> ('c, 'd) dual ->
                (('a, 'c) choose, ('b, 'd) offer) dual

  val flip   : ('a, 'b) dual -> ('b, 'a) dual
end

module ImplicitProofs : sig
  type ('s, 't, 'a) session

  val ret   : 'a -> ('s, 's, 'a) session

  val (>>=) : ('s, 't, 'a) session ->
              ('a -> ('t, 'u, 'b) session) ->
              ('s, 'u, 'b) session

  val (>>)  : ('s, 't, 'a) session ->
              ('t, 'u, 'b) session ->
              ('s, 'u, 'b) session

  val send  : 'a -> (('r, 'a) send * ('s, 'a) recv, 'r * 's, unit) session
  val recv  : (('r, 'a) recv * ('s, 'a) send, 'r * 's, 'a) session
  val mock_recv : 'a -> (('r, 'a) recv * ('s, 'a) send, 'r * 's, 'a) session
  val sel1  : (('r1, 's1) choose * ('r2, 's2) offer, 'r1 * 'r2, unit) session
  val sel2  : (('r1, 's1) choose * ('r2, 's2) offer, 's1 * 's2, unit) session
  val offer : ('r1 * 'r2, 'u, 'a) session ->
              ('s1 * 's2, 'u, 'a) session ->
              (('r1, 's1) offer * ('r2, 's2) choose, 'u, 'a) session
  val close : (epsilon * epsilon, unit, unit) session

  val run : ('r1 * 'r2, unit, 'b) session ->
            ('r2 * 'r1, unit, 'a) session -> 'a
end