-- | This module defines the `Network` monad, which represents programs run on
-- individual nodes in a distributed system with explicit sends and receives.
-- To run a `Network` program, we provide a `runNetwork` function that supports
-- multiple message transport backends.
module Choreography.Network where

import Choreography.Location
import Control.Monad.Freer
import Control.Monad.IO.Class

-- * The Network monad

-- | Effect signature for the `Network` monad.
data NetworkSig m a where
  -- | Local computation.
  Run :: m a
      -> NetworkSig m a
  -- | Sending.
  Send :: Show a
       => a
       -> LocTm
       -> NetworkSig m ()
  -- | Receiving.
  Recv :: Read a
       => LocTm
       -> NetworkSig m a
  -- | Broadcasting.
  BCast :: Show a
        => a
        -> [LocTm]
        -> NetworkSig m ()

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

-- * Network operations

-- | Perform a local computation.
run :: m a -> Network m a
run :: forall (m :: * -> *) a. m a -> Network m a
run m a
m = NetworkSig m a -> Freer (NetworkSig m) a
forall (f :: * -> *) a. f a -> Freer f a
toFreer (NetworkSig m a -> Freer (NetworkSig m) a)
-> NetworkSig m a -> Freer (NetworkSig m) a
forall a b. (a -> b) -> a -> b
$ m a -> NetworkSig m a
forall (m :: * -> *) a. m a -> NetworkSig m a
Run m a
m

-- | Send a message to a receiver.
send :: Show a => a -> LocTm -> Network m ()
send :: forall a (m :: * -> *). Show a => a -> LocTm -> Network m ()
send a
a LocTm
l = NetworkSig m () -> Freer (NetworkSig m) ()
forall (f :: * -> *) a. f a -> Freer f a
toFreer (NetworkSig m () -> Freer (NetworkSig m) ())
-> NetworkSig m () -> Freer (NetworkSig m) ()
forall a b. (a -> b) -> a -> b
$ a -> LocTm -> NetworkSig m ()
forall a (m :: * -> *). Show a => a -> LocTm -> NetworkSig m ()
Send a
a LocTm
l

-- | Receive a message from a sender.
recv :: Read a => LocTm -> Network m a
recv :: forall a (m :: * -> *). Read a => LocTm -> Network m a
recv LocTm
l = NetworkSig m a -> Freer (NetworkSig m) a
forall (f :: * -> *) a. f a -> Freer f a
toFreer (NetworkSig m a -> Freer (NetworkSig m) a)
-> NetworkSig m a -> Freer (NetworkSig m) a
forall a b. (a -> b) -> a -> b
$ LocTm -> NetworkSig m a
forall a (m :: * -> *). Read a => LocTm -> NetworkSig m a
Recv LocTm
l

-- | Broadcast a message to all participants.
broadcast :: Show a => a -> [LocTm] -> Network m ()
broadcast :: forall a (m :: * -> *). Show a => a -> [LocTm] -> Network m ()
broadcast a
a [LocTm]
ls = NetworkSig m () -> Freer (NetworkSig m) ()
forall (f :: * -> *) a. f a -> Freer f a
toFreer (NetworkSig m () -> Freer (NetworkSig m) ())
-> NetworkSig m () -> Freer (NetworkSig m) ()
forall a b. (a -> b) -> a -> b
$ a -> [LocTm] -> NetworkSig m ()
forall a (m :: * -> *). Show a => a -> [LocTm] -> NetworkSig m ()
BCast a
a [LocTm]
ls

-- * Message transport backends

-- | A message transport backend defines a /configuration/ of type @c@ that
-- carries necessary bookkeeping information, then defines @c@ as an instance
-- of `Backend` and provides a `runNetwork` function.
class Backend c where
  locs :: c -> [LocTm]
  runNetwork :: MonadIO m => c -> LocTm -> Network m a -> m a