Choreography.Polymorphism

Types, functions, and structures for writing choreographies with variable numbers of participants.

The root abstraction

newtype PIndexed ls f

A mapping, accessed by Member terms, from types (Symbols) to values. The types of the values depend on the indexing type; this relation is expressed by the type-level function f. If the types of the values don't depend on the index, use Quire. If the types vary only in that they are Located at the indexing party, use Faceted. PIndexed generalizes those two types in a way that's not usually necessary when writing choreographies.

Constructors

PIndexed

Fields

• pindex :: PIndex ls f

type PIndex ls f = forall l. KnownSymbol l => Member l ls -> f l

An impredicative quantified type. Wrapping it up in PIndexed wherever possible will avoid a lot of type errors and headache.

sequenceP :: forall b (ls :: [LocTy]) m. (KnownSymbols ls, Monad m) => PIndexed ls (Compose m b) -> m (PIndexed ls b)

Sequence computations indexed by parties. Converts a PIndexed of computations into a computation yielding a PIndexed. Strongly analogous to sequence. In most cases, the choreographic functions below will be easier to use than messing around with Compose.

A type-indexed vector type

newtype Quire parties a

A collection of values, all of the same type, assigned to each element of the type-level list.

Constructors

Quire

Fields

• asPIndexed :: PIndexed parties (Const a)

Instances

KnownSymbols parties => Foldable (Quire parties)

Defined in Choreography.Polymorphism

Methods

fold :: Monoid m => Quire parties m -> m

foldMap :: Monoid m => (a -> m) -> Quire parties a -> m

foldMap' :: Monoid m => (a -> m) -> Quire parties a -> m

foldr :: (a -> b -> b) -> b -> Quire parties a -> b

foldr' :: (a -> b -> b) -> b -> Quire parties a -> b

foldl :: (b -> a -> b) -> b -> Quire parties a -> b

foldl' :: (b -> a -> b) -> b -> Quire parties a -> b

foldr1 :: (a -> a -> a) -> Quire parties a -> a

foldl1 :: (a -> a -> a) -> Quire parties a -> a

toList :: Quire parties a -> [a]

null :: Quire parties a -> Bool

length :: Quire parties a -> Int

elem :: Eq a => a -> Quire parties a -> Bool

maximum :: Ord a => Quire parties a -> a

minimum :: Ord a => Quire parties a -> a

sum :: Num a => Quire parties a -> a

product :: Num a => Quire parties a -> a

KnownSymbols parties => Traversable (Quire parties)

Defined in Choreography.Polymorphism

Methods

traverse :: Applicative f => (a -> f b) -> Quire parties a -> f (Quire parties b)

sequenceA :: Applicative f => Quire parties (f a) -> f (Quire parties a)

mapM :: Monad m => (a -> m b) -> Quire parties a -> m (Quire parties b)

sequence :: Monad m => Quire parties (m a) -> m (Quire parties a)

KnownSymbols parties => Applicative (Quire parties)

Defined in Choreography.Polymorphism

Methods

pure :: a -> Quire parties a

(<*>) :: Quire parties (a -> b) -> Quire parties a -> Quire parties b

liftA2 :: (a -> b -> c) -> Quire parties a -> Quire parties b -> Quire parties c

(*>) :: Quire parties a -> Quire parties b -> Quire parties b

(<*) :: Quire parties a -> Quire parties b -> Quire parties a

KnownSymbols parties => Functor (Quire parties)

Defined in Choreography.Polymorphism

Methods

fmap :: (a -> b) -> Quire parties a -> Quire parties b

(<$) :: a -> Quire parties b -> Quire parties a

(KnownSymbols parties, Show a) => Show (Quire parties a)

Defined in Choreography.Polymorphism

Methods

showsPrec :: Int -> Quire parties a -> ShowS

show :: Quire parties a -> String

showList :: [Quire parties a] -> ShowS

(KnownSymbols parties, Eq a) => Eq (Quire parties a)

Defined in Choreography.Polymorphism

Methods

(==) :: Quire parties a -> Quire parties a -> Bool

(/=) :: Quire parties a -> Quire parties a -> Bool

