typed-protocols: new interface

cabal.project

@@ -1,4 +1,4 @@
-index-state: 2021-02-15T00:00:00Z
+index-state: 2021-03-15T00:00:00Z
 
 packages: ./typed-protocols
           ./typed-protocols-cborg

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

@@ -22,6 +22,7 @@ import qualified Data.ByteString.Builder.Extra as BS
 import qualified Data.ByteString as BS
 import qualified Data.ByteString.Lazy as LBS
 import qualified Data.ByteString.Lazy.Internal as LBS (smallChunkSize)
+import           Data.Singletons
 
 import           Network.TypedProtocol.Core
 import           Network.TypedProtocol.Codec
@@ -44,19 +45,19 @@ type DeserialiseFailure = CBOR.DeserialiseFailure
 mkCodecCborStrictBS
   :: forall ps m. MonadST m
 
-  => (forall (pr :: PeerRole) (st :: ps) (st' :: ps).
-             PeerHasAgency pr st
-          -> Message ps st st' -> CBOR.Encoding)
+  => (forall (st :: ps) (st' :: ps).
+             SingI st
+          => Message ps st st' -> CBOR.Encoding)
 
-  -> (forall (pr :: PeerRole) (st :: ps) s.
-             PeerHasAgency pr st
-          -> CBOR.Decoder s (SomeMessage st))
+  -> (forall (st :: ps) s.
+             SingI st
+          => CBOR.Decoder s (SomeMessage st))
 
   -> Codec ps DeserialiseFailure m BS.ByteString
 mkCodecCborStrictBS cborMsgEncode cborMsgDecode =
     Codec {
-      encode = \stok msg -> convertCborEncoder (cborMsgEncode stok) msg,
-      decode = \stok     -> convertCborDecoder (cborMsgDecode stok)
+      encode = \msg -> convertCborEncoder cborMsgEncode msg,
+      decode =         convertCborDecoder cborMsgDecode
     }
   where
     convertCborEncoder :: (a -> CBOR.Encoding) -> a -> BS.ByteString
@@ -98,19 +99,19 @@ convertCborDecoderBS cborDecode liftST =
 mkCodecCborLazyBS
   :: forall ps m. MonadST m
 
-  => (forall (pr :: PeerRole) (st :: ps) (st' :: ps).
-             PeerHasAgency pr st
-          -> Message ps st st' -> CBOR.Encoding)
+  => (forall (st :: ps) (st' :: ps).
+             SingI st
+          => Message ps st st' -> CBOR.Encoding)
 
-  -> (forall (pr :: PeerRole) (st :: ps) s.
-             PeerHasAgency pr st
-          -> CBOR.Decoder s (SomeMessage st))
+  -> (forall (st :: ps) s.
+             SingI st
+          => CBOR.Decoder s (SomeMessage st))
 
   -> Codec ps CBOR.DeserialiseFailure m LBS.ByteString
 mkCodecCborLazyBS  cborMsgEncode cborMsgDecode =
     Codec {
-      encode = \stok msg -> convertCborEncoder (cborMsgEncode stok) msg,
-      decode = \stok     -> convertCborDecoder (cborMsgDecode stok)
+      encode = \msg -> convertCborEncoder cborMsgEncode msg,
+      decode =         convertCborDecoder cborMsgDecode
     }
   where
     convertCborEncoder :: (a -> CBOR.Encoding) -> a -> LBS.ByteString

typed-protocols-cborg/typed-protocols-cborg.cabal

@@ -23,6 +23,7 @@ library
   build-depends:     base            >=4.12  && <4.15,
                      bytestring      >=0.10  && <0.11,
                      cborg           >=0.2.1 && <0.3,
+                     singletons,       
 
                      io-classes,
                      typed-protocols

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

@@ -35,6 +35,8 @@ module Network.TypedProtocol.Driver.Simple (
   runDecoderWithChannel,
   ) where
 
+import Data.Singletons
+
 import Network.TypedProtocol.Core
 import Network.TypedProtocol.Pipelined
 import Network.TypedProtocol.Driver
@@ -83,29 +85,35 @@ instance Show (AnyMessage ps) => Show (TraceSendRecv ps) where
   show (TraceRecvMsg msg) = "Recv " ++ show msg
 
 
-driverSimple :: forall ps failure bytes m.
+driverSimple :: forall ps (pr :: PeerRole) failure bytes m.
                 (MonadThrow m, Exception failure)
              => Tracer m (TraceSendRecv ps)
              -> Codec ps failure m bytes
              -> Channel m bytes
-             -> Driver ps (Maybe bytes) m
+             -> Driver ps pr (Maybe bytes) m
 driverSimple tracer Codec{encode, decode} channel@Channel{send} =
     Driver { sendMessage, recvMessage, startDState = Nothing }
   where
-    sendMessage :: forall (pr :: PeerRole) (st :: ps) (st' :: ps).
-                   PeerHasAgency pr st
+    sendMessage :: forall (st :: ps) (st' :: ps).
+                   SingI st
+                => (RelativeAgencyEq (StateAgency st)
+                                      WeHaveAgency
+                                     (Relative pr (StateAgency st)))
                 -> Message ps st st'
                 -> m ()
-    sendMessage stok msg = do
-      send (encode stok msg)
+    sendMessage _ msg = do
+      send (encode msg)
       traceWith tracer (TraceSendMsg (AnyMessage msg))
 
-    recvMessage :: forall (pr :: PeerRole) (st :: ps).
-                   PeerHasAgency pr st
+    recvMessage :: forall (st :: ps).
+                   SingI st
+                => (RelativeAgencyEq (StateAgency st)
+                                      TheyHaveAgency
+                                     (Relative pr (StateAgency st)))
                 -> Maybe bytes
                 -> m (SomeMessage st, Maybe bytes)
-    recvMessage stok trailing = do
-      decoder <- decode stok
+    recvMessage _ trailing = do
+      decoder <- decode
       result  <- runDecoderWithChannel channel trailing decoder
       case result of
         Right x@(SomeMessage msg, _trailing') -> do

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

@@ -57,17 +57,17 @@ pingPongClientPeer (SendMsgDone result) =
     -- We do an actual transition using 'yield', to go from the 'StIdle' to
     -- 'StDone' state. Once in the 'StDone' state we can actually stop using
     -- 'done', with a return value.
-    Yield (ClientAgency TokIdle) MsgDone (Done TokDone result)
+    Yield ReflClientAgency MsgDone (Done ReflNobodyAgency result)
 
 pingPongClientPeer (SendMsgPing next) =
 
     -- Send our message.
-    Yield (ClientAgency TokIdle) MsgPing $
+    Yield ReflClientAgency MsgPing $
 
     -- The type of our protocol means that we're now into the 'StBusy' state
     -- and the only thing we can do next is local effects or wait for a reply.
     -- We'll wait for a reply.
-    Await (ServerAgency TokBusy) $ \MsgPong ->
+    Await ReflServerAgency $ \MsgPong ->
 
     -- Now in this case there is only one possible response, and we have
     -- one corresponding continuation 'kPong' to handle that response.
@@ -150,18 +150,18 @@ pingPongClientPeerSender
 pingPongClientPeerSender (SendMsgDonePipelined result) =
   -- Send `MsgDone` and complete the protocol
   SenderYield
-    (ClientAgency TokIdle)
+    ReflClientAgency
     MsgDone
-    (SenderDone TokDone result)
+    (SenderDone ReflNobodyAgency result)
 
 pingPongClientPeerSender (SendMsgPingPipelined receive next) =
   -- Pipelined yield: send `MsgPing`, immediately follow with the next step.
   -- Await for a response in a continuation.
   SenderPipeline
-    (ClientAgency TokIdle)
+    ReflClientAgency
     MsgPing
     -- response handler
-    (ReceiverAwait (ServerAgency TokBusy) $ \MsgPong ->
+    (ReceiverAwait ReflServerAgency $ \MsgPong ->
         ReceiverEffect $ do
           x <- receive
           return (ReceiverDone x))

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

@@ -6,6 +6,8 @@
 
 module Network.TypedProtocol.PingPong.Codec where
 
+import           Data.Singletons
+
 import           Network.TypedProtocol.Codec
 import           Network.TypedProtocol.PingPong.Type
 
@@ -16,28 +18,25 @@ codecPingPong
 codecPingPong =
     Codec{encode, decode}
   where
-    encode :: forall pr (st :: PingPong) (st' :: PingPong)
-           .  PeerHasAgency pr st
-           -> Message PingPong st st'
+    encode :: forall (st :: PingPong) (st' :: PingPong).
+              Message PingPong st st'
            -> String
-    encode (ClientAgency TokIdle) MsgPing = "ping\n"
-    encode (ClientAgency TokIdle) MsgDone = "done\n"
-    encode (ServerAgency TokBusy) MsgPong = "pong\n"
-
-    decode :: forall pr (st :: PingPong)
-           .  PeerHasAgency pr st
-           -> m (DecodeStep String CodecFailure m (SomeMessage st))
-    decode stok =
+    encode MsgPing = "ping\n"
+    encode MsgDone = "done\n"
+    encode MsgPong = "pong\n"
+
+    decode :: forall (st :: PingPong).
+              SingI st
+           => m (DecodeStep String CodecFailure m (SomeMessage st))
+    decode =
       decodeTerminatedFrame '\n' $ \str trailing ->
-        case (stok, str) of
-          (ServerAgency TokBusy, "pong") -> DecodeDone (SomeMessage MsgPong) trailing
-          (ClientAgency TokIdle, "ping") -> DecodeDone (SomeMessage MsgPing) trailing
-          (ClientAgency TokIdle, "done") -> DecodeDone (SomeMessage MsgDone) trailing
+        case (sing :: Sing st, str) of
+          (SingBusy, "pong") -> DecodeDone (SomeMessage MsgPong) trailing
+          (SingIdle, "ping") -> DecodeDone (SomeMessage MsgPing) trailing
+          (SingIdle, "done") -> DecodeDone (SomeMessage MsgDone) trailing
 
-          (ServerAgency _      , _     ) -> DecodeFail failure
+          (_       , _     ) -> DecodeFail failure
             where failure = CodecFailure ("unexpected server message: " ++ str)
-          (ClientAgency _      , _     ) -> DecodeFail failure
-            where failure = CodecFailure ("unexpected client message: " ++ str)
 
 
 decodeTerminatedFrame :: forall m a.

typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec/CBOR.hs

@@ -9,6 +9,7 @@ module Network.TypedProtocol.PingPong.Codec.CBOR where
 import           Control.Monad.Class.MonadST
 
 import           Data.ByteString.Lazy (ByteString)
+import           Data.Singletons
 
 import qualified Codec.CBOR.Encoding as CBOR (Encoding, encodeWord)
 import qualified Codec.CBOR.Read     as CBOR
@@ -25,26 +26,26 @@ codecPingPong
   => Codec PingPong CBOR.DeserialiseFailure m ByteString
 codecPingPong = mkCodecCborLazyBS encodeMsg decodeMsg
  where
-  encodeMsg :: forall (pr :: PeerRole) st st'.
-               PeerHasAgency pr st
-            -> Message PingPong st st'
+  encodeMsg :: forall st st'.
+               Message PingPong st st'
             -> CBOR.Encoding
-  encodeMsg (ClientAgency TokIdle) MsgPing = CBOR.encodeWord 0
-  encodeMsg (ServerAgency TokBusy) MsgPong = CBOR.encodeWord 1
-  encodeMsg (ClientAgency TokIdle) MsgDone = CBOR.encodeWord 2
-
-  decodeMsg :: forall (pr :: PeerRole) s (st :: PingPong).
-               PeerHasAgency pr st
-            -> CBOR.Decoder s (SomeMessage st)
-  decodeMsg stok = do
+  encodeMsg MsgPing = CBOR.encodeWord 0
+  encodeMsg MsgPong = CBOR.encodeWord 1
+  encodeMsg MsgDone = CBOR.encodeWord 2
+
+  decodeMsg :: forall s (st :: PingPong).
+               SingI st
+            => CBOR.Decoder s (SomeMessage st)
+  decodeMsg = do
     key <- CBOR.decodeWord
-    case (stok, key) of
-      (ClientAgency TokIdle, 0) -> return $ SomeMessage MsgPing
-      (ServerAgency TokBusy, 1) -> return $ SomeMessage MsgPong
-      (ClientAgency TokIdle, 2) -> return $ SomeMessage MsgDone
+    case (sing :: Sing st, key) of
+      (SingIdle, 0) -> return $ SomeMessage MsgPing
+      (SingBusy, 1) -> return $ SomeMessage MsgPong
+      (SingIdle, 2) -> return $ SomeMessage MsgDone
 
       -- TODO proper exceptions
-      (ClientAgency TokIdle, _) -> fail "codecPingPong.StIdle: unexpected key"
-      (ServerAgency TokBusy, _) -> fail "codecPingPong.StBusy: unexpected key"
+      (SingIdle, _) -> fail "codecPingPong.StIdle: unexpected key"
+      (SingBusy, _) -> fail "codecPingPong.StBusy: unexpected key"
+      (SingDone, _) -> fail "codecPingPong.StDone: unexpected key"
 
 

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

@@ -29,18 +29,18 @@ pingPongServerPeer
 pingPongServerPeer PingPongServer{..} =
 
     -- In the 'StIdle' the server is awaiting a request message
-    Await (ClientAgency TokIdle) $ \req ->
+    Await ReflClientAgency $ \req ->
 
     -- The client got to choose between two messages and we have to handle
     -- either of them
     case req of
 
       -- The client sent the done transition, so we're in the 'StDone' state
       -- so all we can do is stop using 'done', with a return value.
-      MsgDone -> Done TokDone recvMsgDone
+      MsgDone -> Done ReflNobodyAgency recvMsgDone
 
       -- The client sent us a ping request, so now we're in the 'StBusy' state
       -- which means it's the server's turn to send.
       MsgPing -> Effect $ do
         next <- recvMsgPing
-        pure $ Yield (ServerAgency TokBusy) MsgPong (pingPongServerPeer next)
+        pure $ Yield ReflServerAgency MsgPong (pingPongServerPeer next)

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

@@ -8,6 +8,8 @@
 
 module Network.TypedProtocol.PingPong.Type where
 
+import           Data.Singletons
+
 import           Network.TypedProtocol.Core
 
 
@@ -35,6 +37,22 @@ data PingPong where
   StBusy :: PingPong
   StDone :: PingPong
 
+data SPingPong (st :: PingPong) where
+  SingIdle :: SPingPong StIdle
+  SingBusy :: SPingPong StBusy
+  SingDone :: SPingPong StDone
+
+deriving instance Show (SPingPong st)
+
+type instance Sing = SPingPong
+instance SingI StIdle where
+    sing = SingIdle
+instance SingI StBusy where
+    sing = SingBusy
+instance SingI StDone where
+    sing = SingDone
+
+
 instance Protocol PingPong where
 
   -- | The actual messages in our protocol.
@@ -54,33 +72,9 @@ instance Protocol PingPong where
     MsgPong :: Message PingPong StBusy StIdle
     MsgDone :: Message PingPong StIdle StDone
 
-  -- | We have to explain to the framework what our states mean, in terms of
-  -- who is expected to send and receive in the different states.
-  --
-  -- Idle states are where it is for the client to send a message.
-  --
-  data ClientHasAgency st where
-    TokIdle :: ClientHasAgency StIdle
-
-  -- | Busy states are where the server is expected to send a reply (a pong).
-  --
-  data ServerHasAgency st where
-    TokBusy :: ServerHasAgency StBusy
-
-  -- | In the done state neither client nor server can send messages.
-  --
-  data NobodyHasAgency st where
-    TokDone :: NobodyHasAgency StDone
-
-  exclusionLemma_ClientAndServerHaveAgency TokIdle tok = case tok of {}
-  exclusionLemma_NobodyAndClientHaveAgency TokDone tok = case tok of {}
-  exclusionLemma_NobodyAndServerHaveAgency TokDone tok = case tok of {}
+  type StateAgency StIdle = ClientAgency
+  type StateAgency StBusy = ServerAgency
+  type StateAgency StDone = NobodyAgency
 
 
 deriving instance Show (Message PingPong from to)
-
-instance Show (ClientHasAgency (st :: PingPong)) where
-  show TokIdle = "TokIdle"
-
-instance Show (ServerHasAgency (st :: PingPong)) where
-  show TokBusy = "TokBusy"