Ferrite uses the term protocol to refer to session types in Rust. All protocol in Ferrite implements the
Protocol trait. The name of the protocols are defined based on the behavior of the provider.
Most of the Ferrite protocols also contain continuation protocols, which describe the protocol that
follows after the current protocol have been executed.
We have seen an example protocol in the previous section,
SendValue<String, End>. This means that the type
SendValue<String, End> implements the
This is so because
End is a protocol representing termination, and the type
SendValue<T, A> is a protocol
if the continuation protocol
A, which is
End in this case, is a protocol. The type
describes a protocol which the provider sends a
String value and then terminates with
End. On the other end,
this behavior is inversed, with the client receives the
String value and then waits for the provider to terminate.
For a Rust type to be a Ferrite protocol. It has to follow certain conditions. For example, while we can define a Rust type
SendValue<String, i32>, it is not considered by Ferrite to be a protocol. This is because the continuation
i32 does not implement
SendValue<String, i32> also does not implement
Some protocols also have additional constraints that need to be satisfied. For example, the protocol
also requires the Rust value to be send,
T, to implement
This means that we can only send Rust values that can be safely transferred across threads, and do not contain other local lifetimes.
Using Ferrite, we can define complex protocols that have many layers of nested continuations.
For example, the protocol
SendValue<String, ReceiveValue<i32, SendValue<bool, End>>>
describes a session type which the provider first sends a
String value, then receives
i32 value, then sends a
bool value, before finally terminating.
We will cover in detail each protocol in the upcoming chapters. Below shows a summary of protocols available in Ferrite:
|Send a Rust value of type |
|Receive a Rust value of type |
|Send a channel of session type |
|Receive a channel of session type |
|Provide the client with choices defined in |
|Offer a particular choice defined in |
|Recursive session type, with |