getLeaf :: KnownSymbol p => Quire parties a -> Member p parties -> a

Access a value in a Quire by its index.

stackLeaves :: forall ps a. (forall p. KnownSymbol p => Member p ps -> a) -> Quire ps a

Package a function as a Quire.

qHead :: KnownSymbol p => Quire (p ': ps) a -> a

Get the head item from a Quire.

qTail :: Quire (p ': ps) a -> Quire ps a

Get the tail of a Quire.

qCons :: forall p ps a. a -> Quire ps a -> Quire (p ': ps) a

Prepend a value to a Quire. The corresponding Symbol to bind it to must be provided by type-application if it can't be infered.

qNil :: Quire '[] a

An empty Quire.

qModify :: forall p ps a. (KnownSymbol p, KnownSymbols ps) => Member p ps -> (a -> a) -> Quire ps a -> Quire ps a

Apply a function to a single item in a Quire.

Non-congruent parallel located values

type Faceted parties common a = PIndexed parties (Facet a common)

A unified representation of possibly-distinct homogeneous values owned by many parties.

newtype Facet a common p

Repackages Located with the type arguments correctly arranged for use with PIndexed.

Constructors

Facet

Fields

• getFacet :: Located (p ': common) a

localize :: KnownSymbol l => Member l ls -> Faceted ls common a -> Located (l ': common) a

Get a Located value of a Faceted at a given location.

viewFacet :: KnownSymbol l => Unwrap l -> Member l ls -> Faceted ls common a -> a

In a context where unwrapping located values is possible, get the respective value stored in a Faceted.

Choreographic functions

parallel

Arguments

:: forall ls a ps m. KnownSymbols ls

=> Subset ls ps

The parties who will do the computation must be present in the census.

-> (forall l. KnownSymbol l => Member l ls -> Unwrap l -> m a)

The local computation has access to the identity of the party in question, in additon to the usual unwrapper function.

-> Choreo ps m (Faceted ls '[] a)

Perform a local computation at all of a list of parties, yielding a Faceted.

parallel_ :: forall ls ps m. KnownSymbols ls => Subset ls ps -> (forall l. KnownSymbol l => Member l ls -> Unwrap l -> m ()) -> Choreo ps m ()

Perform a local computation at all of a list of parties, yielding nothing.

_parallel :: forall ls a ps m. KnownSymbols ls => Subset ls ps -> m a -> Choreo ps m (Faceted ls '[] a)

Perform a local computation, that doesn't use any existing Located values and doesn't depend on the respective party's identity, at all of a list of parties, yielding a Faceted.

fanOut

Arguments

:: KnownSymbols qs

=> (forall q. KnownSymbol q => Member q qs -> Choreo ps m (Located (q ': rs) a))

The body. -- kinda sketchy that rs might not be a subset of ps...

-> Choreo ps m (Faceted qs rs a)

Perform a given choreography for each of several parties, giving each of them a return value that form a new Faceted.

fanIn

Arguments

:: (KnownSymbols qs, KnownSymbols rs)

=> Subset rs ps

The recipients.

-> (forall q. KnownSymbol q => Member q qs -> Choreo ps m (Located rs a))

The body.

-> Choreo ps m (Located rs (Quire qs a))

Perform a given choreography for each of several parties; the return values are known to recipients but not necessarily to the loop-parties.

scatter :: forall census sender recipients a m. (KnownSymbol sender, KnownSymbols recipients, Show a, Read a) => Member sender census -> Subset recipients census -> Located '[sender] (Quire recipients a) -> Choreo census m (Faceted recipients '[sender] a)

The owner of a Quire sends its elements to their respective parties, resulting in a Faceted. This represents the "scatter" idea common in parallel computing contexts.

gather :: forall census recipients senders a dontcare m. (KnownSymbols senders, KnownSymbols recipients, Show a, Read a) => Subset senders census -> Subset recipients census -> Faceted senders dontcare a -> Choreo census m (Located recipients (Quire senders a))

The many owners of a Faceted each send their respective values to a constant list of recipients, resulting in a Quire. This represents the "gather" idea common in parallel computing contexts.