Control.SessionTypes.MonadSession

This module provides an interface for writing session typed programs

Primitives

class IxMonad m => MonadSession m where

The MonadSession type class exposes a set of functions that composed together form a session typed program

A type that is an instance of MonadSession must therefore also be an instance of IxMonad.

The functions themselves are generally defined as wrappers over corresponding STTerm constructors.

Minimal complete definition

send, recv, sel1, sel2, offZ, offS, recurse, weaken, var, eps

Methods

send :: a -> m (Cap ctx (a :!> r)) (Cap ctx r) ()

recv :: m (Cap ctx (a :?> r)) (Cap ctx r) a

sel1 :: m (Cap ctx (Sel (s ': xs))) (Cap ctx s) ()

sel2 :: m (Cap ctx (Sel (s ': (t ': xs)))) (Cap ctx (Sel (t ': xs))) ()

offZ :: m (Cap ctx s) r a -> m (Cap ctx (Off '[s])) r a

offS :: m (Cap ctx s) r a -> m (Cap ctx (Off (t ': xs))) r a -> m (Cap ctx (Off (s ': (t ': xs)))) r a

recurse :: m (Cap (s ': ctx) s) r a -> m (Cap ctx (R s)) r a

weaken :: m (Cap ctx s) r a -> m (Cap (t ': ctx) (Wk s)) r a

var :: m (Cap (s ': ctx) s) r a -> m (Cap (s ': ctx) V) r a

eps :: a -> m (Cap ctx Eps) (Cap ctx Eps) a

Instances

Monad m => MonadSession (IxC m)

Methods

send :: a -> IxC m (Cap * ctx ((* :!> a) r)) (Cap * ctx r) ()

recv :: IxC m (Cap * ctx ((* :?> a) r)) (Cap * ctx r) a

sel1 :: IxC m (Cap * ctx (Sel * ((ST * ': s) xs))) (Cap * ctx s) ()

sel2 :: IxC m (Cap * ctx (Sel * ((ST * ': s) ((ST * ': t) xs)))) (Cap * ctx (Sel * ((ST * ': t) xs))) ()

offZ :: IxC m (Cap * ctx s) r a -> IxC m (Cap * ctx (Off * ((ST * ': s) [ST *]))) r a

offS :: IxC m (Cap * ctx s) r a -> IxC m (Cap * ctx (Off * ((ST * ': t) xs))) r a -> IxC m (Cap * ctx (Off * ((ST * ': s) ((ST * ': t) xs)))) r a

recurse :: IxC m (Cap * ((ST * ': s) ctx) s) r a -> IxC m (Cap * ctx (R * s)) r a

weaken :: IxC m (Cap * ctx s) r a -> IxC m (Cap * ((ST * ': t) ctx) (Wk * s)) r a

var :: IxC m (Cap * ((ST * ': s) ctx) s) r a -> IxC m (Cap * ((ST * ': s) ctx) (V *)) r a

eps :: a -> IxC m (Cap * ctx (Eps *)) (Cap * ctx (Eps *)) a

Monad m => MonadSession (STTerm * m)

Methods

send :: a -> STTerm * m (Cap * ctx ((* :!> a) r)) (Cap * ctx r) ()

recv :: STTerm * m (Cap * ctx ((* :?> a) r)) (Cap * ctx r) a

sel1 :: STTerm * m (Cap * ctx (Sel * ((ST * ': s) xs))) (Cap * ctx s) ()

sel2 :: STTerm * m (Cap * ctx (Sel * ((ST * ': s) ((ST * ': t) xs)))) (Cap * ctx (Sel * ((ST * ': t) xs))) ()

offZ :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': s) [ST *]))) r a

offS :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': t) xs))) r a -> STTerm * m (Cap * ctx (Off * ((ST * ': s) ((ST * ': t) xs)))) r a

recurse :: STTerm * m (Cap * ((ST * ': s) ctx) s) r a -> STTerm * m (Cap * ctx (R * s)) r a

weaken :: STTerm * m (Cap * ctx s) r a -> STTerm * m (Cap * ((ST * ': t) ctx) (Wk * s)) r a

var :: STTerm * m (Cap * ((ST * ': s) ctx) s) r a -> STTerm * m (Cap * ((ST * ': s) ctx) (V *)) r a

eps :: a -> STTerm * m (Cap * ctx (Eps *)) (Cap * ctx (Eps *)) a

Combinators

empty :: MonadSession m => m (Cap '[] s) r a -> m (Cap '[] s) r a

A session typed program that is polymorphic in its context can often not be used by interpreters.

We can apply empty to the session typed program before passing it to an interpreter to instantiate that the context is empty.

empty0 :: MonadSession m => m (Cap '[] r) (Cap '[] r) ()

Monadic composable definition of empty

Prefix a session typed program with (empty >>) to instantiate the context to be empty.

selN :: MonadSession m => Ref s xs -> m (Cap ctx (Sel xs)) (Cap ctx s) ()

Allows indexing of selections.

The given Ref type can be used as an indexed to select a branch. This circumvents the need to sequence a bunch of sel1 and sel2 to select a branch.

prog :: MonadSession m => m ('Cap ctx (Sel '[a,b,c,d])) ('Cap ctx Eps) ()

MonadSession m => m ('Cap ctx b) ('Cap ctx Eps) ()
prog2 = prog >> selN (RefS RefZ)

selN1 :: MonadSession m => m (Cap ctx (Sel (s ': xs))) (Cap ctx s) ()

Select the first branch of a selection.

selN2 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': xs)))) (Cap ctx t) ()

Select the second branch of a selection.

selN3 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': (k ': xs))))) (Cap ctx k) ()

Select the third branch of a selection.

selN4 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': (k ': (r ': xs)))))) (Cap ctx r) ()

Select the fourth branch of a selection.

class Select xs s where

Type class for selecting a branch through injection.

Selects the first branch that matches the given session type.

prog :: MonadSession m => m ('Cap ctx (Sel '[Eps, String :!> Eps, Int :!> Eps])) ('Cap ctx Eps) ()
prog = sel >> send "c" >>= eps

It should be obvious that you cannot select a branch using sel if that branch has the same session type as a previous branch.

Minimal complete definition

sel

Methods

sel :: MonadSession m => m (Cap ctx (Sel xs)) (Cap ctx s) ()

Instances

((~) [Bool] tl (TypeEqList (ST *) xs s), Select' [Bool] xs s tl) => Select xs s

Methods

sel :: MonadSession m => m (Cap * ctx (Sel * xs)) (Cap * ctx s) ()

(<&) :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx (Off (t ': xs))) r a -> m (Cap ctx (Off (s ': (t ': xs)))) r a infixr 1

Infix synonym for offS

(<&>) :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a infix 2

Infix synonym for offer

Using both <& and <&> we can now construct an offering as follows:

 branch1 
 <& branch2
 <& branch3
 <&> branch4

This will be parsed as

(branch1
 <& (branch2
 <& (branch3
 <&> branch4)))

offer :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a

Takes two session typed programs and constructs an offering consisting of two branches

recurseFix :: MonadSession m => (m (Cap (s ': ctx) V) r a -> m (Cap (s ': ctx) s) r a) -> m (Cap ctx (R s)) r a

A fixpoint combinator for recursion

The argument function must take a recursion variable as an argument that can be used to denote the point of recursion.

For example:

prog = recurseFix \f -> do
 send 5
 f

This program will send the number 5 an infinite amount of times.

recurse0 :: MonadSession m => m (Cap ctx (R s)) (Cap (s ': ctx) s) ()

Monadic composable definition of recurse

weaken0 :: MonadSession m => m (Cap (t ': ctx) (Wk s)) (Cap ctx s) ()

Monadic composable definition of weaken

var0 :: MonadSession m => m (Cap (s ': ctx) V) (Cap (s ': ctx) s) ()

Monadic composable definition of var

eps0 :: MonadSession m => m (Cap ctx Eps) (Cap ctx Eps) ()

Monadic composable definition of eps