This section defines syntax for distributed exection of processes.

You define your processes and their links as a value of type Exec, and then run it using runExec.

You start with the processes defined as AsyncT m ach i i a` wrapped in ExecProc, then you combine them using ExecFork, ExecLink and ExecSwap until you've linked all the free ports and left with Exec m '[] NextSend a. The latter can be evaluated with runExec to yield the final result of evaluation.

Only one process in the whole execution is allowed to return a result. It is the (only) process that finishes in NextSend state, all the other processes are forced to have their return type Void (and never finish). These conditions are checked statically by the typeclass restrictions of Exec constructors.

Function runExec returns the result of the process that termiates in NextSend.

This section defines the ExecBuilder monad that simplifies the construction of Exec exections. Any Exec value is built like a tree where each node is marked with one of constructors of Exec: ExecFork has two children nodes, ExecProc is a leaf (no children nodes), while ExecSwap and ExecFork have one child each.

This structure, while precisely matching the technical aspect of constructing an execution, are not so convenient for human to build. Especially, if your Exec formala is complex and you want to build it gradually and see intermediate results.

The ExecBuilder monad aids in building Exec values in a modular way and providing the programmer with feedback at each step. Each ExecBuilder action internally stores a function Exec l m i res -> Exec l' m i' res' or a function () -> Exec l m i res (given by the ExecIndex). Two actions can be composed together if the corresponding functions compose.

To get a runnable execution Exec '[] m i res, define a value of type ExecBuilder m ExecIndexInit (ExecIndexSome l i res) () and pass it to runExecBuilder. The result can be passed to runExec to actually run it. The basic actions available in ExecBuilder are forkLeft, forkRight, link and swap.

The following are basic actions you can perform in ExecBuilder. The process, forkLeft, forkRight, link, swap correpond to the constructors of Exec. The difference between forkLeft and forkRight is merely in the order of composing the child nodes.

The execGuard = xreturn () has no effect in the monad, but can be inserted in-between other operations in ExecBuilder to annotate the current context. This can be used to document the code, while having the compiler verify that the annotation is correct. In some rare cases, execGuard can also be used to resolve ambiguous types.

Following are the versions of process, forkLeft and forkRight that take the proofs as explicit arguments instead of implicit typeclass constraints.