Safe Haskell	None
Language	GHC2021

Choreography.Polymorphism

Contents

The root abstraction
A type-indexed vector type
Non-congruent parallel located values
Choreographic functions

Description

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

Synopsis

newtype PIndexed (ls :: [Symbol]) (f :: Symbol -> Type) = PIndexed {
- pindex :: PIndex ls f
}
type PIndex (ls :: [Symbol]) (f :: Symbol -> Type) = forall (l :: Symbol). KnownSymbol l => Member l ls -> f l
sequenceP :: forall (b :: Symbol -> Type) (ls :: [LocTy]) m. (KnownSymbols ls, Monad m) => PIndexed ls (Compose m b) -> m (PIndexed ls b)
newtype Quire (parties :: [Symbol]) a = Quire {
- asPIndexed :: PIndexed parties (Const a :: Symbol -> Type)
}
getLeaf :: forall (p :: Symbol) (parties :: [Symbol]) a. KnownSymbol p => Quire parties a -> Member p parties -> a
stackLeaves :: forall (ps :: [Symbol]) a. (forall (p :: Symbol). KnownSymbol p => Member p ps -> a) -> Quire ps a
qHead :: forall (p :: Symbol) (ps :: [Symbol]) a. KnownSymbol p => Quire (p ': ps) a -> a
qTail :: forall (p :: Symbol) (ps :: [Symbol]) a. Quire (p ': ps) a -> Quire ps a
qCons :: forall (p :: Symbol) (ps :: [Symbol]) a. a -> Quire ps a -> Quire (p ': ps) a
qNil :: Quire ('[] :: [Symbol]) a
qModify :: forall (p :: Symbol) (ps :: [Symbol]) a. (KnownSymbol p, KnownSymbols ps) => Member p ps -> (a -> a) -> Quire ps a -> Quire ps a
type Faceted (parties :: [Symbol]) (common :: [LocTy]) a = PIndexed parties (Facet a common)
newtype Facet a (common :: [LocTy]) (p :: LocTy) = Facet {
- getFacet :: Located (p ': common) a
}
localize :: forall (l :: Symbol) (ls :: [Symbol]) (common :: [LocTy]) a. KnownSymbol l => Member l ls -> Faceted ls common a -> Located (l ': common) a
viewFacet :: forall (l :: Symbol) (ls :: [Symbol]) (common :: [LocTy]) a. KnownSymbol l => Unwrap l -> Member l ls -> Faceted ls common a -> a
parallel :: forall (ls :: [Symbol]) a (ps :: [Symbol]) m. KnownSymbols ls => Subset ls ps -> (forall (l :: Symbol). KnownSymbol l => Member l ls -> Unwrap l -> m a) -> Choreo ps m (Faceted ls ('[] :: [LocTy]) a)
parallel_ :: forall (ls :: [Symbol]) (ps :: [Symbol]) m. KnownSymbols ls => Subset ls ps -> (forall (l :: Symbol). KnownSymbol l => Member l ls -> Unwrap l -> m ()) -> Choreo ps m ()
_parallel :: forall (ls :: [Symbol]) a (ps :: [Symbol]) m. KnownSymbols ls => Subset ls ps -> m a -> Choreo ps m (Faceted ls ('[] :: [LocTy]) a)
fanOut :: forall (qs :: [Symbol]) (ps :: [LocTy]) (m :: Type -> Type) (rs :: [LocTy]) a. KnownSymbols qs => (forall (q :: Symbol). KnownSymbol q => Member q qs -> Choreo ps m (Located (q ': rs) a)) -> Choreo ps m (Faceted qs rs a)
fanIn :: forall (qs :: [Symbol]) (rs :: [Symbol]) (ps :: [Symbol]) (m :: Type -> Type) a. (KnownSymbols qs, KnownSymbols rs) => Subset rs ps -> (forall (q :: Symbol). KnownSymbol q => Member q qs -> Choreo ps m (Located rs a)) -> Choreo ps m (Located rs (Quire qs a))
scatter :: forall (census :: [Symbol]) (sender :: Symbol) (recipients :: [Symbol]) a (m :: Type -> Type). (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)
gather :: forall (census :: [Symbol]) (recipients :: [Symbol]) (senders :: [Symbol]) a (dontcare :: [LocTy]) (m :: Type -> Type). (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 root abstraction

newtype PIndexed (ls :: [Symbol]) (f :: Symbol -> Type) Source #

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 :: [Symbol]) (f :: Symbol -> Type) = forall (l :: Symbol). KnownSymbol l => Member l ls -> f l Source #

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

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

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 :: [Symbol]) a Source #

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 :: Symbol -> Type)

Instances

Instances details

KnownSymbols parties => Applicative (Quire parties) Source #
Instance details 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) Source #
Instance details Defined in Choreography.Polymorphism Methods fmap :: (a -> b) -> Quire parties a -> Quire parties b # (<$) :: a -> Quire parties b -> Quire parties a #
KnownSymbols parties => Foldable (Quire parties) Source #
Instance details 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) Source #
Instance details 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, Show a) => Show (Quire parties a) Source #
Instance details 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) Source #
Instance details Defined in Choreography.Polymorphism Methods (==) :: Quire parties a -> Quire parties a -> Bool # (/=) :: Quire parties a -> Quire parties a -> Bool #

getLeaf :: forall (p :: Symbol) (parties :: [Symbol]) a. KnownSymbol p => Quire parties a -> Member p parties -> a Source #

Access a value in a Quire by its index.

stackLeaves :: forall (ps :: [Symbol]) a. (forall (p :: Symbol). KnownSymbol p => Member p ps -> a) -> Quire ps a Source #

Package a function as a Quire.

qHead :: forall (p :: Symbol) (ps :: [Symbol]) a. KnownSymbol p => Quire (p ': ps) a -> a Source #

Get the head item from a Quire.

qTail :: forall (p :: Symbol) (ps :: [Symbol]) a. Quire (p ': ps) a -> Quire ps a Source #

Get the tail of a Quire.

qCons :: forall (p :: Symbol) (ps :: [Symbol]) a. a -> Quire ps a -> Quire (p ': ps) a Source #

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 ('[] :: [Symbol]) a Source #

An empty Quire.

qModify :: forall (p :: Symbol) (ps :: [Symbol]) a. (KnownSymbol p, KnownSymbols ps) => Member p ps -> (a -> a) -> Quire ps a -> Quire ps a Source #

Apply a function to a single item in a Quire.

Non-congruent parallel located values

type Faceted (parties :: [Symbol]) (common :: [LocTy]) a = PIndexed parties (Facet a common) Source #

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

newtype Facet a (common :: [LocTy]) (p :: LocTy) Source #

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

Constructors

Facet
Fields getFacet :: Located (p ': common) a

localize :: forall (l :: Symbol) (ls :: [Symbol]) (common :: [LocTy]) a. KnownSymbol l => Member l ls -> Faceted ls common a -> Located (l ': common) a Source #

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

viewFacet :: forall (l :: Symbol) (ls :: [Symbol]) (common :: [LocTy]) a. KnownSymbol l => Unwrap l -> Member l ls -> Faceted ls common a -> a Source #

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

Choreographic functions

parallel Source #

Arguments

:: forall (ls :: [Symbol]) a (ps :: [Symbol]) m. KnownSymbols ls
=> Subset ls ps	The parties who will do the computation must be present in the census.
-> (forall (l :: Symbol). 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 ('[] :: [LocTy]) a)

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

parallel_ :: forall (ls :: [Symbol]) (ps :: [Symbol]) m. KnownSymbols ls => Subset ls ps -> (forall (l :: Symbol). KnownSymbol l => Member l ls -> Unwrap l -> m ()) -> Choreo ps m () Source #

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

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

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 Source #

Arguments

:: forall (qs :: [Symbol]) (ps :: [LocTy]) (m :: Type -> Type) (rs :: [LocTy]) a. KnownSymbols qs
=> (forall (q :: Symbol). 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 Source #

Arguments

:: forall (qs :: [Symbol]) (rs :: [Symbol]) (ps :: [Symbol]) (m :: Type -> Type) a. (KnownSymbols qs, KnownSymbols rs)
=> Subset rs ps	The recipients.
-> (forall (q :: Symbol). 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 :: [Symbol]) (sender :: Symbol) (recipients :: [Symbol]) a (m :: Type -> Type). (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) Source #

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 :: [Symbol]) (recipients :: [Symbol]) (senders :: [Symbol]) a (dontcare :: [LocTy]) (m :: Type -> Type). (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)) Source #

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.