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


-- | Model distributed system as type-level multi-party protocol
--   
--   This package provides type to model distributed multi-party protocols,
--   ensuring the continuity of the associated resource state transitions
--   on the type level for all protocol commands and scenarios.
@package protocol
@version 0.1.0.1


-- | This module provides type families to combine/extract the individual
--   states of parties as defined by command constructors into<i>from the
--   combined system</i>protocol state defined as type-level list.
module Control.Protocol.Internal

-- | Extracts party from command type parameter.
type family P (partyCmd :: (party, s, s))

-- | Projects the state of one party from the list of states.
type family Prj (parties :: [pk]) (state :: [k]) (party :: pk) :: k

-- | Injects the state of some party into the party's position in the list
--   of states.
type family Inj (parties :: [pk]) (state :: [k]) (p :: pk) (s' :: k) :: [k]
type NoParty p = Text "Party " :<>: ShowType p :<>: Text " is not found."
type StateError = Text "Specified fewer protocol states than parties."


-- | This module provides type <a>Protocol</a> to model distributed
--   multi-party protocols, ensuring the continuity of the associated
--   resource state transitions on the type level for all protocol commands
--   and scenarios.
--   
--   It accepts used-defined data type for protocol commands (GADT of kind
--   <a>Command</a>) and the list of protocol participants to create
--   protocol type.
--   
--   Command type serves as a single abstract api between all participants
--   - it is defined to allow decoupling type-level requirements for
--   participants implementations.
--   
--   Function '(-&gt;:)' wraps commands into free parameterized monad (see
--   <a>freer-indexed</a>) so that they can be chained into type-aligned
--   scenarios, optionally written using do notation. These scenarios can
--   be interpreted in any monad using <a>runProtocol</a> function, e.g. to
--   print protocol description or diagram or to execute system-level
--   integration tests.
--   
--   See protocol definition and scenario examples in
--   <tt><a>Control.Protocol.Example</a></tt>.
module Control.Protocol

-- | Defines the kind of the command data type used by <a>Protocol</a>:
--   
--   <ul>
--   <li><tt>party</tt> - the type (normally enumerable) that defines
--   parties of the protocol (here it is used as a kind). This type should
--   be singletonized.</li>
--   <li><tt>state</tt> - the kind of the protocol resource state.</li>
--   </ul>
--   
--   The first type-level tuple in command constructors defines the party
--   that sends the command, with the initial and final resource states for
--   that party.
--   
--   The second tuple defines the party that executes command (e.g.,
--   provides some api) with its initial final and states.
--   
--   See <tt><a>Control.Protocol.Example</a></tt> for command example.
type Command party state = (party, state, state) -> (party, state, state) -> Type -> Type

-- | Type synonym to create protocol data type (<a>ProtocolCmd</a> wrapped
--   in <a>XFree</a> - parameterized free monad):
--   
--   <ul>
--   <li><tt>cmd</tt> - user-defined command type constructor that should
--   have the kind <a>Command</a>.</li>
--   <li><tt>parties</tt> - type-level list of participants - it defines
--   the order of participant states in the combined state of the system
--   described by the protocol.</li>
--   </ul>
type Protocol cmd parties = XFree (ProtocolCmd cmd parties)

-- | Protocol data type that wraps a command and explicitly adds command
--   participants.
--   
--   Its only constructor that is not exported adds command participants
--   and combines participant states in type-level list so that they can be
--   chained in type-aligned sequence of commands:
--   
--   <pre>
--   ProtocolCmd ::
--     Sing (from :: p) -&gt;
--     Sing (to :: p) -&gt;
--     cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a -&gt;
--     ProtocolCmd cmd ps s (Inj ps (Inj ps s from fs') to ts') a
--   </pre>
--   
--   Here:
--   
--   <ul>
--   <li><tt>from</tt> - type of party that sends the command.</li>
--   <li><tt>to</tt> - type of party that executes command (e.g., provides
--   some API).</li>
--   </ul>
--   
--   <a>Protocol</a> type synonym should be used to construct this type,
--   and function '(-&gt;:)' should be used instead of the constructor.
data ProtocolCmd (cmd :: Command p k) (parties :: [p]) (s :: [k]) (s' :: [k]) (a :: Type)

-- | Function that wraps command into <a>ProtocolCmd</a> type converted
--   into free parameterized monad.
(->:) :: Sing from -> Sing to -> cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a -> Protocol cmd ps s (Inj ps (Inj ps s from fs') to ts') a
infix 6 ->:

-- | <a>runProtocol</a> interprets protocol scenario in any monad, using
--   passed <tt>runCmd</tt> function that interprets individual commands.
runProtocol :: forall m cmd ps s s' a. Monad m => (forall from to b. Sing (P from) -> Sing (P to) -> cmd from to b -> m b) -> Protocol cmd ps s s' a -> m a


-- | Example command and protocol definition.
module Control.Protocol.Example

-- | Example protocol type.
type MyProtocol = Protocol MyCommand '[Recipient, Broker, Sender]

-- | Example command data type of kind <tt><a>Command</a> <a>Party</a>
--   <a>ChannelState</a></tt>.
data MyCommand :: Command Party ChannelState
[Create] :: MyCommand '(Recipient, None, Ready) '(Broker, None, Ready) ()
[Notify] :: MyCommand '(Recipient, Ready, Ready) '(Sender, None, Ready) ()
[Send] :: String -> MyCommand '(Sender, Ready, Ready) '(Broker, Ready, Busy) ()
[Forward] :: MyCommand '(Broker, Busy, Ready) '(Recipient, Ready, Ready) String

-- | Example protocol scenario.
--   
--   If you modify this scenario to <a>Send</a> before channel is
--   <a>Create</a>d or to <a>Send</a> two messages in a row without
--   forwarding them, the scenario will not compile.
scenario :: String -> MyProtocol '[None, None, None] '[Ready, Ready, Ready] String
data Party
Recipient :: Party
Broker :: Party
Sender :: Party

-- | Example type defining the possible resource states, in this case some
--   communication channel.
data ChannelState
None :: ChannelState
Ready :: ChannelState
Busy :: ChannelState
instance GHC.Classes.Eq Control.Protocol.Example.ChannelState
instance GHC.Show.Show Control.Protocol.Example.ChannelState
instance GHC.Classes.Eq Control.Protocol.Example.Party
instance GHC.Show.Show Control.Protocol.Example.Party
instance GHC.Show.Show (Data.Singletons.Internal.Sing z)
instance Data.Singletons.Prelude.Eq.PEq Control.Protocol.Example.Party
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings Control.Protocol.Example.ShowsPrec_6989586621679083583Sym0
instance Data.Singletons.Prelude.Show.PShow Control.Protocol.Example.Party
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Protocol.Example.ShowsPrec_6989586621679083583Sym1 a6989586621679083580)
instance Data.Singletons.SuppressUnusedWarnings.SuppressUnusedWarnings (Control.Protocol.Example.ShowsPrec_6989586621679083583Sym2 a6989586621679083581 a6989586621679083580)
instance Data.Singletons.Internal.SingKind Control.Protocol.Example.Party
instance Data.Singletons.Prelude.Show.SShow Control.Protocol.Example.Party
instance Data.Singletons.Prelude.Eq.SEq Control.Protocol.Example.Party
instance Data.Singletons.Decide.SDecide Control.Protocol.Example.Party
instance Data.Singletons.Internal.SingI 'Control.Protocol.Example.Recipient
instance Data.Singletons.Internal.SingI 'Control.Protocol.Example.Broker
instance Data.Singletons.Internal.SingI 'Control.Protocol.Example.Sender