| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Choreography.Choreography.Batteries
Description
A zoo of helpful derived functions for writing choreographies.
Synopsis
- locally_ :: KnownSymbol l => Member l ps -> (Unwrap l -> m ()) -> Choreo ps m ()
- _locally :: KnownSymbol l => Member l ps -> m a -> Choreo ps m (Located '[l] a)
- _locally_ :: KnownSymbol l => Member l ps -> m () -> Choreo ps m ()
- purely :: forall l a ps m. KnownSymbol l => Member l ps -> (Unwrap l -> a) -> Choreo ps m (Located '[l] a)
- (~~>) :: forall a l ls' m ps. (Show a, Read a, KnownSymbol l, KnownSymbols ls') => (Member l ps, Unwrap l -> m a) -> Subset ls' ps -> Choreo ps m (Located ls' a)
- (-~>) :: forall a l ls' m ps. (Show a, Read a, KnownSymbol l, KnownSymbols ls') => (Member l ps, m a) -> Subset ls' ps -> Choreo ps m (Located ls' a)
- (*~>) :: forall a l ls' m ps. (Show a, Read a, KnownSymbol l, KnownSymbols ls') => (Member l ps, Unwrap l -> a) -> Subset ls' ps -> Choreo ps m (Located ls' a)
- cond :: KnownSymbols ls => (Subset ls ps, (Subset ls qs, Located qs a)) -> (a -> Choreo ls m b) -> Choreo ps m (Located ls b)
Computation per se
locally_ :: KnownSymbol l => Member l ps -> (Unwrap l -> m ()) -> Choreo ps m () infix 4 Source #
Perform a local computation, yielding nothing.
_locally :: KnownSymbol l => Member l ps -> m a -> Choreo ps m (Located '[l] a) infix 4 Source #
Perform a local computation that doesn't need to unwrap any existing Located values.
_locally_ :: KnownSymbol l => Member l ps -> m () -> Choreo ps m () infix 4 Source #
Perform a local computation that doesn't need to unwrap any existing Located values and yields nothing.
purely :: forall l a ps m. KnownSymbol l => Member l ps -> (Unwrap l -> a) -> Choreo ps m (Located '[l] a) infix 4 Source #
Perform a pure computation at a single location.
Communication
Arguments
| :: forall a l ls' m ps. (Show a, Read a, KnownSymbol l, KnownSymbols ls') | |
| => (Member l ps, Unwrap l -> m a) | A pair of a sender's location and a local computation. |
| -> Subset ls' ps | A receiver's location. |
| -> Choreo ps m (Located ls' a) |
A variant of ~> that sends the result of a local computation.
Arguments
| :: forall a l ls' m ps. (Show a, Read a, KnownSymbol l, KnownSymbols ls') | |
| => (Member l ps, m a) | A pair of a sender's location and a local computation. |
| -> Subset ls' ps | A receiver's location. |
| -> Choreo ps m (Located ls' a) |
Arguments
| :: forall a l ls' m ps. (Show a, Read a, KnownSymbol l, KnownSymbols ls') | |
| => (Member l ps, Unwrap l -> a) | A pair of a sender's location and a local computation. |
| -> Subset ls' ps | A receiver's location. |
| -> Choreo ps m (Located ls' a) |
A variant of ~> that doesn't use the local monad.
Conclaves
Arguments
| :: KnownSymbols ls | |
| => (Subset ls ps, (Subset ls qs, Located qs a)) | Tuple: Proof all the parties involved know the branch-guard and are present, the branch guard |
| -> (a -> Choreo ls m b) | The body of the conditional as a function from the unwrapped value. |
| -> Choreo ps m (Located ls b) |
Conditionally execute choreographies based on a located value. Automatically conclaves.