| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Control.SessionTypes.MonadSession
Contents
Description
This module provides an interface for writing session typed programs
- class IxMonad m => MonadSession m where
- empty :: MonadSession m => m (Cap '[] s) r a -> m (Cap '[] s) r a
- empty0 :: MonadSession m => m (Cap '[] r) (Cap '[] r) ()
- selN :: MonadSession m => Ref s xs -> m (Cap ctx (Sel xs)) (Cap ctx s) ()
- selN1 :: MonadSession m => m (Cap ctx (Sel (s ': xs))) (Cap ctx s) ()
- selN2 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': xs)))) (Cap ctx t) ()
- selN3 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': (k ': xs))))) (Cap ctx k) ()
- selN4 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': (k ': (r ': xs)))))) (Cap ctx r) ()
- class Select xs s where
- (<&) :: 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
- (<&>) :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a
- offer :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a
- recurseFix :: MonadSession m => (m (Cap (s ': ctx) V) r a -> m (Cap (s ': ctx) s) r a) -> m (Cap ctx (R s)) r a
- recurse0 :: MonadSession m => m (Cap ctx (R s)) (Cap (s ': ctx) s) ()
- weaken0 :: MonadSession m => m (Cap (t ': ctx) (Wk s)) (Cap ctx s) ()
- var0 :: MonadSession m => m (Cap (s ': ctx) V) (Cap (s ': ctx) s) ()
- eps0 :: MonadSession m => m (Cap ctx Eps) (Cap ctx Eps) ()
Primitives
class IxMonad m => MonadSession m where Source #
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.
Methods
send :: a -> m (Cap ctx (a :!> r)) (Cap ctx r) () Source #
recv :: m (Cap ctx (a :?> r)) (Cap ctx r) a Source #
sel1 :: m (Cap ctx (Sel (s ': xs))) (Cap ctx s) () Source #
sel2 :: m (Cap ctx (Sel (s ': (t ': xs)))) (Cap ctx (Sel (t ': xs))) () Source #
offZ :: m (Cap ctx s) r a -> m (Cap ctx (Off '[s])) r a Source #
offS :: m (Cap ctx s) r a -> m (Cap ctx (Off (t ': xs))) r a -> m (Cap ctx (Off (s ': (t ': xs)))) r a Source #
recurse :: m (Cap (s ': ctx) s) r a -> m (Cap ctx (R s)) r a Source #
weaken :: m (Cap ctx s) r a -> m (Cap (t ': ctx) (Wk s)) r a Source #
var :: m (Cap (s ': ctx) s) r a -> m (Cap (s ': ctx) V) r a Source #
Combinators
empty :: MonadSession m => m (Cap '[] s) r a -> m (Cap '[] s) r a Source #
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) () Source #
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) () Source #
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) () Source #
Select the first branch of a selection.
selN2 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': xs)))) (Cap ctx t) () Source #
Select the second branch of a selection.
selN3 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': (k ': xs))))) (Cap ctx k) () Source #
Select the third branch of a selection.
selN4 :: MonadSession m => m (Cap ctx (Sel (s ': (t ': (k ': (r ': xs)))))) (Cap ctx r) () Source #
Select the fourth branch of a selection.
class Select xs s where Source #
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
(<&) :: 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 Source #
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 Source #
offer :: MonadSession m => m (Cap ctx s) r a -> m (Cap ctx t) r a -> m (Cap ctx (Off '[s, t])) r a Source #
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 Source #
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) () Source #
Monadic composable definition of recurse
weaken0 :: MonadSession m => m (Cap (t ': ctx) (Wk s)) (Cap ctx s) () Source #
Monadic composable definition of weaken