signature DUAL = sig
  type client
  type server
  type ('c, 's) dual

  val witness : (client, server) dual
end

structure Session :> sig
  type epsilon
  type ('r, 'a) send
  type ('r, 'a) recv
  type ('r, 's) choose
  type ('r, 's) offer

  type ('r, 's) dual

  val epsilon : (epsilon, epsilon) dual
  val send    : ('r, 's) dual -> (('r, 'a) send, ('s, 'a) recv) dual
  val recv    : ('r, 's) dual -> (('r, 'a) recv, ('s, 'a) send) dual
  val choose  : ('r1, 's1) dual -> ('r2, 's2) dual ->
                (('r1, 'r2) choose, ('s1, 's2) offer) dual

  structure 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

  structure ImplicitProofs : sig
    type ('s1, 's2, 'a) session

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

    val >>= : ('s1, 's2, 'a) session * ('a -> ('s2, 's3, 'b) session) ->
              ('s1, 's3, 'b) session

    val >>  : ('s1, 's2, 'a) session * ('s2, 's3, 'b) session ->
              ('s1, 's3, 'b) session

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

    type 's rendezvous

    val newRendezvous : unit -> 's rendezvous
    val request : 's rendezvous -> ('s * 'r, unit, 'a) session -> 'a
    val accept  : 'r rendezvous -> ('s * 'r, unit, 'a) session -> 'a
  end

  structure ModuleLevelProofs : sig
    structure Eps : DUAL
      where type ('a, 'b) dual = ('a, 'b) dual
        and type client = epsilon
        and type server = epsilon

    (* Functors nested within structures is not SML, but it is
     * SML/NJ.  As far as I can tell, we need to do this so that
     * the functors can share the private definition of type dual.
     * Of course, the value-level and implicit duality proofs are
     * Standard Standard ML. *)
    functor Send(A : sig type t structure D : DUAL end) : DUAL
      where type ('a, 'b) dual = ('a, 'b) dual
        and type client = (A.D.client, A.t) send
        and type server = (A.D.server, A.t) recv

    functor Recv(A : sig type t structure D : DUAL end) : DUAL
      where type ('a, 'b) dual = ('a, 'b) dual
        and type client = (A.D.client, A.t) recv
        and type server = (A.D.server, A.t) send

    functor Choose(A : sig structure D : DUAL structure E : DUAL end) : DUAL
      where type ('a, 'b) dual = ('a, 'b) dual
        and type client = (A.D.client, A.E.client) choose
        and type server = (A.D.server, A.E.server) offer

    functor Offer(A : sig structure D : DUAL structure E : DUAL end) : DUAL
      where type ('a, 'b) dual = ('a, 'b) dual
        and type client = (A.D.client, A.E.client) offer
        and type server = (A.D.server, A.E.server) choose

    functor Flip(D : DUAL) : DUAL
      where type ('a, 'b) dual = ('a, 'b) dual
        and type client = D.server
        and type server = D.client
  end
end = struct
  type epsilon         = unit
  type ('a, 'r) send   = unit
  type ('a, 'r) recv   = unit
  type ('r, 's) choose = unit
  type ('r, 's) offer  = unit

  type ('r, 's) dual   = unit

  val epsilon    = ()
  fun send _     = ()
  fun recv _     = ()
  fun choose _ _ = ()
  fun offer _ _  = ()

  structure ValueLevelProofs = struct
    val epsilon = ()
    fun send _ = ()
    fun recv _ = ()
    fun send' _ _ = ()
    fun recv' _ _ = ()
    fun offer _ _ = ()
    fun choose _ _ = ()

    fun flip _ = ()
  end

  structure ImplicitProofs = struct
    type ('s, 't, 'a) session = unit -> 'a

    fun ret a () = a

    infixr >>=
    infixr >>

    fun m >>= k = fn () => k (m ()) ()
    fun m >>  n = m >>= (fn _ => n)

    exception ReceiveAttempted

    fun send _ () = ()
    fun recv () = raise ReceiveAttempted
    fun mock_recv a () = a
    fun sel1 () = ()
    fun sel2 () = ()
    fun offer a _ () = a ()
    fun close () = ()

    type 's rendezvous = unit

    fun newRendezvous () = ()

    fun accept  _ f = f ()
    fun request _ f = f ()
  end

  structure ModuleLevelProofs = struct
    structure Eps = struct
      type client = epsilon
      type server = epsilon
      type ('a, 'b) dual = ('a, 'b) dual
      val witness = ()
    end

    functor Send(A : sig type t structure D : DUAL end) = struct
      type client = (A.D.client, A.t) send
      type server = (A.D.server, A.t) recv
      type ('a, 'b) dual = ('a, 'b) dual
      val witness = ()
    end

    functor Recv(A : sig type t structure D : DUAL end) = struct
      type client = (A.D.client, A.t) recv
      type server = (A.D.server, A.t) send
      type ('a, 'b) dual = ('a, 'b) dual
      val witness = ()
    end

    functor Choose(A : sig structure D : DUAL structure E : DUAL end) = struct
      type client = (A.D.client, A.E.client) choose
      type server = (A.D.server, A.E.server) offer
      type ('a, 'b) dual = ('a, 'b) dual
      val witness = ()
    end

    functor Offer(A : sig structure D : DUAL structure E : DUAL end) = struct
      type client = (A.D.client, A.E.client) offer
      type server = (A.D.server, A.E.server) choose
      type ('a, 'b) dual = ('a, 'b) dual
      val witness = ()
    end

    functor Flip(D : DUAL) = struct
      type client = D.server
      type server = D.client
      type ('a, 'b) dual = ('a, 'b) dual
      val witness = ()
    end
  end
end