Skip to content

Commit 4dca01b

Browse files
cootcoot
committed
typed-protocols-stateful: improved haddocks
1 parent d248fe8 commit 4dca01b

File tree

3 files changed

+72
-18
lines changed

3 files changed

+72
-18
lines changed

‎typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Codec.hs‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -69,13 +69,22 @@ data Codec ps failure (f :: ps -> Type) m bytes = Codec {
6969
StateTokenI st
7070
=> ActiveState st
7171
=> f st
72+
-- local state, which contain extra context for the encoding
73+
-- process.
74+
--
75+
-- TODO: input-output-hk/typed-protocols#57
7276
-> Message ps st st'
77+
-- message to be encoded
7378
-> bytes,
7479

7580
decode :: forall (st :: ps).
7681
ActiveState st
7782
=> StateToken st
7883
-> f st
84+
-- local state, which can contain extra context from the
85+
-- previous message.
86+
--
87+
-- TODO: input-output-hk/typed-protocols#57
7988
-> m (DecodeStep bytes failure m (SomeMessage st))
8089
}
8190

@@ -130,7 +139,9 @@ data AnyMessage ps (f :: ps -> Type) where
130139
, ActiveState st
131140
)
132141
=> f st
142+
-- ^ local state
133143
-> Message ps (st :: ps) (st' :: ps)
144+
-- ^ protocol messsage
134145
-> AnyMessage ps f
135146

136147

@@ -176,6 +187,7 @@ pattern AnyMessageAndAgency stateToken f msg <- AnyMessage f (getAgency -> (msg,
176187
getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateToken st)
177188
getAgency msg = (msg, stateToken)
178189

190+
179191
-- | The 'Codec' round-trip property: decode after encode gives the same
180192
-- message. Every codec must satisfy this property.
181193
--

‎typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Driver.hs‎

Lines changed: 22 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -42,7 +42,15 @@ data Driver ps (pr :: PeerRole) bytes failure dstate f m =
4242
WeHaveAgency
4343
(Relative pr (StateAgency st))
4444
-> f st
45+
-- local state associated to protocol state `st`;
46+
-- local state should not be sent to the remote side.
47+
-- However it provide extra context for the encoder.
48+
--
49+
-- TODO: input-output-hk/typed-protocols#57
4550
-> Message ps st st'
51+
-- message to send
52+
--
53+
-- TODO: input-output-hk/typed-protocols#57
4654
-> m ()
4755

4856
, -- | Receive a message, a blocking action which reads from the network
@@ -55,10 +63,20 @@ data Driver ps (pr :: PeerRole) bytes failure dstate f m =
5563
TheyHaveAgency
5664
(Relative pr (StateAgency st))
5765
-> f st
66+
-- local state which provides extra context for the
67+
-- decoder.
68+
--
69+
-- TODO: input-output-hk/typed-protocols#57
5870
-> dstate
71+
-- decoder state, e.g. bytes left from decoding of
72+
-- a previous message.
73+
--
74+
-- TODO: input-output-hk/typed-protocols#57
5975
-> m (SomeMessage st, dstate)
6076

61-
, initialDState :: dstate
77+
, -- | Initial decoder state.
78+
--
79+
initialDState :: dstate
6280
}
6381

6482

@@ -70,6 +88,9 @@ data Driver ps (pr :: PeerRole) bytes failure dstate f m =
7088
--
7189
-- This runs the peer to completion (if the protocol allows for termination).
7290
--
91+
-- NOTE: this function threads local state (i.e. `f`) through evolution of
92+
-- a protocol (i.e. `Peer`).
93+
--
7394
runPeerWithDriver
7495
:: forall ps (st :: ps) pr bytes failure dstate (f :: ps -> Type) m a.
7596
MonadSTM m

‎typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer.hs‎

Lines changed: 38 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -41,21 +41,22 @@ import Network.TypedProtocol.Core as Core
4141
-- * the protocol itself;
4242
-- * the client\/server role;
4343
-- *.the current protocol state;
44+
-- * the local state type;
4445
-- * the monad in which the peer operates; and
4546
-- * the type of any final result once the peer terminates.
4647
--
4748
-- For example:
4849
--
49-
-- > pingPongClientExample :: Peer PingPong AsClient StIdle m ()
50-
-- > pingPongServerExample :: Peer PingPong AsServer StIdle m Int
50+
-- > reqRespClientExample :: Peer (ReqResp FileAPI) AsClient StIdle State m ()
51+
-- > reqRespServerExample :: Peer (ReqResp FileAPI) AsServer StIdle State m Int
5152
--
5253
-- The actions that a peer can take are:
5354
--
54-
-- * to perform local monadic effects
55-
-- * to terminate with a result (but only in a terminal protocol state)
56-
-- * to send a message (but only in a protocol state in which we have agency)
57-
-- * to wait to receive a message (but only in a protocol state in which the
58-
-- other peer has agency)
55+
-- * perform a local monadic effect,
56+
-- * terminate with a result (but only in a terminal protocol state),
57+
-- * send a message (but only in a protocol state in which we have agency),
58+
-- * wait to receive a message (but only in a protocol state in which the
59+
-- other peer has agency).
5960
--
6061
-- The 'Yield', 'Await' and 'Done' constructors require to provide an evidence
6162
-- that the appropriate peer has agency. This information is supplied using
@@ -96,13 +97,19 @@ data Peer ps pr st f m a where
9697
-- ^ monadic continuation
9798
-> Peer ps pr st f m a
9899

99-
-- | Send a message to the other peer and then continue. This takes the
100-
-- message and the continuation. It also requires evidence that we have
101-
-- agency for this protocol state and thus are allowed to send messages.
100+
-- | Send a message to the other peer and then continue. The constructor
101+
-- requires evidence that we have agency for this protocol state and thus are
102+
-- allowed to send messages. It takes local state associated to the source
103+
-- and target protocol state of the message that is sent. This state is only
104+
-- maintained locally, never shared remotely. It also takes the message and
105+
-- the continuation. It also requires evidence that we have agency for this
106+
-- protocol state and thus are allowed to send messages.
102107
--
103108
-- Example:
104109
--
105-
-- > Yield ReflClientAgency MsgPing $ ...
110+
-- > Yield ReflClientAgency (StateBusy (ReadFile /etc/os-release))
111+
-- > StateIdle
112+
-- > $ MsgResp "..."
106113
--
107114
Yield
108115
:: forall ps pr (st :: ps) (st' :: ps) f m a.
@@ -113,9 +120,9 @@ data Peer ps pr st f m a where
113120
=> WeHaveAgencyProof pr st
114121
-- ^ agency singleton
115122
-> f st
116-
-- ^ initial protocol state
123+
-- ^ associated local state to the source protocol state 'st'
117124
-> f st'
118-
-- ^ final protocol state
125+
-- ^ associated local state to the target protocol state `st'`
119126
-> Message ps st st'
120127
-- ^ protocol message
121128
-> Peer ps pr st' f m a
@@ -134,10 +141,13 @@ data Peer ps pr st f m a where
134141
--
135142
-- Example:
136143
--
137-
-- > Await ReflClientAgency $ \msg ->
138-
-- > case msg of
139-
-- > MsgDone -> ...
140-
-- > MsgPing -> ...
144+
-- > Await ReflClientAgency $ \f msg ->
145+
-- > case (f, msg) of
146+
-- > (StateBusy (ReadFile path), MsgResp resp) ->
147+
-- > ( _continuation
148+
-- > , StateIdle
149+
-- > )
150+
--
141151
--
142152
Await
143153
:: forall ps pr (st :: ps) f m a.
@@ -148,10 +158,21 @@ data Peer ps pr st f m a where
148158
-- ^ agency singleton
149159
-> (forall (st' :: ps).
150160
f st
161+
-- associated local state to the source protocol state 'st'
162+
--
163+
-- TODO: input-output-hk/typed-protocols#57
151164
-> Message ps st st'
152165
-> ( Peer ps pr st' f m a
153166
, f st'
154167
)
168+
-- continuation and associated local state to the target protocol
169+
-- state `st'`
170+
--
171+
-- NOTE: the API is limited to pure transition of local state e.g.
172+
-- `f st -> Message ps st st' -> f st'`,
173+
-- see https://github.com/input-output-hk/typed-protocols/discussions/63
174+
--
175+
-- TODO: input-output-hk/typed-protocols#57
155176
)
156177
-- ^ continuation
157178
-> Peer ps pr st f m a

0 commit comments

Comments
 (0)