Recursive Session Types

Provider Rule: Fix Session

fn fix_session<C, A1, A2>(
  cont: PartialSession<C, A2>
) -> PartialSession<C, Rec<A1>>

• For a protocol A = Rec<A1>, A1 contains recursion points back to A marked with Z.
• A2 is A1 with Z replaced by Rec<A1>.

Example

fn counter(val: u64) -> Session<Rec<SendValue<u64, Z>>>
{
  fix_session(send_value(val, counter(val + 1)))
}

For a equi-recursive definition A = SendValue<u64, A>:

• A1 = SendValue<u64, Z>
• A2 = SendValue<u64, Rec<SendValue<u64, Z>>>

Client Rule: Unfix Session

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

• C1 is in the form HList[…, N: Rec<A1>, …]
• C2 is in the form HList[…, N: A2, …], with the remaining elements being the same as in C1.

Example

fn counter_client() -> Session<ReceiveChannel<Rec<SendValue<u64, Z>>, End>>
{
  receive_channel(move |c1| {
    unfix_session(
      c1,
      receive_value_from(c1, move |x| {
        println!("{}", x);
        include_session(counter_client(), move |c2| {
          send_channel_to(c2, c1, forward(c2))
        })
      }),
    )
  })
}