Munksgaard / session-types

MIT License
555 stars 21 forks source link

Better choose API #28

Open ebfull opened 9 years ago

ebfull commented 9 years ago

Right now the path down a Choose style decision tree is formed by signaling with booleans over the channel, which is not (space) efficient. Further, you must use macros to avoid having to do a bunch of annoying compositions to select the branches you want.

Here's an alternative API which unfortunately requires Rust nightly, but (somehow) works:

#![feature(optin_builtin_traits)]

use std::marker::PhantomData;

trait ChooseFrom { }
impl<Q> ChooseFrom for Finally<Q> {}
impl<P, Q: ChooseFrom> ChooseFrom for Choose<P, Q> {}

struct Finally<Q>(PhantomData<Q>);
struct Choose<P, Q: ChooseFrom>(PhantomData<(P, Q)>);

struct Compound<A, B>(PhantomData<(A, B)>);
trait NotSame { }
impl NotSame for .. { }
impl<A> !NotSame for Compound<A, A> { }

trait Chooser<T> {
    fn num() -> usize;
}

impl<P, Q: ChooseFrom> Chooser<P> for Choose<P, Q> {
    fn num() -> usize { 0 }
}

impl<P> Chooser<P> for Finally<P> {
    fn num() -> usize { 0 }
}

impl<P, S, Q: ChooseFrom + Chooser<S>> Chooser<S> for Choose<P, Q>
    where Compound<S, P>: NotSame {

    fn num() -> usize { 1 + Q::num() }
}

impl<P, Q: ChooseFrom> Choose<P, Q> {
    fn choose<S>(&self) -> usize where Self: Chooser<S> {
        Self::num()
    }
}

fn main() {
    let a: Choose<usize, Choose<isize, Choose<String, Finally<()>>>> = Choose(PhantomData);

    println!("{:?}", a.choose::<String>());
}

Basically, in theory you can just call chan.choose::<Protocol>() and it will signal over the channel that you're switching to that protocol using a single number. Perhaps if there's a monomorphization recursion limit anyway, we could use u8 or u16 instead of usize to make the discriminant as small as possible. (Safety note: if the number wraps around it will cause memory safety violations. Perhaps we can use peano numbers to encode a maximum limit here.)

Also, I believe with inlining LLVM will completely optimize this away.

ebfull commented 9 years ago

There are two well-formedness issues with this:

  1. You need a Finally<T> guard to disambiguate from a nested Choose<P, Q>. I'm going to try to think of a way to avoid it perhaps with the same tricks I was using before, but it might require specialization.
  2. We should enforce the invariant given for<S, P, Q: Choose<S>> Choose<P, Q> does not impl Choose<S>. This is to prevent Choose<P, Choose<Q, Finally<P>>> from existing, as it does not make any sense.
ebfull commented 9 years ago

Unfortunately there doesn't appear to be a way to design the Offer dual of this design within your library without generic handlers.

laumann commented 9 years ago

Sorry for not getting back sooner...

The choose() function is exactly something that we wanted to implement - you solution is way cooler than what have been able to come up with! But the challenge always seems to turn out to be offer(), because ideally you want just a single method

fn offer() -> Chan<E, P> { ... }

But given Chan<Offer<S, T>> we cannot get rustc to infer the correct S or T in the given situations.

I'm wondering though if there is a way to combine #23 with this choose API? That way, choose() might feel more ergonomic, while retaining the offer API (that seems to work OK).

The error messages reported when selecting an non-existing branch are a little obscure though :smile:

<anon>:45:24: 45:39 error: the trait `Chooser<u64>` is not implemented for the type `Finally<()>` [E0277]
<anon>:45     println!("{:?}", a.choose::<u64>());
                                 ^~~~~~~~~~~~~~~
<std macros>:2:25: 2:56 note: in this expansion of format_args!
<std macros>:3:1: 3:54 note: in this expansion of print! (defined in <std macros>)
<anon>:45:5: 45:41 note: in this expansion of println! (defined in <std macros>)
<anon>:45:24: 45:39 help: see the detailed explanation for E0277
error: aborting due to previous error
playpen: application terminated with error code 101
ebfull commented 9 years ago

I implemented this Choose/Offer concept in my library. (I call it Choose/Accept)

It requires doing...

Identity: Choose<S, Choose<R, Finally<Q>>>
Dual: Offer<S, Offer<R, Finally<Q>>>

... in combination with a hack I discovered that allows you to express type inequality (S != T) with (S, T): NotSame:


trait NotSame { }
impl NotSame for .. { }
impl<A> !NotSame for (A, A) { }

It was tricky to get the offer side of this working but I did it. It should be possible to prevent something like Choose<P, Finally<P>> from existing using traits, but it's not really necessary to get this working and inference properly working.

Choose call: https://github.com/ebfull/nemo/blob/master/tests/lib.rs#L180 Accept call: https://github.com/ebfull/nemo/blob/master/tests/lib.rs#L188

The reason I don't think it's possible in your library is that you do not have generic handlers, and it would be messy to try to add them without redesigning a lot of other stuff.

ebfull commented 9 years ago

It's possible in your library without generic handlers.

fn whatever(c: Chan<(), Accept<P, Accept<S, Finally<Q>>>>) {
    c.accept::<P>(|c| { /* do stuff with Chan<(), P> */ })
         .or::<S>(|c| { /* do stuff with Chan<(), S> */ })
         .or::<Q>(|c| { /* do stuff with Chan<(), Q> */ });
}

This would only require reading a single number from the channel (perhaps only a single byte). The discriminant would be carried through a guard type that .accept() and .or() return, subtracted each time, and when the number is zero the closure is handed ownership of the channel.

There are probably downsides to this approach but it's still cool.

laumann commented 9 years ago

This is cool :sunglasses:

The only potential downside I see, is the use of closures - but they seem necessary in this situation. Historically, rustc has not been able to do tail-call optimization in this kind of situation which can quickly lead to trouble.

Is there a way where we could have both accept()/or() and keep some version of the current form for Offer?

ebfull commented 9 years ago

I'm not sure there's a way to preserve the current semantics -- it's barely even possible to achieve my design, as it requires a hack that the Rust developers claim should not be possible.

Closures though aren't a concern unless you're dealing with recursion, in which case you can't use closures anyway, but you will almost certainly run into stack overflows if you're not careful.