**Monthly Downloads**: 10

**Programming language**: Haskell

**License**: GNU General Public License v3.0 only

## README

## Introduction

This package serves as a wrapper over both the Cloud Haskell library (distributed-process) and the sessiontypes library. It provides an interpreter for evaluating session typed programs to Cloud Haskell programs and exposes several combinators for spawning sessions.

## Install

Add `sessiontypes-distributed`

as a dependency in your `.cabal`

file

## Tutorial

Before reading this you should first read the sessiontypes tutorial, which explains session types and what happens under the hood of this library. We also assume that you're already familiar with the distributed-process library.

Similar to that tutorial we will start off by writing a simple session typed program:

```
{-# LANGUAGE RebindableSyntax #-}
import Control.Distributed.Session
import Control.SessionTypes.Indexed
prog :: Session ('Cap '[] (Int :!> String :?> Eps)) ('Cap '[] Eps) String
prog = do
send 5
x <- recv
eps x
```

The program is written quite similarly to an equivalent `STTerm`

program. We now use an indexed monad named `Session`

. It is parameterised similarly, except that it isn't a monad transformer. The `Session`

monad is an indexed monad reader and a wrapper over the `STTerm`

monad that has the `Process`

monad (from distributed-process) as its underlying monad.

One of the features that this library provides above sessiontypes is that we can evaluate a `Session`

to a `Process`

:

```
evalSession :: HasConstraint Serializable s => Session s r a -> SessionInfo -> P.Process a
```

This function takes not only a `Session`

, but also a `SessionInfo`

. The `SessionInfo`

contains information about the dual of the given `Session`

. That is the process that the current process should run in a session with. The `SessionInfo`

stores the process and node identifier of that process, but it also stores a send and receive port that it can use to send and receive messages.
To send and receive a message the value that will be sent must be serializable. However, the type of that value is encoded in the session type and we can't easily reach it. For that purpose we defined a type family `HasConstraint`

that applies a given constraint to all types of kind `Type`

in the session type.

The ability to write a session typed program and evaluate it terms of Cloud Haskell semantics only gives us a static guarantee that this specific program adheres to the given protocol. We would also like there to be another program that runs a session with this program and have it adhere to the dual of that protocol. First we will define duality.

```
type family Dual s = r | r -> s where
Dual (a :!> r) = a :?> Dual r
Dual (a :?> r) = a :!> Dual r
Dual Eps = Eps
```

We can compute the dual of a session type using the type family `Dual`

. For a send the dual is a receive and the dual of a receive is a send. If one program does a send then we expect the dual of that program to do a receive. Likewise, if one program ends the protocol then so should the dual of that program. Duality is a nice property to have, because it allows us to statically enforce that two programs in a session do not deadlock.

The following combinator can be used to spawn a session:

```
callLocalSession :: (HasConstraint Serializable s,
HasConstraint Serializable (Dual s)) =>
Session s r a -> Session (Dual s) r b -> Session k k (a, ProcessId)
```

It takes two `Session`

arguments and we use `Dual`

to say that the second `Session`

must be the dual of the first. The function works similar to the `call`

function in distributed-process. It spawns a local process for the second `Session`

, but runs the first `Session`

on the current process and waits for its result. The returned `ProcessId`

is that of the spawned process.

A similar combinator for spawning a session is `callRemoteSession`

. This time the second `Session`

will be spawned on a remote node. But to do so we have to create a closure of that `Session`

. Unfortunately, this cannot easily be done. The types that occur in a `Closure`

must be of kind `Type`

. However, the indexed of a `Session`

are of kind `Cap`

. So we can't construct a closure of a `Session`

. We managed to work around this problem by defining a GADT that existentially quantifies the indexes of a `Session`

. But we must still be able to enforce duality and apply constraints to the session types. We therefore require that the GADT takes two `Session`

arguments, enforces that these must be dual and applies a `Serializable`

constraint to the session types.

```
data SpawnSession a b where
SpawnSession :: (HasConstraint Serializable s, HasConstraint Serializable (Dual s)) =>
Session s r a -> Session (Dual s) r b -> SpawnSession a b
callRemoteSession :: Serializable a => Static (SerializableDict a) -> NodeId -> Closure (SpawnSession a ()) -> Session k k (a, ProcessId)
```

We can now also show you the type of `callRemoteSession`

that takes a closure of a `SpawnSession`

. Note that if you make use of any function that takes a closure that requires a data type from this library then you will need to use `sessionRemoteTable`

.