Skip to content

Commit 782eee2

Browse files
cootcoot
committed
typed-protocols-stateful: pass initial state through Yield
This removes the need to pass it in messages, like we used to in `MsgResp` in `typed-protocols-examples`. The `Driver` and `Codec` were modified: * `encode` and `sendMessage` receive the initial state of the protocol state transition imposed by a message, which is dual to * `decode` and `recvMessage` receive the final state of the protocol state transition imposed by a message This is seems more natural than always passing the final state. The drawback of this systemic approach is that every `Yield` needs access to both initial and final state of a transition. In previous approach one had more control over which messages require access to the initial state (e.g. `MsgRecv` in `Stateful.ReqResp`) - although it was looking more like a hack since that part of a message wasn't sent over the wire.
1 parent cd80ff7 commit 782eee2

File tree

11 files changed

+64
-57
lines changed

11 files changed

+64
-57
lines changed

‎typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Client.hs‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,12 +30,12 @@ reqRespClientPeer
3030
-> Client (ReqResp req) StIdle State m a
3131

3232
reqRespClientPeer (SendMsgDone a) =
33-
Yield StateDone MsgDone (Done a)
33+
Yield StateIdle StateDone MsgDone (Done a)
3434

3535
reqRespClientPeer (SendMsgReq req next) =
36-
Yield (StateBusy req)
36+
Yield StateIdle (StateBusy req)
3737
(MsgReq req) $
38-
Await $ \_ (MsgResp _ resp) ->
38+
Await $ \_ (MsgResp resp) ->
3939
let client = next resp
4040
in ( Effect $ reqRespClientPeer <$> client
4141
, StateIdle

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -37,12 +37,12 @@ codecReqResp
3737
codecReqResp encodeReq decodeReq encodeResp decodeResp =
3838
Codec { encode, decode }
3939
where
40-
encode :: State st'
40+
encode :: State st
4141
-> Message (ReqResp req) st st'
4242
-> String
4343
encode _ (MsgReq req) = "MsgReq " ++ encodeReq req ++ "\n"
4444
encode _ MsgDone = "MsgDone\n"
45-
encode _ (MsgResp req resp) = "MsgResp " ++ encodeResp req resp ++ "\n"
45+
encode (StateBusy req) (MsgResp resp) = "MsgResp " ++ encodeResp req resp ++ "\n"
4646

4747
decode :: forall (st :: ReqResp req).
4848
ActiveState st
@@ -60,7 +60,7 @@ codecReqResp encodeReq decodeReq encodeResp decodeResp =
6060
(SingBusy, StateBusy req, ("MsgResp", str'))
6161
-- note that we need `req` to decode response of the given type
6262
| Just resp <- decodeResp req str'
63-
-> DecodeDone (SomeMessage (MsgResp req resp)) trailing
63+
-> DecodeDone (SomeMessage (MsgResp resp)) trailing
6464
(_, _, _) -> DecodeFail failure
6565
where failure = CodecFailure ("unexpected server message: " ++ str)
6666

@@ -106,7 +106,7 @@ codecReqRespId eqRespTypes = Codec { encode, decode }
106106

107107
msgRespType :: forall resp. Message (ReqResp FileAPI) (StBusy resp) StIdle
108108
-> Proxy resp
109-
msgRespType (MsgResp _ _) = Proxy
109+
msgRespType (MsgResp _) = Proxy
110110

111111
reqRespType :: forall resp. FileAPI resp -> Proxy resp
112112
reqRespType _ = Proxy

‎typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Server.hs‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ reqRespServerPeer ReqRespServer { reqRespServerDone = a,
3030
MsgDone -> (Done a, StateDone)
3131
MsgReq req ->
3232
( Effect $
33-
(\(resp, k') -> Yield StateIdle (MsgResp req resp) (reqRespServerPeer k'))
33+
(\(resp, k') -> Yield (StateBusy req) StateIdle (MsgResp resp) (reqRespServerPeer k'))
3434
<$> k req
3535
, StateBusy req
3636
)

‎typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Type.hs‎

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -54,12 +54,7 @@ instance Protocol (ReqResp req) where
5454
-- promoted to the state `StBusy` state.
5555
-> Message (ReqResp req) StIdle (StBusy resp)
5656
MsgResp :: Typeable resp
57-
=> req resp -- ^ request, not sent over the wire, just useful in the
58-
-- codec.
59-
--
60-
-- TODO: https://github.com/input-output-hk/typed-protocols/issues/59
61-
62-
-> resp -- ^ respond
57+
=> resp -- ^ respond
6358
-> Message (ReqResp req) (StBusy resp) StIdle
6459
MsgDone :: Message (ReqResp req) StIdle StDone
6560

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ mkCodecCborStrictBS
4848
=> (forall (st :: ps) (st' :: ps).
4949
StateTokenI st
5050
=>ActiveState st
51-
=> f st' -> Message ps st st' -> CBOR.Encoding)
51+
=> f st -> Message ps st st' -> CBOR.Encoding)
5252
-- ^ cbor encoder
5353

5454
-> (forall (st :: ps) s.
@@ -90,7 +90,7 @@ mkCodecCborLazyBS
9090
=> (forall (st :: ps) (st' :: ps).
9191
StateTokenI st
9292
=> ActiveState st
93-
=> f st'
93+
=> f st
9494
-> Message ps st st' -> CBOR.Encoding)
9595
-- ^ cbor encoder
9696

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

Lines changed: 40 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -43,6 +43,7 @@ module Network.TypedProtocol.Stateful.Codec
4343
-- * Testing codec properties
4444
, AnyMessage (..)
4545
, pattern AnyMessageAndAgency
46+
, showAnyMessage
4647
, prop_codecM
4748
, prop_codec
4849
, prop_codec_splitsM
@@ -68,7 +69,7 @@ data Codec ps failure (f :: ps -> Type) m bytes = Codec {
6869
encode :: forall (st :: ps) (st' :: ps).
6970
StateTokenI st
7071
=> ActiveState st
71-
=> f st'
72+
=> f st
7273
-> Message ps st st'
7374
-> bytes,
7475

@@ -130,22 +131,30 @@ data AnyMessage ps (f :: ps -> Type) where
130131
, ActiveState st
131132
)
132133
=> f st
133-
-> f st'
134134
-> Message ps (st :: ps) (st' :: ps)
135135
-> AnyMessage ps f
136136

137-
instance ( forall (st :: ps) (st' :: ps). Show (Message ps st st')
138-
, forall (st :: ps). Show (f st)
139-
)
140-
=> Show (AnyMessage ps f) where
141-
show (AnyMessage st st' msg) = concat [ "AnyMessage "
142-
, show st
143-
, " "
144-
, show st'
145-
, " "
146-
, show msg
147-
]
148137

138+
-- | `showAnyMessage` is can be used to provide `Show` instance for
139+
-- `AnyMessage` if showing `Message` is independent of the state or one accepts
140+
-- showing only partial information included in message constructors or accepts
141+
-- message constructors to carry `Show` instances for its arguments. Note that
142+
-- the proper solution is to define a custom `Show (AnyMessage ps f)` instance
143+
-- for a protocol `ps`, which give access to the state functor `f` in scope of
144+
-- `show`.
145+
--
146+
showAnyMessage :: forall ps f.
147+
( forall st st'. Show (Message ps st st')
148+
, forall st. Show (f st)
149+
)
150+
=> AnyMessage ps f
151+
-> String
152+
showAnyMessage (AnyMessage st msg) =
153+
concat [ "AnyMessage "
154+
, show st
155+
, " "
156+
, show msg
157+
]
149158

150159

151160
-- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the
@@ -156,10 +165,9 @@ pattern AnyMessageAndAgency :: forall ps f. ()
156165
(StateTokenI st, ActiveState st)
157166
=> StateToken st
158167
-> f st
159-
-> f st'
160168
-> Message ps st st'
161169
-> AnyMessage ps f
162-
pattern AnyMessageAndAgency stateToken f f' msg <- AnyMessage f f' (getAgency -> (msg, stateToken))
170+
pattern AnyMessageAndAgency stateToken f msg <- AnyMessage f (getAgency -> (msg, stateToken))
163171
where
164172
AnyMessageAndAgency _ msg = AnyMessage msg
165173
{-# COMPLETE AnyMessageAndAgency #-}
@@ -175,22 +183,22 @@ getAgency msg = (msg, stateToken)
175183
prop_codecM
176184
:: forall ps failure f m bytes.
177185
( Monad m
178-
, Eq (TP.AnyMessage ps)
186+
, Eq (AnyMessage ps f)
179187
)
180188
=> Codec ps failure f m bytes
181189
-> AnyMessage ps f
182190
-> m Bool
183-
prop_codecM Codec {encode, decode} (AnyMessage f f' (msg :: Message ps st st')) = do
184-
r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f' msg]
191+
prop_codecM Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do
192+
r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f msg]
185193
case r :: Either failure (SomeMessage st) of
186-
Right (SomeMessage msg') -> return $ TP.AnyMessage msg' == TP.AnyMessage msg
194+
Right (SomeMessage msg') -> return $ AnyMessage f msg' == a
187195
Left _ -> return False
188196

189197
-- | The 'Codec' round-trip property in a pure monad.
190198
--
191199
prop_codec
192200
:: forall ps failure f m bytes.
193-
(Monad m, Eq (TP.AnyMessage ps))
201+
(Monad m, Eq (AnyMessage ps f))
194202
=> (forall a. m a -> a)
195203
-> Codec ps failure f m bytes
196204
-> AnyMessage ps f
@@ -212,28 +220,28 @@ prop_codec runM codec msg =
212220
--
213221
prop_codec_splitsM
214222
:: forall ps failure f m bytes.
215-
(Monad m, Eq (TP.AnyMessage ps))
223+
(Monad m, Eq (AnyMessage ps f))
216224
=> (bytes -> [[bytes]]) -- ^ alternative re-chunkings of serialised form
217225
-> Codec ps failure f m bytes
218226
-> AnyMessage ps f
219227
-> m Bool
220228
prop_codec_splitsM splits
221-
Codec {encode, decode} (AnyMessage f f' (msg :: Message ps st st')) = do
229+
Codec {encode, decode} a@(AnyMessage f (msg :: Message ps st st')) = do
222230
and <$> sequence
223231
[ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes'
224232
case r :: Either failure (SomeMessage st) of
225-
Right (SomeMessage msg') -> return $ TP.AnyMessage msg' == TP.AnyMessage msg
233+
Right (SomeMessage msg') -> return $ AnyMessage f msg' == a
226234
Left _ -> return False
227235

228-
| let bytes = encode f' msg
236+
| let bytes = encode f msg
229237
, bytes' <- splits bytes ]
230238

231239

232240
-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.
233241
--
234242
prop_codec_splits
235243
:: forall ps failure f m bytes.
236-
(Monad m, Eq (TP.AnyMessage ps))
244+
(Monad m, Eq (AnyMessage ps f))
237245
=> (bytes -> [[bytes]])
238246
-> (forall a. m a -> a)
239247
-> Codec ps failure f m bytes
@@ -250,30 +258,30 @@ prop_codec_splits splits runM codec msg =
250258
prop_codecs_compatM
251259
:: forall ps failure f m bytes.
252260
( Monad m
253-
, Eq (TP.AnyMessage ps)
261+
, Eq (AnyMessage ps f)
254262
, forall a. Monoid a => Monoid (m a)
255263
)
256264
=> Codec ps failure f m bytes
257265
-> Codec ps failure f m bytes
258266
-> AnyMessage ps f
259267
-> m Bool
260268
prop_codecs_compatM codecA codecB
261-
(AnyMessage f f' (msg :: Message ps st st')) =
262-
getAll <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f' msg]
269+
a@(AnyMessage f (msg :: Message ps st st')) =
270+
getAll <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f msg]
263271
case r :: Either failure (SomeMessage st) of
264-
Right (SomeMessage msg') -> return $ All $ TP.AnyMessage msg' == TP.AnyMessage msg
272+
Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a
265273
Left _ -> return $ All False
266-
<> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f' msg]
274+
<> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f msg]
267275
case r :: Either failure (SomeMessage st) of
268-
Right (SomeMessage msg') -> return $ All $ TP.AnyMessage msg' == TP.AnyMessage msg
276+
Right (SomeMessage msg') -> return $ All $ AnyMessage f msg' == a
269277
Left _ -> return $ All False
270278

271279
-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@.
272280
--
273281
prop_codecs_compat
274282
:: forall ps failure f m bytes.
275283
( Monad m
276-
, Eq (TP.AnyMessage ps)
284+
, Eq (AnyMessage ps f)
277285
, forall a. Monoid a => Monoid (m a)
278286
)
279287
=> (forall a. m a -> a)

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -41,7 +41,7 @@ data Driver ps (pr :: PeerRole) bytes failure dstate f m =
4141
=> ReflRelativeAgency (StateAgency st)
4242
WeHaveAgency
4343
(Relative pr (StateAgency st))
44-
-> f st'
44+
-> f st
4545
-> Message ps st st'
4646
-> m ()
4747

@@ -92,9 +92,9 @@ runPeerWithDriver Driver{ sendMessage
9292

9393
go !dstate _ (Done _ x) = return (x, dstate)
9494

95-
go !dstate _ (Yield refl !f msg k) = do
95+
go !dstate _ (Yield refl !f !f' msg k) = do
9696
sendMessage refl f msg
97-
go dstate f k
97+
go dstate f' k
9898

9999
go !dstate !f (Await refl k) = do
100100
(SomeMessage msg, dstate') <- recvMessage refl f dstate

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,8 +112,10 @@ data Peer ps pr st f m a where
112112
)
113113
=> WeHaveAgencyProof pr st
114114
-- ^ agency singleton
115+
-> f st
116+
-- ^ initial protocol state
115117
-> f st'
116-
-- ^ protocol state
118+
-- ^ final protocol state
117119
-> Message ps st st'
118120
-- ^ protocol message
119121
-> Peer ps pr st' f m a

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,13 +54,14 @@ pattern Yield :: forall ps st f m a.
5454
, StateTokenI st'
5555
, StateAgency st ~ ClientAgency
5656
)
57-
=> f st'
57+
=> f st
58+
-> f st'
5859
-> Message ps st st'
5960
-- ^ protocol message
6061
-> Client ps st' f m a
6162
-- ^ continuation
6263
-> Client ps st f m a
63-
pattern Yield f msg k = TP.Yield ReflClientAgency f msg k
64+
pattern Yield f f' msg k = TP.Yield ReflClientAgency f f' msg k
6465

6566

6667
-- | Client role pattern for 'TP.Await'

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

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -54,13 +54,14 @@ pattern Yield :: forall ps st f m a.
5454
, StateTokenI st'
5555
, StateAgency st ~ ServerAgency
5656
)
57-
=> f st'
57+
=> f st
58+
-> f st'
5859
-> Message ps st st'
5960
-- ^ protocol message
6061
-> Server ps st' f m a
6162
-- ^ continuation
6263
-> Server ps st f m a
63-
pattern Yield f msg k = TP.Yield ReflServerAgency f msg k
64+
pattern Yield f f' msg k = TP.Yield ReflServerAgency f f' msg k
6465

6566

6667
-- | Server role pattern for 'TP.Await'

0 commit comments

Comments
 (0)