all parties have resource state of the same kind

definitions/src/Control/Protocol.hs

@@ -2,46 +2,60 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
 
 module Control.Protocol
   ( Protocol,
     ProtocolCmd (..),
     Command,
-    PartyCmd (..),
-    type (|:),
     (->:),
     comment,
   )
 where
 
-import Control.Protocol.Internal
 import Control.XFreer
 import Data.Kind
 import Data.Singletons
+import GHC.TypeLits (ErrorMessage (..), TypeError)
 
-data PartyCmd p = forall s. Cmd p s s
+type Command p k = (p, k, k) -> (p, k, k) -> Type -> Type
 
-type Command p = PartyCmd p -> PartyCmd p -> Type -> Type
-
-data ProtocolCmd (cmd :: Command p) (parties :: [p]) (s :: DList) (s' :: DList) (a :: Type) where
+data ProtocolCmd (cmd :: Command p k) (parties :: [p]) (s :: [k]) (s' :: [k]) (a :: Type) where
   Comment :: String -> ProtocolCmd cmd ps s s ()
   ProtocolCmd ::
     Sing (from :: p) ->
     Sing (to :: p) ->
-    cmd (Cmd from (PartySt ps s from) fs') (Cmd to (PartySt ps s to) ts') a ->
-    ProtocolCmd cmd ps s (ProtoSt ps s from fs' to ts') a
+    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 Protocol parties cmd = XFree (ProtocolCmd parties cmd)
+type Protocol cmd parties = XFree (ProtocolCmd cmd parties)
 
 infix 6 ->:
 
 (->:) ::
   Sing from ->
   Sing to ->
-  cmd (Cmd from (PartySt ps s from) fs') (Cmd to (PartySt ps s to) ts') a ->
-  Protocol cmd ps s (ProtoSt ps s from fs' to ts') a
+  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
 (->:) f t c = xfree $ ProtocolCmd f t c
 
 comment :: String -> Protocol ps cmd s s ()
 comment = xfree . Comment
+
+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)
+
+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 "\nSpecified fewer protocol states than parties."

definitions/src/Control/Protocol/Example/Command.hs

@@ -21,28 +21,18 @@ $( singletons
        data Party = Recipient | Broker | Sender
          deriving (Show, Eq)
 
-       data RState
-         = RNone
-         | RReady
-         deriving (Show, Eq)
-
-       data BState
-         = BNone
-         | BEmpty
-         | BFull
-         deriving (Show, Eq)
-
-       data SState
-         = SNone
-         | SReady
+       data ChannelState
+         = None
+         | Ready
+         | Busy
          deriving (Show, Eq)
        |]
  )
 
-data MyCommand :: Command Party where
-  Create :: MyCommand (Cmd Recipient RNone RReady) (Cmd Broker BNone BEmpty) ()
-  Notify :: MyCommand (Cmd Recipient RReady RReady) (Cmd Sender SNone SReady) ()
-  Send :: String -> MyCommand (Cmd Sender SReady SReady) (Cmd Broker BEmpty BFull) ()
-  Forward :: MyCommand (Cmd Broker BFull BEmpty) (Cmd Recipient RReady RReady) String
+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
 
 type MyProtocol = Protocol MyCommand '[Recipient, Broker, Sender]

definitions/src/Control/Protocol/Example/Scenario.hs

