Session types are, essentially, a technique for using a rich type system like that of Rust or OCaml to express semantic meaning and prevent the representation of certain kinds of illegal states, especially with respect to causality.
What is the use-case?
Let’s take the somewhat contrived example of a system representing packaging and shipping boxes. I want to create a Package datastructure, pack data into it, close it (preventing adding data), address it, and then ship it. It makes no sense to send an un-addressed Package, or to insert data into a closed one.
We could represent this like this:
We would then have lots of runtime typechecking of whether boxes submitted for shipping were addressed and such, which costs time and is error-prone. Wouldn’t it be nice if the compiler could enforce this?
How is it implemented?
The easiest way to implement this is with three different types: an OpenPackage, a ClosedPackage, and an Addressed Package.
Crucially, the contents field is pub. You can poke and prod and change that data all you want.
This has a few capabilities: pack, which takes control of whatever is supposed to go in the package and creates an OpenPackage around it, unpack, which destroys the OpenPackage and gives back its contents, and finally close, which converts the OpenPackage to a ClosedPackage.
This leads naturally to the ClosedPackage struct:
Very similar, but without the pub attribute. This means that a ClosedPackage isn’t in danger of having its contents manipulated in any way.
ClosedPackages can be opened again, yielding an OpenPackage, or addressed, creating an AddressedPackage.
Finally, the AddressedPackage struct represents one with a specified destination. I used a String for the address here, but it would be trivial to create a generic version.
To understand the access controls here, just think of a physical package. The address is on the outside; anyone can read it or cross it out with a sharpie. The contents, however, are sealed away.
This struct can be turned back into a ClosedPackage by receiveing it:
Finally, I created an example function to “send” the package somewhere.
This ends up printing out:
In the real world, the Rust crate hyper makes heavy use of session types to ensure the integrity of HTTP requests and responses.