Typestate is the concept of encoding state machines in a programming language’s type system. While not specific to Rust, typestate has been explored elsewhere at length in the context of Rust. Typestate boils down to four ideas:
Each state is represented as a unique type.
State transitions are only available as methods for the corresponding state type.
Taking a state transition returns a state machine of the new state type.
State transitions invalidate old state.
For example, here’s a state machine for a send-then-receive channel:
transmute. The use of #[repr(transparent)] ensures that the layout of Channel is stable across transmutations of the marker type.This pattern works effectively for simple finite state machines, where the logic to determine the next state is straightforward. In this note, I will explore situations where determining the next state is not so simple. In the process, we’ll talk about type-level programming, or how you can use Rust’s type system to encode computations on types.
As a first example, consider a basic information flow control problem. In our program we have low security values (anyone can read them) and high security values (only authorized users can read them). We represent this idea like so:
We would like to have a vector of these items with the following property:
If all of the items are low security, anyone can read any item.
If any of the items are high security, only an authorized user can read any item.
For example, our vector should pass this test:
A basic type-state attempt looks like this. We can create and read a low-security vector:
And we can protect a high-security vector through a witness:
Now, to the main idea: how can we implement push? There are four possible state combinations: a high/low security vector with a high/low security item. While we can implement each combination as a separate method, it’s simpler to consider the underlying logic. push should return a vector of level max(vec_level, item_level) where max(hi, lo) = hi.
Our goal is to encode max as a type-level computation, i.e. an operator on types. The high-level idea:
Traits definitions are function signatures from types to types.
Trait type parameters represent inputs and associated types represent outputs.
Trait implementations define individual mappings from inputs to outputs.
Here are those ideas in action to compute the max security level:
MaxLevel alias. In brief: L as ComputeMaxLevel<R> says "treat L as the trait object ComputeMaxLevel<R>". This is necessary since multiple computation traits may have associated Output with L, so the explicit cast disambiguates the MaxLevel computation from the rest.Here’s an example of using the type operator:
Now, we can implement SecureVec::push in one method:
Notice the usage of MaxLevel in the return type of push. This is the key use of the type operator as a type-level computation. The other main component is the where clause: when used generically (over any possible ItemLevel), we have to use a trait bound to ensure that ComputeMaxLevel can be "called" on ItemLevel.
Excellent! We’ve now used a type-level computation to more abstractly specify typestate in our information flow control API. Next, we’ll look at an example with a more complex type-level program.
When two parties synchronously communicate with each other (e.g. a client and server exchanging information), that communication protocol can be modeled as a session type. We’re going to look at session types implemented in Rust. While their full implementation is beyond the scope of the post (see the linked paper or my course notes), I will focus on the aspects of session types that showcase type-level programming.
Session types are a domain-specific language of state machines, described by this grammar:
For example, this session type describes a ping server that sends and receives a ping in a loop, exiting on demand. The label/goto scheme uses de Bruijn indices to locally encode label names as integers.
The grammar, and this example, can be encoded in Rust like so:
The runtime communication API uses the type-state concept as a channel whose type changes as the protocol advances. Initially, a Chan is created for the server and the client (the “dual” of the server). Here’s an example where the type annotations show the change.
Note that the Chan has two type arguments: an environment Env and a current action Sigma. The environment contains a list of session types generated by calls to label. When we goto, we look up the corresponding type in the Env list and make that the type of the current channel.
You might wonder how the methods like c.offer() and c.recv() are actually implemented. Once the session type framework is established, they aren’t very interesting — perform an operation, then transmute to the new type-state. For example, recv:
See the session-types crate for the full implementation if you’re interested.
We’re going to look at two type-level operations in this framework:
Dual types: given a description of the protocol from one party’s perspective (e.g. PingServer) we can automatically generate a matching PingClient protocol. This is the Dual<PingServer> reference above.
Labels and gotos: to implement label/goto, we need a notion of a dynamically-sized list of types that we can push, index, and change.
The idea of a dual session type is that if I’m sending to you, you should be receiving from me. Similarly, if I offer to branch left or right, you should be choosing which branch to take. In Rust, the dual of Send<i32, Close> should be Recv<i32, Close>.
Dual session types are useful because they prevent errors. If you had to manually specify both halves of the protocol, you might accidentally mis-match one side.
We can write down an inductive procedure for generating a dual type as follows, using the notation to mean "the dual of ".
In the context of type-level programming, is an operator that takes as input a type, and produces a type. Like with MaxLevel, we encode that concept as a trait:
Unlike before, ComputeDual only takes one argument Self, so it does not need additional parameters. Like before, we use an alias to simplify later usage of the trait.
The key idea is that each of the logical rules above cleanly translates into a corresponding trait implementation. First, the base cases:
To represent the inductive cases (e.g. Send), we use a where clause to perform an inductive computation. For example:
Again, compare this code to the original rule:
Usually, a where bound constrains a trait implementation, e.g. ToString for Vec<T> is only implemented where T: ToString. Here, we re-purpose the bound to perform a computation, i.e. inductively getting the Dual of S.
Type: Trait, so we can’t say S: Dual as Dual is a type. We use ComputeDual in the trait bound, then Dual<S> when used as a type.As another example, here’s the Dual rule for Choose:
With these rules in hand, we can now easily specify our client type:
That’s it! We’ve successfully encoded dual session types as a type operator in Rust.
At this point, you may wonder — the translation from the pretty logic to the ugly traits involves a lot of syntax. Take a look at the type-operators crate for using a macro to automatically perform the translation.
Our final challenge is to implement the label and goto operators. We start with the following skeleton, needing to fill in the ?:
We are going to encode Env as a list of session types. To do so, we need to resolve four questions:
How do we represent a list of types?
How do we push to a list of types?
How do we get the -th type in a list of types?
How do we drop the first types in a list of types?
Like in a functional programming language, we will use a linked-list nil/cons style to represent a type list.
Then to get the -th type in a list, we can use a type-level operator encoded as a trait, using a familiar pattern:
Think for a moment about the inductive definition of Nth as you might write it in OCaml or Haskell. It probably looks something like this:
Just like with dual session types, we can straightforwardly encode these logical rules into trait implementations. However, because we are using a Peano encoding of the natural numbers, we’ll tweak the second rule to look like this:
Then the encoding of Nth into Rust traits becomes 1-to-1:
Similarly, we can create a function that drops the first N elements from a type list:
With these type-level operators in hand, we can finish our label and goto implementations. Now, label is a simple Push:
The goto function is more complex. We need to both get the Nth element of an environment, and drop the first N elements.
Note that because we use Env with two type-level operators, we have to add both as bounds combined with +.
The relationship between types, traits, and logic programming has been an enduring theme in the Rust community. "Lowering Rust traits to logic" and the ongoing efforts on chalk both show how resolving trait bounds is equivalent to executing a logic program.
In this note, I tried to go in the opposite direction — showing how domain-specific type-systems, whose rules are often written as logical relations, can be lowered into Rust traits. I think this is valuable because:
Domain-specific type systems enable powerful compile-time checks on complex properties. Checking that communication protocols are followed, or that secure information is protected, usually requires external model checkers. Here, we just need Rust!
Encoding logic rules into Rust traits in a practical way is not obvious at first glance. There aren’t many examples of this pattern to generalize from.
For example, if we took our type operators above, we could concisely encode their logic as a logic program (using Prolog-esque syntax):
Seeing this pattern, we can construct a general translation. A type operator is a relation with Self as the first argument, Output as the last argument, and additional arguments in between. So a general relation Rel(Self, Arg1, .., ArgN, Output) translates to:
An unconditional fact like Rel(Tself, T1, ... TN, Tout) becomes an impl block without a where clause:
And a complex conditional fact like:
Becomes an impl block with a where clause:
In drawing this connection between traits and logic programs, I hope that you might find it easier to encode new domain-specific type systems in Rust. These examples also demonstrate that there’s a lot of exciting future work in developing libraries and best practices for type-level programming!