Receive Channel

Provider Rule: Receive Channel

fn receive_channel<N, C1, C2, A, B>(
  cont: impl FnOnce(N) -> PartialSession<C2, B>
) -> PartialSession<C1, ReceiveChannel<A, B>>

• N is the length of C1.
• C1 is in the form HList![0: A0, 1: A1, ...]
• C2 is in the form HList![0: A0, 1: A1, ..., N: A], with A appended to the end of C1 and the remaining elements unchanged.

Example

    let p: Session<ReceiveChannel<End, End>> =
      receive_channel(move |c| wait(c, terminate()));

Client Rule: Send Channel To

fn send_channel_to <N, M, C1, C2, A1, A2, B>(
  n: N, m: M,
  cont: PartialSession<C2, B>,
) -> PartialSession<C1, B>

• C1 is in the form HList[…, N: ReceiveChannel<A1, A2>, … M: A1, …]
• C2 is in the form HList[…, N: A2, …, M: Empty, …], with the remaining elements being same as C1.
• M may come before N.

Example

    let p1: Session<ReceiveValue<String, End>> = todo!();

    let p2: Session<ReceiveChannel<ReceiveValue<String, End>, End>> = todo!();

    let p3: Session<End> = include_session(p1, move |c1| {
      include_session(p2, move |c2| {
        send_channel_to(c2, c1, wait(c2, terminate()))
      })
    });