6 ms·
Session Types for Rust
- asimpletune 8y agoI’m not sure if I’m misunderstanding the purpose of session-types, but it seem that this a lot like finagle but for rust? Session type is basically just a finagle service, etc... Or are they more like go channels?
- steveklabnik 8y agoSession types are more like “encode a state machine in your type system so it’s impossible to mess it up”. They don’t inherently have to do with network services, though since network services follow protocols that can be represented as state machines (think “the S in REST”), they’re a good application of session types. That said, it looks like this library is not purely about session types, but applying them to channels. (Which are go-style, yes.)
- agumonkey 8y agoare they used in non academic contexts ?
- Munksgaard 8y agoI'm one of the authors of the original paper/repository. 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.
- agumonkey 8y agoVery nice
- paulddraper 8y agoSession types are essentially a type-checked FSM. So if your type checker passes, your FSM obeys the protocol requirements. (Namely, it does not pass between states in an illegal manner.)
- cwillu 8y agoThis sounds a lot like the invariant that they're checking is that, _given a conforming counter-party_, nothing illegal will happen. But this doesn't tell you anything about what happens to you when your peer passes between states in an illegal manner. I'd expect this to have been emphasised in the paper. Especially if their threat model includes it, it would be a key selling point.
- deleted 8y ago[deleted]
- reificator 8y agoIf you're interested in this, you may want to take a look at this article as well: https://insanitybit.github.io/2016/05/30/beyond-memory-safety-with-types https://insanitybit.github.io/2016/05/30/beyond-memory-safet... 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-imap-client-in-rust https://insanitybit.github.io/2016/06/28/implementing-an-ima...
- agumonkey 8y agois it different from phantom types ? more general ?
- staticassertion 8y agoI wrote that insanitybit post. It's unrelated to Phantom types. 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.
- agumonkey 8y agoBut state machine and communication protocols.. aren't they isomorphic ?
- staticassertion 8y agoSure, feel free to read 'communication protocol' where I say state machine.
- agumonkey 8y agooh ok; I double-misread your above comment. My assumption was that phantom types were also about encoding state machines in types and thus could work for communication protocols too just like your session type article; hence the question about the difference between the two.
- choeger 8y agoWell. Rust is about to turn into Haskell 2.0
- smt88 8y agoIs that good or bad? Sounds like it's good, but I've never used Haskell, so I don't know.
- deleted 8y ago[deleted]
- duncan-donuts 8y agoAs someone that knows only a little about Rust and Haskell, why?
- choeger 8y agoType-level programming. It basically guarantees more correctness at the cost of steeper entry barriers. In consequence you end up with (some extension of) Haskell and a probably correct implementation that no one can start to implement ;).
- AaronFriel 8y agoThe power of these is that a handful of implementations can act as enormous levers to create useful abstractions for everyone else. As an example, Rust's type system is difficult to implement and hard to prove correct - there was a problem with `std::thread::scoped`'s soundness for example - but once done, the work can be leveraged into higher (and often simpler) abstractions! Session types in Rust are exciting to me because we might see implementations of consensus algorithms leverage the type system for correctness. Everyone else then gets to benefit from a simple API on those (complicated) types.
- steveklabnik 8y agoYou don’t need that powerful of a type system to do this kind of thing; Rust is still pretty far behind Haskell in terms of raw power.
- wcrichton 8y agoI taught this concept in my course on Programming Languages at Stanford. If you’d like a more pedagogic introduction to both session types and their implementation, check out the course notes: http://cs242.stanford.edu/f18/lectures/07-2-session-types.html http://cs242.stanford.edu/f18/lectures/07-2-session-types.ht...
- deleted 8y ago[deleted]
- larsberg 8y agoIf you're interested in this topic, I'd highly recommend watching Stephanie Balzer's sessions at the Oregon Programming Language Summer School on “Session-Typed Concurrent Programming”. The lectures are available online (https://www.cs.uoregon.edu/research/summerschool/summer18/topics.php#Balzer https://www.cs.uoregon.edu/research/summerschool/summer18/to...). 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_deadlock_freedom.pdf http://www.cs.cmu.edu/~balzers/publications/manifest_deadloc...
- YorkshireSeason 8y agoIn what sense does this work really advance session types? Prima facie it looks like yet another tiny delta on Honda's original work that cannot and does not get around session types' core problem of data-dependent communication topology. Let me quote from the paper (Page 22, Section 6): "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.
- twic 8y agoI am pleased to see that this was done without macros, even custom derives. There are a couple of macros in the library to make some use cases easier, but they aren't essential. 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.
- chrismorgan 8y agoI don’t believe that strict “session types” are a good fit for Rust: it’s shoehorning a concept, simultaneously specialised (it’s for channels) and generalised (as in “left” and “right”), into Rust in a way that works, but is not as pleasant as can be achieved with little effort. (There’s not much actual code in session-types/src/lib.rs—most of it is interfaces and macros because it made life hard for itself by being too generic.) 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 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.
- bsaul 8y agoDo you know of any programming language where this type of things (having functions defined only for certain enum values, or anything equivalent) would be doable properly, without hacking the typesystem ?
- syspec 8y agoI never understood the idea of shortening variable names a few characters. Recv vs Received, especially when there’s a also a Rec type mentioned in the reader as well. It’s not like Send, was shortened to Snd
- hu3 8y agoQuite confusing indeed: Rec<Recv<String, Var<Z>>>
- userbinator 8y agoRead (or indeed, write) a lot of code and you'll quickly realise why. It's the same reason acronyms and abbreviations exist in human languages. Also, "recv" and "send" are both 4 characters, which is nice.
- nitrogen 8y agoThese days people type the first four letters and rely on IDE autocomplete to finish the other 42.
- oh_sigh 8y agoProbably because someone important couldn't remember if it was receive or recieve
- theoh 8y agoIt's mysterious, all right. https://unix.stackexchange.com/questions/128708/why-wasnt-creat-called-create https://unix.stackexchange.com/questions/128708/why-wasnt-cr... 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 https://en.wikipedia.org/wiki/Baudot_code So at a certain point abbreviations became both useful and fashionable: https://en.wikipedia.org/wiki/Abbreviation https://en.wikipedia.org/wiki/Abbreviation (See also http://www.thepotteries.org/mark/w/wedgwood-date.html http://www.thepotteries.org/mark/w/wedgwood-date.html for a 19th C example of three-letter coding.)
- emilfihlman 8y ago>Using this library, you can implement bi-directional process communication with compile-time assurance that neither party will violate the communication protocol. 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.
- theoh 8y agoThis is about validating code, not about maintaining the integrity of the system in the presence of corruption or a party that is deliberately trying to break things. It's actually helpful to be able to check that the system is sound in theory. Nobody is suggesting that you can use that as an excuse to get sloppy.
- empath75 8y agoIt’s about validating that your own code matches the spec. Not validating that anybody you’re communicating with does. Though if you wrote the client and the server then you know that both do.
- myWindoonn 8y agoI wish I knew how to get this point across to people. The way I think of it is that a type-checker which validates a single program at a time isn't capable of proving certain facts which hold when access to filesystems or networks are involved.