FreeST Sharing is caring
Table of contents
You’ve come far in FreeST, you’ve used channels in many different ways but you ask yourself “Can I connect more than two processes with linear channels?”, and the answer is a reluctant “Yes, but…”. Linear channels are expressive but can only connect two participants.
One way to implement one-to-many, many-to-one or even many-to-many communication is to use lists of channel ends and iterate through them as needed. This solution works only when the number of clients and servers is fixed and known à priori. But even in this case the solution looks simpler than it is. Reading on a FreeST’s channel is a blocking operation, and thus, reading values from a list of channels may become a slow sequential operation if writers are not ready.
To fulfil the use-cases left open by linear channels, FreeST offers unrestricted, or shared, channels. Shared channels are simpler in their types but they can be copied and used (or not) by as many processes as needed. The most important aspect of shared channels for you to remember is shared channels are stateless, they offer the same behaviour forever.
We can express a shared integer stream from the point of view of the reader as *?Int. Many processes can receive from this channel as long as there are processes on the other side available to send integer values.
There are four shared session types at your disposal:
*?T
*!T
*+{l, ..}
*&{l, ..}
Why do choices have no continuation? You might ask. Because shared session types offer the same behaviour forever, and the choice by itself is the behaviour offered. There cannot be a continuation different from the choice itself.
Reading and Writing on Shared Channels
Let us a consider the type of a stream of integer values as seen from the producer side.
type IntStream = *!Int
To produce an unbounded number of integers n on an IntStream channel end one may write:
produce : Int -> IntStream -> Diverge
produce n p = p |> send n |> produce n
Type Diverge is a mark for functions that do not terminate; it is defined as ().
To consume a stream and print its values we may write:
consume : dualof IntStream -> Diverge
consume c =
let (x, c') = receive c in
print @Int x;
consume c'
In all cases (linear or unrestricted) variables c and c' denote the same channel end. When c is of a linear type the type of c' may differ from that of c. But unrestricted types offer an uniform behaviour, so that one may write instead:
consume : dualof IntStream -> Diverge
consume c =
let (x, _) = receive c in
print @Int x;
consume c
In order to simplify reading from shared channels, FreeST offers function receive_ that discards the channel from the pair and returns the value read. One can then write:
consume : dualof IntStream -> Diverge
consume c =
c |> receive_ @Int |> print @Int ;
consume c
We can then write a simple program that consumes and prints numbers from two producers:
main : Diverge
main =
let c = forkWith @IntStream @() consume in
fork (\_: () -> produce 1 c);
produce 2 c
Discarding Shared Channels
Linear channels cannot be discarded; they must be used until the end, that is Close or Wait depending on the point of view (if they terminate at all). Shared channels on the other hand may be discarded at any time. This program creates a channel that it never uses.
main : (IntStream, dualof IntStream)
main =
new @IntStream ()
Notice that shared channels can never be closed even if they are not used.
A more interesting example consumes a finite number of values from an integer stream. The result is the sum of the numbers read.
consume : Int -> dualof IntStream -> Int
consume n c =
if n == 0
then 0
else receive_ @Int c + consume (n - 1) c
The main function is now composed of two infinite producers and one finite consumer.
main : Int
main =
let (p, c) = new @IntStream () in
fork (\_: () 1-> produce 1 p);
fork (\_: () 1-> produce 2 p);
consume 5 c
We have also rearranged the code in such a way that consume runs on the main thread, so that the program may terminate once the five values are read. The program should print a number between 5 and 10.
Session initiation
If shared channels are more practical than linear ones, why bother with linear channels? Well, you can’t serialize a tree directly on a shared channel for example. Shared channels lack the capacity of expressing interesting protocols.
The trick with shared channels is to use them not as a single communication point, but as a rendez-vous point to establish more complex communication in a linear channel by exchanging endpoints. We call this process session initiation.
Let’s think of a very useful case in programming, a shared data structure, in this case a single memory cell.
type Cell = +{ Read: ?Int
, Write: !Int
}; Close
The Cell session type describes our possible interaction with an Int memory cell.
type SharedCell = *?Cell
The SharedCell type describes a channel on which a client can receive another channel with the Cell type. An example of a client that writes to the cell is:
cellClient : SharedCell -> ()
cellClient c =
c |> receive_ @Cell -- acquire a linear channel
|> select Write -- interact on the linear channel
|> send 5
|> close
However, it is the server that bears the important part of session initiation: to create the new channel and send one of its ends. To aid session initiation, FreeST offers the accept function which creates the channel endpoints, sends one to the client and returns the other. Taking advantage of pattern-matching on external choice types, we may thus write:
cellServer : dualof SharedCell -> ()
cellServer c = serve $ accept @Cell c
serve : dualof Cell -> ()
serve (Read s) = s |> send 0 |> wait
serve (Write s) = receiveAndWait @Int s ; ()
To use a single function we may use the match-with destructor for external choice types. The match returns the continuation channel, so that we may wait for the other side to close the channel.
cellServer : dualof SharedCell -> ()
cellServer c =
match accept @Cell c with {
Read s ->
send 0 s,
Write s ->
let (i, c) = receive s in c
} |> wait
We usually initiate sessions at the server side for we usually have more clients that servers and hence spare all clients from the process of creating and distributing channels. Nevertheless sessions may easily be started at the client side if needed.
The accept function can be easily written with new and send as follows:
accept : *!a -> dualof a
accept ch =
let (x, y) = new @a () in
send x ch;
y