typed-protocols: moved outstanding counter into IsPipelined kind

Author: coot

typed-protocols-examples/src/Network/TypedProtocol/Driver/Simple.hs

@@ -131,7 +131,7 @@ runPeer
   => Tracer m (TraceSendRecv ps)
   -> Codec ps failure m bytes
   -> Channel m bytes
-  -> Peer ps pr 'NonPipelined Z st m a
+  -> Peer ps pr 'NonPipelined st m a
   -> m (a, Maybe bytes)
 runPeer tracer codec channel peer =
     runPeerWithDriver driver peer
@@ -152,7 +152,7 @@ runPipelinedPeer
   => Tracer m (TraceSendRecv ps)
   -> Codec ps failure m bytes
   -> Channel m bytes
-  -> Peer ps pr ('Pipelined c) Z st m a
+  -> Peer ps pr ('Pipelined Z c) st m a
   -> m (a, Maybe bytes)
 runPipelinedPeer tracer codec channel peer =
     runPipelinedPeerWithDriver driver peer
@@ -196,8 +196,8 @@ runConnectedPeers :: (MonadAsync m, MonadCatch m,
                   => m (Channel m bytes, Channel m bytes)
                   -> Tracer m (Role, TraceSendRecv ps)
                   -> Codec ps failure m bytes
-                  -> Peer ps             pr  'NonPipelined Z st m a
-                  -> Peer ps (FlipAgency pr) 'NonPipelined Z st m b
+                  -> Peer ps             pr  'NonPipelined st m a
+                  -> Peer ps (FlipAgency pr) 'NonPipelined st m b
                   -> m (a, b)
 runConnectedPeers createChannels tracer codec client server =
     createChannels >>= \(clientChannel, serverChannel) ->
@@ -214,8 +214,8 @@ runConnectedPeersPipelined :: (MonadAsync m, MonadCatch m,
                            => m (Channel m bytes, Channel m bytes)
                            -> Tracer m (PeerRole, TraceSendRecv ps)
                            -> Codec ps failure m bytes
-                           -> Peer ps             pr  ('Pipelined c) Z st m a
-                           -> Peer ps (FlipAgency pr) 'NonPipelined  Z st m b
+                           -> Peer ps             pr  ('Pipelined Z c) st m a
+                           -> Peer ps (FlipAgency pr) 'NonPipelined    st m b
                            -> m (a, b)
 runConnectedPeersPipelined createChannels tracer codec client server =
     createChannels >>= \(clientChannel, serverChannel) ->
@@ -240,8 +240,8 @@ runConnectedPeersAsymmetric
     -> Tracer m (Role, TraceSendRecv ps)
     -> Codec ps failure m bytes
     -> Codec ps failure m bytes
-    -> Peer ps             pr  ('Pipelined c) Z st m a
-    -> Peer ps (FlipAgency pr) 'NonPipelined  Z st m b
+    -> Peer ps             pr  ('Pipelined Z c) st m a
+    -> Peer ps (FlipAgency pr) 'NonPipelined    st m b
     -> m (a, b)
 runConnectedPeersAsymmetric createChannels tracer codec codec' client server =
     createChannels >>= \(clientChannel, serverChannel) ->

typed-protocols-examples/src/Network/TypedProtocol/PingPong/Client.hs

@@ -54,7 +54,7 @@ data PingPongClient m a where
 pingPongClientPeer
   :: Functor m
   => PingPongClient m a
-  -> Client PingPong NonPipelined Z StIdle m a
+  -> Client PingPong NonPipelined StIdle m a
 
 pingPongClientPeer (SendMsgDone result) =
     -- We do an actual transition using 'yield', to go from the 'StIdle' to
@@ -94,7 +94,7 @@ data PingPongClientPipelined c m a where
    -> PingPongClientPipelined   c m a
 
 
-data PingPongClientIdle (n :: Outstanding) c m a where
+data PingPongClientIdle (n :: N) c m a where
   -- | Send a `Ping` message but alike in `PingPongClient` do not await for the
   -- response, instead supply a monadic action which will run on a received
   -- `Pong` message.
@@ -139,20 +139,20 @@ data PingPongClientIdle (n :: Outstanding) c m a where
 pingPongClientPeerPipelined
   :: Functor m
   => PingPongClientPipelined c m a
-  -> Client PingPong (Pipelined c) Z StIdle m a
+  -> Client PingPong (Pipelined Z c) StIdle m a
 pingPongClientPeerPipelined (PingPongClientPipelined peer) =
     pingPongClientPeerIdle peer
 
 
 pingPongClientPeerIdle
-  :: forall (n :: Outstanding) c m a. Functor m
-  => PingPongClientIdle             n        c m a
-  -> Client PingPong (Pipelined c) n StIdle   m a
+  :: forall (n :: N) c m a. Functor m
+  => PingPongClientIdle         n c         m a
+  -> Client PingPong (Pipelined n c) StIdle m a
 pingPongClientPeerIdle = go
   where
-    go :: forall (n' :: Outstanding).
-          PingPongClientIdle             n'        c m a
-       -> Client PingPong (Pipelined c) n' StIdle   m a
+    go :: forall (n' :: N).
+          PingPongClientIdle         n' c         m a
+       -> Client PingPong (Pipelined n' c) StIdle m a
 
     go (SendMsgPingPipelined receive next) =
       -- Pipelined yield: send `MsgPing`, immediately follow with the next step.

typed-protocols-examples/src/Network/TypedProtocol/PingPong/Server.hs

@@ -26,7 +26,7 @@ data PingPongServer m a = PingPongServer {
 pingPongServerPeer
   :: Monad m
   => PingPongServer m a
-  -> Server PingPong NonPipelined Z StIdle m a
+  -> Server PingPong NonPipelined StIdle m a
 pingPongServerPeer PingPongServer{..} =
 
     -- In the 'StIdle' the server is awaiting a request message

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

@@ -37,7 +37,7 @@ data ReqRespClient req resp m a where
 reqRespClientPeer
   :: Monad m
   => ReqRespClient req resp m a
-  -> Client (ReqResp req resp) NonPipelined Z StIdle m a
+  -> Client (ReqResp req resp) NonPipelined StIdle m a
 
 reqRespClientPeer (SendMsgDone result) =
     -- We do an actual transition using 'yield', to go from the 'StIdle' to
@@ -68,7 +68,7 @@ reqRespClientPeer (SendMsgReq req next) =
 
 requestOnce :: forall req resp m.
                Monad m
-            => (forall x. Server (ReqResp req resp) NonPipelined Z StIdle m x)
+            => (forall x. Server (ReqResp req resp) NonPipelined StIdle m x)
             -> (req -> m resp)
 requestOnce server req = (\(resp, _, _) -> resp)
                      <$> reqRespClientPeer client `connect` server
@@ -88,52 +88,52 @@ data ReqRespClientPipelined req resp c m a where
   -- | A 'PingPongSender', but starting with zero outstanding pipelined
   -- responses, and for any internal collect type @c@.
   ReqRespClientPipelined ::
-      ReqRespIdle            req resp c Z m a
-   -> ReqRespClientPipelined req resp c   m a
+      ReqRespIdle            req resp Z c m a
+   -> ReqRespClientPipelined req resp   c m a
 
 
-data ReqRespIdle req resp c n m a where
+data ReqRespIdle req resp n c m a where
   -- | Send a `Req` message but alike in `ReqRespClient` do not await for the
   -- resopnse, instead supply a monadic action which will run on a received
   -- `Pong` message.
   SendMsgReqPipelined
     :: req
     -> (resp -> m c)                     -- receive action
-    -> ReqRespIdle req resp c (S n) m a  -- continuation
-    -> ReqRespIdle req resp c    n  m a
+    -> ReqRespIdle req resp (S n) c m a  -- continuation
+    -> ReqRespIdle req resp    n  c m a
 
   CollectPipelined
-    :: Maybe   (ReqRespIdle req resp c (S n) m a)
-    -> (c -> m (ReqRespIdle req resp c    n  m a))
-    ->          ReqRespIdle req resp c (S n) m a
+    :: Maybe   (ReqRespIdle req resp (S n) c m a)
+    -> (c -> m (ReqRespIdle req resp    n  c m a))
+    ->          ReqRespIdle req resp (S n) c m a
 
   -- | Termination of the req-resp protocol.
   SendMsgDonePipelined
-    :: a -> ReqRespIdle req resp c Z m a
+    :: a -> ReqRespIdle req resp Z c m a
 
 
 -- | Interpret a pipelined client as a 'Peer' on the client side of
 -- the 'ReqResp' protocol.
 --
 reqRespClientPeerPipelined
   :: Functor m
-  => ReqRespClientPipelined req resp       c           m a
-  -> Client (ReqResp req resp) (Pipelined c) Z StIdle m a
+  => ReqRespClientPipelined req resp         c         m a
+  -> Client (ReqResp req resp) (Pipelined  Z c) StIdle m a
 reqRespClientPeerPipelined (ReqRespClientPipelined peer) =
     reqRespClientPeerIdle peer
 
 
 reqRespClientPeerIdle
   :: forall req resp n c m a.
      Functor m
-  => ReqRespIdle   req resp                c  n         m a
-  -> Client (ReqResp req resp) (Pipelined c) n StIdle  m a
+  => ReqRespIdle   req resp               n c          m a
+  -> Client (ReqResp req resp) (Pipelined n c) StIdle  m a
 
 reqRespClientPeerIdle = go
   where
     go :: forall n'.
-          ReqRespIdle   req resp                c  n'        m a
-       -> Client (ReqResp req resp) (Pipelined c) n' StIdle m a
+          ReqRespIdle   req resp               n' c         m a
+       -> Client (ReqResp req resp) (Pipelined n' c) StIdle m a
 
     go (SendMsgReqPipelined req receive next) =
       -- Pipelined yield: send `MsgReq`, immediately follow with the next step.

typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Examples.hs

@@ -72,7 +72,7 @@ reqRespClientMapPipelined :: forall req resp m.
 reqRespClientMapPipelined reqs0 =
     ReqRespClientPipelined (go [] Zero reqs0)
   where
-    go :: [resp] -> Nat o -> [req] -> ReqRespIdle req resp resp o m [resp]
+    go :: [resp] -> Nat o -> [req] -> ReqRespIdle req resp o resp m [resp]
     go resps Zero reqs =
       case reqs of
         []        -> SendMsgDonePipelined (reverse resps)
@@ -86,7 +86,7 @@ reqRespClientMapPipelined reqs0 =
         (\resp -> return $ go (resp:resps) o reqs)
 
     sendReq :: [resp] -> Nat o -> req -> [req]
-            -> ReqRespIdle req resp resp o m [resp]
+            -> ReqRespIdle req resp o resp m [resp]
     sendReq resps o req reqs' =
       SendMsgReqPipelined req
         (\resp -> return resp)

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

@@ -26,7 +26,7 @@ data ReqRespServer req resp m a = ReqRespServer {
 reqRespServerPeer
   :: Monad m
   => ReqRespServer req resp m a
-  -> Server (ReqResp req resp) NonPipelined Z StIdle m a
+  -> Server (ReqResp req resp) NonPipelined StIdle m a
 reqRespServerPeer ReqRespServer{..} =
 
     -- In the 'StIdle' the server is awaiting a request message

typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Client.hs

@@ -18,14 +18,14 @@ import           Network.TypedProtocol.Peer.Client
 reqResp2Client :: forall req resp m.
                   ()
                => [Either req req]
-               -> Client (ReqResp2 req resp) (Pipelined (Either resp resp)) Z StIdle m [Either resp resp]
+               -> Client (ReqResp2 req resp) (Pipelined Z (Either resp resp)) StIdle m [Either resp resp]
 reqResp2Client = send Zero
   where
     -- pipeline all the requests, either through `MsgReq` or `MsgReq'`.
     send :: forall (n :: N).
             Nat n
          -> [Either req req] -- requests to send
-         -> Client (ReqResp2 req resp) (Pipelined (Either resp resp))  n StIdle m [Either resp resp]
+         -> Client (ReqResp2 req resp) (Pipelined  n (Either resp resp)) StIdle m [Either resp resp]
 
     send !n (Left req : reqs) =
       YieldPipelined (MsgReq  req) receiver (send (Succ n) reqs)
@@ -47,7 +47,7 @@ reqResp2Client = send Zero
     -- collect all the responses
     collect :: Nat n
             -> [Either resp resp] -- all the responses received so far
-            -> Client (ReqResp2 req resp) (Pipelined (Either resp resp)) n StIdle m [Either resp resp]
+            -> Client (ReqResp2 req resp) (Pipelined n (Either resp resp)) StIdle m [Either resp resp]
 
     collect Zero !resps = Yield MsgDone (Done (reverse resps))
 

typed-protocols-examples/src/Network/TypedProtocol/Trans/Wedge.hs

@@ -109,7 +109,7 @@ type PingPong2 = Wedge PingPong.PingPong PingPong.StIdle
                        PingPong.PingPong PingPong.StIdle
 
 
-pingPong2Client :: Client.Client PingPong2 NonPipelined Client.Z StIdle m ()
+pingPong2Client :: Client.Client PingPong2 NonPipelined StIdle m ()
 pingPong2Client =
     Client.Yield (MsgStart AtFst)
   $ Client.Yield (MsgFst PingPong.MsgPing)
@@ -122,7 +122,7 @@ pingPong2Client =
   $ Client.Done ()
 
 
-pingPong2Client' :: forall m. Client.Client PingPong2 (Pipelined ()) Client.Z StIdle m ()
+pingPong2Client' :: forall m. Client.Client PingPong2 (Pipelined Client.Z ()) StIdle m ()
 pingPong2Client' =
     --
     -- Pipeline first protocol

typed-protocols-examples/test/Network/TypedProtocol/ReqResp/Tests.hs

@@ -112,7 +112,7 @@ directPipelined (ReqRespClientPipelined client0) server0 =
   where
     go :: forall n.
           Queue n c
-       -> ReqRespIdle   req resp c n m a
+       -> ReqRespIdle   req resp n c m a
        -> ReqRespServer req resp     m b
        -> m (a, b)
     go EmptyQ (SendMsgDonePipelined clientResult) ReqRespServer{recvMsgDone} =

typed-protocols/src/Network/TypedProtocol/Core.hs

@@ -41,6 +41,8 @@ module Network.TypedProtocol.Core
   , NobodyHasAgencyProof
   , FlipAgency
   , IsPipelined (..)
+  , Outstanding
+  , N (..)
   , ActiveAgency
   , ActiveAgency' (..)
   , IsActiveState (..)
@@ -478,13 +480,27 @@ type family FlipAgency pr where
   FlipAgency AsServer = AsClient
 
 
+-- | A type level inductive natural number.
+data N = Z | S N
+
 -- | Promoted data type which indicates if 'Peer' is used in
 -- pipelined mode or not.
 --
 data IsPipelined where
     -- | Pipelined peer which is using `c :: Type` for collecting responses
     -- from a pipelined messages.
-    Pipelined    :: Type -> IsPipelined
+    Pipelined    :: N -> Type -> IsPipelined
 
     -- | Non-pipelined peer.
     NonPipelined :: IsPipelined
+
+-- | Type level count of the number of outstanding pipelined yields for which
+-- we have not yet collected a receiver result. Used in 'PeerSender' to ensure
+-- 'SenderCollect' is only used when there are outstanding results to collect,
+-- and to ensure 'SenderYield', 'SenderAwait' and 'SenderDone' are only used
+-- when there are none.
+--
+type        Outstanding :: IsPipelined -> N
+type family Outstanding pl where
+  Outstanding 'NonPipelined    = Z
+  Outstanding ('Pipelined n _) = n