Purely evaluates a given STTerm using the input defined by Stream.

The output is described in terms of the session type actions within the given program

An example of how to use this function goes as follows:

 prog :: STTerm Identity ('Cap '[] (Int :!> String :?> Eps)) ('Cap '[] Eps) String
 prog = send 5 >> recv >>= eps

 strm = S_Send $ S_Recv "foo" S_Eps

>>> run prog strm
O_Send 5 $ O_Recv "foo" $ O_Eps "foo"

Instead of describing the session typed actions, it returns a list of the results of all branches of all offerings.

prog = offer (eps 10) (eps 5)
strm = S_OffS S_Eps S_Eps

>>> runAll prog strm
[10,5]

Same as runAll but applies head to the resulting list

>>> runSingle prog strm
10

run cannot deal with lifted computations. This makes it limited to session typed programs without any use of lift.

This function allows us to evaluate lifted computations, but as a consequence is no longer entirely pure.

Monadic version of runAll.

Monad version of runSingle

We use the Stream data type to supply input for the receives in a session typed programs.

We annotate a Stream with a capability for the following three reasons:

1. Each recv may return a value of a different type.
2. Given reason 1 and that we can have branching, we must also be able to branch in the stream.
3. We can now write a function that recursively generates input for a recursive program

Similar to STTerm, Stream has a constructor for each session type. Each constructor takes an argument that is another Stream type, except for S_Recv that takes an additional argument that will be used as input, and S_Eps that denotes the end of the stream.

At first it might be confusing which constructors and in what order these constructors should be placed to form a Stream that can be used as input for some STTerm.

This is actually not that difficult at all. A Stream is session typed and that session type must be equal to the session type of the STTerm. As such one merely needs to create a Stream that has the same session type and if you don't the type checker will tell you what it incorrect.

There are two things that you need to be aware of when constructor a Stream.

• The Stream constructors for offering (S_OffZ and S_OffS) require that you define input for all branches of the offering. This can be quite cumbersome, so we include a S_Off1 and S_Off2 constructor that behave similarly to S_Sel1 and S_Sel2.
• You are not guaranteed that a Stream can be used for all session typed programs that have the same session type. Specifically when it comes to selection can we not guarantee this. The session type for selection only tells us about which branches could be selected. It does not tell us which branch was selected as this is runtime dependent.

The Output data type describes the session type actions that were done