Suggestion: User provided Message types

[gterzian]

Hi there. Great work on this library, I really like the concept!

I was experimenting with adding a V parameter to Chan that would allow the user to provide an enum to parametrize the inner channel. I'm not sure why, perhaps as a way to remove the unsafe inner sending and receiving?

It did break the inner implemenation of Choose, which I solved by adding a Selectable trait that would be implemented by the user to provide the sel1/sel2 values themselves instead of the default true/false(in the same enum V).

On the downside, you would definitely loose quite a lot of 'labeling' capacity on the definition of the protocol side, since you end up with a bunch of Send and Recv that all get this same enum as parameter. So something descriptive like type Paint = Recv<(Vec<PaintRequest>, FrameTreeId), Var<Z>>; would be transformed into a much less descriptive type Paint = Recv<Msg, Var<Z>>; On the other hand, perhaps some people in some cases would prefer to just define one enums for all messages, instead of separate types for each particular step.

I got as far as making the two simple tests pass, by some miracle I guess.

Anyway, this is just meant as a way of sharing the results of this experiment. Perhaps consider adding a second API endpoint with this kind of typing that would include safe sending on the underlying channel for those who require it?

[laumann]

Hi @gterzian, thanks for feedback and the suggestion!

Hmmm, it looks like the Selectable idea is about adding n-ary choice instead of binary. Is that correct? We debated this a lot but did not come up with a method that wouldn't make the types too convoluted. Our "best" effort was developing Choose3/Offer3, Choose4/Offer4, etc and providing a number of variants for that. But we figured that it was just adding some stuff for ergonomics and not much else.

---

(Note, I wrote the text below before really reading the Selectable code, I'll just leave it as it is)

The typical use that I've seen of channels (normal CSP channels) are exactly using enums to list the various types of messages that can be transmitted. So you have something like:

enum Msg {
    Paint(Payload),
    Exit(Status)
    ForceExit,
}

let (tx, rx) = channel::<Msg>();

but this leaves you no way of saying anything about the order of messages. In general we ended up not using enums in the transmitted values because the enums sort of model the protocol themselves. With session types, the Paint, Exit, ForceExit, etc then become different paths through the protocol. (I tend to think of it as a kind of "unpacking" of the Msg protocol). Only Payload and Status would survive in the session type.

type P = Rec<Choose<Send<Payload, Var<Z>>,
             Choose<Send<Status, Eps>, Eps>>>;

When using session typed channels, I don't think it should be necessary to use an enum as a message unless, for some reason, the payload itself has to be a enum.

[gterzian]

it looks like the Selectable idea is about adding n-ary choice instead of binary

I didn't implement it, so it wasn't very clear, my idea was that it would be a binary choice except that the two values would be provided by the user in the form of 'choosing' from two variants of the enum, and the trait would be a way for the protocol internals to know which corresponds to sel1 and which to sel2. Like:

enum Msg {
    Paint(Payload),
    Exit(Status)
    ForceExit,
    Left,
    Right
}

impl Selectable<Msg> for Msg {
    fn sel1(&self) -> Msg::Left
    fn sel2(&self) -> Msg::Right
}

(This would have required also implementing PartialEq for the enum, I'm not even sure how that would look like).

But I think this is probably not something a user would actually want to do. It was really just a way to make the typing of the channel work, since currently a bool is being sent internally as part of Choose, and that wasn't possible anymore once the internal channels could only send and receive Msg variants...

this leaves you no way of saying anything about the order of messages. In general we ended up not using enums in the transmitted values because the enums sort of model the protocol themselves.

Yes I agree. I think the current setup is probably more appropriate for your use case, where one would really want to model each steps precisely.

....

Have you tried swapping out the internal channel for other stuff, like an ipc_channel, or looked into how a protocol could communicate over the network while retaining (some of) the current guarantees?

[Munksgaard]

Have you tried swapping out the internal channel for other stuff, like an ipc_channel, or looked into how a protocol could communicate over the network while retaining (some of) the current guarantees?

It would indeed be interesting to try to create an alternative library for either of these situations, but we have not done much in that direction. I think the main problem is, that over a network (or with ipc) you're potentially dealing with malicious counter-parties. The current session-types library primarily works as a help for the developer, it is a sort of enhanced type checking, but if the counter-party breaks the protocol, unexpected things could happen. Thankfully, that shouldn't be possible using our library, because both sides of the session channel are compiled at the same time, with the same protocol, but it's harder to guarantee over the wire, especially when you take malicious users into consideration.

I'm sure others are working on that problem, but I must admit that I don't know what the state of the art is.

[gterzian]

Ok, thanks for the info!