Session Types for Rust
github.com
github.com
The underlying concept in Rust is basically a type-level enum (state machine), encoding the variant (state) as a phantom type in a generic parameter; that, you can express without the full baggage of what is called session types, and with greater freedom.
The situation is similar to the Either enum with its Left and Right variants: it was in the standard library well before Rust 1.0 because it was easy, but it was eventually abandoned in favour of good semantics: most users should use Result, and the rest should write their own two-variant enums. Similarly, if you encode your state machine in Rust types yourself, you end up with clearer and more obvious code.
The main thing this library does is get you the specific channel behaviour; that may be useful in some situations, but you can implement the underlying concept atop regular channels without much difficulty, and it gives you considerably more freedom in the API.
Here’s a small macro library that I wrote a few years ago, with an example that demonstrates this general concept: https://github.com/chris-morgan/phantom-enum
I find myself wishing more and more often that Rust enum variants could be used as types, and that type refinement could work like in TypeScript.
(I do realise that what I’m advocating is targeting a potentially different and broader sector to session-types, but I maintain my position: doing it from scratch yourself is fairly straightforward, normally easy and more powerful.)
You can achieve all of this with different types instead of one type with a phantom enum type parameter, too; see the insanitybit article linked elsewhere in these comments. The primary benefit of the phantom enum type parameter approach is when you have methods that apply in multiple, or all, states, so that you don’t need to duplicate them. Sometimes you want extra data in particular states; you can achieve that in the type parameter approach by making the enum not phantom, and rather a struct with extra data, or you can achieve that by just using distinct types. Which is most appropriate varies case by case.
Other than that, TypeScript has decent support for the concept, though with standalone functions rather than methods: you’d define your “variants” as types (or interfaces), define the “enum” as the union of those types (e.g. `Foo | Bar`), and then have your functions take either the entire “enum” type, or specific “variant” types. In place of Rust’s `match`, you will then use type guards to narrow the “enum” type down to one (or more, if you like) of the “variant” types. See https://www.typescriptlang.org/docs/handbook/advanced-types.... for a bit of info.
Edit: It's called a partial function, and I confused Julia with Pony. The former might be able to express it, the latter can handle it in some way, but I'm not familiar with either type system.
EDIT: Sorry, I remembered the site name and saw IMAP in the title, but ended up clicking the wrong article. Updated the above link from https://insanitybit.github.io/2016/06/28/implementing-an-ima...
A session type allows you to encode a state machine into your type system. What this means is that, at compile time, you can validate that your code can't transition into an invalid state.
I've seen that approach used but I can't really comment too much on the differences as I've never used it myself. I find my approach simple in practice (I've shipped Python code that takes the same approach, sans affine types) because it separates the types out.
So, essentially, I write my non-sesssiony struct with all of its methods, and then I wrap that in the session types. This lets me easily drop into the non-session type if necessary, and the sessions types act as thin wrappers. My imap client worked the same way, if I recall.
The downside is likely boilerplate.
I toyed with phantom type in kotlin recently (toy examples); I'm curious how it would be done in python.
Her recent work (sponsored, in part, by Mozilla Research) really advances session types and the ability to get termination/progress guarantees: http://www.cs.cmu.edu/~balzers/publications/manifest_deadloc...
"The typing discipline presented in the previous sections, while rich enough to account for a wide range of interesting programs, cannot type programs that spawn a statically undetermined number of shared sessions that are then to be used."
That has been the problem of this approach to typing message passing for nearly 3 decades, and like all predecessor papers in this theory tradition, an ad-hoc approach is proposed that makes core session types incredibly complicated without solving the problem. In order to get a publication out of this, a different problem is solved, a yet another Curry-Howard corresponce for some small delta of Linear Logic is given.
There is a tendency in the Rust community to reach for macros as soon as anything a bit complicated or verbose comes up. I think this most often ends up sacrificing true understandability on the altar of a slick surface syntax, and it doesn't help us write or understand well in the long run.
It’s not like Send, was shortened to Snd
Rec<Recv<String, Var<Z>>>Also, "recv" and "send" are both 4 characters, which is nice.
The case where things are given three or four letter codes is more comprehensible. Baudot code from the 19th C calls letters and figures LTRS and FIGS, though I'm not sure when exactly that got established as the normative spelling. Presumably LTRS and FIGS can be printed on a smaller keycap than the full word.
https://en.wikipedia.org/wiki/Baudot_code
So at a certain point abbreviations became both useful and fashionable:
https://en.wikipedia.org/wiki/Abbreviation
(See also http://www.thepotteries.org/mark/w/wedgwood-date.html for a 19th C example of three-letter coding.)
And in any case; what does raw power really mean?
The two languages appear to have fairly widely different aims, and both see type-system cleverness as a boon, so it should come as little surprise that they don't all have the same tricks.
Neat!
No, you cannot. "Assurance of not violating communication protocol" and "process communication" together are an oxymoron. If you do this, you deserve all the possible failures that come along with it.
Please don't write infrastructure code that depends on "assurances" instead of checking and validating communications.
There's usually little value in worrying too much about how a real platform won't correspond precisely to that assumed platform, since the goal of validation is to remove a class of errors, not all errors.
It's the same idea here. Obviously nothing can stop, say, faulty network hardware from causing protocol violations. But that doesn't stop us from meaningfully saying that, under the correct set of assumptions, protocol violations are statically prevented at compile time.
Session type is basically just a finagle service, etc...
Or are they more like go channels?
That said, it looks like this library is not purely about session types, but applying them to channels. (Which are go-style, yes.)
Part of the motivation behind our work was to try and apply it to the Servo project (Mozilla's experimental browser engine, of which parts have already been integrated into Firefox), which is highly parallelized. They had issues with their internal communication because of their expansive use of threads, and we wanted to see if session types could be applied to fix that. Unfortunately, Servo is a rapidly moving target, so while we did manage to convert some parts of the project to use our session types library, we never got around to finishing the work, and now I believe that they've found different solutions to their challenges.
With regards to your first question, this library is solely for in-process communication. The concept could be expanded to cover inter-process communication as well as communication over the network, and actually has been in other similar session type projects, but focusing on in-process communication allows us to make stronger guarantees.
So if your type checker passes, your FSM obeys the protocol requirements. (Namely, it does not pass between states in an illegal manner.)