| Safe Haskell | None |
|---|---|
| Language | GHC2021 |
Choreography.Choreo
Description
This module defines Choreo, the monad for writing choreographies.
Synopsis
- type Unwrap (l :: LocTy) = forall a. (a @ l) -> a
- data ChoreoSig (m :: Type -> Type) a where
- Local :: forall (l :: Symbol) (m :: Type -> Type) a1. KnownSymbol l => Proxy l -> (Unwrap l -> m a1) -> ChoreoSig m (a1 @ l)
- Comm :: forall a1 (l :: Symbol) (l' :: Symbol) (m :: Type -> Type). (Show a1, Read a1, KnownSymbol l, KnownSymbol l') => Proxy l -> (a1 @ l) -> Proxy l' -> ChoreoSig m (a1 @ l')
- Cond :: forall a1 (l :: Symbol) (m :: Type -> Type) a. (Show a1, Read a1, KnownSymbol l) => Proxy l -> (a1 @ l) -> (a1 -> Choreo m a) -> ChoreoSig m a
- Cond_ :: forall a1 (l :: Symbol) (m :: Type -> Type) b. (Bounded a1, Enum a1, Show a1, Read a1, KnownSymbol l) => Proxy l -> (a1 @ l) -> (a1 -> Choreo m (b @ l)) -> ChoreoSig m (b @ l)
- type Choreo (m :: Type -> Type) = Freer (ChoreoSig m)
- runChoreo :: Monad m => Choreo m a -> m a
- insertLoc :: forall (l :: Symbol). KnownSymbol l => Proxy l -> Set LocTm -> Set LocTm
- insertLocs :: [LocTm] -> Set LocTm -> Set LocTm
- enumerate :: forall a (m :: Type -> Type) b. (Bounded a, Enum a) => [LocTm] -> (a -> Choreo m b) -> Set LocTm
- participants :: forall (m :: Type -> Type) a. [LocTm] -> Choreo m a -> Set LocTm
- epp :: forall (m :: Type -> Type) a. [LocTm] -> Choreo m a -> LocTm -> Network m a
- locally :: forall (l :: Symbol) m a. KnownSymbol l => Proxy l -> (Unwrap l -> m a) -> Choreo m (a @ l)
- (~>) :: forall a (l :: Symbol) (l' :: Symbol) (m :: Type -> Type). (Show a, Read a, KnownSymbol l, KnownSymbol l') => (Proxy l, a @ l) -> Proxy l' -> Choreo m (a @ l')
- cond :: forall a (l :: Symbol) (m :: Type -> Type) b. (Show a, Read a, KnownSymbol l) => (Proxy l, a @ l) -> (a -> Choreo m b) -> Choreo m b
- cond_ :: forall a (l :: Symbol) (m :: Type -> Type) b. (Bounded a, Enum a, Show a, Read a, KnownSymbol l) => (Proxy l, a @ l) -> (a -> Choreo m (b @ l)) -> Choreo m (b @ l)
- (~~>) :: forall a (l :: Symbol) (l' :: Symbol) m. (Show a, Read a, KnownSymbol l, KnownSymbol l') => (Proxy l, Unwrap l -> m a) -> Proxy l' -> Choreo m (a @ l')
- cond' :: forall a (l :: Symbol) m b. (Show a, Read a, KnownSymbol l) => (Proxy l, Unwrap l -> m a) -> (a -> Choreo m b) -> Choreo m b
- cond_' :: forall a (l :: Symbol) m b. (Bounded a, Enum a, Show a, Read a, KnownSymbol l) => (Proxy l, Unwrap l -> m a) -> (a -> Choreo m (b @ l)) -> Choreo m (b @ l)
The Choreo monad
type Unwrap (l :: LocTy) = forall a. (a @ l) -> a Source #
A constrained version of unwrap that only unwraps values located at a
specific location.
data ChoreoSig (m :: Type -> Type) a where Source #
Effect signature for the Choreo monad. m is a monad that represents
local computations.
Constructors
| Local :: forall (l :: Symbol) (m :: Type -> Type) a1. KnownSymbol l => Proxy l -> (Unwrap l -> m a1) -> ChoreoSig m (a1 @ l) | |
| Comm :: forall a1 (l :: Symbol) (l' :: Symbol) (m :: Type -> Type). (Show a1, Read a1, KnownSymbol l, KnownSymbol l') => Proxy l -> (a1 @ l) -> Proxy l' -> ChoreoSig m (a1 @ l') | |
| Cond :: forall a1 (l :: Symbol) (m :: Type -> Type) a. (Show a1, Read a1, KnownSymbol l) => Proxy l -> (a1 @ l) -> (a1 -> Choreo m a) -> ChoreoSig m a | |
| Cond_ :: forall a1 (l :: Symbol) (m :: Type -> Type) b. (Bounded a1, Enum a1, Show a1, Read a1, KnownSymbol l) => Proxy l -> (a1 @ l) -> (a1 -> Choreo m (b @ l)) -> ChoreoSig m (b @ l) |
enumerate :: forall a (m :: Type -> Type) b. (Bounded a, Enum a) => [LocTm] -> (a -> Choreo m b) -> Set LocTm Source #
Apply function f to every possible value of type a, and collect all the resulting participants.
participants :: forall (m :: Type -> Type) a. [LocTm] -> Choreo m a -> Set LocTm Source #
Compute the set of locations participating in this choreography.
epp :: forall (m :: Type -> Type) a. [LocTm] -> Choreo m a -> LocTm -> Network m a Source #
Endpoint projection.
Choreo operations
Arguments
| :: forall (l :: Symbol) m a. 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
| :: forall a (l :: Symbol) (l' :: Symbol) (m :: Type -> Type). (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
| :: forall a (l :: Symbol) (m :: Type -> Type) b. (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
| :: forall a (l :: Symbol) (m :: Type -> Type) b. (Bounded a, Enum a, 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 @ l)) | A function that describes the follow-up choreographies based on the value of scrutinee. |
| -> Choreo m (b @ l) |
Conditionally execute choreographies at participating locations, based on a located value.
Arguments
| :: forall a (l :: Symbol) (l' :: Symbol) m. (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
| :: forall a (l :: Symbol) m b. (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.
Arguments
| :: forall a (l :: Symbol) m b. (Bounded a, Enum a, 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 @ l)) | A function that describes the follow-up choreographies based on the result of the local computation. |
| -> Choreo m (b @ l) |
A variant of cond_ that conditonally executes choregraphies at participating locations,
based on the result of a local computation.