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

import Choreography.Choreography
import Choreography.Choreography.Batteries ((*~>))
import Choreography.Core
import Choreography.Locations
import Control.Monad (void)
import Data.Foldable (toList)
import Data.Functor.Compose (Compose (Compose, getCompose))
import Data.Functor.Const (Const (Const, getConst))
import GHC.TypeLits

-- * The root abstraction

-- | A mapping, accessed by `Member` terms, from types (`Symbol`s) 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 t`Quire`.
--   If the types vary only in that they are `Located` at the indexing party, use `Faceted`.
--   t`PIndexed` generalizes those two types in a way that's not usually necessary when writing choreographies.
newtype PIndexed ls f = PIndexed {forall (ls :: [Symbol]) (f :: Symbol -> *).
PIndexed ls f -> PIndex ls f
pindex :: PIndex ls f}

-- | An impredicative quantified type. Wrapping it up in t`PIndexed` 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 t`PIndexed` of computations into a computation yielding a t`PIndexed`.
--   Strongly analogous to 'Data.Traversable.sequence'.
--   In most cases, the [choreographic functions](#g:choreographicfunctions) below will be easier to use
--   than messing around with `Data.Functor.Compose.Compose`.
sequenceP ::
  forall b (ls :: [LocTy]) m.
  (KnownSymbols ls, Monad m) =>
  PIndexed ls (Compose m b) ->
  m (PIndexed ls b)
sequenceP :: forall (b :: Symbol -> *) (ls :: [Symbol]) (m :: * -> *).
(KnownSymbols ls, Monad m) =>
PIndexed ls (Compose m b) -> m (PIndexed ls b)
sequenceP (PIndexed PIndex ls (Compose m b)
f) = case forall (ls :: [Symbol]). KnownSymbols ls => TySpine ls
tySpine @ls of
  TySpine ls
TyCons -> do
    b <- Compose m b h -> m (b h)
forall {k1} {k2} (f :: k1 -> *) (g :: k2 -> k1) (a :: k2).
Compose f g a -> f (g a)
getCompose (Compose m b h -> m (b h)) -> Compose m b h -> m (b h)
forall a b. (a -> b) -> a -> b
$ Member h ls -> Compose m b h
PIndex ls (Compose m b)
f Member h ls
Member h (h : ts)
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First
    PIndexed fTail <- sequenceP (PIndexed $ f . Later)
    let retVal :: PIndex ls b
        retVal Member l ls
First = b h
b l
b
        retVal (Later Member l xs1
ltr) = Member l ts -> b l
PIndex ts b
fTail Member l ts
Member l xs1
ltr
    pure $ PIndexed retVal
  TySpine ls
TyNil -> PIndexed ls b -> m (PIndexed ls b)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (PIndexed ls b -> m (PIndexed ls b))
-> PIndexed ls b -> m (PIndexed ls b)
forall a b. (a -> b) -> a -> b
$ PIndex ls b -> PIndexed ls b
forall (ls :: [Symbol]) (f :: Symbol -> *).
PIndex ls f -> PIndexed ls f
PIndexed \case {}

-- * A type-indexed vector type

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

-- | Access a value in a t`Quire` by its index.
getLeaf :: (KnownSymbol p) => Quire parties a -> Member p parties -> a
getLeaf :: forall (p :: Symbol) (parties :: [Symbol]) a.
KnownSymbol p =>
Quire parties a -> Member p parties -> a
getLeaf (Quire (PIndexed PIndex parties (Const a)
q)) Member p parties
p = Const a p -> a
forall {k} a (b :: k). Const a b -> a
getConst (Const a p -> a) -> Const a p -> a
forall a b. (a -> b) -> a -> b
$ Member p parties -> Const a p
PIndex parties (Const a)
q Member p parties
p

-- | Package a function as a t`Quire`.
stackLeaves :: forall ps a. (forall p. (KnownSymbol p) => Member p ps -> a) -> Quire ps a
stackLeaves :: forall (ps :: [Symbol]) a.
(forall (p :: Symbol). KnownSymbol p => Member p ps -> a)
-> Quire ps a
stackLeaves forall (p :: Symbol). KnownSymbol p => Member p ps -> a
f = PIndexed ps (Const a) -> Quire ps a
forall (parties :: [Symbol]) a.
PIndexed parties (Const a) -> Quire parties a
Quire (PIndexed ps (Const a) -> Quire ps a)
-> (PIndex ps (Const a) -> PIndexed ps (Const a))
-> PIndex ps (Const a)
-> Quire ps a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PIndex ps (Const a) -> PIndexed ps (Const a)
forall (ls :: [Symbol]) (f :: Symbol -> *).
PIndex ls f -> PIndexed ls f
PIndexed (PIndex ps (Const a) -> Quire ps a)
-> PIndex ps (Const a) -> Quire ps a
forall a b. (a -> b) -> a -> b
$ a -> Const a l
forall {k} a (b :: k). a -> Const a b
Const (a -> Const a l) -> (Member l ps -> a) -> Member l ps -> Const a l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Member l ps -> a
forall (p :: Symbol). KnownSymbol p => Member p ps -> a
f

-- | Get the head item from a t`Quire`.
qHead :: (KnownSymbol p) => Quire (p ': ps) a -> a
qHead :: forall (p :: Symbol) (ps :: [Symbol]) a.
KnownSymbol p =>
Quire (p : ps) a -> a
qHead (Quire (PIndexed PIndex (p : ps) (Const a)
f)) = Const a p -> a
forall {k} a (b :: k). Const a b -> a
getConst (Const a p -> a) -> Const a p -> a
forall a b. (a -> b) -> a -> b
$ Member p (p : ps) -> Const a p
PIndex (p : ps) (Const a)
f Member p (p : ps)
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First

-- | Get the tail of a t`Quire`.
qTail :: Quire (p ': ps) a -> Quire ps a
qTail :: forall (p :: Symbol) (ps :: [Symbol]) a.
Quire (p : ps) a -> Quire ps a
qTail (Quire (PIndexed PIndex (p : ps) (Const a)
f)) = PIndexed ps (Const a) -> Quire ps a
forall (parties :: [Symbol]) a.
PIndexed parties (Const a) -> Quire parties a
Quire (PIndexed ps (Const a) -> Quire ps a)
-> (PIndex ps (Const a) -> PIndexed ps (Const a))
-> PIndex ps (Const a)
-> Quire ps a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PIndex ps (Const a) -> PIndexed ps (Const a)
forall (ls :: [Symbol]) (f :: Symbol -> *).
PIndex ls f -> PIndexed ls f
PIndexed (PIndex ps (Const a) -> Quire ps a)
-> PIndex ps (Const a) -> Quire ps a
forall a b. (a -> b) -> a -> b
$ Member l (p : ps) -> Const a l
PIndex (p : ps) (Const a)
f (Member l (p : ps) -> Const a l)
-> (Member l ps -> Member l (p : ps)) -> Member l ps -> Const a l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Member l ps -> Member l (p : ps)
forall {k} (x :: k) (xs1 :: [k]) (y :: k).
Member x xs1 -> Member x (y : xs1)
Later

-- | Prepend a value to a t`Quire`.
--   The corresponding `Symbol` 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
qCons :: forall (p :: Symbol) (ps :: [Symbol]) a.
a -> Quire ps a -> Quire (p : ps) a
qCons a
a (Quire (PIndexed PIndex ps (Const a)
f)) = PIndexed (p : ps) (Const a) -> Quire (p : ps) a
forall (parties :: [Symbol]) a.
PIndexed parties (Const a) -> Quire parties a
Quire (PIndexed (p : ps) (Const a) -> Quire (p : ps) a)
-> (PIndex (p : ps) (Const a) -> PIndexed (p : ps) (Const a))
-> PIndex (p : ps) (Const a)
-> Quire (p : ps) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PIndex (p : ps) (Const a) -> PIndexed (p : ps) (Const a)
forall (ls :: [Symbol]) (f :: Symbol -> *).
PIndex ls f -> PIndexed ls f
PIndexed (PIndex (p : ps) (Const a) -> Quire (p : ps) a)
-> PIndex (p : ps) (Const a) -> Quire (p : ps) a
forall a b. (a -> b) -> a -> b
$ \case
  Member l (p : ps)
First -> a -> Const a l
forall {k} a (b :: k). a -> Const a b
Const a
a
  Later Member l xs1
mps -> Member l ps -> Const a l
PIndex ps (Const a)
f Member l ps
Member l xs1
mps

-- | An empty t`Quire`.
qNil :: Quire '[] a
qNil :: forall a. Quire '[] a
qNil = PIndexed '[] (Const a) -> Quire '[] a
forall (parties :: [Symbol]) a.
PIndexed parties (Const a) -> Quire parties a
Quire (PIndexed '[] (Const a) -> Quire '[] a)
-> PIndexed '[] (Const a) -> Quire '[] a
forall a b. (a -> b) -> a -> b
$ PIndex '[] (Const a) -> PIndexed '[] (Const a)
forall (ls :: [Symbol]) (f :: Symbol -> *).
PIndex ls f -> PIndexed ls f
PIndexed \case {}

-- | Apply a function to a single item in a t`Quire`.
qModify :: forall p ps a. (KnownSymbol p, KnownSymbols ps) => Member p ps -> (a -> a) -> Quire ps a -> Quire ps a
qModify :: forall (p :: Symbol) (ps :: [Symbol]) a.
(KnownSymbol p, KnownSymbols ps) =>
Member p ps -> (a -> a) -> Quire ps a -> Quire ps a
qModify Member p ps
First a -> a
f Quire ps a
q = a -> a
f (Quire (p : xs') a -> a
forall (p :: Symbol) (ps :: [Symbol]) a.
KnownSymbol p =>
Quire (p : ps) a -> a
qHead Quire ps a
Quire (p : xs') a
q) a -> Quire xs' a -> Quire (p : xs') a
forall (p :: Symbol) (ps :: [Symbol]) a.
a -> Quire ps a -> Quire (p : ps) a
`qCons` Quire (p : xs') a -> Quire xs' a
forall (p :: Symbol) (ps :: [Symbol]) a.
Quire (p : ps) a -> Quire ps a
qTail Quire ps a
Quire (p : xs') a
q
qModify (Later Member p xs1
m) a -> a
f Quire ps a
q = case forall (ls :: [Symbol]). KnownSymbols ls => TySpine ls
tySpine @ps of TySpine ps
TyCons -> Quire (y : xs1) a -> a
forall (p :: Symbol) (ps :: [Symbol]) a.
KnownSymbol p =>
Quire (p : ps) a -> a
qHead Quire ps a
Quire (y : xs1) a
q a -> Quire xs1 a -> Quire (y : xs1) a
forall (p :: Symbol) (ps :: [Symbol]) a.
a -> Quire ps a -> Quire (p : ps) a
`qCons` Member p xs1 -> (a -> a) -> Quire xs1 a -> Quire xs1 a
forall (p :: Symbol) (ps :: [Symbol]) a.
(KnownSymbol p, KnownSymbols ps) =>
Member p ps -> (a -> a) -> Quire ps a -> Quire ps a
qModify Member p xs1
m a -> a
f (Quire (y : xs1) a -> Quire xs1 a
forall (p :: Symbol) (ps :: [Symbol]) a.
Quire (p : ps) a -> Quire ps a
qTail Quire ps a
Quire (y : xs1) a
q)

instance forall parties. (KnownSymbols parties) => Functor (Quire parties) where
  fmap :: forall a b. (a -> b) -> Quire parties a -> Quire parties b
fmap a -> b
f Quire parties a
q = case forall (ls :: [Symbol]). KnownSymbols ls => TySpine ls
tySpine @parties of
    TySpine parties
TyCons -> a -> b
f (Quire (h : ts) a -> a
forall (p :: Symbol) (ps :: [Symbol]) a.
KnownSymbol p =>
Quire (p : ps) a -> a
qHead Quire parties a
Quire (h : ts) a
q) b -> Quire ts b -> Quire (h : ts) b
forall (p :: Symbol) (ps :: [Symbol]) a.
a -> Quire ps a -> Quire (p : ps) a
`qCons` (a -> b) -> Quire ts a -> Quire ts b
forall a b. (a -> b) -> Quire ts a -> Quire ts b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (Quire (h : ts) a -> Quire ts a
forall (p :: Symbol) (ps :: [Symbol]) a.
Quire (p : ps) a -> Quire ps a
qTail Quire parties a
Quire (h : ts) a
q)
    TySpine parties
TyNil -> Quire parties b
Quire '[] b
forall a. Quire '[] a
qNil

instance forall parties. (KnownSymbols parties) => Applicative (Quire parties) where
  pure :: forall a. a -> Quire parties a
pure a
a = PIndexed parties (Const a) -> Quire parties a
forall (parties :: [Symbol]) a.
PIndexed parties (Const a) -> Quire parties a
Quire (PIndexed parties (Const a) -> Quire parties a)
-> (PIndex parties (Const a) -> PIndexed parties (Const a))
-> PIndex parties (Const a)
-> Quire parties a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PIndex parties (Const a) -> PIndexed parties (Const a)
forall (ls :: [Symbol]) (f :: Symbol -> *).
PIndex ls f -> PIndexed ls f
PIndexed (PIndex parties (Const a) -> Quire parties a)
-> PIndex parties (Const a) -> Quire parties a
forall a b. (a -> b) -> a -> b
$ Const a l -> Member l parties -> Const a l
forall a b. a -> b -> a
const (a -> Const a l
forall {k} a (b :: k). a -> Const a b
Const a
a)
  Quire parties (a -> b)
qf <*> :: forall a b.
Quire parties (a -> b) -> Quire parties a -> Quire parties b
<*> Quire parties a
qa = case forall (ls :: [Symbol]). KnownSymbols ls => TySpine ls
tySpine @parties of
    TySpine parties
TyCons -> Quire (h : ts) (a -> b) -> a -> b
forall (p :: Symbol) (ps :: [Symbol]) a.
KnownSymbol p =>
Quire (p : ps) a -> a
qHead Quire parties (a -> b)
Quire (h : ts) (a -> b)
qf (Quire (h : ts) a -> a
forall (p :: Symbol) (ps :: [Symbol]) a.
KnownSymbol p =>
Quire (p : ps) a -> a
qHead Quire parties a
Quire (h : ts) a
qa) b -> Quire ts b -> Quire (h : ts) b
forall (p :: Symbol) (ps :: [Symbol]) a.
a -> Quire ps a -> Quire (p : ps) a
`qCons` (Quire (h : ts) (a -> b) -> Quire ts (a -> b)
forall (p :: Symbol) (ps :: [Symbol]) a.
Quire (p : ps) a -> Quire ps a
qTail Quire parties (a -> b)
Quire (h : ts) (a -> b)
qf Quire ts (a -> b) -> Quire ts a -> Quire ts b
forall a b. Quire ts (a -> b) -> Quire ts a -> Quire ts b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Quire (h : ts) a -> Quire ts a
forall (p :: Symbol) (ps :: [Symbol]) a.
Quire (p : ps) a -> Quire ps a
qTail Quire parties a
Quire (h : ts) a
qa)
    TySpine parties
TyNil -> Quire parties b
Quire '[] b
forall a. Quire '[] a
qNil

instance forall parties. (KnownSymbols parties) => Foldable (Quire parties) where
  foldMap :: forall m a. Monoid m => (a -> m) -> Quire parties a -> m
foldMap a -> m
f Quire parties a
q = case forall (ls :: [Symbol]). KnownSymbols ls => TySpine ls
tySpine @parties of
    TySpine parties
TyCons -> a -> m
f (Quire (h : ts) a -> a
forall (p :: Symbol) (ps :: [Symbol]) a.
KnownSymbol p =>
Quire (p : ps) a -> a
qHead Quire parties a
Quire (h : ts) a
q) m -> m -> m
forall a. Semigroup a => a -> a -> a
<> (a -> m) -> Quire ts a -> m
forall m a. Monoid m => (a -> m) -> Quire ts a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap a -> m
f (Quire (h : ts) a -> Quire ts a
forall (p :: Symbol) (ps :: [Symbol]) a.
Quire (p : ps) a -> Quire ps a
qTail Quire parties a
Quire (h : ts) a
q)
    TySpine parties
TyNil -> m
forall a. Monoid a => a
mempty

instance forall parties. (KnownSymbols parties) => Traversable (Quire parties) where
  sequenceA :: forall (f :: * -> *) a.
Applicative f =>
Quire parties (f a) -> f (Quire parties a)
sequenceA Quire parties (f a)
q = case forall (ls :: [Symbol]). KnownSymbols ls => TySpine ls
tySpine @parties of
    TySpine parties
TyCons -> a -> Quire ts a -> Quire (h : ts) a
forall (p :: Symbol) (ps :: [Symbol]) a.
a -> Quire ps a -> Quire (p : ps) a
qCons (a -> Quire ts a -> Quire (h : ts) a)
-> f a -> f (Quire ts a -> Quire (h : ts) a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Quire (h : ts) (f a) -> f a
forall (p :: Symbol) (ps :: [Symbol]) a.
KnownSymbol p =>
Quire (p : ps) a -> a
qHead Quire parties (f a)
Quire (h : ts) (f a)
q f (Quire ts a -> Quire (h : ts) a)
-> f (Quire ts a) -> f (Quire (h : ts) a)
forall a b. f (a -> b) -> f a -> f b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Quire ts (f a) -> f (Quire ts a)
forall (t :: * -> *) (f :: * -> *) a.
(Traversable t, Applicative f) =>
t (f a) -> f (t a)
forall (f :: * -> *) a.
Applicative f =>
Quire ts (f a) -> f (Quire ts a)
sequenceA (Quire (h : ts) (f a) -> Quire ts (f a)
forall (p :: Symbol) (ps :: [Symbol]) a.
Quire (p : ps) a -> Quire ps a
qTail Quire parties (f a)
Quire (h : ts) (f a)
q)
    TySpine parties
TyNil -> Quire parties a -> f (Quire parties a)
forall a. a -> f a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Quire parties a
Quire '[] a
forall a. Quire '[] a
qNil

instance forall parties a. (KnownSymbols parties, Eq a) => Eq (Quire parties a) where
  Quire parties a
q1 == :: Quire parties a -> Quire parties a -> Bool
== Quire parties a
q2 = Quire parties Bool -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and (Quire parties Bool -> Bool) -> Quire parties Bool -> Bool
forall a b. (a -> b) -> a -> b
$ a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) (a -> a -> Bool) -> Quire parties a -> Quire parties (a -> Bool)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Quire parties a
q1 Quire parties (a -> Bool) -> Quire parties a -> Quire parties Bool
forall a b.
Quire parties (a -> b) -> Quire parties a -> Quire parties b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Quire parties a
q2

instance forall parties a. (KnownSymbols parties, Show a) => Show (Quire parties a) where
  show :: Quire parties a -> String
show Quire parties a
q = [(String, a)] -> String
forall a. Show a => a -> String
show ([(String, a)] -> String) -> [(String, a)] -> String
forall a b. (a -> b) -> a -> b
$ Subset parties parties -> [String]
forall (ls :: [Symbol]) (ps :: [Symbol]).
KnownSymbols ls =>
Subset ls ps -> [String]
toLocs (forall (xs :: [Symbol]). Subset xs xs
forall {k} (xs :: [k]). Subset xs xs
refl @parties) [String] -> [a] -> [(String, a)]
forall a b. [a] -> [b] -> [(a, b)]
`zip` Quire parties a -> [a]
forall a. Quire parties a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Quire parties a
q

-- Many more instances are possible...

-- * Non-congruent parallel located values

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

-- | Repackages `Located` with the type arguments correctly arranged for use with t`PIndexed`.
newtype Facet a common p = Facet {forall a (common :: [Symbol]) (p :: Symbol).
Facet a common p -> Located (p : common) a
getFacet :: Located (p ': common) a}

-- | Get a `Located` value of a `Faceted` at a given location.
localize :: (KnownSymbol l) => Member l ls -> Faceted ls common a -> Located (l ': common) a
localize :: forall (l :: Symbol) (ls :: [Symbol]) (common :: [Symbol]) a.
KnownSymbol l =>
Member l ls -> Faceted ls common a -> Located (l : common) a
localize Member l ls
l (PIndexed PIndex ls (Facet a common)
f) = Facet a common l -> Located (l : common) a
forall a (common :: [Symbol]) (p :: Symbol).
Facet a common p -> Located (p : common) a
getFacet (Facet a common l -> Located (l : common) a)
-> Facet a common l -> Located (l : common) a
forall a b. (a -> b) -> a -> b
$ Member l ls -> Facet a common l
PIndex ls (Facet a common)
f Member l ls
l

-- | In a context where unwrapping located values is possible, get the respective value stored in a `Faceted`.
viewFacet :: (KnownSymbol l) => Unwrap l -> Member l ls -> Faceted ls common a -> a
viewFacet :: forall (l :: Symbol) (ls :: [Symbol]) (common :: [Symbol]) a.
KnownSymbol l =>
Unwrap l -> Member l ls -> Faceted ls common a -> a
viewFacet Unwrap l
un Member l ls
l = Member l (l : common) -> Located (l : common) a -> a
Unwrap l
un Member l (l : common)
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First (Located (l : common) a -> a)
-> (Faceted ls common a -> Located (l : common) a)
-> Faceted ls common a
-> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Member l ls -> Faceted ls common a -> Located (l : common) a
forall (l :: Symbol) (ls :: [Symbol]) (common :: [Symbol]) a.
KnownSymbol l =>
Member l ls -> Faceted ls common a -> Located (l : common) a
localize Member l ls
l

{-
unsafeFacet :: [Maybe a] -> Member l ls -> Facet a common l -- providing this as a helper function is pretty sketchy, if we don't need it delete it.
unsafeFacet (Just a : _) First = Facet $ wrap a
unsafeFacet (Nothing : _) First = Empty
unsafeFacet (_ : as) (Later l) = unsafeFacet as l
unsafeFacet [] _ = error "The provided list isn't long enough to use as a Faceted over the intended parties."
-}

-- * #choreographicfunctions# Choreographic functions

-- | Perform a local computation at all of a list of parties, yielding a `Faceted`.
parallel ::
  forall ls a ps m.
  (KnownSymbols ls) =>
  -- | The parties who will do the computation must be present in the census.
  Subset ls ps ->
  -- | The local computation has access to the identity of the party in question,
  --   in additon to the usual unwrapper function.
  (forall l. (KnownSymbol l) => Member l ls -> Unwrap l -> m a) -> -- Could promote this to PIndexed too, but ergonomics might be worse?
  Choreo ps m (Faceted ls '[] 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 '[] a)
parallel Subset ls ps
ls forall (l :: Symbol).
KnownSymbol l =>
Member l ls -> Unwrap l -> m a
m = (forall (q :: Symbol).
 KnownSymbol q =>
 Member q ls -> Choreo ps m (Located '[q] a))
-> Choreo ps m (Faceted ls '[] a)
forall (qs :: [Symbol]) (ps :: [Symbol]) (m :: * -> *)
       (rs :: [Symbol]) 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)
fanOut \Member q ls
mls -> Member q ps -> (Unwrap q -> m a) -> Choreo ps m (Located '[q] a)
forall (l :: Symbol) (ps :: [Symbol]) (m :: * -> *) a.
KnownSymbol l =>
Member l ps -> (Unwrap l -> m a) -> Choreo ps m (Located '[l] a)
locally (Subset ls ps -> forall (x :: Symbol). Member x ls -> Member x ps
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper Subset ls ps
ls Member q ls
mls) (Member q ls -> Unwrap q -> m a
forall (l :: Symbol).
KnownSymbol l =>
Member l ls -> Unwrap l -> m a
m Member q ls
mls)

-- | 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 ()
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_ Subset ls ps
ls forall (l :: Symbol).
KnownSymbol l =>
Member l ls -> Unwrap l -> m ()
m = Freer (ChoreoSig ps m) (Faceted ls '[] ())
-> Freer (ChoreoSig ps m) ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (Freer (ChoreoSig ps m) (Faceted ls '[] ())
 -> Freer (ChoreoSig ps m) ())
-> Freer (ChoreoSig ps m) (Faceted ls '[] ())
-> Freer (ChoreoSig ps m) ()
forall a b. (a -> b) -> a -> b
$ Subset ls ps
-> (forall (l :: Symbol).
    KnownSymbol l =>
    Member l ls -> Unwrap l -> m ())
-> Freer (ChoreoSig ps m) (Faceted ls '[] ())
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 '[] a)
parallel Subset ls ps
ls Member l ls -> Unwrap l -> m ()
forall (l :: Symbol).
KnownSymbol l =>
Member l ls -> Unwrap l -> m ()
m

-- | 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`.
_parallel :: forall ls a ps m. (KnownSymbols ls) => Subset ls ps -> m a -> Choreo ps m (Faceted ls '[] a)
_parallel :: forall (ls :: [Symbol]) a (ps :: [Symbol]) (m :: * -> *).
KnownSymbols ls =>
Subset ls ps -> m a -> Choreo ps m (Faceted ls '[] a)
_parallel Subset ls ps
ls m a
m = Subset ls ps
-> (forall (l :: Symbol).
    KnownSymbol l =>
    Member l ls -> Unwrap l -> m a)
-> Choreo ps m (Faceted ls '[] a)
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 '[] a)
parallel Subset ls ps
ls \Member l ls
_ Unwrap l
_ -> m a
m

-- | Perform a given choreography for each of several parties, giving each of them a return value that form a new `Faceted`.
fanOut ::
  (KnownSymbols qs) =>
  -- | The body.  -- kinda sketchy that rs might not be a subset of ps...
  (forall q. (KnownSymbol q) => Member q qs -> Choreo ps m (Located (q ': rs) a)) ->
  Choreo ps m (Faceted qs rs a)
fanOut :: forall (qs :: [Symbol]) (ps :: [Symbol]) (m :: * -> *)
       (rs :: [Symbol]) 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)
fanOut forall (q :: Symbol).
KnownSymbol q =>
Member q qs -> Choreo ps m (Located (q : rs) a)
body = PIndexed qs (Compose (Freer (ChoreoSig ps m)) (Facet a rs))
-> Freer (ChoreoSig ps m) (PIndexed qs (Facet a rs))
forall (b :: Symbol -> *) (ls :: [Symbol]) (m :: * -> *).
(KnownSymbols ls, Monad m) =>
PIndexed ls (Compose m b) -> m (PIndexed ls b)
sequenceP (PIndex qs (Compose (Freer (ChoreoSig ps m)) (Facet a rs))
-> PIndexed qs (Compose (Freer (ChoreoSig ps m)) (Facet a rs))
forall (ls :: [Symbol]) (f :: Symbol -> *).
PIndex ls f -> PIndexed ls f
PIndexed (PIndex qs (Compose (Freer (ChoreoSig ps m)) (Facet a rs))
 -> PIndexed qs (Compose (Freer (ChoreoSig ps m)) (Facet a rs)))
-> PIndex qs (Compose (Freer (ChoreoSig ps m)) (Facet a rs))
-> PIndexed qs (Compose (Freer (ChoreoSig ps m)) (Facet a rs))
forall a b. (a -> b) -> a -> b
$ Freer (ChoreoSig ps m) (Facet a rs l)
-> Compose (Freer (ChoreoSig ps m)) (Facet a rs) l
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Freer (ChoreoSig ps m) (Facet a rs l)
 -> Compose (Freer (ChoreoSig ps m)) (Facet a rs) l)
-> (Freer (ChoreoSig ps m) (Located (l : rs) a)
    -> Freer (ChoreoSig ps m) (Facet a rs l))
-> Freer (ChoreoSig ps m) (Located (l : rs) a)
-> Compose (Freer (ChoreoSig ps m)) (Facet a rs) l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located (l : rs) a -> Facet a rs l
forall a (common :: [Symbol]) (p :: Symbol).
Located (p : common) a -> Facet a common p
Facet (Located (l : rs) a -> Facet a rs l)
-> Freer (ChoreoSig ps m) (Located (l : rs) a)
-> Freer (ChoreoSig ps m) (Facet a rs l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Freer (ChoreoSig ps m) (Located (l : rs) a)
 -> Compose (Freer (ChoreoSig ps m)) (Facet a rs) l)
-> (Member l qs -> Freer (ChoreoSig ps m) (Located (l : rs) a))
-> Member l qs
-> Compose (Freer (ChoreoSig ps m)) (Facet a rs) l
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Member l qs -> Freer (ChoreoSig ps m) (Located (l : rs) a)
forall (q :: Symbol).
KnownSymbol q =>
Member q qs -> Choreo ps m (Located (q : rs) a)
body)

-- | 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) =>
  -- | The recipients.
  Subset rs ps ->
  -- | The body.
  (forall q. (KnownSymbol q) => Member q qs -> Choreo ps m (Located rs a)) ->
  Choreo ps m (Located rs (Quire qs a))
fanIn :: forall (qs :: [Symbol]) (rs :: [Symbol]) (ps :: [Symbol])
       (m :: * -> *) 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))
fanIn Subset rs ps
rs forall (q :: Symbol).
KnownSymbol q =>
Member q qs -> Choreo ps m (Located rs a)
body = do
  (PIndexed x) <- PIndexed
  qs (Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)))
-> Freer (ChoreoSig ps m) (PIndexed qs (Const (Located rs a)))
forall (b :: Symbol -> *) (ls :: [Symbol]) (m :: * -> *).
(KnownSymbols ls, Monad m) =>
PIndexed ls (Compose m b) -> m (PIndexed ls b)
sequenceP (PIndex qs (Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)))
-> PIndexed
     qs (Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)))
forall (ls :: [Symbol]) (f :: Symbol -> *).
PIndex ls f -> PIndexed ls f
PIndexed (PIndex
   qs (Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)))
 -> PIndexed
      qs (Compose (Freer (ChoreoSig ps m)) (Const (Located rs a))))
-> PIndex
     qs (Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)))
-> PIndexed
     qs (Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)))
forall a b. (a -> b) -> a -> b
$ Freer (ChoreoSig ps m) (Const (Located rs a) l)
-> Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)) l
forall {k} {k1} (f :: k -> *) (g :: k1 -> k) (a :: k1).
f (g a) -> Compose f g a
Compose (Freer (ChoreoSig ps m) (Const (Located rs a) l)
 -> Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)) l)
-> (Choreo ps m (Located rs a)
    -> Freer (ChoreoSig ps m) (Const (Located rs a) l))
-> Choreo ps m (Located rs a)
-> Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)) l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Located rs a -> Const (Located rs a) l
forall {k} a (b :: k). a -> Const a b
Const (Located rs a -> Const (Located rs a) l)
-> Choreo ps m (Located rs a)
-> Freer (ChoreoSig ps m) (Const (Located rs a) l)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Choreo ps m (Located rs a)
 -> Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)) l)
-> (Member l qs -> Choreo ps m (Located rs a))
-> Member l qs
-> Compose (Freer (ChoreoSig ps m)) (Const (Located rs a)) l
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Member l qs -> Choreo ps m (Located rs a)
forall (q :: Symbol).
KnownSymbol q =>
Member q qs -> Choreo ps m (Located rs a)
body)
  rs `congruently` \Unwraps rs
un -> (forall (p :: Symbol). KnownSymbol p => Member p qs -> a)
-> Quire qs a
forall (ps :: [Symbol]) a.
(forall (p :: Symbol). KnownSymbol p => Member p ps -> a)
-> Quire ps a
stackLeaves ((forall (p :: Symbol). KnownSymbol p => Member p qs -> a)
 -> Quire qs a)
-> (forall (p :: Symbol). KnownSymbol p => Member p qs -> a)
-> Quire qs a
forall a b. (a -> b) -> a -> b
$ \Member p qs
q -> Subset rs rs -> Located rs a -> a
Unwraps rs
un Subset rs rs
forall {k} (xs :: [k]). Subset xs xs
refl (Const (Located rs a) p -> Located rs a
forall {k} a (b :: k). Const a b -> a
getConst (Const (Located rs a) p -> Located rs a)
-> Const (Located rs a) p -> Located rs a
forall a b. (a -> b) -> a -> b
$ Member p qs -> Const (Located rs a) p
PIndex qs (Const (Located rs a))
x Member p qs
q)

-- | The owner of a t`Quire` sends its elements to their respective parties, resulting in a `Faceted`.
--   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)
scatter :: forall (census :: [Symbol]) (sender :: Symbol)
       (recipients :: [Symbol]) 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)
scatter Member sender census
sender Subset recipients census
recipients Located '[sender] (Quire recipients a)
values = (forall (q :: Symbol).
 KnownSymbol q =>
 Member q recipients -> Choreo census m (Located '[q, sender] a))
-> Choreo census m (Faceted recipients '[sender] a)
forall (qs :: [Symbol]) (ps :: [Symbol]) (m :: * -> *)
       (rs :: [Symbol]) 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)
fanOut \Member q recipients
r ->
  (Member sender census
sender, \Unwrap sender
un -> Member sender '[sender]
-> Located '[sender] (Quire recipients a) -> Quire recipients a
Unwrap sender
un Member sender '[sender]
forall {k} (xs1 :: [k]) (x :: k) (xs' :: [k]).
(xs1 ~ (x : xs')) =>
Member x (x : xs')
First Located '[sender] (Quire recipients a)
values Quire recipients a -> Member q recipients -> a
forall (p :: Symbol) (parties :: [Symbol]) a.
KnownSymbol p =>
Quire parties a -> Member p parties -> a
`getLeaf` Member q recipients
r) (Member sender census, Unwrap sender -> a)
-> Subset '[q, sender] census
-> Choreo census m (Located '[q, sender] a)
forall a (l :: Symbol) (ls' :: [Symbol]) (m :: * -> *)
       (ps :: [Symbol]).
(Show a, Read a, KnownSymbol l, KnownSymbols ls') =>
(Member l ps, Unwrap l -> a)
-> Subset ls' ps -> Choreo ps m (Located ls' a)
*~> Subset recipients census
-> forall (x :: Symbol). Member x recipients -> Member x census
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper Subset recipients census
recipients Member q recipients
r Member q census
-> Subset '[sender] census -> Subset '[q, sender] census
forall {k} (x :: k) (ys :: [k]) (xs :: [k]).
Member x ys -> Subset xs ys -> Subset (x : xs) ys
@@ Member sender census
sender Member sender census
-> Subset '[] census -> Subset '[sender] census
forall {k} (x :: k) (ys :: [k]) (xs :: [k]).
Member x ys -> Subset xs ys -> Subset (x : xs) ys
@@ Subset '[] census
forall {k} (ys :: [k]). Subset '[] ys
nobody

-- | The many owners of a `Faceted` each send their respective values to a constant list of recipients, resulting in a t`Quire`.
--   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)) -- could be Faceted senders recipients instead...
gather :: forall (census :: [Symbol]) (recipients :: [Symbol])
       (senders :: [Symbol]) a (dontcare :: [Symbol]) (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))
gather Subset senders census
senders Subset recipients census
recipients (PIndexed PIndex senders (Facet a dontcare)
values) = Subset recipients census
-> (forall (q :: Symbol).
    KnownSymbol q =>
    Member q senders -> Choreo census m (Located recipients a))
-> Choreo census m (Located recipients (Quire senders a))
forall (qs :: [Symbol]) (rs :: [Symbol]) (ps :: [Symbol])
       (m :: * -> *) 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))
fanIn Subset recipients census
recipients \Member q senders
s ->
  (Subset senders census
-> forall (x :: Symbol). Member x senders -> Member x census
forall {k} (xs :: [k]) (ys :: [k]).
Subset xs ys -> forall (x :: k). Member x xs -> Member x ys
inSuper Subset senders census
senders Member q senders
s, Facet a dontcare q -> Located (q : dontcare) a
forall a (common :: [Symbol]) (p :: Symbol).
Facet a common p -> Located (p : common) a
getFacet (Facet a dontcare q -> Located (q : dontcare) a)
-> Facet a dontcare q -> Located (q : dontcare) a
forall a b. (a -> b) -> a -> b
$ Member q senders -> Facet a dontcare q
PIndex senders (Facet a dontcare)
values Member q senders
s) (Member q census, Located (q : dontcare) a)
-> Subset recipients census
-> Choreo census m (Located recipients a)
forall a (l :: Symbol) (ls' :: [Symbol]) s (ls :: [Symbol])
       (ps :: [Symbol]) (m :: * -> *).
(Show a, Read a, KnownSymbol l, KnownSymbols ls',
 CanSend s l a ls ps) =>
s -> Subset ls' ps -> Choreo ps m (Located ls' a)
~> Subset recipients census
recipients