@@ -1,6 +1,5 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE RebindableSyntax #-}
-{-# LANGUAGE TypeOperators #-}
 {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
 
 module Control.Protocol.Example.Scenario where
@@ -20,7 +19,7 @@ b = SBroker
 s :: Sing Sender
 s = SSender
 
-scenario :: String -> MyProtocol (RNone |: BNone |: SNone) (RReady |: BEmpty |: SReady) String
+scenario :: String -> MyProtocol '[None, None, None] '[Ready, Ready, Ready] String
 scenario str = do
   r ->: b $ Create
   r ->: s $ Notify

definitions/src/Control/Protocol/Internal.hs

@@ -1,58 +0,0 @@
-{-# LANGUAGE DataKinds #-}
-{-# LANGUAGE GADTs #-}
-{-# LANGUAGE PolyKinds #-}
-{-# LANGUAGE TypeFamilies #-}
-{-# LANGUAGE TypeOperators #-}
-{-# LANGUAGE UndecidableInstances #-}
-{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
-
-module Control.Protocol.Internal
-  ( DList (..),
-    type (|:),
-    PartySt,
-    ProtoSt,
-  )
-where
-
-import GHC.TypeLits (ErrorMessage (..), TypeError)
-
-infixr 3 :|, |:
-
-data DList = DNil | forall a. a :| DList
-
-type family (|:) (s :: k1) (t :: k2) :: DList where
-  s |: DNil = s :| DNil
-  s |: (t :| ss) = s :| t :| ss
-  s |: t = s :| t :| DNil
-
-type family PartySt (parties :: [k]) (state :: DList) (party :: k) where
-  PartySt (p ': _) (s ':| _) p = s
-  PartySt (_ ': ps) (_ ':| ss) p = PartySt ps ss p
-  PartySt '[] DNil p = TypeError (NoParty p)
-  PartySt '[] _ p = TypeError (NoParty p :<>: PartyError)
-  PartySt _ DNil p = TypeError (NoParty p :<>: StateError)
-
-type family ProtoSt (parties :: [k]) (state :: DList) (from :: k) fs' (to :: k) ts' where
-  ProtoSt '[] DNil from _ to _ = TypeError (NoParties from to)
-  ProtoSt '[] _ from _ to _ = TypeError (NoParties from to :<>: PartyError)
-  ProtoSt _ DNil from _ to _ = TypeError (NoParties from to :<>: StateError)
-  ProtoSt (from ': ps) (_ ':| ss) from fs' to ts' = fs' ':| ProtoSt1 ps ss to ts'
-  ProtoSt (to ': ps) (_ ':| ss) from fs' to ts' = ts' ':| ProtoSt1 ps ss from fs'
-  ProtoSt (_ ': ps) (s ':| ss) from fs' to ts' = s ':| ProtoSt ps ss from fs' to ts'
-
-type family ProtoSt1 (parties :: [k]) (state :: DList) (p :: k) s' where
-  ProtoSt1 '[] DNil p _ = TypeError (NoParty p)
-  ProtoSt1 '[] _ p _ = TypeError (NoParty p :<>: PartyError)
-  ProtoSt1 _ DNil p _ = TypeError (NoParty p :<>: StateError)
-  ProtoSt1 (p ': _) (_ ':| ss) p s' = s' ':| ss
-  ProtoSt1 (_ ': ps) (s ':| ss) p s' = s ':| ProtoSt1 ps ss p s'
-
-type NoParties p1 p2 =
-  Text "Parties " :<>: ShowType p1 :<>: Text " and " :<>: ShowType p2
-    :<>: Text " are not found."
-
-type NoParty p = Text "Party " :<>: ShowType p :<>: Text " is not found."
-
-type PartyError = Text "\nSpecified fewer protocol parties than states."
-
-type StateError = Text "\nSpecified fewer protocol states than parties."

definitions/src/Simplex/Messaging/Broker.hs

@@ -11,13 +11,12 @@
 module Simplex.Messaging.Broker where
 
 import Control.Monad.Trans.Except
-import Control.Protocol (PartyCmd (..))
 import Polysemy.Internal
 import Simplex.Messaging.Protocol
 
 instance Monad m => PartyProtocol m Broker where
   api ::
-    SimplexCommand from (Cmd Broker s s') a ->
+    SimplexCommand from '(Broker, s, s') a ->
     Connection Broker s ->
     ExceptT String m (a, Connection Broker s')
   api (CreateConn _) = apiStub
@@ -29,7 +28,7 @@ instance Monad m => PartyProtocol m Broker where
   api (DeleteMsg _ _) = apiStub
 
   action ::
-    SimplexCommand (Cmd Broker s s') to a ->
+    SimplexCommand '(Broker, s, s') to a ->
     Connection Broker s ->
     ExceptT String m a ->
     ExceptT String m (Connection Broker s')
@@ -40,14 +39,14 @@ type SimplexBroker = SimplexParty Broker
 
 api' ::
   Member SimplexBroker r =>
-  SimplexCommand from (Cmd Broker s s') a ->
+  SimplexCommand from '(Broker, s, s') a ->
   Connection Broker s ->
   Sem r (Either String (a, Connection Broker s'))
 api' cmd conn = send $ Api cmd conn
 
 action' ::
   Member SimplexBroker r =>
-  SimplexCommand (Cmd Broker s s') to a ->
+  SimplexCommand '(Broker, s, s') to a ->
   Connection Broker s ->
   Either String a ->
   Sem r (Either String (Connection Broker s'))

definitions/src/Simplex/Messaging/Client.hs

@@ -11,20 +11,19 @@
 module Simplex.Messaging.Client where
 
 import Control.Monad.Trans.Except
-import Control.Protocol (PartyCmd (..))
 import Polysemy.Internal
 import Simplex.Messaging.Protocol
 
 instance Monad m => PartyProtocol m Recipient where
   api ::
-    SimplexCommand from (Cmd Recipient s s') a ->
+    SimplexCommand from '(Recipient, s, s') a ->
     Connection Recipient s ->
     ExceptT String m (a, Connection Recipient s')
   api (PushConfirm _ _) = apiStub
   api (PushMsg _ _) = apiStub
 
   action ::
-    SimplexCommand (Cmd Recipient s s') to a ->
+    SimplexCommand '(Recipient, s, s') to a ->
     Connection Recipient s ->
     ExceptT String m a ->
     ExceptT String m (Connection Recipient s')
@@ -37,13 +36,13 @@ instance Monad m => PartyProtocol m Recipient where
 
 instance Monad m => PartyProtocol m Sender where
   api ::
-    SimplexCommand from (Cmd Sender s s') a ->
+    SimplexCommand from '(Sender, s, s') a ->
     Connection Sender s ->
     ExceptT String m (a, Connection Sender s')
   api (SendInvite _) = apiStub
 
   action ::
-    SimplexCommand (Cmd Sender s s') to a ->
+    SimplexCommand '(Sender, s, s') to a ->
     Connection Sender s ->
     ExceptT String m a ->
     ExceptT String m (Connection Sender s')
@@ -56,14 +55,14 @@ type SimplexSender = SimplexParty Sender
 
 rApi ::
   Member SimplexRecipient r =>
-  SimplexCommand from (Cmd Recipient s s') a ->
+  SimplexCommand from '(Recipient, s, s') a ->
   Connection Recipient s ->
   Sem r (Either String (a, Connection Recipient s'))
 rApi cmd conn = send $ Api cmd conn
 
 rAction ::
   Member SimplexRecipient r =>
-  SimplexCommand (Cmd Recipient s s') to a ->
+  SimplexCommand '(Recipient, s, s') to a ->
   Connection Recipient s ->
   Either String a ->
   Sem r (Either String (Connection Recipient s'))
@@ -71,14 +70,14 @@ rAction cmd conn res = send $ Action cmd conn res
 
 sApi ::
   Member SimplexSender r =>
-  SimplexCommand from (Cmd Sender s s') a ->
+  SimplexCommand from '(Sender, s, s') a ->
   Connection Sender s ->
   Sem r (Either String (a, Connection Sender s'))
 sApi cmd conn = send $ Api cmd conn
 
 sAction ::
   Member SimplexSender r =>
-  SimplexCommand (Cmd Sender s s') to a ->
+  SimplexCommand '(Sender, s, s') to a ->
   Connection Sender s ->
   Either String a ->
   Sem r (Either String (Connection Sender s'))

definitions/src/Simplex/Messaging/Protocol.hs

@@ -25,75 +25,75 @@ import Simplex.Messaging.Types
 
 type SimplexProtocol = Protocol SimplexCommand '[Recipient, Broker, Sender]
 
-data SimplexCommand :: Command Party where
+data SimplexCommand :: Command Party ConnState where
   CreateConn ::
     PublicKey ->
     SimplexCommand
-      (Cmd Recipient None New)
-      (Cmd Broker None New)
+      '(Recipient, None, New)
+      '(Broker, None, New)
       CreateConnResponse
   Subscribe ::
     Enabled rs bs =>
     ConnId ->
     SimplexCommand
-      (Cmd Recipient rs rs)
-      (Cmd Broker bs bs)
+      '(Recipient, rs, rs)
+      '(Broker, bs, bs)
       ()
   Unsubscribe ::
     Enabled rs bs =>
     ConnId ->
     SimplexCommand
-      (Cmd Recipient rs rs)
-      (Cmd Broker bs bs)
+      '(Recipient, rs, rs)
+      '(Broker, bs, bs)
       ()
   SendInvite ::
     Invitation ->
     SimplexCommand
-      (Cmd Recipient New Pending)
-      (Cmd Sender None New)
+      '(Recipient, New, Pending)
+      '(Sender, None, New)
       ()
   ConfirmConn ::
     SenderConnId ->
     Encrypted ->
     SimplexCommand
-      (Cmd Sender New Confirmed)
-      (Cmd Broker New New)
+      '(Sender, New, Confirmed)
+      '(Broker, New, New)
       ()
   PushConfirm ::
     ConnId ->
     Message ->
     SimplexCommand
-      (Cmd Broker New New)
-      (Cmd Recipient Pending Confirmed)
+      '(Broker, New, New)
+      '(Recipient, Pending, Confirmed)
       ()
   SecureConn ::
     ConnId ->
     PublicKey ->
     SimplexCommand
-      (Cmd Recipient Confirmed Secured)
-      (Cmd Broker New Secured)
+      '(Recipient, Confirmed, Secured)
+      '(Broker, New, Secured)
       ()
   SendMsg ::
     (ss == Confirmed || ss == Secured) ~ True =>
     SenderConnId ->
     Encrypted ->
     SimplexCommand
-      (Cmd Sender ss Secured)
-      (Cmd Broker Secured Secured)
+      '(Sender, ss, Secured)
+      '(Broker, Secured, Secured)
       ()
   PushMsg ::
     ConnId ->
     Message ->
     SimplexCommand
-      (Cmd Broker Secured Secured)
-      (Cmd Recipient Secured Secured)
+      '(Broker, Secured, Secured)
+      '(Recipient, Secured, Secured)
       ()
   DeleteMsg ::
     ConnId ->
     MessageId ->
     SimplexCommand
-      (Cmd Recipient Secured Secured)
-      (Cmd Broker Secured Secured)
+      '(Recipient, Secured, Secured)
+      '(Broker, Secured, Secured)
       ()
 
 -- connection type stub for all participants, TODO move from idris
@@ -106,11 +106,11 @@ data
 
 class Monad m => PartyProtocol m (p :: Party) where
   api ::
-    SimplexCommand from (Cmd p s s') a ->
+    SimplexCommand from '(p, s, s') a ->
     Connection p s ->
     ExceptT String m (a, Connection p s')
   action ::
-    SimplexCommand (Cmd p s s') to a ->
+    SimplexCommand '(p, s, s') to a ->
     Connection p s ->
     ExceptT String m a ->
     ExceptT String m (Connection p s')
@@ -123,11 +123,11 @@ actionStub _ _ = throwE "action not implemented"
 
 data SimplexParty (p :: Party) m a where
   Api ::
-    SimplexCommand from (Cmd p s s') x ->
+    SimplexCommand from '(p, s, s') x ->
     Connection p s ->
     SimplexParty p m (Either String (x, Connection p s'))
   Action ::
-    SimplexCommand (Cmd p s s') to x ->
+    SimplexCommand '(p, s, s') to x ->
     Connection p s ->
     Either String x ->
     SimplexParty p m (Either String (Connection p s'))

definitions/src/Simplex/Messaging/Scenarios.hs

@@ -26,7 +26,7 @@ b = SBroker
 s :: Sing Sender
 s = SSender
 
-establishConnection :: SimplexProtocol (None |: None |: None) (Secured |: Secured |: Secured) ()
+establishConnection :: SimplexProtocol '[None, None, None] '[Secured, Secured, Secured] ()
 establishConnection = do
   comment "Establish simplex messaging connection and send first message"
   r ->: b $ CreateConn "BODbZxmtKUUF1l8pj4nVjQ"