protocol (empty) → 0.1.0.0

raw patch · 8 files changed

+333/−0 lines, 8 filesdep +basedep +freer-indexeddep +singletonssetup-changed

Dependencies added: base, freer-indexed, singletons

Files

CHANGELOG.md +4/−0
LICENSE +30/−0
README.md +5/−0
Setup.hs +2/−0
protocol.cabal +46/−0
src/Control/Protocol.hs +120/−0
src/Control/Protocol/Example.hs +83/−0
src/Control/Protocol/Internal.hs +43/−0

+ CHANGELOG.md view

@@ -0,0 +1,4 @@+## 0.1.0.0++- Initial release+- `Protocol` data type to define protocol and `runProtocol` to interpret it.

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright Evgeny Poberezkin (c) 2020++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Author name here nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

+ README.md view

@@ -0,0 +1,5 @@+# protocol++Model distributed system as type-level multi-party protocol.++See [docs on hackage](http://hackage.haskell.org/package/protocol/docs/Control-Protocol.html).

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ protocol.cabal view

@@ -0,0 +1,46 @@+cabal-version: 1.12++-- This file has been generated from package.yaml by hpack version 0.33.0.+--+-- see: https://github.com/sol/hpack+--+-- hash: 891acf4772c5e0911b5e56fb7dd8b4a457d91866ed95b4a3142d852a9c0b9b2a++name:           protocol+version:        0.1.0.0+synopsis:       Model distributed system as type-level multi-party protocol+description:    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.+category:       Control, Distributed Computing, Distributed Systems, Protocol+homepage:       https://github.com/epoberezkin/protocol#readme+bug-reports:    https://github.com/epoberezkin/protocol/issues+author:         Evgeny Poberezkin+maintainer:     evgeny@poberezkin.com+copyright:      2020 Evgeny Poberezkin+license:        BSD3+license-file:   LICENSE+build-type:     Simple+extra-source-files:+    README.md+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/epoberezkin/protocol++library+  exposed-modules:+      Control.Protocol+      Control.Protocol.Example+      Control.Protocol.Internal+  other-modules:+      Paths_protocol+  hs-source-dirs:+      src+  ghc-options: -Wall -Wcompat -Werror=incomplete-patterns -Wunused-type-patterns -Wredundant-constraints -Wincomplete-record-updates -Wincomplete-uni-patterns -Wno-name-shadowing+  build-depends:+      base >=4.7 && <5+    , freer-indexed ==0.1.*+    , singletons ==2.6.*+  default-language: Haskell2010

+ src/Control/Protocol.hs view

