Control.SessionTypes.Debug

This module describes an interpreter for purely evaluating session typed programs

that is based on the paper Beauty in the beast by Swierstra, W., & Altenkirch, T.

Impurity in a session typed programs mainly comes from three things: receives, branching and lifting.

Using the session type we can easily determine the type of the message that each receive should expect.

This information allows us to define a stream of values of different types that provides input for each receive.

In the sessiontyped-distributed library we send and receive booleans to enable branching.

It is also possible to provide some kind of input that makes this choice.

The current structure of the Lift constructor does not allow us to purely evaluate a Lift.

As such a session typed program may not contain a lift for it to be purely evaluated. See runM as an alternative.

Pure

run :: HasConstraint Show s => STTerm m s (Cap ctx Eps) a -> Stream s -> Output s a

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"

runAll :: HasConstraint Show s => STTerm m s (Cap ctx Eps) a -> Stream s -> [a]

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]

runSingle :: HasConstraint Show s => STTerm m s (Cap ctx Eps) a -> Stream s -> a

Same as runAll but applies head to the resulting list

>>> runSingle prog strm
10

runM :: (Monad m, HasConstraint Show s) => STTerm m s (Cap ctx Eps) a -> Stream s -> m (Output s a)

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.

runAllM :: (Monad m, HasConstraint Show s) => STTerm m s (Cap ctx Eps) a -> Stream s -> m [a]

Monadic version of runAll.

runSingleM :: (Monad m, HasConstraint Show s) => STTerm m s (Cap ctx Eps) a -> Stream s -> m a

Monad version of runSingle

Input

data Stream :: Cap Type -> Type where

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.

Constructors

S_Send :: Stream (Cap ctx s) -> Stream (Cap ctx (a :!> s))

S_Recv :: a -> Stream (Cap ctx s) -> Stream (Cap ctx (a :?> s))

S_Sel1 :: Stream (Cap ctx s) -> Stream (Cap ctx (Sel (s ': xs)))

S_Sel2 :: Stream (Cap ctx (Sel (t ': xs))) -> Stream (Cap ctx (Sel (s ': (t ': xs))))

S_OffZ :: Stream (Cap ctx s) -> Stream (Cap ctx (Off '[s]))

S_OffS :: Stream (Cap ctx s) -> Stream (Cap ctx (Off (t ': xs))) -> Stream (Cap ctx (Off (s ': (t ': xs))))

S_Off1 :: Stream (Cap ctx s) -> Stream (Cap ctx (Off (s ': xs)))

S_Off2 :: Stream (Cap ctx (Off (t ': xs))) -> Stream (Cap ctx (Off (s ': (t ': xs))))

S_Rec :: Stream (Cap (s ': ctx) s) -> Stream (Cap ctx (R s))

S_Weaken :: Stream (Cap ctx s) -> Stream (Cap (t ': ctx) (Wk s))

S_Var :: Stream (Cap (s ': ctx) s) -> Stream (Cap (s ': ctx) V)

S_Eps :: Stream (Cap '[] Eps)

Instances

HasConstraint Eq s => Eq (Stream s)

Methods

(==) :: Stream s -> Stream s -> Bool

(/=) :: Stream s -> Stream s -> Bool

HasConstraint Show s => Show (Stream s)

Methods

showsPrec :: Int -> Stream s -> ShowS

show :: Stream s -> String

showList :: [Stream s] -> ShowS

HasConstraint NFData s => NFData (Stream s)

Methods

rnf :: Stream s -> ()

Output

data Output :: Cap Type -> Type -> Type where

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

Constructors

O_Send :: a -> Output (Cap ctx r) b -> Output (Cap ctx (a :!> r)) b

O_Recv :: a -> Output (Cap ctx r) b -> Output (Cap ctx (a :?> r)) b

O_Sel1 :: Output (Cap ctx s) b -> Output (Cap ctx (Sel (s ': xs))) b

O_Sel2 :: Output (Cap ctx (Sel xs)) b -> Output (Cap ctx (Sel (s ': xs))) b

O_OffZ :: Output (Cap ctx s) a -> Output (Cap ctx (Off '[s])) a

O_OffS :: Output (Cap ctx s) b -> Output (Cap ctx (Off (t ': xs))) b -> Output (Cap ctx (Off (s ': (t ': xs)))) b

O_Off1 :: Output (Cap ctx s) a -> Output (Cap ctx (Off (s ': xs))) a

O_Off2 :: Output (Cap ctx (Off (t ': xs))) a -> Output (Cap ctx (Off (s ': (t ': xs)))) a

O_Rec :: Output (Cap (s ': ctx) s) b -> Output (Cap ctx (R s)) b

O_Var :: Output (Cap (s ': ctx) s) b -> Output (Cap (s ': ctx) V) b

O_Weaken :: Output (Cap ctx s) b -> Output (Cap (t ': ctx) (Wk s)) b

O_Eps :: b -> Output (Cap '[] Eps) b

O_Lift :: Output s b -> Output s b

Instances

(HasConstraint Eq s, Eq a) => Eq (Output s a)

Methods

(==) :: Output s a -> Output s a -> Bool

(/=) :: Output s a -> Output s a -> Bool

(HasConstraint Show s, Show a) => Show (Output s a)

Methods

showsPrec :: Int -> Output s a -> ShowS

show :: Output s a -> String

showList :: [Output s a] -> ShowS

(HasConstraint NFData s, NFData a) => NFData (Output s a)

Methods

rnf :: Output s a -> ()