zero() might not be implemented correctly

[ebfull]

impl<E, P> Chan<(P, E), Var<Z>> {
    /// Recurse to the environment on the top of the environment stack.
    #[must_use]
    pub fn zero(self) -> Chan<(P, E), P> {
        unsafe { transmute(self) }
    }
}

impl<E, P, N> Chan<(P, E), Var<S<N>>> {
    /// Pop the top environment from the environment stack.
    #[must_use]
    pub fn succ(self) -> Chan<E, Var<N>> {
        unsafe { transmute(self) }
    }
}

Compare zero to succ. I believe zero should be restoring the original environment when it pops the protocol. That is, zero should return Chan<E, P>.

(I could be wrong as I've just begun using session types.)

[ebfull]

edit: actually, I understand succ now. My point above still stands.

[ebfull]

It occurs to me that you could actually combine these two operations into one:

use std::marker::PhantomData;

struct Foo<E, P>(PhantomData<(E, P)>);
struct Var<N>(PhantomData<N>);
struct S<N>(PhantomData<N>);
struct Z;

trait Pop<N> {
    type FinalE;
    type FinalP;
}

impl<A, B> Pop<Z> for (A, B) {
    type FinalE = B;
    type FinalP = A;
}

impl<A, B: Pop<N>, N> Pop<S<N>> for (A, B) {
    type FinalE = B::FinalE;
    type FinalP = B::FinalP;
}

impl<N, E: Pop<N>> Foo<E, Var<N>> {
    fn pop(self) -> Foo<E::FinalE, E::FinalP> {
        Foo(PhantomData)
    }
}

fn test1<A>(a: Foo<(A, ()), Var<Z>>) -> Foo<(), A> {
    a.pop()
}

fn test2<A, B>(a: Foo<(A, (B, ())), Var<S<Z>>>) -> Foo<(), B> {
    a.pop()
}

fn main() {}

I can't imagine a situation where you wouldn't want .succ() until you had to .zero(), since you can't do anything else anyway.

[Munksgaard]

Compare zero to succ. I believe zero should be restoring the original environment when it pops the protocol. That is, zero should return Chan<E, P>.

That is definitely another possible design, but I think it has a couple of drawbacks: Mainly, the current design allows us to do looping without having to enter the protocol scope every time we recurse:

fn foo(c: Chan<(), Rec<Var<Z>>) {
    let mut c = c.enter;
    loop {
        // Do some work
        c = c.zero();
    }
}

If we were to modify the library as you suggest, looping would instead look something like this:

fn foo(mut c: Chan<(), Rec<Var<Z>>) {
    loop {
        let _c = c.enter()
        // Do some work
        c = _c.zero();
    }
}

Furthermore, to accommodate this, we'd have to change the signature of enter to the following:

enter: Chan<E, Rec<P>>  -> Chan<(Rec<P>, E), P>

I think that the current design is better, but that's just my opinion :)

NB: Forgive me for any typos or syntax errors, I haven't tested the code above.

It occurs to me that you could actually combine these two operations into one

This is an interesting idea, but I'll have to consider it more in detail later today.

[ebfull]

If we were to modify the library as you suggest, looping would instead look something like this:

Interesting! Thank you for the insight.

I modified my "combine into one operation" idea to fit those semantics:

use std::marker::PhantomData;

struct Foo<E, P>(PhantomData<(E, P)>);
struct Var<N>(PhantomData<N>);
struct S<N>(PhantomData<N>);
struct Z;

trait Pop<N> {
    type FinalE;
    type FinalP;
}

impl<A, B> Pop<Z> for (A, B) {
    type FinalE = (A, B);
    type FinalP = A;
}

impl<A, B: Pop<N>, N> Pop<S<N>> for (A, B) {
    type FinalE = B::FinalE;
    type FinalP = B::FinalP;
}

impl<N, E: Pop<N>> Foo<E, Var<N>> {
    fn pop(self) -> Foo<E::FinalE, E::FinalP> {
        Foo(PhantomData)
    }
}

fn test1<A>(a: Foo<(A, ()), Var<Z>>) -> Foo<(A, ()), A> {
    a.pop()
}

fn test2<A, B>(a: Foo<(A, (B, ())), Var<S<Z>>>) -> Foo<(B, ()), B> {
    a.pop()
}

fn main() {}

[Munksgaard]

Ah, yes, I see what you're doing! Combining succ and zero into one operation like this is a great idea, as far as I can tell, especially if it doesn't require any additional annotations from the user (which it doesn't look like this will). I'd be interested to see an actual PR for this, if you want to make one?

[ebfull]

Sure.