Safe Haskell	None
Language	GHC2021

Choreography.Network

Contents

The Network monad
Network operations
Message transport backends

Description

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.

Synopsis

data NetworkSig (m :: Type -> Type) a where
- Run :: forall (m :: Type -> Type) a. m a -> NetworkSig m a
- Send :: forall a1 (m :: Type -> Type). Show a1 => a1 -> LocTm -> NetworkSig m ()
- Recv :: forall a (m :: Type -> Type). Read a => LocTm -> NetworkSig m a
- BCast :: forall a1 (m :: Type -> Type). Show a1 => a1 -> [LocTm] -> NetworkSig m ()
type Network (m :: Type -> Type) = Freer (NetworkSig m)
run :: m a -> Network m a
send :: forall a (m :: Type -> Type). Show a => a -> LocTm -> Network m ()
recv :: forall a (m :: Type -> Type). Read a => LocTm -> Network m a
broadcast :: forall a (m :: Type -> Type). Show a => a -> [LocTm] -> Network m ()
class Backend c where
- locs :: c -> [LocTm]
- runNetwork :: MonadIO m => c -> LocTm -> Network m a -> m a

The Network monad

data NetworkSig (m :: Type -> Type) a where Source #

Effect signature for the Network monad.

Constructors

Run :: forall (m :: Type -> Type) a. m a -> NetworkSig m a	Local computation.
Send :: forall a1 (m :: Type -> Type). Show a1 => a1 -> LocTm -> NetworkSig m ()	Sending.
Recv :: forall a (m :: Type -> Type). Read a => LocTm -> NetworkSig m a	Receiving.
BCast :: forall a1 (m :: Type -> Type). Show a1 => a1 -> [LocTm] -> NetworkSig m ()	Broadcasting.

type Network (m :: Type -> Type) = Freer (NetworkSig m) Source #

Monad that represents network programs.

Network operations

run :: m a -> Network m a Source #

Perform a local computation.

send :: forall a (m :: Type -> Type). Show a => a -> LocTm -> Network m () Source #

Send a message to a receiver.

recv :: forall a (m :: Type -> Type). Read a => LocTm -> Network m a Source #

Receive a message from a sender.

broadcast :: forall a (m :: Type -> Type). Show a => a -> [LocTm] -> Network m () Source #

Broadcast a message to all participants.

Message transport backends

class Backend c where Source #

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.

Methods

locs :: c -> [LocTm] Source #

runNetwork :: MonadIO m => c -> LocTm -> Network m a -> m a Source #

Instances

Instances details

Backend HttpConfig Source #
Instance details Defined in Choreography.Network.Http Methods locs :: HttpConfig -> [LocTm] Source # runNetwork :: MonadIO m => HttpConfig -> LocTm -> Network m a -> m a Source #
Backend LocalConfig Source #
Instance details Defined in Choreography.Network.Local Methods locs :: LocalConfig -> [LocTm] Source # runNetwork :: MonadIO m => LocalConfig -> LocTm -> Network m a -> m a Source #
Backend LocalMsgCountConfig Source #
Instance details Defined in Choreography.Network.LocalMsgCount Methods locs :: LocalMsgCountConfig -> [LocTm] Source # runNetwork :: MonadIO m => LocalMsgCountConfig -> LocTm -> Network m a -> m a Source #