Writing Session-Typed Ferrite Programs in Rust (Draft)

Welcome to Writing Session-Typed Ferrite Programs in Rust! This is an introductory guide on how to use Ferrite, an EDSL (embedded domain specific language), for writing session-typed programs in Rust.

In this book you will learn about writing Ferrite programs with linear session types, which channel variables must be used exactly once. This is in contrast with normal Rust programs with affine types, which variables can be used at most once.

You will learn how session types can be used to define communication protocols between different parts of a Rust program. You will see how Ferrite can help elminate the boilerplates of managing communication using plain Rust channels, and enforce protocol compliance through linearity.

Finally you will also learn about shared session types, which you can use to define services that can be safely shared among multiple linear clients. You will learn how shared session types can be used to implement common communication patterns such as client-server communication.

Work In Progress

Ferrite is currently still in development, with parts of the code subject to change. This book is also a work in progress, with most of the content yet to be written. Keep an eye on the ferrite and ferrite-book repositories for any update.

Getting Started

In this section, we will get a quick taste of Ferrite with a high level overview of the language. You will learn about how to start using Ferrite to build a toy example program in Ferrite.

This book assumes that you already know the basic concepts in Rust, as well as advanced concepts such as generic types, traits, associated types, and asynchronous programming. If you haven't learned these concepts, we highly recommend you to first read the relevant sections in the Rust book, and the Async book.

Installation

Ferrite is an open source project with the source code available at GitHub. Ferrite is also published at crates.io as the Cargo crate ferrite-session.

To start using Ferrite, simply create a new Cargo project and add ferrite-session as a dependency in Cargo.toml. Ferrite uses tokio to spawn async tasks, so you should add that as a dependency as well.

[dependencies]
tokio = "1.6.1"
ferrite-session = "0.1.4"
...

To use the constructs provided by Ferrite, import everything from the ferrite_session::prelude module. You'd also need to provide a tokio runtime for Ferrite to spawn its async tasks. This can be done by adding the #[tokio::main] attribute to your main function.

use ferrite_session::prelude::*;

#[tokio::main]
async fn main() { ... }

Next, we will learn how to use Ferrite to write a simple hello world program.

Hello World

In this chapter we will look at two simple programs that implement hello world in Ferrite.

Hello Protocol

A session type, a.k.a. a protocol, describes a communication protocol between two parties: a provider and a client. The provider offers a service as described by the session type, and the client consumes the provided service in a linear fashion.

In this example, we will define a simple Hello protocol that has the session type SendValue<String, End>:

type Hello = SendValue<String, End>;

Our Hello protocol pretty much self describe the communication protocol: The provider would send a Rust String value and then terminates. Conversely, a client for Hello would receive a Rust String value, and then waits for the provider to terminate.

The type SendValue<T, A> defines a session type that sends a Rust value T, and then continues with the continuation session type A. The type End defines a session type that simply terminates. When we combine both SendValue and End to get SendValue<String, End>, we are effectively defining a session type that sends a Rust value of type String, and then continues as session type End, which happens to simply terminates.

Hello World Provider

We first look at how a provider for the Hello protocol can be implemented:

  let hello_provider: Session<Hello> =
    send_value("Hello World!".to_string(), terminate());

In the above example, we define a variable named hello_provider with the Rust type Session<Hello>. The Rust type Session<A> denotes a Ferrite program that is providing a session type A. In this case, hello_provider is a Ferrite program that provides the Hello protocol.

In the body of hello_provider, we use the Ferrite functions send_value and terminate to build up our Ferrite program. According to the Hello protocol, the first step hello_provider needs to do is to send a String value. To do that, we create a Rust string "Hello World!".to_string(), and then send it by calling send_value("Hello World!".to_string(), ... ).

Other than the "Hello World!" string in the first argument, send_value also expects a second argument, which is the continuation after our string value is sent. In our case, The continuation session type of SendValue<String, End> is End. As such, there is nothing left to do other than terminating the Ferrite program, which we can do it by calling terminate().

Run Session

Up to this point, we have only defined a Ferrite program named hello_provider, but we have not yet execute the program. To run it, we would typically need to pair it with a client that consumes the offered protocol Hello. However Ferrite provides a special case for Ferrite programs that offer the session types SendValue<T, End>. So we can run our hello_provider by calling run_session_with_result:

  let result: String = run_session_with_result(hello_provider).await;

  println!("{}", result);

Ferrite provides run_session_with_result as a default way of handling Ferrite programs offering the session type SendValue<T, End>, because they are trivial to handle. This can be done by receiving the Rust value sent from the provider, waits for the provider to terminate, and then returns to the caller. The function is an async function, so we have to use the .await syntax to wait for Ferrite to run the program and return the results.

After getting the result back, we can print the received string using println!, and we can expect "Hello World!" to be printed at this point.

Full Hello World Program

Putting everything together, our first hello world program is written as follows:

use ferrite_session::prelude::*;

type Hello = SendValue<String, End>;

#[tokio::main]
async fn main()
{
  let hello_provider: Session<Hello> =
    send_value("Hello World!".to_string(), terminate());

  let result: String = run_session_with_result(hello_provider).await;

  println!("{}", result);
}

Our Rust program defines an async main function using the #[tokio::main] attribute provided by tokio. Inside the main body, we define our provider Ferrite program as hello_provider, and then immediately run it using run_session_with_result. Finally we get back the result string and print it to the terminal.

Client Communication

In the previous chapter, we defined a hello provider and then run it immediately using run_session_with_result. However in practical applications, our Ferrite programs will typically have more complex session types, and we would want to run multiple programs in parallel that communicate with each others.

To demonstrate that, instead of running hello_provider directly, we can define a hello_client that communicates with a provider of the Hello protocol, and then link it with hello_provider.

First, we define hello_client to have the following type:

let hello_client: Session<ReceiveChannel<Hello, End>> = ...

Our hello_client has the Rust type Session<ReceiveChannel<Hello, End>>, indicating that it is a Ferrite program offering the session type ReceiveChannel<Hello, End>. Here we encounter a new session type in the form ReceiveChannel<A, B>, which is used to receive a channel of session type A offered by some provider, and then continue offering session type B.

Channels

Ferrite allows sending and receiving of channels, which represent the client end point to communicate with a provider that offers the channel's session type. At high level, we can think of receiving a channel using ReceiveChannel<A, B> is similar to plain Rust functions with function traits like FnOnce(A) -> B. In other words, ReceiveChannel is the equivalent of function types in Ferrite.

There is however one important distinction of ReceiveChannel from regular Rust functions. That is channels received from ReceiveChannel must be used linearly, i.e. they cannot be ignored or dropped. We will revisit this property in later chapters to see why linearity is important, and why bare Rust code is not sufficient to support linearity.

Now back to our hello_client example. The session type ReceiveChannel<Hello, End> indicates that hello_client is receiving a channel of session type Hello, and then terminates with End. To implement such a session type, we can implement hello_client as follows:

  let hello_client: Session<ReceiveChannel<Hello, End>> =
    receive_channel(|a| {
      receive_value_from(a, move |greeting| {
        println!("Received greetings from provider: {}", greeting);
        wait(a, terminate())
      })
    });

Our hello_client body looks slightly more complicated than hello_provider. To understand what's going on, we will go through each line of hello_client's body. Starting with receive_channel:

receive_channel(|provider| { ... })

To match the final session type ReceiveChannel<Hello, End> that is offered by hello_client, we use receive_channel to receive a channel of session type Hello, and then binds it to the channel variable a. This is similar to a Rust function accepting an argument and bind it to a variable.

Inside the continuation ..., since we have received the Hello channel already, we will continue to offer the session type End. To do that, we just need to eventually terminate hello_client. However we cannot terminate hello_client just yet, because the channel variable a is linear, and we must fully consume it before we can terminate.

Recall that Hello is a type alias, so the actual session type of the channel variable a is SendValue<String, End>. But instead of having to offer that, we are acting as the client to consume the session type SendValue<String, End>. Since the provider is expected to send a String value, as a client we are expected to receive a String value from the provider. We can do that using receive_value_from:

receive_value_from(provider, move |greeting| {
  println!("Received greetings from provider: {}", greeting);
  ...
})

We use receive_value_from to receive a value sent from the a channel, and then bind the received String value to the Rust variable greeting. We then print out the value of greeting using println!. Following that, in the continuation ..., the session type of a changes from SendValue<String, End> to become End.

Unlike regular Rust variables, each time we interacts with a channel variable, the session type of the channel variable is updated to its continuation session type. Since Ferrite channels are linear, we have to continuously interact with the channel until it is fully terminated.

After calling receive_value_from, we have the channel variable a with session type End, and we need to offer the session type End by terminating. But we can't terminate just yet, because End simply indicates that the provider will eventually terminates, but may not yet been terminated. Hence we would first have to wait for a to terminate using wait:

wait(provider, terminate())

We use wait to wait for the provider on the other side of a channel to terminate. After that, the a channel is discarded, and we don't have anymore unused channel variable. With that, we can finally terminate our program using terminate().

Linking Provider With Client

We have now defined a hello_client program that can accept channel from any provider offering the session type Hello. In theory, we can call hello_client with any provider that offers Hello, not just hello_provider.

To link hello_client specifically with hello_provider, we have to explicitly ask Ferrite to perform the linking. This can be done using apply_channel:

  let main: Session<End> = apply_channel(hello_client, hello_provider);

The apply_channel construct is provided by Ferrite to link a client Ferrite program of session type ReceiveChannel<A, B> with a provider Ferrite program of session type A, resulting in a new Ferrite program of session type B as the result.

We can think of the form apply_channel(f, x) as being similar similar to regular function application in the form f(x). With f having the Rust type FnOnce(A) -> B and x having the Rust type A, the result type of applying x to func would be B.

Run Session

After applying hello_provider to hello_client, we now have a single main program. When main is executed, it will run both hello_provider and hello_client in parallel, and establish a communication channel between the two processes.

Since main has the session type End, we can use the Ferrite construct run_session to run the program:

  run_session(main).await;

run_session accepts any Ferrite program offering the session type End, executes the program, and wait for it to terminate. run_session is similar to run_session_with_result, other than it does not expect the Ferrite program to send back any Rust value as the result.

Full Program

Putting everything together, we now have our second hello world program that is made of a hello_provider and a hello_client communicating with each others.

use ferrite_session::prelude::*;

type Hello = SendValue<String, End>;

#[tokio::main]
async fn main()
{
  let hello_provider: Session<Hello> =
    send_value("Hello World!".to_string(), terminate());

  let hello_client: Session<ReceiveChannel<Hello, End>> =
    receive_channel(|a| {
      receive_value_from(a, move |greeting| {
        println!("Received greetings from provider: {}", greeting);
        wait(a, terminate())
      })
    });

  let hello_client_partial: PartialSession<
    HList![SendValue<String, End>],
    End,
  > = receive_value_from(Z, move |greeting| {
    println!("Received greetings from provider: {}", greeting);
    wait(Z, terminate())
  });

  let main: Session<End> = apply_channel(hello_client, hello_provider);

  run_session(main).await;
}

Type Errors

The way we write a Ferrite program is quite different from how we typically write a Rust program. This is because Ferrite makes use of Rust's type system to provide additional safeguard on how session type channels can be used.

We can take a quick look of some error messages raised when our Ferrite programs are written incorrectly.

An Incorrect Hello Provider

Let's consider the hello_provider program that we have written in the previous chapter:

  let hello_provider: Session<Hello> =
    send_value("Hello World!".to_string(), terminate());

According to the Hello protocol, SendValue<String, End>, hello_provider is supposed to send a string value before terminating. But what if we implement hello_provider such that it terminates immediately without sending a string?

let hello_provider_incorrect: Session<Hello> = terminate();

In this case, if we try to compile our program, we would get a compile error from Rust showing a message similar to as follows:

error[E0308]: mismatched types
 |   let hello_provider_incorrect: Session<Hello> = terminate();
 |                                 --------------   ^^^^^^^^^^^ expected struct `ferrite_session::prelude::SendValue`, found struct `ferrite_session::prelude::End`
 |                                 |
 |                                 expected due to this
 |
 = note: expected struct `PartialSession<(), ferrite_session::prelude::SendValue<String, ferrite_session::prelude::End>>`
            found struct `PartialSession<_, ferrite_session::prelude::End>`

The error message above has been slightly prettified to make it more readable, but the content remains the same. First of all, we see that the error is about type mismatch between a PartialSession type, which we will cover in a later chapter.

Inside the second type parameter of PartialSession, notice that there is a mismatch between the expected session type SendValue < String, End >, and the actual session type End. From that, we can deduce that hello_provider_incorrect has violated the Hello protocol, by instead offering the protocol End.

An Incorrect Hello Client

The error message we get from hello_provider_incorrect is relatively simple, as the type mismatch is on the offered channel. On the other hand, recall that hello_client deals with two channels: one with the receiver end of Hello, and one that offers the session type End.

  let hello_client: Session<ReceiveChannel<Hello, End>> =
    receive_channel(|a| {
      receive_value_from(a, move |greeting| {
        println!("Received greetings from provider: {}", greeting);
        wait(a, terminate())
      })
    });

Based on the protocol specification, it looks like hello_client should be able to receive a Hello channel, ignores the channel, and proceed to terminate immediately. So let's try implementing a new client to do just that:

let hello_client_incorrect: Session<ReceiveChannel<Hello, End>> =
  receive_channel(|provider| {
    terminate()
  });

In hello_client_incorrect, the provider channel is ignored after we have received it, and we proceed to call terminate immediately. If we try to build this, we would instead get the following compile error:

error[E0277]: the trait bound `(ferrite_session::prelude::SendValue<String, ferrite_session::prelude::End>, ()): ferrite_session::internal::base::EmptyContext` is not satisfied
 |
 |     terminate()
 |     ^^^^^^^^^ the trait `ferrite_session::internal::base::EmptyContext` is not implemented for `(ferrite_session::prelude::SendValue<String, ferrite_session::prelude::End>, ())`
 |
 |
 |   C: EmptyContext,
 |      ------------ required by this bound in `ferrite_session::prelude::terminate`
 |
 = help: the following implementations were found:
           <(ferrite_session::prelude::Empty, R) as ferrite_session::internal::base::EmptyContext>

The error can look a bit scary, but it mainly boils down to two constructs: a new type (SendValue<String, End>, ()) and a new trait EmptyContext.

The type (SendValue<String, End>, ()) represents the linear context in hello_client_incorrect, when the expression terminate() is called. We will cover the details of linear context in a later chapter. For now it is sufficient to know that it is used to track the provider channel we have just received, and it has the session type SendValue<String, End>.

The EmptyContext trait is essentially telling us that in order to use the terminate() construct, the current linear context must be empty. However because we have not yet used up the provider channel, the linear context is thus not empty, and so we cannot terminate just yet.

Enforcing Linear Usage at Compile Time

The error from hello_client_incorrect shows us how Ferrite enforces linear usage of session type channels at compile time. This can greatly reduce the chance of us writing incorrect Ferrite programs that just abort in the middle of communicating with other processes.

The linear usage of Ferrite channels is different from the affine usage of Rust objects. Consider an equivalent of hello_client implemented using Rust channels:

fn hello_client_rust(receiver: Receiver<String>) {
  // drops receiver immediately
}

In standard Rust programs, we establish communication between concurrent processes by explicitly passing the sender or receiver end of a Rust channel as function argument. However since the Rust channel is just an affine Rust object, it is possible that one party drops the channel half way, intentionally or not.

In the simple case of our Hello protocol, the dropping of a channel might not seem critical. But what if the protocol is slightly more complicated?

Let's say we have an Ping protocol with the session type ReceiveValue<String, SendValue<String, End>>. This would require the provider to receive a string value before sending back another string value, and vice versa for the client. If a client drops the channel without sending a value to the provider, the provider would potentially wait forever without receiving the string.

Even if the provider can somehow detect that the client has dropped the channel half way, it would still have to raise a runtime error to signal the error on protocol violation. We would then have to write a lot of tests to make sure such errors never happen in practice. Even so the tests may not be exhaustive enough to cover all corner cases.

By enforcing the linear usage of channels at compile time, Ferrite helps eliminate a broad range of communication errors that can happen due to incorrect implementations. As we will see in later chapters, using Ferrite we can safely implement complex communication protocols in our Rust programs, without having to worry about our programs not correctly following these protocols.

Session Types

This chapter provides some supplementary overview of session types, the type theory that Ferrite is based on. In the discussion we will talk about some concepts related to logic and type theory. For readers who are unfamiliar with these topics, feel free to skip this chapter and move on to the next chapter.

Background on Session Types

So far we have been talking about session types without going into details what it is. Broadly speaking, session types can refer to a branch of type systems used to model structured communication-based programming. Session types are also known as behavioural types, since the types describe the behaviour of a program.

From the theoretical perspective, session types establish a correspondence with linear logic. This makes session-typed languages slightly different from functional languages such as Rust and Haskell, which have their roots in lambda calculus and intuitionistic logic.

Throughout this book, we will learn about various concepts of session types from the perspective of a Rust programmer. While this may not be a comprehensive overview of session types themselves, we aim to cover enough of the basics so that you can explore more deeply into session types through other resources.

Linear, Affine, and Structural Rules

One notable distiction between session types and Rust is that session typed variables are linear, while Rust variables are affine by default. We will try to understand what that really means.

A common explanation of linear vs affine is that linear variables must be used exactly once, while affine variables can be used at most once. However that is not entirely accurate.

To be more precise, type theorists differentiate different kinds of type systems based on which structural rules are allowed in the type system:

  • In a normal type system like Haskell, variables are allowed to be used more than once (contraction). Variables are also allowed to be discarded (weakening).

  • In an affine type system like Rust, variables are not allowed to be used more than once (no contraction), unless they specifically implement Copy or Clone. However variables are still allowed to be discarded (weakening).

  • In a linear type system like Ferrite, variables are not allowed to be used more than once (no contraction), and variables are not allowed to be discarded (no weakening).

As we have seen in the previous chapter, Ferrite programs like hello_client interact with channel variables multiple times, with the session type of the channel changing every time after interaction. Under linear typing rules, we cannot make multiple copies of the channel, and we also cannot discard the channel until it is explicitly terminated.

Intuitionistic vs Classical Linear Logic

Since session types cover a family of programming languages, readers with some familiarity with session types may notice that Ferrite's implementation is quite different from some other session types implementations in the wild, such as session-types and sesh.

Ferrite's implementation of session types is based on intuitionistic linear logic. This is in contrast with the classical linear logic formulation that is used by some other session types implementations.

From the programmers' perspective, there are some key differences when using the intuitionistic formulation of session types in Ferrite. For example, you may notice that there is no need for dualization in Ferrite. This means that the session type signature remain the same from the perspective of both the provider and the client.

As illustrated in the previous chapter, while the provider hello_provider sends a string value through a channel with the session type SendValue<String, End>, the client hello_client receives a value from a channel of the same session type.

In comparison, with classical formulation, we would instead have to explicitly dualize the session type. As a result, the session type of the channel given to hello_client would instead have the session type ReceiveValue<String, End>.

Both intuitionistic and classical formulation of session types share the same foundation, viewed from different angles. From the perspective of a type theorist, it may be more convenient to formulate proofs with the help of dualization in the classical formulation.

From the perspective of a programmer, it may be more intuitive to understand session types in the intuitionistic formulation. Intuitionistic session types have closer semantics with lambda calculus, and this makes it easier for programmers to bridge the concepts with their existing knowledge in functional programming.

We leave it to informed readers to decide whether the intuitionistic formulation of Ferrite provides better intuition for programming in session types. For the purpose of this book, it is only important for us to clarify the distinctions, so that readers are better informed when comparing Ferrite with other session types implementations.

Learn More

If you are interested to learn more about session types, there are a wealth of type theoretic resources available. To get started, we recommend the following learning materials by our co-author:

Other than that, the research group ABCD also publishes a comprehensive list of resources related to session types, including a list of session types implementations.

Main Concepts

In this section, we will explore some of the core concepts of Ferrite. The constructs in Ferrite follow closely with the concepts in session types, with some slight differences that will be addressed here.

Protocols

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 Protocol trait. 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 SendValue<String, End> 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 like SendValue<String, i32>, it is not considered by Ferrite to be a protocol. This is because the continuation type i32 does not implement Protocol. Therefore SendValue<String, i32> also does not implement Protocol.

Some protocols also have additional constraints that need to be satisfied. For example, the protocol SendValue<T, A> also requires the Rust value to be send, T, to implement Send and 'static. 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 an i32 value, then sends a bool value, before finally terminating.

Overview of Linear Protocols in Ferrite

We will cover in detail each protocol in the upcoming chapters. Below shows a summary of protocols available in Ferrite:

ProtocolProvider Description
EndTermination
SendValue<T, A>Send a Rust value of type T, and continue as session type A
ReceiveValue<T, A>Receive a Rust value of type T, and continue as session type A
SendChannel<A, B>Send a channel of session type A, and continue as session type B
ReceiveChannel<A, B>Receive a channel of session type A, and continue as session type B
ExternalChoice<Choice>Provide the client with choices defined in Choice
InternalChoice<Choice>Offer a particular choice defined in Choice
Rec<F>Recursive session type, with F being a session type containing recursion markers such as Z.

Linear Context

A Ferrite program offers exactly one protocol, as denoted by the type Session<A>, with A being the provided protocol. For example, when we define our hello_provider program that offers SendValue<String, End>, the type of the program is Session<SendValue<String, End>>. When we implement hello_provider as send_value("Hello World!".to_string(), terminate()), we are implicitly sending the string value "Hello World!" to the offered channel of the protocol SendValue<String, End>.

Although a Ferrite program can only have one offered channel, it can also interact with other Ferrite programs and act as the client of the offered channels. Since there can be more than one client channels available, we need to identify the different channels available using channel variables. So in the case of hello_client, we bind the channel variable a to the client channel of protocol SendValue<String, End>, so that it can receive a string value from the provider.

  let hello_client: Session<ReceiveChannel<Hello, End>> =
    receive_channel(|a| {
      receive_value_from(a, move |greeting| {
        println!("Received greetings from provider: {}", greeting);
        wait(a, terminate())
      })
    });

Type Level List

Ferrite tracks the linear usage of channel variables in a linear context. A linear context is encoded as a Rust type containing zero or more protocols, in the form of a type level list. We can use the HList! macro to define a list of Rust types. For example:

  • HList![] is an empty type level list.
  • HList![String] is a type level list with just one element, String.
  • HList![String, i32, bool] is a type level list containing 3 Rust types: String, i32, and bool.
  • HList![SendValue<String, End>, ReceiveValue<i32, End>, End] is a type level list containing 3 Ferrite protocols: SendValue<String, End>, ReceiveValue<i32, End>, and End.

Behind the scene, the HList! macro desugars a type level list into nested tuples of the form (A0, (A1, (A2, (..., (An, ()))))). This is similar to how linked lists are constructed in Lisp. We start by treating the unit type () as the empty list. To prepend an element A to the front of another list R, we use the tuple constructor (,) to form the new list (A, R), with A being the head of the list and R being the tail of the list. So for example:

  • HList![] desugars to ().
  • HList![String] desugars to (String, ()).
  • HList![String, i32, bool] desugars to (String, (i32, (bool, ()))).
  • HList![SendValue<String, End>, ReceiveValue<i32, End>, End] desugars to (SendValue<String, End>, (ReceiveValue<i32, End>, (End, ()))).

When we encounter compile errors while writing Ferrite programs, we can often see desugared type level lists shown in the error messages. To understand the error messages, we just need to recognize the patterns and think of them as being the same as the pretty printed HList![...] elements.

The Context trait

Ferrite requires linear contexts to implement the Context trait. This is automatically implemented for a type level list, if all its elements implement the Protocol trait. So for example:

  • HList![] is a valid linear context, and it is an empty context.
  • HList![SendValue<String, End>] is a linear context with one protocol, SendValue<String, End>.
  • HList![SendValue<String, End>, ReceiveValue<i32, End>, End] is a linear context, because all 3 elements are valid Ferrite protocols.
  • HList![String, i32, bool] is not a linear context, because none of them are valid Ferrite protocols.
  • HList![SendValue<String, End>, String] is not a linear context, because the second element String is not a Ferrite protocol.
  • HList![SendValue<String, End>, ReceiveValue<i32, i32>] is not a linear context, because the second element ReceiveValue<i32, i32> is not a valid Ferrite protocol.

All Ferrite program has an associated linear context, and a program usually starts with an empty linear context HList![]. For the case of hello_client, in the beginning it also starts with the empty context. When we use receive_channel inside hello_client, a new channel is then added to the linear context in the continuation. As a result, the linear context in the continuation after receive_channel becomes HList![SendValue<String, End>], with the channel variable a referring to the first channel SendValue<String, End>.

Empty Slots

When a Ferrite program has a non-empty linear context, it would have to fully consume all linear channels before it can finally terminate. For the case of hello_client, this would mean that the linear context HList![SendValue<String, End>] has to be fully consumed. We do that by first receiving the value using receive_value_from(a, ...). In the continuation, the linear context would be updated to become HList![End] after the value is received. At this point we would then wait for the channel to terminate using wait(a, ...).

After the channel a is terminated, the original position of the channel in the linear context is updated with a special empty slot called Empty. This is used to indicate that the channel has been fully consumed, and it may be safe for the program to terminate. So in the continuation after wait(a, ...), the linear context is updated to become HList![Empty].

Compared to End, Empty is not a protocol. So we cannot for example define a Ferrite program that offers Empty. However Empty is treated as a valid element in a linear context. So a type level list like HList![Empty, SendValue<String, End>] also implements Context.

Empty Context

When we call terminate(), Ferrite checks whether a linear context is empty using the EmptyContext trait. This trait is implemented if the linear context is an empty list HList![], or if all elements in the linear context is Empty. So HList![], HList![Empty], HList![Empty, Empty], and so on all implement EmptyContext.

When we try to call terminate() with a non-empty linear context, we will get a compile error stating that the type HList![...] does not implement EmptyContext. When encountering such error, we can inspect the list and see which element is not empty, and update our Ferrite program to fully consume the channel accordingly.

Sessions

We have seen that Ferrite programs have the Rust type Session<A>, where the type A must implement the Protocol trait. A Ferrite program of type Session<A> starts with an empty linear context, and offers the protocol A. More generally, it is also possible to define partial Ferrite programs with non-empty linear context. In such cases, these programs would have the Rust type PartialSession<C, A>.

Partial Sessions

A partial Ferrite program of type PartialSession<C, A> have a linear context C which implements Context, and offers the session type A. The linear context C may be non-empty, and if so the partial program must fully consume the linear context before it can terminate.

In the special case when the linear context is empty, the partial program is then equivalent to the full Ferrite program. In fact, the type Session<A> is defined to be a type alias of PartialSession<(), A>, or PartialSession<HList![], A>.

When we write our Ferrite program, the program is actually made of many fragments of PartialSession that are composed together. For example, the program fragment wait(a, terminate()) in hello_client has the Rust type PartialSession<HList![End], End>, and the program fragment receive_value_from(a, wait(a, terminate())) has the Rust type PartialSession<HList![SendValue<String, End>], End>.

Ferrite constructs such as receive_value_from implements the typing rules of how the linear context and the offered protocol should be updated before and after the given Ferrite expression. For example, given that the channel variable a refers to the first element of the linear context, the Rust expression receive_value_from(a, cont) should have the type in the form PartialSession<HList![SendValue<T, A>], B>, and the continuation expression cont should have the Rust type in the form PartialSession<HList![A], B>. i.e. receive_value_from updates the protocol of the first channel in the linear context from SendValue<T, A> to A for any protocol A.

Closed Ferrite Programs

Now that we have learned about PartialSession, a question that might arise is why don't we just define hello_client to have the type PartialSession<HList![ReceiveValue<String, End>], End> instead of Session<ReceiveChannel<ReceiveValue<String, End>, End>>? The reason is because a partial session has free variables that are not captured by the program. Consider the following invalid program:

let hello_client_incorrect
  : PartialSession<HList![ReceiveValue<String, End>], End>
  = receive_value_from(a, move |greeting| {
      println!("Received greetings from provider: {}", greeting);
      wait(a, terminate())
    });

The channel variable a is not defined anywhere, or in other words we have a free variable a, hence the program would not compile. We can think of defining partial sessions directly being equivalent to defining Rust expressions containing free variables such as x + 1. Without the surrounding code, we wouldn't able to know where x is from and whether the expression is valid with a given x. To make such expression to be valid, we would instead define a closure that captures the free variable x, forming the closed expression |x| { x + 1 }.

The same principle also applies to Ferrite programs. In practice, we would write Ferrite programs having the Session type instead of PartialSession so that there are no free channel variables that escape the program.

Channel Selectors

In the code for hello_client, we have seen that the receive_channel construct introduces a new channel variable to our continuation, which we bind to the variable a. The channel variable a is then used in both receive_value_from(a, ...) and wait(a, ...) to access the given channel in the linear context. In this chapter, we will peek a bit into the mechanics of how the channel variables provide access to channels in the linear context.

Context Lenses

Recall from the previous chapter that a linear context has the form HList![A0, A1, ...], with each element implementing Protocol. During the execution of a Ferrite program, the session type of the channels in the linear context will be updated in each step, until the final linear context has the form HList![Empty, Empty, ...] to be safely terminated.

When some Ferrite constructs such as receive_value_from are called, a channel variable needs to be given so that the construct can know which channel in the linear context it should access. Since the linear context is represented as a type level list, the channels are in fact not named in the linear context. Instead, channel variables such as a in hello_client actually have types that implement context lenses to access channels in the linear context by position.

Conceptually, a type N that implements the ContextLens trait provides access to a particular element in the type level list, and update it to a new type. For example in hello_client, the type of a implements ContextLens for accessing the linear contexts HList![SendValue<String, End>], and updates it to HList[End], then finally updates it to HList![Empty].

Type Level Natural Numbers

To define types that implement the ContextLens trait, Ferrite uses type level natural numbers to implement the access to channels in the type level list by the corresponding position. A type level natural number starts with the type Z, which corresponds to the number 0. Following that, we have the type S<Z>, which means the successor of Z, to correspond to the number 1. Similarly, we have S<S<Z>> corresponding to the successor of 1, which is 2, and so on. So we have the types Z, S<Z>, S<S<Z>>, S<S<S<Z>>>, ... corresponding to the number sequence 0, 1, 2, 3, ...

For each of the type level natural numbers, Ferrite implements the ContextLens trait for accessing channels at the corresponding zero-indexed position in the linear context. So for example:

  • The type Z can update any linear context in the form HList![A0, ...] to HList![B, ...], with the first element A0 replaced with B and the remaining elements unchanged.

  • The type S<Z> can update any linear context in the form HList![A0, A1, ...] to HList![A0, B, ...], with the second element A1 replaced with B and the remaining elements unchanged.

  • The type S<S<Z>> can update any linear context in the form HList![A0, A1, A2, ...] to HList![A0, A1, B, ...], with the third element A3 replaced with B and the remaining elements unchanged.

As demonstration, we can deduce that the channel variable a in hello_client has the type Z, because there is only one channel in the linear context and it is the one that we are interested in. Z implements the ContextLens for updating the first element in any linear context. So receive_channel_from can use Z to update the linear context from HList![ReceiveValue<String, End>] to HList![End], and it can also use Z to update the linear context from HList![End] to HList![Empty].

The ContextLens Trait

The full definition of the ContextLens trait is in the form ContextLens<C1, A, B, Target=C2>. It means that a type N that implements ContextLens<C1, A, B, Target=C2> provides the operation to access a channel of session type A that can be found in C1, update it to B, and result in the new context C2. This can be elaborated with the implementations by the natural numbers:

  • Z: ContextLens<HList![A0, ...], A0, B, Target=HList![B, ...]>

  • S<Z>: ContextLens<HList![A0, A1, ...], A0, B, Target=HList![A0, B, ...]>

  • S<S<Z>>: ContextLens<HList![A0, A1, A2,...], A0, B, Target=HList![A0, A1, B, ...]>

Following the above template, we can know that in the case of hello_client, the type Z does implements the required ContextLens traits:

  • Z: ContextList<
      HList![ReceiveValue<String, End>],
      ReceiveValue<String, End>,
      End,
      Target=HList![End]>

  • Z: ContextList<
      HList![End],
      End,
      Empty,
      Target=HList![Empty]>

Writing Partial Ferrite Programs

Now that we know how context lenses are actually implemented, it would in fact be possible for us to write partial Ferrite programs of type PartialSession, by hard coding the specific context lenses to access the channels in the linear context. For example, we could have written a partial version of hello_client as follows:

  let hello_client_partial: PartialSession<
    HList![SendValue<String, End>],
    End,
  > = receive_value_from(Z, move |greeting| {
    println!("Received greetings from provider: {}", greeting);
    wait(Z, terminate())
  });

While writing such program is possible, the code is not ergonomic and is generally not recommended. This is because we are hardcoding the position of the channels in the linear context, instead of using meaningful identifiers. This would also reduce readability and makes it more difficult to add or remove channels to the program.

This style of programming using the position is similar to programming using De Bruijn index. While this is useful for internal implementation, we as programmers tend to prefer using named variables to improve readability and better structure our code.

Type Errors Using Context Lenses

When we write Ferrite programs that contain invalid access to channels in the linear context, we may get compile errors showing that types like Z do not implement a particular context lens. As an example, consider the following incorrect version of hello_client that tries to send a value to a instead of receiving from it:

let hello_client_incorrect
  : Session<ReceiveChannel<SendValue<String, End>, End>>
  = receive_channel(|a| {
      send_value_to(a, "Hello World!".to_string(),
        wait(a, terminate()))
    });

If we try to compile the program, we would get an error message similar to the following:

error[E0277]: the trait bound `Z: ContextLens<(SendValue<String, End>, ()), ReceiveValue<String, _>, _>` is not satisfied
   |
