Munksgaard / session-types

MIT License
550 stars 21 forks source link

Recursive protocols without Rec and Var #32

Open ebfull opened 8 years ago

ebfull commented 8 years ago

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 commented 8 years ago

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 commented 1 year ago

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?