dandri/simplex-chat
1
0
Fork 0
mirror of https://github.com/simplex-chat/simplex-chat.git synced 2026-05-24 17:25:42 +00:00
Code Issues Packages Projects Releases Wiki Activity

type classes to ensure consistency of implementation types with command types

Browse Source
This commit is contained in:
Evgeny Poberezkin
2020-05-11 20:45:17 +01:00
parent f07f99c94f
commit 6eb75a5bdb
5 changed files with 358 additions and 140 deletions
Download Patch File Download Diff File Expand all files Collapse all files
definitions/src/Simplex/Messaging/Broker.hs
+19 -30
View File
@@ -1,7 +1,12 @@
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeOperators #-}
module Simplex.Messaging.Broker where
@@ -9,35 +14,19 @@ import ClassyPrelude
import Simplex.Messaging.Protocol
import Simplex.Messaging.Types
-- For some reason PrfCmd type-class requirement is not enforced here:
-- if I change one of the connection states to one for which
-- instance of PrfCmd does not exist (i.e. Command cannot be constructed),
-- it compiles anyway.
-- Creating Command instance here would prevent compilation
-- in case the types are incorrect, as it is done in Client.hs
instance ProtocolFunc Broker CreateConnCmd
CreateConnRequest CreateConnResponse -- request response
None New Idle Idle -- connection states
where
protoFunc _ = bCreateConn
instance Prf HasState Sender s
=> ProtocolCommandOf Broker
CreateConnRequest CreateConnResponse
Recipient Broker
(None <==> None <==| s)
(New <==> New <==| s)
Idle Idle 0 0
where
command = CreateConn
protoCmd = bCreateConn
bCreateConn :: Connection Broker None Idle
-> CreateConnRequest
-> Either String
(CreateConnResponse, Connection Broker New Idle)
bCreateConn (Connection str) _ = Right (CreateConnResponse "1" "2", Connection str)
-- TODO stub
-- below code should NOT compile, but it does
instance ProtocolFunc Broker CreateConnCmd
CreateConnRequest CreateConnResponse -- request response
None Secured Idle Idle -- "Secured" should not be allowed here,
where -- such command does not exist, so no instance of
protoFunc _ = bCreateConn' -- PrfCmd exist...? But it compiles.
bCreateConn' :: Connection Broker None Idle
-> CreateConnRequest
-> Either String
(CreateConnResponse, Connection Broker Secured Idle)
bCreateConn' (Connection str) _ = Right (CreateConnResponse "1" "2", Connection str)
-> Either String (CreateConnResponse, Connection Broker New Idle)
bCreateConn = protoCmdStub
definitions/src/Simplex/Messaging/Client.hs
+18 -10
View File
@@ -1,8 +1,12 @@
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
module Simplex.Messaging.Client where
@@ -10,16 +14,20 @@ import ClassyPrelude
import Simplex.Messaging.Protocol
import Simplex.Messaging.Types
instance ProtocolAction Recipient CreateConnCmd
CreateConnRequest CreateConnResponse -- request responce
None New Idle Idle -- connection states
where
protoAction _ = \(Connection str) _ _ -> Connection str -- TODO stub
instance Prf HasState Sender s
=> ProtocolActionOf Recipient
CreateConnRequest CreateConnResponse
Recipient Broker
(None <==> None <==| s)
(New <==> New <==| s)
Idle Idle 0 0
where
action = CreateConn
protoAction = rCreateConn
rCreateConn :: Connection Recipient None Idle
-> CreateConnRequest
-> Either String CreateConnResponse
-> Connection Recipient New Idle
rCreateConn = protoAction $ CreateConn @None
-> Either String (Connection Recipient New Idle)
rCreateConn = protoActionStub
definitions/src/Simplex/Messaging/Protocol.hs
+74 -99
View File
@@ -1,4 +1,5 @@
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE EmptyCase #-}
@@ -41,7 +42,7 @@ $(singletons [d|
| Drained -- (broker, recipient) drained (no messages)
deriving (Show, ShowSing, Eq)
data ConnectionSubscription = Subscribed | Idle
data ConnSubscription = Subscribed | Idle
|])
-- broker connection states
@@ -96,7 +97,7 @@ data EstablishedState (s :: ConnectionState) :: Type where
-- connection type stub for all participants, TODO move from idris
data Connection (p :: Participant)
(s :: ConnectionState)
(ss :: ConnectionSubscription) :: Type where
(ss :: ConnSubscription) :: Type where
Connection :: String -> Connection p s ss -- TODO replace with real type definition
@@ -112,19 +113,16 @@ data (<==>) (rs :: ConnectionState) (bs :: ConnectionState) :: Type where
deriving instance Show (rs <==> bs)
data AllConnState (rs :: ConnectionState)
(bs :: ConnectionState)
(ss :: ConnectionState) :: Type where
data family (<==|) rb (ss :: ConnectionState) :: Type
data instance (<==|) (rs <==> bs) ss :: Type where
(:<==|) :: Prf HasState Sender ss
=> rs <==> bs
-> Sing ss
-> AllConnState rs bs ss
-> rs <==> bs <==| ss
deriving instance Show (AllConnState rs bs ss)
type family (<==|) rb ss where
(rs <==> bs) <==| (ss :: ConnectionState) = AllConnState rs bs ss
deriving instance Show (rs <==> bs <==| ss)
-- example of states of connection for all participants
-- recipient <==> broker <==| sender
st2 :: Pending <==> New <==| Confirmed
st2 = SPending :<==> SNew :<==| SConfirmed
@@ -134,32 +132,16 @@ st2 = SPending :<==> SNew :<==| SConfirmed
-- stBad = SPending :<==> SConfirmed :<==| SConfirmed
-- data type with all available protocol commands
$(singletons [d|
data ProtocolCmd = CreateConnCmd
| SubscribeCmd
| UnsubscribeCmd
| SendInviteCmd
| ConfirmConnCmd
| PushConfirmCmd
| SecureConnCmd
| SendWelcomeCmd
| SendMsgCmd
| PushMsgCmd
| DeleteMsgCmd
| Comp -- result of composing multiple commands
|])
infixl 4 :>>, :>>=
data Command (cmd :: ProtocolCmd) arg result
data Command arg result
(from :: Participant) (to :: Participant)
state state'
(ss :: ConnectionSubscription) (ss' :: ConnectionSubscription)
(ss :: ConnSubscription) (ss' :: ConnSubscription)
(messages :: Nat) (messages' :: Nat)
:: Type where
CreateConn :: Prf HasState Sender s
=> Command CreateConnCmd
=> Command
CreateConnRequest CreateConnResponse
Recipient Broker
(None <==> None <==| s)
@@ -169,7 +151,7 @@ data Command (cmd :: ProtocolCmd) arg result
Subscribe :: ( (r /= None && r /= Disabled) ~ True
, (b /= None && b /= Disabled) ~ True
, Prf HasState Sender s )
=> Command SubscribeCmd
=> Command
() ()
Recipient Broker
(r <==> b <==| s)
@@ -179,7 +161,7 @@ data Command (cmd :: ProtocolCmd) arg result
Unsubscribe :: ( (r /= None && r /= Disabled) ~ True
, (b /= None && b /= Disabled) ~ True
, Prf HasState Sender s )
=> Command UnsubscribeCmd
=> Command
() ()
Recipient Broker
(r <==> b <==| s)
@@ -187,7 +169,7 @@ data Command (cmd :: ProtocolCmd) arg result
Subscribed Idle n n
SendInvite :: Prf HasState Broker s
=> Command SendInviteCmd
=> Command
String () -- invitation - TODO
Recipient Sender
(New <==> s <==| None)
@@ -195,7 +177,7 @@ data Command (cmd :: ProtocolCmd) arg result
ss ss n n
ConfirmConn :: Prf HasState Recipient s
=> Command ConfirmConnCmd
=> Command
SecureConnRequest ()
Sender Broker
(s <==> New <==| New)
@@ -203,7 +185,7 @@ data Command (cmd :: ProtocolCmd) arg result
ss ss n (n+1)
PushConfirm :: Prf HasState Sender s
=> Command PushConfirmCmd
=> Command
SecureConnRequest ()
Broker Recipient
(Pending <==> New <==| s)
@@ -211,7 +193,7 @@ data Command (cmd :: ProtocolCmd) arg result
Subscribed Subscribed n n
SecureConn :: Prf HasState Sender s
=> Command SecureConnCmd
=> Command
SecureConnRequest ()
Recipient Broker
(Confirmed <==> New <==| s)
@@ -219,7 +201,7 @@ data Command (cmd :: ProtocolCmd) arg result
ss ss n n
SendWelcome :: Prf HasState Recipient s
=> Command SendWelcomeCmd
=> Command
() ()
Sender Broker
(s <==> Secured <==| Confirmed)
@@ -227,7 +209,7 @@ data Command (cmd :: ProtocolCmd) arg result
ss ss n (n+1)
SendMsg :: Prf HasState Recipient s
=> Command SendMsgCmd
=> Command
SendMessageRequest ()
Sender Broker
(s <==> Secured <==| Secured)
@@ -235,7 +217,7 @@ data Command (cmd :: ProtocolCmd) arg result
ss ss n (n+1)
PushMsg :: Prf HasState 'Sender s
=> Command PushMsgCmd
=> Command
MessagesResponse () -- TODO, has to be a single message
Broker Recipient
(Secured <==> Secured <==| s)
@@ -243,100 +225,93 @@ data Command (cmd :: ProtocolCmd) arg result
Subscribed Subscribed n n
DeleteMsg :: Prf HasState Sender s
=> Command DeleteMsgCmd
=> Command
() () -- TODO needs message ID parameter
Recipient Broker
(Secured <==> Secured <==| s)
(Secured <==> Secured <==| s)
ss ss n (n-1)
-- this command has to be removed - this is here to allow proof
-- that any command can be constructed
AnyCmd :: Command cmd a b from to s1 s2 ss1 ss2 n1 n2
Return :: b -> Command a b from to state state ss ss n n
Return :: b -> Command Comp a b from to state state ss ss n n
(:>>=) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> (b -> Command b c from2 to2 s2 s3 ss2 ss3 n2 n3)
-> Command a c from1 to2 s1 s3 ss1 ss3 n1 n3
(:>>=) :: Command cmd1 a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> (b -> Command cmd2 b c from2 to2 s2 s3 ss2 ss3 n2 n3)
-> Command Comp a c from1 to2 s1 s3 ss1 ss3 n1 n3
(:>>) :: Command cmd1 a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> Command cmd2 c d from2 to2 s2 s3 ss2 ss3 n2 n3
-> Command Comp a d from1 to2 s1 s3 ss1 ss3 n1 n3
(:>>) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> Command c d from2 to2 s2 s3 ss2 ss3 n2 n3
-> Command a d from1 to2 s1 s3 ss1 ss3 n1 n3
Fail :: String
-> Command Comp a String from to state (None <==> None <==| None) ss ss n n
-> Command a String from to state (None <==> None <==| None) ss ss n n
-- redifine Monad operators to compose commands
-- using `do` notation with RebindableSyntax extension
(>>=) :: Command cmd1 a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> (b -> Command cmd2 b c from2 to2 s2 s3 ss2 ss3 n2 n3)
-> Command Comp a c from1 to2 s1 s3 ss1 ss3 n1 n3
(>>=) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> (b -> Command b c from2 to2 s2 s3 ss2 ss3 n2 n3)
-> Command a c from1 to2 s1 s3 ss1 ss3 n1 n3
(>>=) = (:>>=)
(>>) :: Command cmd1 a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> Command cmd2 c d from2 to2 s2 s3 ss2 ss3 n2 n3
-> Command Comp a d from1 to2 s1 s3 ss1 ss3 n1 n3
(>>) :: Command a b from1 to1 s1 s2 ss1 ss2 n1 n2
-> Command c d from2 to2 s2 s3 ss2 ss3 n2 n3
-> Command a d from1 to2 s1 s3 ss1 ss3 n1 n3
(>>) = (:>>)
fail :: String -> Command Comp a String from to state (None <==> None <==| None) ss ss n n
fail :: String -> Command a String from to state (None <==> None <==| None) ss ss n n
fail = Fail
-- show and validate expexcted command participants
infix 6 -->
(-->) :: Sing from -> Sing to
-> ( Command cmd a b from to s s' ss ss' n n'
-> Command cmd a b from to s s' ss ss' n n' )
-> ( Command a b from to s s' ss ss' n n'
-> Command a b from to s s' ss ss' n n' )
(-->) _ _ = id
-- extract connection state of specfic participant
type family PConnSt (p :: Participant) state where
PConnSt Recipient (AllConnState r b s) = r
PConnSt Broker (AllConnState r b s) = b
PConnSt Sender (AllConnState r b s) = s
PConnSt Recipient (r <==> b <==| s) = r
PConnSt Broker (r <==> b <==| s) = b
PConnSt Sender (r <==> b <==| s) = s
-- Type classes to ensure consistency of types of implementations
-- of participants actions/functions and connection state transitions (types)
-- with types of protocol commands defined above.
-- TODO for some reason this type class is not enforced -
-- it still allows to construct invalid implementations.
-- See comment in Broker.hs
-- As done in Client.hs it type-checks, but it looks ugly
class PrfCmd cmd arg res from to s s' ss ss' n n' where
command :: Command cmd arg res from to s s' ss ss' n n'
instance Prf HasState Sender s
=> PrfCmd CreateConnCmd
CreateConnRequest CreateConnResponse
Recipient Broker
(AllConnState None None s)
(AllConnState New New s)
Idle Idle 0 0
where
command = CreateConn
class me ~ p => ProtocolCommandOf (me :: Participant)
arg res
(from :: Participant) (p :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
(n :: Nat) (n' :: Nat)
where
command :: Command arg res from p state state' ss ss' n n'
protoCmd :: Connection p (PConnSt p state) ss
-> arg
-> Either String (res, Connection p (PConnSt p state') ss')
protoCmdStub :: Connection p ps ss
-> arg
-> Either String (res, Connection p ps' ss')
protoCmdStub _ _ = Left "Command not implemented"
class ProtocolFunc (p :: Participant) (cmd :: ProtocolCmd) arg res ps ps' ss ss' where
protoFunc :: ( PrfCmd cmd arg res from p s s' ss ss' n n'
, PConnSt p s ~ ps
, PConnSt p s' ~ ps' )
=> Command cmd arg res
from p -- participant receives this command
s s' ss ss' n n'
-> ( Connection p ps ss
-> arg
-> Either String (res, Connection p ps' ss') )
class me ~ p => ProtocolActionOf (me :: Participant)
arg res
(p :: Participant) (to :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
(n :: Nat) (n' :: Nat)
where
action :: Command arg res p to state state' ss ss' n n'
protoAction :: Connection p (PConnSt p state) ss
-> arg
-> Either String res
-> Either String (Connection p (PConnSt p state') ss')
class ProtocolAction (p :: Participant) (cmd :: ProtocolCmd) arg res ps ps' ss ss' where
protoAction :: ( PrfCmd cmd arg res p to s s' ss ss' n n'
, PConnSt p s ~ ps
, PConnSt p s' ~ ps' )
=> Command cmd arg res
p to -- participant sends this command
s s' ss ss' n n'
-> ( Connection p ps ss
-> arg
-> Either String res
-> Connection p ps' ss' )
protoActionStub :: Connection p ps ss
-> arg
-> Either String res
-> Either String (Connection p ps' ss')
protoActionStub _ _ _ = Left "Action not implemented"
definitions/src/Simplex/Messaging/Scenarios.hs
+1 -1
View File
@@ -23,7 +23,7 @@ b = SBroker
s :: Sing Sender
s = SSender
establishConnection :: Command Comp
establishConnection :: Command
CreateConnRequest ()
Recipient Broker
(None <==> None <==| None)
definitions/src/Simplex/Messaging/Test.hs
+246
View File
@@ -0,0 +1,246 @@
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
{-# OPTIONS_GHC -freduction-depth=0 #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NoStarIsType #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Simplex.Messaging.Test where
import ClassyPrelude
import Data.Kind
import Data.Singletons
import Data.Singletons.ShowSing
import Data.Singletons.TH
import Data.Type.Predicate
import Data.Type.Predicate.Auto
import Simplex.Messaging.Types
$(singletons [d|
data Participant = Recipient | Broker | Sender
data ConnectionState = None -- (all) not available or removed from the broker
| New -- (participants: all) connection created (or received from sender)
| Pending -- (recipient) sent to sender out-of-band
| Confirmed -- (recipient) confirmed by sender with the broker
| Secured -- (all) secured with the broker
| Disabled -- (broker, recipient) disabled with the broker by recipient
| Drained -- (broker, recipient) drained (no messages)
deriving (Show, ShowSing, Eq)
data ConnSubscription = Subscribed | Idle
|])
-- broker connection states
type Prf1 t a = Auto (TyPred t) a
data BrokerCS :: ConnectionState -> Type where
BrkNew :: BrokerCS New
BrkSecured :: BrokerCS Secured
BrkDisabled :: BrokerCS Disabled
BrkDrained :: BrokerCS Drained
BrkNone :: BrokerCS None
instance Auto (TyPred BrokerCS) New where auto = autoTC
instance Auto (TyPred BrokerCS) Secured where auto = autoTC
instance Auto (TyPred BrokerCS) Disabled where auto = autoTC
instance Auto (TyPred BrokerCS) Drained where auto = autoTC
instance Auto (TyPred BrokerCS) None where auto = autoTC
-- sender connection states
data SenderCS :: ConnectionState -> Type where
SndNew :: SenderCS New
SndConfirmed :: SenderCS Confirmed
SndSecured :: SenderCS Secured
SndNone :: SenderCS None
instance Auto (TyPred SenderCS) New where auto = autoTC
instance Auto (TyPred SenderCS) Confirmed where auto = autoTC
instance Auto (TyPred SenderCS) Secured where auto = autoTC
instance Auto (TyPred SenderCS) None where auto = autoTC
-- allowed participant connection states
data HasState (p :: Participant) (s :: ConnectionState) :: Type where
RcpHasState :: HasState Recipient s
BrkHasState :: Prf1 BrokerCS s => HasState Broker s
SndHasState :: Prf1 SenderCS s => HasState Sender s
class Prf t p s where auto' :: t p s
instance Prf HasState Recipient s
where auto' = RcpHasState
instance Prf1 BrokerCS s => Prf HasState Broker s
where auto' = BrkHasState
instance Prf1 SenderCS s => Prf HasState Sender s
where auto' = SndHasState
-- connection type stub for all participants, TODO move from idris
data Connection (p :: Participant)
(s :: ConnectionState)
(ss :: ConnSubscription) :: Type where
Connection :: String -> Connection p s ss -- TODO replace with real type definition
-- data types for connection states of all participants
infixl 7 <==>, <==| -- types
infixl 7 :<==>, :<==| -- constructors
data (<==>) (rs :: ConnectionState) (bs :: ConnectionState) :: Type where
(:<==>) :: (Prf HasState Recipient rs, Prf HasState Broker bs)
=> Sing rs
-> Sing bs
-> rs <==> bs
deriving instance Show (rs <==> bs)
data family (<==|) rcpBrk (ss :: ConnectionState) :: Type
data instance (<==|) (rs <==> bs) ss :: Type where
(:<==|) :: Prf HasState Sender ss
=> rs <==> bs
-> Sing ss
-> rs <==> bs <==| ss
deriving instance Show (rs <==> bs <==| ss)
-- type family (<==|) rb ss where
-- (rs <==> bs) <==| (ss :: ConnectionState) = AllConnState rs bs ss
-- recipient <==> broker <==| sender
st2 :: Pending <==> New <==| Confirmed
st2 = SPending :<==> SNew :<==| SConfirmed
-- this must not type check
-- stBad :: 'Pending <==> 'Confirmed <==| 'Confirmed
-- stBad = SPending :<==> SConfirmed :<==| SConfirmed
-- data type with all available protocol commands
$(singletons [d|
data ProtocolCmd = CreateConnCmd
| SubscribeCmd
| Comp -- result of composing multiple commands
|])
data Command (cmd :: ProtocolCmd) arg result
(from :: Participant) (to :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
:: Type where
CreateConn :: Prf HasState Sender s
=> Command CreateConnCmd
CreateConnRequest CreateConnResponse
Recipient Broker
(None <==> None <==| s)
(New <==> New <==| s)
Idle Idle
Subscribe :: ( (r /= None && r /= Disabled) ~ True
, (b /= None && b /= Disabled) ~ True
, Prf HasState Sender s )
=> Command SubscribeCmd
() ()
Recipient Broker
(r <==> b <==| s)
(r <==> b <==| s)
Idle Subscribed
-- extract connection state of specfic participant
type family PConnSt (p :: Participant) state where
PConnSt Recipient (r <==> b <==| s) = r
PConnSt Broker (r <==> b <==| s) = b
PConnSt Sender (r <==> b <==| s) = s
-- Type classes to ensure consistency of types of implementations
-- of participants actions/functions and connection state transitions (types)
-- with types of protocol commands defined above.
-- TODO for some reason this type class is not enforced -
-- it still allows to construct invalid implementations.
-- See comment in Broker.hs
-- As done in Client.hs it type-checks, but it looks ugly
-- class PrfCmd cmd arg res from to s1 s2 s3 s1' s2' s3' ss ss' where
-- command :: Command cmd arg res from to (AllConnState s1 s2 s3) (AllConnState s1' s2' s3') ss ss'
-- instance Prf HasState Sender s
-- => PrfCmd CreateConnCmd
-- CreateConnRequest CreateConnResponse
-- Recipient Broker
-- None None s
-- New New s
-- Idle Idle
-- where
-- command = CreateConn
-- data Cmd cmd arg res from to ss ss' :: Type where
-- Cmd :: Command cmd arg res
-- from to
-- (AllConnState s1 s2 s3)
-- (AllConnState s1' s2' s3')
-- ss ss'
-- -> Cmd cmd arg res from to ss ss'
class ProtocolFunc
(cmd :: ProtocolCmd) arg res
(from :: Participant) (p :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
where
pfCommand :: Command (cmd :: ProtocolCmd) arg res
(from :: Participant) (p :: Participant)
state state'
(ss :: ConnSubscription) (ss' :: ConnSubscription)
protoFunc :: Connection p (PConnSt p state) ss
-> arg
-> Either String (res, Connection p (PConnSt p state') ss')
-- For some reason PrfCmd type-class requirement is not enforced here:
-- if I change one of the connection states to one for which
-- instance of PrfCmd does not exist (i.e. Command cannot be constructed),
-- it compiles anyway.
-- Creating Command instance here would prevent compilation
-- in case the types are incorrect, as it is done in Client.hs
instance Prf HasState Sender s
=> ProtocolFunc CreateConnCmd
CreateConnRequest CreateConnResponse
Recipient Broker
(None <==> None <==| s)
(New <==> New <==| s)
Idle Idle -- connection states
where
pfCommand = CreateConn
protoFunc = brkCreateConn
brkCreateConn :: Connection Broker None Idle
-> CreateConnRequest
-> Either String (CreateConnResponse, Connection Broker New Idle)
brkCreateConn (Connection str) _ = Right (CreateConnResponse "1" "2", Connection str)
-- TODO stub
-- -- below code should NOT compile, but it does
-- instance ProtocolFunc Broker CreateConnCmd
-- CreateConnRequest CreateConnResponse -- request response
-- None New Idle Idle -- "Secured" should not be allowed here,
-- where -- such command does not exist, so no instance of
-- protoFunc _ = \(Connection str) _ -> Right (CreateConnResponse "1" "2", Connection str) -- PrfCmd exist...? But it compiles.
-- bCreateConn' :: Connection Broker None Idle
-- -> CreateConnRequest
-- -> Either String
-- (CreateConnResponse, Connection Broker New Idle)
-- bCreateConn' = protoFunc $ CreateConn @None