diff --git a/definitions/src/Simplex/Messaging/Broker.hs b/definitions/src/Simplex/Messaging/Broker.hs index eb430b90fa..16eadaf5a8 100644 --- a/definitions/src/Simplex/Messaging/Broker.hs +++ b/definitions/src/Simplex/Messaging/Broker.hs @@ -1,7 +1,6 @@ {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} module Simplex.Messaging.Broker where @@ -10,6 +9,12 @@ 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 @@ -22,3 +27,17 @@ bCreateConn :: Connection Broker None Idle (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) diff --git a/definitions/src/Simplex/Messaging/Client.hs b/definitions/src/Simplex/Messaging/Client.hs index c71e1ccd03..96d4bbbf47 100644 --- a/definitions/src/Simplex/Messaging/Client.hs +++ b/definitions/src/Simplex/Messaging/Client.hs @@ -1,8 +1,8 @@ {-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-} {-# OPTIONS_GHC -fno-warn-orphans #-} {-# LANGUAGE DataKinds #-} -{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} module Simplex.Messaging.Client where @@ -15,11 +15,11 @@ instance ProtocolAction Recipient CreateConnCmd CreateConnRequest CreateConnResponse -- request responce None New Idle Idle -- connection states where - protoAction _ = rCreateConn + protoAction _ = \(Connection str) _ _ -> Connection str -- TODO stub rCreateConn :: Connection Recipient None Idle -> CreateConnRequest -> Either String CreateConnResponse -> Connection Recipient New Idle -rCreateConn (Connection str) _ _ = Connection str -- TODO stub +rCreateConn = protoAction $ CreateConn @None diff --git a/definitions/src/Simplex/Messaging/Protocol.hs b/definitions/src/Simplex/Messaging/Protocol.hs index 3ee78f0b2d..b3883a8c0f 100644 --- a/definitions/src/Simplex/Messaging/Protocol.hs +++ b/definitions/src/Simplex/Messaging/Protocol.hs @@ -297,20 +297,26 @@ type family PConnSt (p :: Participant) state where PConnSt Sender (AllConnState r b s) = s --- type class to ensure consistency of types of implementations +-- Type classes to ensure consistency of types of implementations -- of participants actions/functions and connection state transitions (types) --- with types of protocol commands defined here +-- with types of protocol commands defined above. --- TODO it still allows to construct invalid implementations --- there should be added proof that such command can be constructed --- (or it should be constructed by implementations, but it looks ugly) +-- 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 --- TODO have to be specific commands, as is it allows to construct any command --- not matching any real command in the protocol -instance PrfCmd cmd arg res from to s s' ss ss' n n' where - command = AnyCmd @cmd @arg @res @from @to @s @s' @ss @ss' @n @n' 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'