@@ -0,0 +1,120 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}++-- |+-- Module : Control.Protocol+-- Copyright : (c) Evgeny Poberezkin+-- License : BSD3+--+-- Maintainer  : evgeny@poberezkin.com+-- Stability   : experimental+-- Portability : non-portable+--+-- This module provides type 'Protocol' 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 'Command') 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 '(->:)' wraps commands into free parameterized monad (see <https://hackage.haskell.org/package/freer-indexed freer-indexed>)+-- so that they can be chained into type-aligned scenarios, optionally written using do notation.+-- These scenarios can be interpreted in any monad using 'runProtocol' function,+-- e.g. to print protocol description or diagram or to execute system-level integration tests.+--+-- See protocol definition and scenario examples in @<./Control-Protocol-Example.html Control.Protocol.Example>@.+module Control.Protocol+  ( Command,+    Protocol,+    ProtocolCmd,+    (->:),+    runProtocol,+  )+where++import Control.Protocol.Internal+import Control.XFreer+import Data.Kind+import Data.Singletons++-- | Defines the kind of the command data type used by 'Protocol':+--+--     * @party@ - the type (normally enumerable) that defines parties of the protocol (here it is used as a kind). This type should be singletonized.+--     * @state@ - the kind of the protocol resource state.+--+-- 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 @<./Control-Protocol-Example.html Control.Protocol.Example>@ for command example.+type Command party state = (party, state, state) -> (party, state, state) -> Type -> Type++-- | 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:+--+-- > ProtocolCmd ::+-- >   Sing (from :: p) ->+-- >   Sing (to :: p) ->+-- >   cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a ->+-- >   ProtocolCmd cmd ps s (Inj ps (Inj ps s from fs') to ts') a+--+-- Here:+--+--     * @from@ - type of party that sends the command.+--     * @to@ - type of party that executes command (e.g., provides some API).+--+-- 'Protocol' type synonym should be used to construct this type, and function '(->:)' should be used instead of the constructor.+data ProtocolCmd (cmd :: Command p k) (parties :: [p]) (s :: [k]) (s' :: [k]) (a :: Type) where+  ProtocolCmd ::+    Sing (from :: p) ->+    Sing (to :: p) ->+    cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a ->+    ProtocolCmd cmd ps s (Inj ps (Inj ps s from fs') to ts') a++-- | Type synonym to create protocol data type ('ProtocolCmd' wrapped in 'XFree' - parameterized free monad):+--+--     * @cmd@ - user-defined command type constructor that should have the kind 'Command'.+--     * @parties@ - type-level list of participants - it defines the order of participant states in the combined state of the system described by the protocol.+type Protocol cmd parties = XFree (ProtocolCmd cmd parties)++infix 6 ->:++-- | Function that wraps command into 'ProtocolCmd' type converted into free parameterized monad.+(->:) ::+  -- | party that sends command+  Sing from ->+  -- | party that executes command+  Sing to ->+  -- | command - its initial states for both parties are projected from system state+  cmd '(from, Prj ps s from, fs') '(to, Prj ps s to, ts') a ->+  -- | final protocol state injects final states of both participants+  Protocol cmd ps s (Inj ps (Inj ps s from fs') to ts') a+(->:) f t c = xfree $ ProtocolCmd f t c++-- | 'runProtocol' interprets protocol scenario in any monad,+-- using passed 'runCmd' function that interprets individual commands.+runProtocol ::+  forall m cmd ps s s' a.+  Monad m =>+  -- | function to interpret a command+  (forall from to b. (Sing (P from) -> Sing (P to) -> cmd from to b -> m b)) ->+  -- | protocol scenario (see example in @'Control.Protocol.Example.Scenario'@)+  Protocol cmd ps s s' a ->+  m a+runProtocol runCmd = loop+  where+    loop :: forall s1 s2 b. Protocol cmd ps s1 s2 b -> m b+    loop (Pure x) = return x+    loop (Bind c f) = run c >>= loop . f+    run :: forall s1 s2 b. ProtocolCmd cmd ps s1 s2 b -> m b+    run (ProtocolCmd from to cmd) = runCmd from to cmd

+ src/Control/Protocol/Example.hs view

@@ -0,0 +1,83 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}+{-# OPTIONS_GHC -fno-warn-unused-top-binds #-}++-- |+-- Module : Control.Protocol.Example+-- Copyright : (c) Evgeny Poberezkin+-- License : BSD3+--+-- Maintainer  : evgeny@poberezkin.com+-- Stability   : experimental+-- Portability : non-portable+--+-- Example command and protocol definition.+module Control.Protocol.Example+  ( MyProtocol,+    MyCommand (..),+    scenario,+    Party (..),+    ChannelState (..),+  )+where++import Control.Protocol+import Control.XMonad.Do+import Data.Singletons.TH+import Prelude hiding ((>>), (>>=))++$( singletons+     [d|+       data Party = Recipient | Broker | Sender+         deriving (Show, Eq)+       |]+ )++-- | Example type defining the possible resource states, in this case some communication channel.+data ChannelState+  = None+  | Ready+  | Busy+  deriving (Show, Eq)++-- | Example command data type of kind @'Command' 'Party' 'ChannelState'@.+data MyCommand :: Command Party ChannelState where+  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 type.+type MyProtocol = Protocol MyCommand '[Recipient, Broker, Sender]++r :: Sing Recipient+r = SRecipient++b :: Sing Broker+b = SBroker++s :: Sing Sender+s = SSender++-- | Example protocol scenario.+--+-- If you modify this scenario to 'Send' before channel is 'Create'd or+-- to 'Send' two messages in a row without forwarding them, the scenario will not compile.+scenario :: String -> MyProtocol '[None, None, None] '[Ready, Ready, Ready] String+scenario str = do+  r ->: b $ Create+  r ->: s $ Notify+  s ->: b $ Send str+  -- s ->: b $ Send str+  b ->: r $ Forward

+ src/Control/Protocol/Internal.hs view

@@ -0,0 +1,43 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}++-- |+-- Module : Control.Protocol.Internal+-- Copyright : (c) Evgeny Poberezkin+-- License : BSD3+--+-- Maintainer  : evgeny@poberezkin.com+-- Stability   : experimental+-- Portability : non-portable+--+-- This module provides type families to combine/extract the individual states of parties+-- as defined by command constructors into/from the combined system/protocol state defined as type-level list.+module Control.Protocol.Internal where++import GHC.TypeLits (ErrorMessage (..), TypeError)++-- | Extracts party from command type parameter.+type family P (partyCmd :: (party, s, s)) where+  P '(p, _, _) = p++-- | Projects the state of one party from the list of states.+type family Prj (parties :: [pk]) (state :: [k]) (party :: pk) :: k where+  Prj (p ': _) (s ': _) p = s+  Prj (_ ': ps) (_ ': ss) p = Prj ps ss p+  Prj '[] _ p = TypeError (NoParty p)+  Prj _ '[] p = TypeError (NoParty p :$$: StateError)++-- | 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] where+  Inj (p ': _) (_ ': ss) p s' = s' ': ss+  Inj (_ ': ps) (s ': ss) p s' = s ': Inj ps ss p s'+  Inj '[] _ p _ = TypeError (NoParty p)+  Inj _ '[] p _ = TypeError (NoParty p :$$: StateError)++type NoParty p = Text "Party " :<>: ShowType p :<>: Text " is not found."++type StateError = Text "Specified fewer protocol states than parties."