-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Type-safe and efficient choreographies with location-set polymorphism.
--   
--   MultiChor is a library for functional choreographic programming in
--   Haskell.
@package MultiChor
@version 1.0.1.0


-- | This module defines locations (AKA parties) and functions/relations
--   pertaining to type-level lists of locations.
module Choreography.Locations

-- | Term-level locations.
type LocTm = String

-- | Type-level locations.
type LocTy = Symbol

-- | A term-level proof that a <a>LocTy</a> is a member of a
--   <tt>[LocTy]</tt>. These are frequently used both for proofs <i>per
--   se</i> and to identify individuals in lists of locations.
--   
--   For example: <tt>player :: Member players census</tt> is a proof that
--   the type-level <a>Symbol</a>, <tt>player</tt>, is in <tt>census</tt>,
--   and it can also be used as a <b>term-level</b> identifier for the
--   <b>type-level</b> <tt>player</tt>, similar to how a <tt>proxy</tt>
--   might be used.
--   
--   Pattern matching on these values is like pattern matching on a
--   successor-based <tt>Nat</tt>; in this sense a <tt>Member x xs</tt> is
--   an index into <tt>xs</tt> at which <tt>x</tt> can be found.
data Member (x :: k) (xs :: [k])
[First] :: forall xs x xs'. xs ~ (x ': xs') => Member x (x ': xs')
[Later] :: Member x xs -> Member x (y ': xs)

-- | A term level proof that one type-level list represents a subset of
--   another, embodied by a total function from proof-of-membership in the
--   sublist to proof-of-membership in the superlist. (If you make one with
--   a partial funciton, all bets are off.)
newtype Subset xs ys
Subset :: (forall x. Member x xs -> Member x ys) -> Subset xs ys

-- | Convert a proof of membership in the sublist to a proof of membership
--   in the superlist. Frequently used to show that a location is part of a
--   larger set of locations.
[inSuper] :: Subset xs ys -> forall x. Member x xs -> Member x ys

-- | The subset relation is reflexive.
refl :: Subset xs xs

-- | The sublist relation is transitive.
transitive :: Subset xs ys -> Subset ys zs -> Subset xs zs

-- | The `[]` case of subset proofs. Typlically used to build subset proofs
--   using membership proofs using <a>@@</a>.
nobody :: Subset '[] ys

-- | Any lists is a subset of the list made by consing itself with any
--   other item.
consSet :: forall xs x xs'. xs ~ (x ': xs') => Subset xs' (x ': xs')

-- | Cons an element to the superset in a <a>Subset</a> value.
consSuper :: forall xs ys y. Subset xs ys -> Subset xs (y ': ys)

-- | Cons an element to the subset in a <a>Subset</a> value; requires proof
--   that the new head element is already a member of the superset. Used
--   like ":" for subset proofs. Suppose you have <tt>(alice :: Member
--   <a>Alice</a> census)</tt> and we want a <i>subset</i> proof instead of
--   membership; we can write:
--   
--   <pre>
--   &gt;&gt;&gt; proof :: Subset '["Alice"] census = alice @@ nobody
--   </pre>
(@@) :: Member x ys -> Subset xs ys -> Subset (x ': xs) ys
infixr 5 @@

-- | Convert a proof-level location to a term-level location.
toLocTm :: forall (l :: LocTy) (ps :: [LocTy]). KnownSymbol l => Member l ps -> LocTm

-- | Get the term-level list of names-as-strings for a proof-level list of
--   parties.
toLocs :: forall (ls :: [LocTy]) (ps :: [LocTy]). KnownSymbols ls => Subset ls ps -> [LocTm]

-- | Term-level markers of the spine/structure of a type-level list.
--   Pattern matching on them recovers both the spine of the list and, if
--   applicable, <a>KnownSymbol</a>[<tt>s</tt>] instances for the head and
--   tail.
data TySpine ps

-- | Denotes that the list has a head and tail, and exposes
--   <a>KnownSymbol</a> and <a>KnownSymbols</a> constraints respectively.
[TyCons] :: (KnownSymbol h, KnownSymbols ts) => TySpine (h ': ts)

-- | Denotes that the list is empty.
[TyNil] :: TySpine '[]

-- | The type-level-list version of <a>KnownSymbol</a>. Denotes that both
--   the spine of the list and each of its elements is known at
--   compile-time. This knowlege is typically recovered by recursively
--   pattern-matching on <tt>tySpine @ls</tt>.
class KnownSymbols ls

-- | Pattern matching on <tt>tySpine @ls</tt> will normally have two cases,
--   for when <tt>ls</tt> is empty or not. Contextual knowledge may let one
--   or the other case be skipped. Within those cases, the knowledge
--   afforded by <a>tySpine</a>'s constructors can be used.
tySpine :: KnownSymbols ls => TySpine ls
instance Choreography.Locations.KnownSymbols '[]
instance (Choreography.Locations.KnownSymbols ls, GHC.TypeLits.KnownSymbol l) => Choreography.Locations.KnownSymbols (l : ls)


-- | Additional functions/relations pertaining to locations and type-level
--   lists of locations.
module Choreography.Locations.Batteries

-- | Quickly build membership proofs, when the membership can be directly
--   observed by GHC.
class ExplicitMember (x :: k) (xs :: [k])
explicitMember :: ExplicitMember x xs => Member x xs

-- | Quickly build subset proofs, when the subset relation can be directly
--   observed by GHC.
class ExplicitSubset xs ys
explicitSubset :: ExplicitSubset xs ys => Subset xs ys

-- | Alias <a>refl</a>. When used as an identifier, this is more
--   descriptive.
allOf :: forall ps. Subset ps ps

-- | Any element <tt>p</tt> is a member of the list <tt>'[p]</tt>.
singleton :: forall p. Member p (p ': '[])

-- | A <a>Member</a> value for the first item in a list. Note that
--   type-applicaiton is different than with <a>First</a>, to which this is
--   otherwise redundant.
listedFirst :: forall p1 ps. Member p1 (p1 ': ps)

-- | A <a>Member</a> value for the second item in a list.
listedSecond :: forall p2 p1 ps. Member p2 (p1 ': (p2 ': ps))

-- | A <a>Member</a> value for the third item in a list.
listedThird :: forall p3 p2 p1 ps. Member p3 (p1 ': (p2 ': (p3 ': ps)))

-- | A <a>Member</a> value for the forth item in a list.
listedForth :: forall p4 p3 p2 p1 ps. Member p4 (p1 ': (p2 ': (p3 ': (p4 ': ps))))

-- | A <a>Member</a> value for the fifth item in a list.
listedFifth :: forall p5 p4 p3 p2 p1 ps. Member p5 (p1 ': (p2 ': (p3 ': (p4 ': (p5 ': ps)))))

-- | A <a>Member</a> value for the sixth item in a list.
listedSixth :: forall p6 p5 p4 p3 p2 p1 ps. Member p6 (p1 ': (p2 ': (p3 ': (p4 ': (p5 ': (p6 ': ps))))))

-- | Use any membership proof to to safely call code that only works on a
--   non-empy list.
quorum1 :: forall ps p a. KnownSymbols ps => Member p ps -> (forall q qs. (KnownSymbol q, KnownSymbols qs, ps ~ (q ': qs)) => a) -> a

-- | Declare a proof-value with the given string as the variable name,
--   proving that that string is a member of any list in which it
--   explicitly apprears.
mkLoc :: String -> Q [Dec]
instance forall k (xs :: [k]) (ys :: [k]) (x :: k). (Choreography.Locations.Batteries.ExplicitSubset xs ys, Choreography.Locations.Batteries.ExplicitMember x ys) => Choreography.Locations.Batteries.ExplicitSubset (x : xs) ys
instance forall k (ys :: [k]). Choreography.Locations.Batteries.ExplicitSubset '[] ys
instance forall a (x :: a) (xs :: [a]) (y :: a). Choreography.Locations.Batteries.ExplicitMember x xs => Choreography.Locations.Batteries.ExplicitMember x (y : xs)
instance forall a (x :: a) (xs :: [a]). Choreography.Locations.Batteries.ExplicitMember x (x : xs)


-- | This module defines the freer monad <a>Freer</a>, which allows
--   manipulating effectful computations algebraically.
--   
--   It is unlikely you need this, except maybe to define your own backends
--   or something. We may hide/remove it in future versions.
module Control.Monad.Freer

-- | Freer monads.
--   
--   A freer monad <tt>Freer f a</tt> represents an effectful computation
--   that returns a value of type <tt>a</tt>. The parameter <tt>f :: *
--   -&gt; *</tt> is a effect signature that defines the effectful
--   operations allowed in the computation. <tt>Freer f a</tt> is called a
--   freer monad in that it's a <a>Monad</a> given any <tt>f</tt>.
data Freer f a

-- | A pure computation.
[Return] :: a -> Freer f a

-- | An effectful computation where the first argument <tt>f b</tt> is the
--   effect to perform and returns a result of type <tt>b</tt>; the second
--   argument <tt>b -&gt; Freer f a</tt> is a continuation that specifies
--   the rest of the computation given the result of the performed effect.
[Do] :: f b -> (b -> Freer f a) -> Freer f a

-- | Lift an effect into the freer monad.
toFreer :: f a -> Freer f a

-- | Interpret the effects in a freer monad in terms of another monad.
interpFreer :: Monad m => (forall b. f b -> m b) -> Freer f a -> m a
instance GHC.Base.Functor (Control.Monad.Freer.Freer f)
instance GHC.Base.Applicative (Control.Monad.Freer.Freer f)
instance GHC.Base.Monad (Control.Monad.Freer.Freer f)


-- | This module defines the <a>Network</a> monad, which represents
--   programs run on individual nodes in a distributed system with explicit
--   sends and receives. To run a <a>Network</a> program, we provide a
--   <a>runNetwork</a> function that supports multiple message transport
--   backends. Two such backends are provided in
--   <a>Choreography.Network.Http</a> and
--   <a>Choreography.Network.Local</a>, and there should be enough tools
--   here for you to write more as needed.
module Choreography.Network

-- | Effect signature for the <a>Network</a> monad.
data NetworkSig m a

-- | Local computation.
[Run] :: m a -> NetworkSig m a

-- | Sending.
[Send] :: Show a => a -> [LocTm] -> NetworkSig m ()

-- | Receiving.
[Recv] :: Read a => LocTm -> NetworkSig m a

-- | Monad that represents network programs.
type Network m = Freer (NetworkSig m)

-- | Perform a local computation.
run :: m a -> Network m a

-- | Send a message to a receiver.
send :: Show a => a -> [LocTm] -> Network m ()

-- | Receive a message from a sender.
recv :: Read a => LocTm -> Network m a

-- | A message transport backend defines a <i>configuration</i> of type
--   <tt>c</tt> that carries necessary bookkeeping information, then
--   defines <tt>c</tt> as an instance of <a>Backend</a> and provides a
--   <a>runNetwork</a> function.
class Backend c
runNetwork :: (Backend c, MonadIO m) => c -> LocTm -> Network m a -> m a


-- | This module defines the multi-thread backend for the <a>Network</a>
--   monad.
module Choreography.Network.Local

-- | Each location is associated with a message buffer which stores
--   messages sent from other locations.
type MsgBuf = HashMap LocTm (Chan String)

-- | A backend for running choreographies using <a>Haskell threads</a> as
--   the locations and buffered <a>Chan</a> channels for communication.
newtype LocalConfig
LocalConfig :: HashMap LocTm MsgBuf -> LocalConfig
[locToBuf] :: LocalConfig -> HashMap LocTm MsgBuf

-- | Make a channel for each of the listed locations, on which messages
--   from that location can be recieved.
newEmptyMsgBuf :: [LocTm] -> IO MsgBuf

-- | Make a local backend for the listed parties. Make just the one backend
--   and then have all your threads use the same one.
mkLocalConfig :: [LocTm] -> IO LocalConfig

-- | List the parties known to the backend.
locs :: LocalConfig -> [LocTm]

-- | Run a <a>Network</a> behavior using the channels in a
--   <a>LocalConfig</a> for communication. Call this inside a concurrent
--   thread.
runNetworkLocal :: MonadIO m => LocalConfig -> LocTm -> Network m a -> m a
instance Choreography.Network.Backend Choreography.Network.Local.LocalConfig


-- | This module implments the HTTP message transport backend for the
--   <a>Network</a> monad.
module Choreography.Network.Http

-- | A backend for running <a>Network</a> behaviors over HTTP. The
--   configuration specifies how locations are mapped to network hosts and
--   ports.
newtype HttpConfig
HttpConfig :: HashMap LocTm BaseUrl -> HttpConfig
[locToUrl] :: HttpConfig -> HashMap LocTm BaseUrl

-- | The address of a party/location.
type Host = String

-- | The port of a party/location.
type Port = Int

-- | Create a HTTP backend configuration from a association list that maps
--   locations to network hosts and ports.
mkHttpConfig :: [(LocTm, (Host, Port))] -> HttpConfig

-- | The list of locations known to a backend.
locs :: HttpConfig -> [LocTm]

-- | The channels a location uses to recieve messages from various peers.
type RecvChans = HashMap LocTm (Chan String)

-- | Make the channels that will be used to recieve messages.
mkRecvChans :: HttpConfig -> IO RecvChans

-- | A <a>Servant.API</a> API.
type API = "send" :> Capture "from" LocTm :> ReqBody '[PlainText] String :> PostNoContent

-- | Run a <a>Network</a> behavior, using the provided HTTP backend.
runNetworkHttp :: MonadIO m => HttpConfig -> LocTm -> Network m a -> m a
instance Choreography.Network.Backend Choreography.Network.Http.HttpConfig


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

-- | Monad for writing choreographies. <tt>ps</tt> is the "census", the
--   list of parties who are present in (that part of) the choreography.
--   <tt>m</tt> is the local monad afforded to parties by <a>locally'</a>.
type Choreo ps m = Freer (ChoreoSig ps m)

-- | Communicate a value to all present parties.
broadcast' :: (Show a, Read a, KnownSymbol l) => Member l ps -> (Member l ls, Located ls a) -> Choreo ps m a
infix 4 `broadcast'`

-- | Access to the inner "local" monad. Since the type of <a>locally'</a>
--   restricts the census to a single party, you'll usually want to use
--   <a>locally</a> instead.
locally' :: KnownSymbol l => (Unwrap l -> m a) -> Choreo '[l] 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.
congruently' :: KnownSymbols ls => (Unwraps ls -> a) -> Choreo ls m a
infix 4 `congruently'`

-- | Lift a choreography of involving fewer parties into the larger party
--   space. Adds a `Located ls` layer to the return type.
enclave :: KnownSymbols ls => Subset ls ps -> Choreo ls m a -> Choreo ps m (Located ls a)
infix 4 `enclave`

-- | Endpoint projection.
epp :: forall ps b m. (Monad m, KnownSymbols ps) => Choreo ps m b -> LocTm -> Network m b

-- | Run a <a>Choreo</a> 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.
runChoreo :: forall p ps b m. Monad m => Choreo (p ': ps) m b -> m b

-- | A single value known to many parties.
data Located (ls :: [LocTy]) 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 Unwrap (q :: LocTy) = forall ls a. Member q 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.)
type Unwraps (qs :: [LocTy]) = forall ls a. Subset qs ls -> Located ls a -> a

-- | Un-nest located values.
flatten :: Subset ls ms -> Subset ls ns -> Located ms (Located ns a) -> Located ls a
infix 3 `flatten`

-- | Cast a <a>Located</a> value to a smaller ownership set; useful when
--   working with functions whos arguments have explict ownership sets.
othersForget :: Subset ls owners -> Located owners a -> Located ls a

-- | Wrap a value as a located value. This should be safe to export, while
--   exporting the constuctor would enable pattern matching.
wrap :: a -> Located l a


-- | Operations for writing choreographies.
module Choreography.Choreography

-- | Perform a local computation at a given location.
locally :: KnownSymbol (l :: LocTy) => Member l ps -> (Unwrap l -> m a) -> Choreo ps m (Located '[l] a)
infix 4 `locally`

-- | Perform the exact same pure computation in replicate at multiple
--   locations. The computation can not use anything local to an individual
--   party, including their identity.
congruently :: forall ls a ps m. KnownSymbols ls => Subset ls ps -> (Unwraps ls -> a) -> Choreo ps m (Located ls a)
infix 4 `congruently`

-- | Unwrap a value known to the entire census.
naked :: KnownSymbols ps => Subset ps qs -> Located qs a -> Choreo ps m a

-- | Writing out the first argument to <a>~&gt;</a> can be done a few
--   different ways depending on context, represented by this class.
class (KnownSymbol loc) => CanSend struct loc val owners census | struct -> loc val owners census
presentToSend :: CanSend struct loc val owners census => struct -> Member loc census
ownsMessagePayload :: CanSend struct loc val owners census => struct -> Member loc owners
structMessagePayload :: CanSend struct loc val owners census => struct -> Located owners val

-- | Send a value from one party to the entire census.
broadcast :: forall l a ps ls m s. (Show a, Read a, KnownSymbol l, KnownSymbols ps, CanSend s l a ls ps) => s -> Choreo ps m a

-- | Communication between a sender and a list of receivers.
(~>) :: (Show a, Read a, KnownSymbol l, KnownSymbols ls', CanSend s l a ls ps) => s -> Subset ls' ps -> Choreo ps m (Located ls' a)
infix 4 ~>

-- | Lift a choreography involving fewer parties into the larger party
--   space. This version, where the returned value is Located at the entire
--   enclave, does not add a Located layer.
enclaveToAll :: forall ls a ps m. KnownSymbols ls => Subset ls ps -> Choreo ls m (Located ls a) -> Choreo ps m (Located ls a)
infix 4 `enclaveToAll`

-- | Lift a choreography of involving fewer parties into the larger party
--   space. This version, where the returned value is already Located, does
--   not add a Located layer.
enclaveTo :: forall ls a rs ps m. KnownSymbols ls => Subset ls ps -> Subset rs ls -> Choreo ls m (Located rs a) -> Choreo ps m (Located rs a)
infix 4 `enclaveTo`
instance GHC.TypeLits.KnownSymbol l => Choreography.Choreography.CanSend (Choreography.Locations.Member l ps, (Choreography.Locations.Member l ls, Choreography.Core.Located ls a)) l a ls ps
instance (GHC.TypeLits.KnownSymbol l, Choreography.Locations.Batteries.ExplicitMember l ls) => Choreography.Choreography.CanSend (Choreography.Locations.Member l ps, Choreography.Core.Located ls a) l a ls ps
instance GHC.TypeLits.KnownSymbol l => Choreography.Choreography.CanSend (Choreography.Locations.Member l ls, Choreography.Locations.Subset ls ps, Choreography.Core.Located ls a) l a ls ps


-- | A zoo of helpful derived functions for writing choreographies.
module Choreography.Choreography.Batteries

-- | Perform a local computation, yielding nothing.
locally_ :: KnownSymbol l => Member l ps -> (Unwrap l -> m ()) -> Choreo ps m ()
infix 4 `locally_`

-- | Perform a local computation that doesn't need to unwrap any existing
--   <a>Located</a> values.
_locally :: KnownSymbol l => Member l ps -> m a -> Choreo ps m (Located '[l] a)
infix 4 `_locally`

-- | Perform a local computation that doesn't need to unwrap any existing
--   <a>Located</a> values and yields nothing.
_locally_ :: KnownSymbol l => Member l ps -> m () -> Choreo ps m ()
infix 4 `_locally_`

-- | Perform a pure computation at a single location.
purely :: forall l a ps m. KnownSymbol l => Member l ps -> (Unwrap l -> a) -> Choreo ps m (Located '[l] a)
infix 4 `purely`

-- | A variant of <a>~&gt;</a> that sends the result of a local
--   computation.
(~~>) :: forall a l ls' m ps. (Show a, Read a, KnownSymbol l, KnownSymbols ls') => (Member l ps, Unwrap l -> m a) -> Subset ls' ps -> Choreo ps m (Located ls' a)
infix 4 ~~>

-- | A variant of <a>~&gt;</a> that sends the result of a local action that
--   doesn't use existing <a>Located</a> variables.
(-~>) :: forall a l ls' m ps. (Show a, Read a, KnownSymbol l, KnownSymbols ls') => (Member l ps, m a) -> Subset ls' ps -> Choreo ps m (Located ls' a)
infix 4 -~>

-- | A variant of <a>~&gt;</a> that doesn't use the local monad.
(*~>) :: forall a l ls' m ps. (Show a, Read a, KnownSymbol l, KnownSymbols ls') => (Member l ps, Unwrap l -> a) -> Subset ls' ps -> Choreo ps m (Located ls' a)
infix 4 *~>

-- | Conditionally execute choreographies based on a located value.
--   Automatically enclaves.
cond :: KnownSymbols ls => (Subset ls ps, (Subset ls qs, Located qs a)) -> (a -> Choreo ls m b) -> Choreo ps m (Located ls b)


-- | Types, functions, and structures for writing choreographies with
--   variable numbers of participants.
module Choreography.Polymorphism

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

-- | An impredicative quantified type. Wrapping it up in <a>PIndexed</a>
--   wherever possible will avoid a lot of type errors and headache.
type PIndex ls f = forall l. (KnownSymbol l) => Member l ls -> f l

-- | Sequence computations indexed by parties. Converts a <a>PIndexed</a>
--   of computations into a computation yielding a <a>PIndexed</a>.
--   Strongly analogous to <a>sequence</a>. In most cases, the
--   <a>choreographic functions</a> below will be easier to use than
--   messing around with <a>Compose</a>.
sequenceP :: forall b (ls :: [LocTy]) m. (KnownSymbols ls, Monad m) => PIndexed ls (Compose m b) -> m (PIndexed ls b)

-- | A collection of values, all of the same type, assigned to each element
--   of the type-level list.
newtype Quire parties a
Quire :: PIndexed parties (Const a) -> Quire parties a
[asPIndexed] :: Quire parties a -> PIndexed parties (Const a)

-- | Access a value in a <a>Quire</a> by its index.
getLeaf :: KnownSymbol p => Quire parties a -> Member p parties -> a

-- | Package a function as a <a>Quire</a>.
stackLeaves :: forall ps a. (forall p. KnownSymbol p => Member p ps -> a) -> Quire ps a

-- | Get the head item from a <a>Quire</a>.
qHead :: KnownSymbol p => Quire (p ': ps) a -> a

-- | Get the tail of a <a>Quire</a>.
qTail :: Quire (p ': ps) a -> Quire ps a

-- | Prepend a value to a <a>Quire</a>. The corresponding <a>Symbol</a> to
--   bind it to must be provided by type-application if it can't be
--   infered.
qCons :: forall p ps a. a -> Quire ps a -> Quire (p ': ps) a

-- | An empty <a>Quire</a>.
qNil :: Quire '[] a

-- | Apply a function to a single item in a <a>Quire</a>.
qModify :: forall p ps a. (KnownSymbol p, KnownSymbols ps) => Member p ps -> (a -> a) -> Quire ps a -> Quire ps a

-- | A unified representation of possibly-distinct homogeneous values owned
--   by many parties.
type Faceted parties common a = PIndexed parties (Facet a common)

-- | Repackages <a>Located</a> with the type arguments correctly arranged
--   for use with <a>PIndexed</a>.
newtype Facet a common p
Facet :: Located (p ': common) a -> Facet a common p
[getFacet] :: Facet a common p -> Located (p ': common) a

-- | Get a <a>Located</a> value of a <a>Faceted</a> at a given location.
localize :: KnownSymbol l => Member l ls -> Faceted ls common a -> Located (l ': common) a

-- | In a context where unwrapping located values is possible, get the
--   respective value stored in a <a>Faceted</a>.
viewFacet :: KnownSymbol l => Unwrap l -> Member l ls -> Faceted ls common a -> a

-- | Perform a local computation at all of a list of parties, yielding a
--   <a>Faceted</a>.
parallel :: forall ls a ps m. KnownSymbols ls => Subset ls ps -> (forall l. KnownSymbol l => Member l ls -> Unwrap l -> m a) -> Choreo ps m (Faceted ls '[] a)

-- | Perform a local computation at all of a list of parties, yielding
--   nothing.
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, that doesn't use any existing
--   <a>Located</a> values and doesn't depend on the respective party's
--   identity, at all of a list of parties, yielding a <a>Faceted</a>.
_parallel :: forall ls a ps m. KnownSymbols ls => Subset ls ps -> m a -> Choreo ps m (Faceted ls '[] a)

-- | Perform a given choreography for each of several parties, giving each
--   of them a return value that form a new <a>Faceted</a>.
fanOut :: KnownSymbols qs => (forall q. KnownSymbol q => Member q qs -> Choreo ps m (Located (q ': rs) a)) -> Choreo ps m (Faceted qs rs a)

-- | Perform a given choreography for each of several parties; the return
--   values are known to recipients but not necessarily to the
--   loop-parties.
fanIn :: (KnownSymbols qs, KnownSymbols rs) => Subset rs ps -> (forall q. KnownSymbol q => Member q qs -> Choreo ps m (Located rs a)) -> Choreo ps m (Located rs (Quire qs a))

-- | The owner of a <a>Quire</a> sends its elements to their respective
--   parties, resulting in a <a>Faceted</a>. This represents the "scatter"
--   idea common in parallel computing contexts.
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 many owners of a <a>Faceted</a> each send their respective values
--   to a constant list of recipients, resulting in a <a>Quire</a>. This
--   represents the "gather" 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))
instance Choreography.Locations.KnownSymbols parties => GHC.Base.Functor (Choreography.Polymorphism.Quire parties)
instance Choreography.Locations.KnownSymbols parties => GHC.Base.Applicative (Choreography.Polymorphism.Quire parties)
instance Choreography.Locations.KnownSymbols parties => Data.Foldable.Foldable (Choreography.Polymorphism.Quire parties)
instance Choreography.Locations.KnownSymbols parties => Data.Traversable.Traversable (Choreography.Polymorphism.Quire parties)
instance (Choreography.Locations.KnownSymbols parties, GHC.Classes.Eq a) => GHC.Classes.Eq (Choreography.Polymorphism.Quire parties a)
instance (Choreography.Locations.KnownSymbols parties, GHC.Show.Show a) => GHC.Show.Show (Choreography.Polymorphism.Quire parties a)


-- | This is just a wrapper module to allow more concise imports. For
--   documentation, you should probably start in <a>Choreography.Core</a>.
module Choreography

-- | Run a choreography with a message transport backend...
runChoreography :: (Backend config, MonadIO m, KnownSymbols ps) => config -> Choreo ps m a -> LocTm -> m a