Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Recursive protocols without Rec and Var #32

Open
ebfull opened this issue Nov 14, 2015 · 2 comments
Open

Recursive protocols without Rec and Var #32

ebfull opened this issue Nov 14, 2015 · 2 comments

Comments

@ebfull
Copy link

ebfull commented Nov 14, 2015

Associated types are powerful enough to avoid needing an environment stack or recursive session types.

pub trait HasDual {
    type Dual: SessionType;
}

pub trait Alias {
    type Id: HasDual;
}

pub struct Goto<A: Alias>(PhantomData<A>);
pub struct GotoDual<A: Alias>(PhantomData<A>);

impl<A: Alias> HasDual for Goto<A> {
    type Dual = GotoDual<A>;
}

impl<A: Alias> HasDual for GotoDual<A> {
    type Dual = Goto<A>;
}

Cool, but it requires ugly struct definitions and impls at every depth. I think this downside is mentioned throughout session type literature. It's not practical, they said. Just use recursive session types, they said.

But wait, there's macros!

proto!(Atm = {
    Recv String,
    AtmMenu = Accept {
        AtmDeposit = {
            Recv u64,
            Send u64,
            Goto AtmMenu
        },
        AtmWithdraw = {
            Recv u64,
            Send bool,
            Goto AtmMenu
        },
        AtmGetBalance = {
            Send u64,
            Goto AtmMenu
        },
        End
    }
});

Unfortunately the macro necessary to expand such a construct is ridiculously complex (and this is after omitting recursion, choose/offer, etc.):

#[macro_export]
macro_rules! proto(
    (@form_ty End) => (End);
    (@form_ty Goto $t:ty) => (Goto<$t>);
    (@form_ty Recv $t:ty, $($rest:tt)*) => (Recv<$t, proto!(@form_ty $($rest)*)>);
    (@form_ty Send $t:ty, $($rest:tt)*) => (Send<$t, proto!(@form_ty $($rest)*)>);
    (@form_ty {$($stuff:tt)*}) => (proto!(@form_ty $($stuff)*));
    (@form_ty $i:ty = {$($stuff:tt)*}) => (<$i as Alias>::Id);
    (@form_ty $i:ty = $t:ident {$($stuff:tt)*}) => (<$i as Alias>::Id);
    (@new_aliases () $($others:tt)*) => (
        proto!(@construct_alias $($others)*);
    );
    (@new_aliases ({$($some:tt)*}$($rest:tt)*) $($others:tt)*) => (
        proto!(@new_aliases ($($some)* $($rest)*) $($others)*);
    );
    (@new_aliases (, $($rest:tt)*) $($others:tt)*) => (
        proto!(@new_aliases ($($rest)*) $($others)*);
    );
    (@new_aliases ($alias:ident = {$($astuff:tt)*} $($lol:tt)*) $($others:tt)*) => (
        proto!(@new_aliases ($($lol)*) ($alias = {$($astuff)*}) $($others)*);
    );
    (@new_aliases ($alias:ident = $t:ident {$($astuff:tt)*} $($lol:tt)*) $($others:tt)*) => (
        proto!(@new_aliases ($($lol)*) ($alias = {$t {$($astuff)*}}) $($others)*);
    );
    (@new_aliases ($x:ident $($rest:tt)*) $($others:tt)*) => (
        proto!(@new_aliases ($($rest)*) $($others)*);
    );
    (@construct_final ($alias:ident, $($arest:tt)*)) => (
        #[allow(dead_code)]
        struct $alias;

        impl Alias for $alias {
            type Id = proto!(@form_ty $($arest)*);
        }
    );
    (@construct_final ($alias:ident, $($arest:tt)*) $($rest:tt)*) => (
        proto!(@construct_final ($alias, $($arest)*));
        proto!(@construct_final $($rest)*);
    );
    (@construct_alias @eps $($rest:tt)*) => (
        proto!(@construct_final $($rest)*);
    );
    (@construct_alias ($alias:ident = {$($rest:tt)*}) $($others:tt)*) => (
        proto!(@new_aliases ($($rest)*) $($others)* ($alias, $($rest)*));
    );
    ($start:ident = {$($rest:tt)*}) => (
        proto!(@construct_alias ($start = {$($rest)*}) @eps);
    );
);
@ebfull
Copy link
Author

ebfull commented Nov 14, 2015

By the way, the above macro might be useful for users to reason about Rec and Var. You can think of Rec like loop { } and Var like continue.

proto!(Whatever = loop {
        Recv usize,
        Choose {
            {
                Recv usize,
                Send usize,
                continue
            },
            {
                Send usize,
                End
            },
            {
                loop {
                    Recv usize,
                    Choose {
                        continue,
                        continue 1
                    }
                }
            }
        }
    }
);

@maxime-tournier
Copy link

Now that GATs are stabilized, it seems one could easily leverage them to define type-level fixpoints:

pub trait Fix {
    type Def<T>: HasDual where T: HasDual;
}

impl<T> Chan<T>
where
    T: Fix,
{
    pub fn fix(self) -> Chan<<T as Fix>::Def<T>> {
        unsafe { transmute(self) }
    }
}

impl<T> HasDual for T where T: Fix {
    type Dual = T;
}

// example use
struct MyLoop();

impl Fix for MyLoop {
    type Def<T> = Recv<usize, Send<usize, T>> where T: HasDual;
}

fn srv(mut c: Chan<MyLoop>) {
    loop {
	let cc = c.fix();
	let (cc, value) = cc.recv();
	c = cc.send(value);
    }
}

Would there be any downside with this approach?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants