Authors — Simon Gay, António Ravara
ISBN — 978-87-93519-82-4
File — behavioral/RE_9788793519817.pdf
Given the book is quite large and not every chapter is important to the matter at hands, only some chapters are reviewed.
The primary criteria of selection was based on what seemed the most useful, I looked for type-first approaches and the generation of programs, these matters are relevant in “Rust-land” to make use of the advanced type-system and macros.
Table of Contents
This chapter presents a tool and specification language called Hypha for the type-based analysis of processes that communicate on linear channels.
The specification language is appropriate for modeling concurrent processes that exchange messages over session channels. The syntax of the language is present in the original document.
Hypha distinguishes between ephemeral input, written as $u?(x_1, \dots, x_n).P$, and persistent input, written as $^*u?(x_1, \dots, x_n)$.
In the case of ephemeral input, the process then waits for one message from $u$, the message is considered to be an $n$-tuple, and then executes $P$.
For permanent input, which waits for an arbitrary number of messages, each received message spawns a new copy of $P$.
Hypha also ensures that its programs are deadlock free, however, it is important to note that not every deadlock free program is a valid Hypha program.
A process is deadlock free if every residual of P that cannot reduce further does not contain pending communications.
A process is lock free if every residual $Q$ of $P$ in which there are pending communications can reduce further to a state in which such operations complete.
As previously referred, Hypha’s typesystem ensures that well-type processes are guaranteed to be deadlock free. To that end, Hypha implements a type reconstruction algorithm for this type system and finds a typing derivation for a given process, provided there is one.
In Hypha, channels have three properties:
Hypha’s typing rules are meant to enforce the following channel properties:
This chapter reviews existing literature on Session Types and Haskell, related on how to exploit the type system to provide static guarantees over programs.
Session types are a kind of behavioral type capturing the communication behavior of concurrent processes. Commonly, session types capture the sequence of sends and receives performed over a channel and the types of the messages carried by these interactions.
A relevant aspect of session type is their requirement for linear usage of channels, every send being required to have exactly on receive and vice versa. This makes the implementation of session types on language that lack linear concepts, a challenge.
Haskell provides a library for message-passing concurrency, its primitives are as follows:
newChan :: IO (Chan a) -- channel creation
readChan :: Chan a -> IO a -- read from a channel
writeChan :: Chan a -> a -> IO () -- write to a channel
forkIO :: IO () -> IO ThreadId -- process forking
Functions operate within the IO monad to encapsulate side-effectful computations. While channel typing ensures data safety, communication safety is not ensured.
A significant proportion of communication safety (mainly the order of interactions) can be enforced with just algebraic data types, polymorphism, and a type-based encoding of duality.
send :: Chan (Send a t) -> a -> IO (Chan t)
recv :: Chan (Recv a t) -> -> IO (a, Chan t)
close :: Chan End -> IO ()
data Send a t = Send a (Chan t)
data Recv a t = Recv a (Chan t)
data End
The send combinator takes as parameters a channel which can transfer values of type Send a t and a value x of type a returning a new channel which can transfer the values of type t.
This is implemented via the constructor Send, pairing the value x with the new channel c',
sending those on the channel c, and returning the new continuation channel c'.
The recv combinator is somewhat dual to this.
It takes a channel c on which is received a pair of a value x of type a and channel c' which can transfer values of type t.
The pair (x, c') is then returned.
The close combinator discards its channel which has only the capability of transferring End values, which are uninhabited.
A possible way to capture duality is via a type family.
Type families are primitive recursive functions, with strong syntatic restrictions to enforce termination.
Defining the closed type family Dual:
type family Dual s where
Dual (Send a t) = Recv a (Dual t)
Dual (Recv a t) = Send a (Dual t)
Dual End = End
Duality is used to type the fork operation,
which spawns a process with a fresh channel, returning a channel of the dual type:
fork :: Link s => (Chan s -> IO ()) -> IO (Chan (Dual s))
This chapter presents FuSe, an OCaml module that implements binary sessions and enables a hybrid form of session type checking without external tools or language extensions.
The approach combines static and dynamic checks.
The summary overlooks several details and only extracts the more relevant parts from the API design perspective.
Before presenting the API, there were some changes to the representation as to cope with the LaTeX/code conversion:
A_i.~A.a'.in.+*.The FuSe high-level API is as follows:
val create : unit -> A x ~A
val close : end -> unit
val send : a'-> !a'.A -> A
val receive : ?a'.A -> a' x A
val select : (~(A_k) -> [l_i : ~{A_i}]_{i in I}) -> +*[l_i : A_i]_{i in I} -> A_k
val branch : &[l_i : A_i]_{i in I} -> [l_i : A_i]_{i in I}
send sends a message of type a' over an endpoint of type !a'.A and returns the same endpoint with its type changed to A to reflect that the communication has occurred.receive waits for a message of type a' from an endpoint of type ?a'.A and returns a pair with the message of type a' from an endpoint of type ?a'.A and returns a pair with the message and the same endpoint with its type changed to A.branch and select deal with sessions that may continue along different interaction paths. Each path is associated with a label l_i.
select takes a label l_k and an endpoint of type +*[l_i : A_i]_{i in I} where k in I, sends the label over the endpoint and returns the endpoint with its type changed to A_k.branch waits for a label from an endpoint of type &[l_i : A_i]_{i in I} and returns the continuation endpoint injected into a disjoint union.