20 |     send_value_to(a, "Hello World!".to_string(),
   |     ^^^^^^^^^^^^^ the trait `ContextLens<(SendValue<String, End>, ()), ReceiveValue<String, _>, _>` is not implemented for `Z`
   |
   |
49 |   N: ContextLens<C, ReceiveValue<T, B>, B>,
   |      ------------------------------------- send_value_to`
   |
   = help: the following implementations were found:
             <Z as ContextLens<(A1, C), A1, A2>>

The key meaning for the error message above is that the type Z does not implement ContextLens<HList![SendValue<String, End>], ReceiveValue<String, End>, End>. This is because although Z implements access to the first element of any non-empty linear context, the first element in the linear context of hello_client has the protocol SendValue<String, End>, but the call to send_value_to(a, ...) requires the first element of the linear context to have the protocol ReceiveValue<String, End>.

Error messages such as above may be difficult to understand for readers who are new to Ferrite. But hopefully with some exercise, we should be able to get familiar with the error message and understand the meaning behind them.

Running Sessions

When we define a Ferrite program with Rust expressions like let program: Session<...> = ..., the program is not executed until we run it at a later time. Ferrite provides two public functions, run_session and run_session_with_result to execute the Ferrite programs.

run_session

async fn run_session(session: Session<End>)

run_session is an async function that accepts a Ferrite program of type Session<End>, and blocks until the program has finished executed.

Since run_session requires the offered protocol to be End, this means that we cannot use it to execute Ferrite programs that offer other protocols, such as ReceiveValue<String, End>. Intuitively, this is because Ferrite cannot know in general how to run Ferrite programs offering any protocol. For instance, how are we supposed to finish run a Ferrite program that offers ReceiveValue<String, End>, if we do not have any string value to send to it?

apply_channel

fn apply_channel<A: Protocol, B: Protocol>(
  f: Session<ReceiveChannel<A, B>>,
  a: Session<A>,
) -> Session<B>

While we cannot execute Ferrite programs offering protocols other than End, we can link that Ferrite program with another program so that as a whole, the resulting Ferrite would offer the protocol End. We have seen one such example of linking hello_provider with hello_client using apply_channel in the previous chapter.

In general, if we have a provider that offers the protocol A, and a client that offers the protocol ReceiveChannel<A, B>, we can call apply_channel(client, provider) to get a new program that would spawn the provider, and forwards the offered channel to the client.

include_session

When we have a Ferrite program that offers protocols like ReceiveValue<i32, End>, we could also write another program that include the first program directly using include_session and interacts with it. This allows us to write new Ferrite programs that offer End if we knows how to interact with the original program.

As an example, consider a show_number program that receives an integer and then prints out the value it receives:

  let show_number: Session<ReceiveValue<i32, End>> = receive_value(|x| {
    println!("The magic number is: {}", x);
    terminate()
  });

We cannot run show_number directly, because it expects an integer to be sent to it. But we can now write a main program that includes show_number as follows:

  let main: Session<End> = include_session(show_number, |chan| {
    send_value_to(chan, 42, wait(chan, terminate()))
  });

  run_session(main).await;

We call include_session by passing it the original show_number program that we want to include. We also pass it a continuation closure, which gives us a channel variable chan that binds to the channel offered by show_number. We then sends the number 42 to chan, wait for it to terminate, and then terminate main.

Because the protocol offered by main is End, we can now run the full program using run_session.

run_session_with_result

async fn run_session_with_result<T: Send + 'static>(
  session: Session<SendValue<T, End>>
) -> T

Although in general Ferrite can only run programs offering End, there is another special case that Ferrite knows how to handle, which is programs that offer protocol in the form SendValue<T, A>. In this case, Ferrite knows to receive the value sent by the program, then wait for the program to terminate before returning the received value to the caller.

It is often more practical to use run_session_with_result instead of run_session, because we may want to write Rust programs that spawn Ferrite processes, then wait for some result to return.

We have seen an example use of run_session_with_result with the hello provider, which we get back the result "Hello World!" string sent by the Ferrite program.

Hole Driven Development

Just like learning any new programming language, it may be overwhelming to write your first session type program in Ferrite. To help you unstuck when encountering compile errors, we encourage the use of typed holes to discover what is needed to complete your program.

The use of typed holes are common in languages like Haskell, Agda, and Idris. In Rust, there isn't officially support for using typed holes, but we can somewhat emulate the feature using techniques described in this chapter.

Todo Placeholder

Suppose we are a total beginner again, and we want to write our first hello world provider. We start by defining the session type we want, which is SendValue<String, End>, and we can then write down the outline for our Ferrite program as follows:

let hello_provider: Session<SendValue<String, End>> = todo!();

The todo! macro allows us to put a placeholder in unfinished Rust code so that we can try and compile the code and see if there is any type error. By writing our code step by step and filling the blank with todo!(), we can narrow down the potential places where our code is incorrect.

At this stage, we should be able to compile our program with no error. This shows that the protocol that we have defined, SendValue<String, End>, is a valid session type. If we have gotten a compile error otherwise, it could have been caused by us trying to write an invalid protocol like SendValue<String, String>.

When using todo!(), the Rust compiler might emit warnings about unreacheable code. Since we are still writing our program, we can add the #![allow(unreachable_code)] pragma to disable the warning temporarily until we finish writing the code.

Unit Placeholder

Now that we have defined the outline, we can move to the next step and try to write the first step. By looking at the first part SendValue<String, ...>, we know that we have to send a string value. But we might not know what should be done after sending the value, so we could write something like follows:

let hello_provider: Session<SendValue<String, End>> =
  send_value("Hello World!".to_string(), todo!());

We can try to compile our code again, and Rust will accept the code we have written. However the use of todo!() does not tell us how we should continue our program. In languages like Haskell, we could have used _ instead of todo!(), and GHC would tell us what should be the type of the expression in the hole. In Rust, we would instead use the unit type () to deliberately cause a compile error:

let hello_provider: Session<SendValue<String, End>> =
  send_value("Hello World!".to_string(), ());

Now if we compile our code, we would get a compile error from Rust that looks like follows:

error[E0308]: mismatched types
 |
 |       send_value("Hello World!".to_string(), ());
 |                                              ^^ expected struct `PartialSession`, found `()`
 |
 = note: expected struct `PartialSession<(), End>`
         found unit type `()`

With this compile error, we can know that we are supposed to fill in the hole with Rust expression that has the type PartialSession<(), End>, or Session<End>.

Sometimes we may also intuitively think of a type that should be in a hole. In such case, we can also use the todo!() as T pattern to verify if our intuition is correct. So we can for example write:

let hello_provider: Session<SendValue<String, End>> =
  send_value("Hello World!".to_string(), todo!() as Session<End>);

And our code will compile successfully. If we were to annotate it with an invalid type, such as todo()! as Session<ReceiveValue<String, End>> again, Rust will also return a compile error.

Now that we know the continuation needs to have the type Session<End>, we can then fill in the blank with terminate() and complete our program.

Underscores

Now that we have finished hello_provider, we can try implementing hello_client once again. Supposed we know that the first expression to match ReceiveChannel<...> is receive_channel, but we don't know what would be in the linear context, we can write our program as follows:

let hello_client: Session<ReceiveChannel<SendValue<String, End>, End>> =
  receive_channel(move |a| {
    todo!() as PartialSession<HList![_], End>
  });

The code above will still compile successfully with Rust, so we know that in our continuation, we have one element in the linear context as denoted by HList![_], but we don't yet know what it is. Rust allows us to use _ as a wildcard in places where it can infer the type, such as the case when we use it in todo!() as .... Using this technique, we can also slowly narrow down our type definition and not get overwhelmed by an overly long error message.

Now we can try and fill in the _ with a bogus protocol like End and see what happens:

let hello_client: Session<ReceiveChannel<SendValue<String, End>, End>> =
  receive_channel(move |a| {
    todo!() as PartialSession<HList![End], End>
  });

Now if we try to compile our program again, we would get a compile error that looks like follows:

error[E0271]: type mismatch resolving `<() as AppendContext<(SendValue<String, End>, ())>>::Appended == (End, ())`
 |
 |       receive_channel(move |a| {
 |       ^^^^^^^^^^^^^^^ expected struct `SendValue`, found struct `End`
 |
 = note: expected type `(SendValue<String, End>, ())`
           found tuple `(End, ())`

The key information is in the last two lines, which states that there is a type mismatch between the expected type (SendValue<String, End>, ()) and the actual type (End, ()). Recall from previous chapter that this is the desugared versions of the expected list HList![SendValue<String, End>] and the actual list HList![End]. Using this information, we are able to fill in the correct type for our hole:

let hello_client: Session<ReceiveChannel<SendValue<String, End>, End>> =
  receive_channel(move |a| {
    todo!() as PartialSession<HList![SendValue<String, End>], End>
  });

When writing complex session type programs, we can also use _ in places where we do not care about the actual type. For example, we may be interested to know whether the there is one channel in the linear context in the form SendValue<String, ...>. In that can we can also write our code as follows:

let hello_client: Session<ReceiveChannel<SendValue<String, End>, End>> =
  receive_channel(move |a| {
    todo!() as PartialSession<HList![SendValue<String, _>], _>
  });

Now that we know the first session type in the linear context is in the form SendValue<String, ...>, we can attempt to write the next part of our program. However suppose that we forgot that the behavior of protocols is inverted on the client side, we may try to write a program that sends a value to channel a instead of receiving from it:

let hello_client: Session<ReceiveChannel<SendValue<String, End>, End>> =
  receive_channel(move |a| {
    send_value_to(a, "Hello World!".to_string(), todo!())
  });

If we try to compile the code, we would get an error such as follows, which is the same error as previously described:

error[E0277]: the trait bound `Z: ContextLens<(SendValue<String, End>, ()), ReceiveValue<String, _>, _>` is not satisfied
 |
 |         send_value_to(a, "Hello World!".to_string(), todo!())
 |         ^^^^^^^^^^^^^ the trait `ContextLens<(SendValue<String, End>, ()), ReceiveValue<String, _>, _>` is not implemented for `Z`
 |

With the help of todo!(), we are able to spot the type errors in our program before finish writing the whole program. It saves us the effort of figuring out what to fill in the blank inside send_value_to(a, "Hello World!".to_string(), ...), as our program is incorrect anyway.

Comment

Sometimes we may have written too much code, and by the time we try to compile our program, we get a big list of compile errors that are difficult to decipher. In such case, it may be helpful to comment out part of our Ferrite program and replace them with todo!(), to find out the initial place where the error occured.

For example, suppose we finished writing the wrong implementation of hello_client, we can debug our code by commenting out the code to become something like:

let hello_client: Session<ReceiveChannel<SendValue<String, End>, End>> =
  receive_channel(move |a| {
    todo!()
    // send_value_to(a, "Hello World!".to_string(),
    //   wait(a, terminate()))
  });

If we build our program at this step, the compilation will be successful again. We can then move forward to the next step of our program while still commenting out the remaining part:

let hello_client: Session<ReceiveChannel<SendValue<String, End>, End>> =
  receive_channel(move |a| {
    send_value_to(a, "Hello World!".to_string(),
      todo!())
    //   wait(a, terminate()))
  });

At this step, we would then get a compile error. We can then know that the cause of the error is from our use of send_value_to, and is unaffected by the remaining expression wait(a, terminate()) because they have been commented out and replaced with todo!().

Rust IDE

When developing Ferrite programs, it may be helpful to use Rust IDEs such as Rust Analayzer. The IDE would show the hints on the types of the variables and functions. Using and IDE, we can for example easily see that the type of channel variables, such as a in hello_client has the type Z. This can be useful especially for beginners, who may be unfamiliar with the various types defined in Ferrite.

Ferrite Constructs

This section contains draft definitions of all linear Ferrite constructs. Detailed explanation will be added at a later time.

Termination

Provider Rule: Terminate

fn terminate<C>() -> PartialSession<C, End>
  • C must be an empty linear context that implements EmptyContext. e.g:
    • HList![]
    • HList![Empty]
    • HList![Empty, Empty, ...]

Example:

    let p: Session<End> = terminate();

Client Rule: Wait

fn wait<N, C1, C2, A>(
  n: N,
  cont: PartialSession<C2, A>
) -> PartialSession<C1, A>
  • C1 is in the form HList[…, N: End, …].
  • C2 is in the form HList[…, N: Empty, …] with the remaining elements in C1 unchanged.

Example:

    let p: Session<ReceiveChannel<End, End>> =
      receive_channel(move |c| wait(c, terminate()));

Client Rule: Wait All

macro wait_all! <C1, C2, B> (
  [$channels],
  $cont: PartialSession<C2, B>
) -> PartialSession<C1, B>
  • Expands wait_all!([c1, c2, …], cont) to wait(c1, wait(c2, … cont).

Example:

    let p: Session<ReceiveChannel<End, ReceiveChannel<End, End>>> =
      receive_channel(move |c1| {
        receive_channel(move |c2| wait_all!([c1, c2], terminate()))
      });

Forward

fn forward<N, C, A>(n: N) -> PartialSession<C, A>
  • C is in the form HList![…, N: A, …] with the remaining elements being Empty.

Example:

  let p: Session<
    ReceiveChannel<ReceiveValue<String, End>, ReceiveValue<String, End>>,
  > = receive_channel(move |c| forward(c));

Include Session

fn include_session<N, C1, C2, A, B>(
  session: Session<A>,
  cont: impl FnOnce(N) -> PartialSession<C2, B>,
) -> PartialSession<C1, B>
  • N is the length of C1.
  • C1 is in the form HList![0: A0, 1: A1, ...]
  • C2 is in the form HList![0: A0, 1: A1, ..., N: A], with A appended to the end of C1 and the remaining elements unchanged.

Example

    let p1: Session<End> = terminate();
    let p2: Session<End> = include_session(p1, move |c| wait(c, terminate()));

Apply Channel

fn apply_channel<A, B>(
  f: Session<ReceiveChannel<A, B>>,
  a: Session<A>,
) -> Session<B>

Example:

    let p1: Session<ReceiveValue<String, End>> = todo!();

    let p2: Session<
      ReceiveChannel<ReceiveValue<String, End>, SendValue<u64, End>>,
    > = todo!();

    let p3: Session<SendValue<u64, End>> = apply_channel(p2, p1);

Step

fn step<C, A>(
  cont: impl Future< Output = PartialSession<C, A>>
) -> PartialSession<C, A>
  • Wraps an async block yielding a PartialSession.

Example:

  use std::time::Duration;

  use tokio::time::sleep;

  let p: Session<End> = step(async move {
    sleep(Duration::from_secs(1)).await;
    terminate()
  });

Run Session

async fn run_session(session: Session<End>)
  • Evaluates a Session<End> and blocks until the process terminates.

Example:

    let p: Session<End> = step(async move {
      sleep(Duration::from_secs(3)).await;
      println!("Hello World!");
      terminate()
    });

    run_session(p).await;

Run Session With Result

async fn run_session_with_result<T>(
  session: Session<SendValue<T, End>>
) -> T
  • Evaluates a Session<SendValue<T, End>> and blocks until the process terminates
  • Returns the result sent by the process

Example:

    let p: Session<SendValue<String, End>> = step(async move {
      sleep(Duration::from_secs(3)).await;
      send_value("Hello World!".to_string(), terminate())
    });

    let res = run_session_with_result(p).await;
    println!("{}", res);

Receive Value

Provider Rule: Receive Value

fn receive_value<T, C, A>(
  cont: impl FnOnce(T) -> PartialSession<C, A>
) ->
  PartialSession<C, ReceiveValue<T, A>>
  • T: Send + 'static, i.e. T must not contain borrowed reference and is safe to be shared across threads.

Example

    let greeter: Session<ReceiveValue<String, End>> =
      receive_value(move |name| {
        println!("Hello, {}!", name);
        terminate()
      });

Client Rule: Send Value To

fn send_value_to<N, C1, C2, A, B, T>(
  n: N,
  val: T,
  cont: PartialSession<C2, B>,
) -> PartialSession<C1, B>
  • C1 is in the form HList[…, N: ReceiveValue<T, A>, …].
  • C2 is in the form HList[…, N: A, …], with the remaining elements unchanged.

Example:

    let p: Session<ReceiveChannel<ReceiveValue<u64, End>, End>> =
      receive_channel(move |c| send_value_to(c, 42, wait(c, terminate())));

Send Value

Provider Rule: Send Value

fn send_value<T, C, A>(
  val: T,
  cont: PartialSession<C, A>,
) ->
  PartialSession<C, SendValue<T, A>>

Example

    let p: Session<SendValue<String, End>> =
      send_value("Hello World!".to_string(), terminate());

Client Rule: Receive Value From

fn receive_value_from<N, C1, C2, T, A, B>(
  n: N,
  cont: impl FnOnce(T) -> PartialSession<C2, B>,
) -> PartialSession<C1, B>
  • C1 is in the form HList[…, N: SendValue<T, A>, …].
  • C2 is in the form HList[…, N: A, …], with the remaining elements being the same as C1.

Example

    let p: Session<ReceiveChannel<SendValue<String, End>, End>> =
      receive_channel(move |c| {
        receive_value_from(c, move |name| {
          println!("Hello, {}!", name);
          wait(c, terminate())
        })
      });

Receive Channel

Provider Rule: Receive Channel

fn receive_channel<N, C1, C2, A, B>(
  cont: impl FnOnce(N) -> PartialSession<C2, B>
) -> PartialSession<C1, ReceiveChannel<A, B>>
  • N is the length of C1.
  • C1 is in the form HList![0: A0, 1: A1, ...]
  • C2 is in the form HList![0: A0, 1: A1, ..., N: A], with A appended to the end of C1 and the remaining elements unchanged.

Example

    let p: Session<ReceiveChannel<End, End>> =
      receive_channel(move |c| wait(c, terminate()));

Client Rule: Send Channel To

fn send_channel_to <N, M, C1, C2, A1, A2, B>(
  n: N, m: M,
  cont: PartialSession<C2, B>,
) -> PartialSession<C1, B>
  • C1 is in the form HList[…, N: ReceiveChannel<A1, A2>, … M: A1, …]
  • C2 is in the form HList[…, N: A2, …, M: Empty, …], with the remaining elements being same as C1.
  • M may come before N.

Example

    let p1: Session<ReceiveValue<String, End>> = todo!();

    let p2: Session<ReceiveChannel<ReceiveValue<String, End>, End>> = todo!();

    let p3: Session<End> = include_session(p1, move |c1| {
      include_session(p2, move |c2| {
        send_channel_to(c2, c1, wait(c2, terminate()))
      })
    });

Send Channel

Provider Rule: Send Channel From

fn send_channel_from<N, C1, C2, A, B>(
  n: N,
  cont: PartialSession<C2, B>,
) -> PartialSession<C1, SendChannel<A, B>>
  • C1 is in the form HList[…, N: A, …].
  • C2 is in the form HList[…, N: Empty, …], with the remaining elements being same as in C1.

Example

    let p1: Session<SendValue<String, End>> = todo!();

    let p: Session<SendChannel<SendValue<String, End>, End>> =
      include_session(p1, move |c| send_channel_from(c, terminate()));

Client Rule: Receive Channel From

fn receive_channel_from<C1, C2, N, M, A1, A2, B>(
  n: N,
  cont: impl FnOnce(M) -> PartialSession<C2, B>,
) -> PartialSession<C1, B>
  • M is the length of C1.
  • C1 is in the form HList[…, N: SendChannel<A1, A2>, …].
  • C2 is in the form HList[…, N: A2, …, M: A1], with all elements in C1 except slot N unchanged, and have M appended to the end.

Example

    let p: Session<
      ReceiveChannel<SendChannel<ReceiveValue<String, End>, End>, End>,
    > = receive_channel(move |c1| {
      receive_channel_from(c1, move |c2| {
        send_value_to(
          c2,
          "Hello World!".to_string(),
          wait_all!([c1, c2], terminate()),
        )
      })
    });

Binary External Choice

Provider Rule: Offer Choice

macro offer_choice! <C, A, B> {
  Left => $expr: PartialSession<C, A>,
  Right => $expr: PartialSession<C, B>,
} ->
  PartialSession<C, ExternalChoice<Either<A, B>>>

Example

    use ferrite_session::{
      either::*,
      prelude::*,
    };

    let p: Session<
      ExternalChoice<Either<ReceiveValue<String, End>, SendValue<u64, End>>>,
    > = offer_choice! {
      Left =>
        receive_value(move |name| {
          println!("Hello, {}!", name);
          terminate()
        })
      Right =>
        send_value(42, terminate())
    };

Client Rule: Choose Left

macro choose! <N, C1, C2, A1, A2, B> (
  n: N, Left,
  cont: PartialSession<C2, B>
) ->  PartialSession<C1, B>
  • C1 is in the form HList[…, N: ExternalChoice<Either<A1, A2>>, …]
  • C2 is in the form HList[…, N: A1, …], with the remaining elements being the same as in C1.

Example

    let p: Session<
      ReceiveChannel<
        ExternalChoice<Either<ReceiveValue<String, End>, SendValue<u64, End>>>,
        End,
      >,
    > = receive_channel(move |c| {
      choose!(
        c,
        Left,
        send_value_to(c, "Hello World!".to_string(), wait(c, terminate()))
      )
    });

Client Rule: Choose Right

macro choose! <N, C1, C2, A1, A2, B> (
  $n: N, Right,
  $cont: PartialSession<C2, B>
) ->  PartialSession<C1, B>
  • C1 is in the form HList[…, N: ExternalChoice<Either<A1, A2>>, …]
  • C2 is in the form HList[…, N: A2, …], with the remaining elements being the same as in C1.

Example

    let p: Session<
      ReceiveChannel<
        ExternalChoice<Either<ReceiveValue<String, End>, SendValue<u64, End>>>,
        End,
      >,
    > = receive_channel(move |c| {
      choose!(
        c,
        Right,
        receive_value_from(c, move |x| {
          println!("{}", x);
          wait(c, terminate())
        })
      )
    });

Binary Internal Choice

Provider Rule: Offer Left

macro offer_case! <C, A, B> (
  Left,
  $cont: PartialSession<C, A>
) ->
  PartialSession<C, InternalChoice<Either<A, B>>>

Example

    let p: Session<
      InternalChoice<Either<ReceiveValue<String, End>, SendValue<u64, End>>>,
    > = offer_case!(
      Left,
      receive_value(move |name| {
        println!("Hello, {}!", name);
        terminate()
      })
    );

Provider Rule: Offer Right

macro offer_case! <C, A, B> (
  Right,
  $cont: PartialSession<C, B>
) ->
  PartialSession<C, InternalChoice<Either<A, B>>>

Example

    let p: Session<
      InternalChoice<Either<ReceiveValue<String, End>, SendValue<u64, End>>>,
    > = offer_case!(Right, send_value(42, terminate()));

Client Rule: Case

macro case! <N, C1, C2, C3, A1, A2, B> {
  $n: N;
  Left => $cont1: PartialSession<C2, B>,
  Right => $cont1: PartialSession<C3, B>,
} ->
  PartialSession<C1, B>
  • C1 is in the form HList[…, N: InternalChoice<Either<A1, A2>>, …].
  • C2 is in the form HList[…, N: A1, …], with the remaining elements being the same as in C1.
  • C3 is in the form HList[…, N: A2, …], with the remaining elements being the same as in C1.

Example

    let p: Session<
      ReceiveChannel<
        InternalChoice<Either<ReceiveValue<String, End>, SendValue<u64, End>>>,
        End,
      >,
    > = receive_channel(move |c| {
      case! { c;
        Left =>
          send_value_to(c,
            "Alice".to_string(),
            wait(c, terminate())),
        Right =>
          receive_value_from(c, move |x| {
            println!("{}", x);
            wait(c, terminate())
          })
      }
    });

N-ary Choice

macro define_choice! {
  $choice ;
  $label1: $protocol1,
  $label2: $protocol2,
  ...
}

  • Define N branches of labeled choices

  • Choices are in the form { L0: A0, L1: A1, ... } are desugard into HList![A0, A1, ...].

  • Labeled are defined as type aliases to prisms, e.g.

    type L0 = Z;
type L1 = S<Z>;
...

Example: Either

define_choice! { Either<A, B>;
  Left: A,
  Right: B,
}

Example

define_choice! { MyChoices;
  Foo: ReceiveValue<String, End>,
  Bar: SendValue<u64, End>,
  Baz: End,
}

Recursive Session Types

Provider Rule: Fix Session

fn fix_session<C, A1, A2>(
  cont: PartialSession<C, A2>
) -> PartialSession<C, Rec<A1>>
  • For a protocol A = Rec<A1>, A1 contains recursion points back to A marked with Z.
  • A2 is A1 with Z replaced by Rec<A1>.

Example

fn counter(val: u64) -> Session<Rec<SendValue<u64, Z>>>
{
  fix_session(send_value(val, counter(val + 1)))
}

For a equi-recursive definition A = SendValue<u64, A>:

  • A1 = SendValue<u64, Z>
  • A2 = SendValue<u64, Rec<SendValue<u64, Z>>>

Client Rule: Unfix Session

fn unfix_session<N, C1, C2, A1, A2, B>(
  n: N,
  cont: PartialSession<C2, B>,
) -> PartialSession<C1, B>
  • C1 is in the form HList[…, N: Rec<A1>, …]
  • C2 is in the form HList[…, N: A2, …], with the remaining elements being the same as in C1.

Example

fn counter_client() -> Session<ReceiveChannel<Rec<SendValue<u64, Z>>, End>>
{
  receive_channel(move |c1| {
    unfix_session(
      c1,
      receive_value_from(c1, move |x| {
        println!("{}", x);
        include_session(counter_client(), move |c2| {
          send_channel_to(c2, c1, forward(c2))
        })
      }),
    )
  })
}

Shared Session Types

This section contains draft definitions of all shared Ferrite constructs. Detailed explanation will be added at a later time.

Shared Provider

Accept Shared Session

fn accept_shared_session<A1, A2>(
  cont: Session<A2>
) -> SharedSession<LinearToShared<A1>>
  • For a shared protocol S = LinearToShared<A1>, A1 contains recursion points back to SharedToLinear<S> marked with Release.
  • A2 is A1 with Release replaced by SharedToLinear<LinearToShared<A1>>
  • Equi-synchronizing constraint applies, i.e. must use Release instead of End
  • Returns a SharedSession instead of PartialSession

Example

Consider an equi-recursive definition

S = LinearToShared<SendValue<u64, SharedToLinear<S>>>
  • A1 = SendValue<u64, Release>
  • A2 = 
    SendValue<u64,
  LinearToShared<
    SharedToLinear<
      SendValue<u64, Release>>>

Detach Shared Session

fn detach_shared_session<A>(
  cont: SharedSession<LinearToShared<A>>
) -> Session<SharedToLinear<A>>
  • Continuation is a SharedSession instead of PartialSession
  • Returns a Session with empty linear context.

Example

fn shared_counter(
  count: u64
) -> SharedSession<LinearToShared<SendValue<u64, Release>>>
{
  accept_shared_session(send_value(
    count,
    detach_shared_session(shared_counter(count + 1)),
  ))
}

Shared Forward

fn shared_forward<A, C>(
  channel: SharedChannel<LinearToShared<A>>
) -> PartialSession<C, SharedToLinear<A>>
  • Forward all subsequent shared acquires to another shared process connected to the given shared channel

Run Shared Session

fn run_shared_session<S>(
  session: SharedSession<S>
) -> SharedChannel<S>
  • Just like PartialSession, SharedSession is an unevaluated shared session type program.
  • run_shared_session evaluates a SharedSession and returns SharedChannel, a cloneable handle to communicate with the spawned shared process.

Example

  let counter_channel = run_shared_session(shared_counter(0));

Client for Shared Channels

Acquire Shared Session

fn acquire_shared_session<N, C1, C2, A1, A2, B>(
  shared: SharedChannel<LinearToShared<A1>>,
  cont: impl FnOnce(N) -> PartialSession<C2, B>,
) -> PartialSession<C1, B>

Example

Consider an equi-recursive definition

S = LinearToShared<SendValue<u64, SharedToLinear<S>>>
  • A1 = SendValue<u64, Release>
  • C1 = HList![…]
  • N is the length of C1.
  • C2 = HList![…,
  N: SendValue<u64,
      LinearToShared<
        SharedToLinear<
          SendValue<u64, Release>
        >>]

Release Shared Session

fn release_shared_session<N, C1, C2, A, B>(
  n: N,
  cont: PartialSession<C2, B>,
) -> PartialSession<C1, B>

Example

Consider an equi-recursive definition

S = LinearToShared<SendValue<u64, SharedToLinear<S>>>
  • A1 = SendValue<u64, Release>
  • C1 = HList![…,
  N: LinearToShared<
      SharedToLinear<
        SendValue<u64, Release>
      >>,
  …]
  • C2 = HList![…, N: Empty, …]

Example Client

fn shared_counter_client(
  counter: SharedChannel<LinearToShared<SendValue<u64, Release>>>
) -> Session<End>
{
  acquire_shared_session(counter, move |c| {
    receive_value_from(c, move |x| {
      println!("{}", x);
      release_shared_session(c, terminate())
    })
  })
}