| Safe Haskell | Safe-Inferred |
|---|---|
| Language | GHC2021 |
Choreography.Choreo
Description
This module defines Choreo, the monad for writing choreographies.
Synopsis
- type Unwrap l = forall a. (a @ l) -> a
- data ChoreoSig m a where
- type Choreo m = Freer (ChoreoSig m)
- runChoreo :: Monad m => Choreo m a -> m a
- epp :: Choreo m a -> LocTm -> Network m a
- locally :: KnownSymbol l => Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)
- (~>) :: (Show a, Read a, KnownSymbol l, KnownSymbol l') => (Proxy l, a @ l) -> Proxy l' -> Choreo m (a @ l')
- cond :: (Show a, Read a, KnownSymbol l) => (Proxy l, a @ l) -> (a -> Choreo m b) -> Choreo m b
- (~~>) :: (Show a, Read a, KnownSymbol l, KnownSymbol l') => (Proxy l, Unwrap l -> m a) -> Proxy l' -> Choreo m (a @ l')
- cond' :: (Show a, Read a, KnownSymbol l) => (Proxy l, Unwrap l -> m a) -> (a -> Choreo m b) -> Choreo m b
The Choreo monad
type Unwrap l = forall a. (a @ l) -> a Source #
A constrained version of unwrap that only unwraps values located at a
specific location.
data ChoreoSig m a where Source #
Effect signature for the Choreo monad. m is a monad that represents
local computations.
Constructors
| Local :: KnownSymbol l => Proxy l -> (Unwrap l -> m a) -> ChoreoSig m (a @ l) | |
| Comm :: (Show a, Read a, KnownSymbol l, KnownSymbol l') => Proxy l -> (a @ l) -> Proxy l' -> ChoreoSig m (a @ l') | |
| Cond :: (Show a, Read a, KnownSymbol l) => Proxy l -> (a @ l) -> (a -> Choreo m b) -> ChoreoSig m b |
Choreo operations
Arguments
| :: KnownSymbol l | |
| => Proxy l | Location performing the local computation. |
| -> (Unwrap l -> m a) | The local computation given a constrained unwrap funciton. |
| -> Choreo m (a @ l) |
Perform a local computation at a given location.
Arguments
| :: (Show a, Read a, KnownSymbol l, KnownSymbol l') | |
| => (Proxy l, a @ l) | A pair of a sender's location and a value located at the sender |
| -> Proxy l' | A receiver's location. |
| -> Choreo m (a @ l') |
Communication between a sender and a receiver.
Arguments
| :: (Show a, Read a, KnownSymbol l) | |
| => (Proxy l, a @ l) | A pair of a location and a scrutinee located on it. |
| -> (a -> Choreo m b) | A function that describes the follow-up choreographies based on the value of scrutinee. |
| -> Choreo m b |
Conditionally execute choreographies based on a located value.
Arguments
| :: (Show a, Read a, KnownSymbol l, KnownSymbol l') | |
| => (Proxy l, Unwrap l -> m a) | A pair of a sender's location and a local computation. |
| -> Proxy l' | A receiver's location. |
| -> Choreo m (a @ l') |
A variant of ~> that sends the result of a local computation.
Arguments
| :: (Show a, Read a, KnownSymbol l) | |
| => (Proxy l, Unwrap l -> m a) | A pair of a location and a local computation. |
| -> (a -> Choreo m b) | A function that describes the follow-up choreographies based on the result of the local computation. |
| -> Choreo m b |
A variant of cond that conditonally executes choregraphies based on the
result of a local computation.