Choreography.Core

This module defines Choreo, the monad for writing choreographies, and the closely related Located data type. Not everything here is user-friendly; this is were we declare the foundational concepts. These get repackaged in more convienent ways in Choreography.Choreography and Choreography.Choreography.Batteries.

The Choreo monad and its operators

type Choreo ps m = Freer (ChoreoSig ps m)

Monad for writing choreographies. ps is the "census", the list of parties who are present in (that part of) the choreography. m is the local monad afforded to parties by locally'.

broadcast' infix 4

Arguments

:: (Show a, Read a, KnownSymbol l)

=> Member l ps

Proof the sender is present

-> (Member l ls, Located ls a)

Proof the sender knows the value, the value.

-> Choreo ps m a

Communicate a value to all present parties.

locally'

Arguments

:: KnownSymbol l

=> (Unwrap l -> m a)

The local action(s), which can use an unwraper function.

-> Choreo '[l] m a

Access to the inner "local" monad. Since the type of locally' restricts the census to a single party, you'll usually want to use locally instead.

congruently' infix 4

Arguments

:: KnownSymbols ls

=> (Unwraps ls -> a)

The computation, which can use an unwraper function.

-> Choreo ls m a

Perform the exact same computation in replicate at all participating locations. The computation can not use anything local to an individual party, including their identity.

conclave :: KnownSymbols ls => Subset ls ps -> Choreo ls m a -> Choreo ps m (Located ls a) infix 4

Lift a choreography of involving fewer parties into the larger party space. Adds a `Located ls` layer to the return type.

Running choreographies

epp

Arguments

:: forall ps b m. (Monad m, KnownSymbols ps)

=> Choreo ps m b

A choreography

-> LocTm

A String identifying a party. At present there is no enforcement that the party will actually be in the census of the choreography; some bugs may be possible if it is not.

-> Network m b

Returns the implementation of the party's role in the choreography.

Endpoint projection.

runChoreo :: forall p ps b m. Monad m => Choreo (p ': ps) m b -> m b

Run a Choreo monad with centralized semantics. This basically pretends that the choreography is a single-threaded program and runs it all at once, ignoring all the location aspects.

Located values

data Located (ls :: [LocTy]) a

A single value known to many parties.

Instances

(KnownSymbol l, ExplicitMember l ls) => CanSend (Member l ps, Located ls a) l a ls ps

Defined in Choreography.Choreography

Methods

presentToSend :: (Member l ps, Located ls a) -> Member l ps

ownsMessagePayload :: (Member l ps, Located ls a) -> Member l ls

structMessagePayload :: (Member l ps, Located ls a) -> Located ls a

KnownSymbol l => CanSend (Member l ps, (Member l ls, Located ls a)) l a ls ps

Defined in Choreography.Choreography

Methods

presentToSend :: (Member l ps, (Member l ls, Located ls a)) -> Member l ps

ownsMessagePayload :: (Member l ps, (Member l ls, Located ls a)) -> Member l ls

structMessagePayload :: (Member l ps, (Member l ls, Located ls a)) -> Located ls a

KnownSymbol l => CanSend (Member l ls, Subset ls ps, Located ls a) l a ls ps

Defined in Choreography.Choreography

Methods

presentToSend :: (Member l ls, Subset ls ps, Located ls a) -> Member l ps

ownsMessagePayload :: (Member l ls, Subset ls ps, Located ls a) -> Member l ls

structMessagePayload :: (Member l ls, Subset ls ps, Located ls a) -> Located ls a

type Unwrap (q :: LocTy) = forall ls a. Member q ls -> Located ls a -> a

Unwraps values known to the specified party. You should not be able to build such a function in normal code; these functions are afforded only for use in "local" computation.

type Unwraps (qs :: [LocTy]) = forall ls a. Subset qs ls -> Located ls a -> a

Unwraps values known to the specified list of parties. You should not be able to build such a function in normal code; these functions are afforded only for use in "local" computation. (Could be dangerous if the list is empty, but the API is designed so that no value of type `Unwraps '[]` will ever actually get evaluated.)

flatten :: Subset ls ms -> Subset ls ns -> Located ms (Located ns a) -> Located ls a infix 3

Un-nest located values.

othersForget :: Subset ls owners -> Located owners a -> Located ls a

Cast a Located value to a smaller ownership set; useful when working with functions whos arguments have explict ownership sets.

wrap :: a -> Located l a

Wrap a value as a located value. This should be safe to export, while exporting the constuctor would enable pattern matching.