diff --git a/.github/workflows/haskell.yml b/.github/workflows/haskell.yml index 5d0cfc73..7d43e42f 100644 --- a/.github/workflows/haskell.yml +++ b/.github/workflows/haskell.yml @@ -93,8 +93,8 @@ jobs: - name: typed-protocols-examples [test] run: cabal run typed-protocols-examples:test - - name: typed-protocols-doc [test] - run: cabal test typed-protocols-doc + # - name: typed-protocols-doc [test] + # run: cabal test typed-protocols-doc stylish-haskell: runs-on: ubuntu-22.04 diff --git a/cabal.project b/cabal.project index 5c9b7552..aec676d4 100644 --- a/cabal.project +++ b/cabal.project @@ -12,11 +12,13 @@ repository cardano-haskell-packages index-state: hackage.haskell.org 2024-08-27T18:06:30Z - , cardano-haskell-packages 2024-06-27T10:53:24Z + , cardano-haskell-packages 2024-07-24T14:16:32Z packages: ./typed-protocols ./typed-protocols-cborg + ./typed-protocols-stateful + ./typed-protocols-stateful-cborg ./typed-protocols-examples - ./typed-protocols-doc + -- ./typed-protocols-doc test-show-details: direct diff --git a/scripts/check-stylish.sh b/scripts/check-stylish.sh index 43ef543a..a90a801e 100755 --- a/scripts/check-stylish.sh +++ b/scripts/check-stylish.sh @@ -5,6 +5,6 @@ export LC_ALL=C.UTF-8 [[ -x '/usr/bin/fd' ]] && FD="fd" || FD="fdfind" -$FD . './typed-protocols' -e hs -E Setup.hs -X stylish-haskell -c .stylish-haskell.yaml -i +$FD . './typed-protocols' -e hs -E Setup.hs -E Core.hs -X stylish-haskell -c .stylish-haskell.yaml -i $FD . './typed-protocols-cborg' -e hs -E Setup.hs -X stylish-haskell -c .stylish-haskell.yaml -i -$FD . './typed-protocols-examples' -e hs -E Setup.hs -X stylish-haskell -c .stylish-haskell.yaml -i +$FD . './typed-protocols-examples' -e hs -E Setup.hs -E Channel.hs -X stylish-haskell -c .stylish-haskell.yaml -i diff --git a/typed-protocols-cborg/src/Network/TypedProtocol/Codec/CBOR.hs b/typed-protocols-cborg/src/Network/TypedProtocol/Codec/CBOR.hs index bb2183a5..990960e2 100644 --- a/typed-protocols-cborg/src/Network/TypedProtocol/Codec/CBOR.hs +++ b/typed-protocols-cborg/src/Network/TypedProtocol/Codec/CBOR.hs @@ -1,13 +1,19 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MonoLocalBinds #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} module Network.TypedProtocol.Codec.CBOR ( module Network.TypedProtocol.Codec - , DeserialiseFailure , mkCodecCborLazyBS , mkCodecCborStrictBS + , convertCborDecoderBS + , convertCborDecoderLBS + -- * Re-exports + , CBOR.DeserialiseFailure (..) ) where import Control.Monad.Class.MonadST (MonadST (..)) @@ -27,8 +33,6 @@ import Network.TypedProtocol.Codec import Network.TypedProtocol.Core -type DeserialiseFailure = CBOR.DeserialiseFailure - -- | Construct a 'Codec' for a CBOR based serialisation format, using strict -- 'BS.ByteString's. -- @@ -44,19 +48,23 @@ 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). + StateTokenI st + => ActiveState st + => Message ps st st' -> CBOR.Encoding) + -- ^ cbor encoder - -> (forall (pr :: PeerRole) (st :: ps) s. - PeerHasAgency pr st + -> (forall (st :: ps) s. + ActiveState st + => StateToken st -> CBOR.Decoder s (SomeMessage st)) + -- ^ cbor decoder - -> Codec ps DeserialiseFailure m BS.ByteString + -> Codec ps CBOR.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 = \stok -> convertCborDecoder (cborMsgDecode stok) } where convertCborEncoder :: (a -> CBOR.Encoding) -> a -> BS.ByteString @@ -66,20 +74,22 @@ mkCodecCborStrictBS cborMsgEncode cborMsgDecode = convertCborDecoder :: (forall s. CBOR.Decoder s a) - -> m (DecodeStep BS.ByteString DeserialiseFailure m a) + -> m (DecodeStep BS.ByteString CBOR.DeserialiseFailure m a) convertCborDecoder cborDecode = convertCborDecoderBS cborDecode stToIO convertCborDecoderBS :: forall s m a. Functor m - => (CBOR.Decoder s a) + => CBOR.Decoder s a + -- ^ cbor decoder -> (forall b. ST s b -> m b) - -> m (DecodeStep BS.ByteString DeserialiseFailure m a) + -- ^ lift ST computation (e.g. 'Control.Monad.ST.stToIO', 'stToPrim', etc) + -> m (DecodeStep BS.ByteString CBOR.DeserialiseFailure m a) convertCborDecoderBS cborDecode liftST = go <$> liftST (CBOR.deserialiseIncremental cborDecode) where go :: CBOR.IDecode s a - -> DecodeStep BS.ByteString DeserialiseFailure m a + -> DecodeStep BS.ByteString CBOR.DeserialiseFailure m a go (CBOR.Done trailing _ x) | BS.null trailing = DecodeDone x Nothing | otherwise = DecodeDone x (Just trailing) @@ -98,19 +108,23 @@ 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). + StateTokenI st + => ActiveState st + => Message ps st st' -> CBOR.Encoding) + -- ^ cbor encoder - -> (forall (pr :: PeerRole) (st :: ps) s. - PeerHasAgency pr st + -> (forall (st :: ps) s. + ActiveState st + => StateToken st -> CBOR.Decoder s (SomeMessage st)) + -- ^ cbor decoder -> 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 = \stok -> convertCborDecoder (cborMsgDecode stok) } where convertCborEncoder :: (a -> CBOR.Encoding) -> a -> LBS.ByteString @@ -127,8 +141,10 @@ mkCodecCborLazyBS cborMsgEncode cborMsgDecode = convertCborDecoderLBS :: forall s m a. Monad m - => (CBOR.Decoder s a) + => CBOR.Decoder s a + -- ^ cbor decoder -> (forall b. ST s b -> m b) + -- ^ lift ST computation (e.g. 'Control.Monad.ST.stToIO', 'stToPrim', etc) -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m a) convertCborDecoderLBS cborDecode liftST = go [] =<< liftST (CBOR.deserialiseIncremental cborDecode) @@ -148,7 +164,7 @@ convertCborDecoderLBS cborDecode liftST = -- We keep a bunch of chunks and supply the CBOR decoder with them -- until we run out, when we go get another bunch. go (c:cs) (CBOR.Partial k) = go cs =<< liftST (k (Just c)) - go [] (CBOR.Partial k) = return $ DecodePartial $ \mbs -> case mbs of + go [] (CBOR.Partial k) = return $ DecodePartial $ \case Nothing -> go [] =<< liftST (k Nothing) Just bs -> go cs (CBOR.Partial k) where cs = LBS.toChunks bs diff --git a/typed-protocols-cborg/typed-protocols-cborg.cabal b/typed-protocols-cborg/typed-protocols-cborg.cabal index e770a0e0..cda8d8ad 100644 --- a/typed-protocols-cborg/typed-protocols-cborg.cabal +++ b/typed-protocols-cborg/typed-protocols-cborg.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: typed-protocols-cborg -version: 0.1.0.4 +version: 0.2.0.0 synopsis: CBOR codecs for typed-protocols -- description: license: Apache-2.0 @@ -21,6 +21,7 @@ library build-depends: base >=4.12 && <4.21, bytestring >=0.10 && <0.13, cborg >=0.2.1 && <0.3, + singletons, io-classes ^>=1.5, typed-protocols diff --git a/typed-protocols-examples/src/Network/TypedProtocol/Channel.hs b/typed-protocols-examples/src/Network/TypedProtocol/Channel.hs index 6330fbdf..3333928a 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/Channel.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/Channel.hs @@ -1,7 +1,9 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} module Network.TypedProtocol.Channel ( Channel (..) @@ -10,8 +12,12 @@ module Network.TypedProtocol.Channel , fixedInputChannel , mvarsAsChannel , handlesAsChannel +#if !defined(mingw32_HOST_OS) + , socketAsChannel +#endif , createConnectedChannels , createConnectedBufferedChannels + , createConnectedBufferedChannelsUnbounded , createPipelineTestChannels , channelEffect , delayChannel @@ -25,8 +31,14 @@ import Control.Monad.Class.MonadTimer.SI import qualified Data.ByteString as BS import qualified Data.ByteString.Lazy as LBS import Data.ByteString.Lazy.Internal (smallChunkSize) +import Data.Proxy import Numeric.Natural +#if !defined(mingw32_HOST_OS) +import Network.Socket (Socket) +import qualified Network.Socket.ByteString.Lazy as Socket +#endif + import qualified System.IO as IO (Handle, hFlush, hIsEOF) @@ -119,12 +131,20 @@ mvarsAsChannel bufferRead bufferWrite = -- -- This is primarily useful for testing protocols. -- -createConnectedChannels :: MonadSTM m => m (Channel m a, Channel m a) +createConnectedChannels :: forall m a. (MonadLabelledSTM m, MonadTraceSTM m, Show a) => m (Channel m a, Channel m a) createConnectedChannels = do -- Create two TMVars to act as the channel buffer (one for each direction) -- and use them to make both ends of a bidirectional channel - bufferA <- atomically $ newEmptyTMVar - bufferB <- atomically $ newEmptyTMVar + bufferA <- atomically $ do + v <- newEmptyTMVar + labelTMVar v "buffer-a" + traceTMVar (Proxy @m) v $ \_ a -> pure $ TraceString ("buffer-a: " ++ show a) + return v + bufferB <- atomically $ do + v <- newEmptyTMVar + traceTMVar (Proxy @m) v $ \_ a -> pure $ TraceString ("buffer-b: " ++ show a) + labelTMVar v "buffer-b" + return v return (mvarsAsChannel bufferB bufferA, mvarsAsChannel bufferA bufferB) @@ -156,11 +176,32 @@ createConnectedBufferedChannels sz = do recv = atomically (Just <$> readTBQueue bufferRead) +-- | Create a pair of channels that are connected via two unbounded buffers. +-- +-- This is primarily useful for testing protocols. +-- +createConnectedBufferedChannelsUnbounded :: forall m a. MonadSTM m + => m (Channel m a, Channel m a) +createConnectedBufferedChannelsUnbounded = do + -- Create two TQueues to act as the channel buffers (one for each + -- direction) and use them to make both ends of a bidirectional channel + bufferA <- newTQueueIO + bufferB <- newTQueueIO + + return (queuesAsChannel bufferB bufferA, + queuesAsChannel bufferA bufferB) + where + queuesAsChannel bufferRead bufferWrite = + Channel{send, recv} + where + send x = atomically (writeTQueue bufferWrite x) + recv = atomically ( Just <$> readTQueue bufferRead) + -- | Create a pair of channels that are connected via N-place buffers. -- -- This variant /fails/ when 'send' would exceed the maximum buffer size. --- Use this variant when you want the 'PeerPipelined' to limit the pipelining --- itself, and you want to check that it does not exceed the expected level of +-- Use this variant when you want the 'Peer' to limit the pipelining itself, +-- and you want to check that it does not exceed the expected level of -- pipelining. -- -- This is primarily useful for testing protocols. @@ -194,7 +235,8 @@ createPipelineTestChannels sz = do -- -- The Handles should be open in the appropriate read or write mode, and in -- binary mode. Writes are flushed after each write, so it is safe to use --- a buffering mode. +-- a buffering mode. On unix named pipes can be used, see +-- 'Network.TypedProtocol.ReqResp.Test.prop_namedPipePipelined_IO' -- -- For bidirectional handles it is safe to pass the same handle for both. -- @@ -251,6 +293,23 @@ delayChannel delay = channelEffect (\_ -> return ()) (\_ -> threadDelay delay) +#if !defined(mingw32_HOST_OS) +socketAsChannel :: Socket + -> Channel IO LBS.ByteString +socketAsChannel sock = + Channel{send, recv} + where + send :: LBS.ByteString -> IO () + send = Socket.sendAll sock + + recv :: IO (Maybe LBS.ByteString) + recv = do + bs <- Socket.recv sock (fromIntegral smallChunkSize) + if LBS.null bs + then return Nothing + else return (Just bs) +#endif + -- | Channel which logs sent and received messages. -- loggingChannel :: ( MonadSay m diff --git a/typed-protocols-examples/src/Network/TypedProtocol/Driver/Simple.hs b/typed-protocols-examples/src/Network/TypedProtocol/Driver/Simple.hs index 5f517bfe..04a4dcfe 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/Driver/Simple.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/Driver/Simple.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} @@ -24,6 +25,7 @@ module Network.TypedProtocol.Driver.Simple -- * Connected peers , runConnectedPeers , runConnectedPeersPipelined + , runConnectedPeersAsymmetric -- * Driver utilities -- | This may be useful if you want to write your own driver. , driverSimple @@ -34,7 +36,7 @@ import Network.TypedProtocol.Channel import Network.TypedProtocol.Codec import Network.TypedProtocol.Core import Network.TypedProtocol.Driver -import Network.TypedProtocol.Pipelined +import Network.TypedProtocol.Peer import Control.Monad.Class.MonadAsync import Control.Monad.Class.MonadThrow @@ -77,29 +79,39 @@ instance Show (AnyMessage ps) => Show (TraceSendRecv ps) where show (TraceRecvMsg msg) = "Recv " ++ show msg -driverSimple :: forall ps failure bytes m. +driverSimple :: forall ps pr 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 } + Driver { sendMessage, recvMessage, initialDState = Nothing } where - sendMessage :: forall (pr :: PeerRole) (st :: ps) (st' :: ps). - PeerHasAgency pr st + sendMessage :: forall (st :: ps) (st' :: ps). + ( StateTokenI st + , ActiveState st + ) + => ReflRelativeAgency (StateAgency st) + WeHaveAgency + (Relative pr (StateAgency st)) -> Message ps st st' -> m () - sendMessage stok msg = do - send (encode stok msg) + sendMessage !_refl msg = do + send (encode msg) traceWith tracer (TraceSendMsg (AnyMessage msg)) - recvMessage :: forall (pr :: PeerRole) (st :: ps). - PeerHasAgency pr st + recvMessage :: forall (st :: ps). + ( StateTokenI st + , ActiveState st + ) + => ReflRelativeAgency (StateAgency st) + TheyHaveAgency + (Relative pr (StateAgency st)) -> Maybe bytes -> m (SomeMessage st, Maybe bytes) - recvMessage stok trailing = do - decoder <- decode stok + recvMessage !_refl trailing = do + decoder <- decode stateToken result <- runDecoderWithChannel channel trailing decoder case result of Right x@(SomeMessage msg, _trailing') -> do @@ -114,15 +126,15 @@ driverSimple tracer Codec{encode, decode} channel@Channel{send} = -- This runs the peer to completion (if the protocol allows for termination). -- runPeer - :: forall ps (st :: ps) pr failure bytes m a . + :: forall ps (st :: ps) pr failure bytes m a. (MonadThrow m, Exception failure) => Tracer m (TraceSendRecv ps) -> Codec ps failure m bytes -> Channel m bytes - -> Peer ps pr st m a - -> m a + -> Peer ps pr 'NonPipelined st m a + -> m (a, Maybe bytes) runPeer tracer codec channel peer = - fst <$> runPeerWithDriver driver peer (startDState driver) + runPeerWithDriver driver peer where driver = driverSimple tracer codec channel @@ -141,9 +153,9 @@ runPipelinedPeer -> Codec ps failure m bytes -> Channel m bytes -> PeerPipelined ps pr st m a - -> m a + -> m (a, Maybe bytes) runPipelinedPeer tracer codec channel peer = - fst <$> runPipelinedPeerWithDriver driver peer (startDState driver) + runPipelinedPeerWithDriver driver peer where driver = driverSimple tracer codec channel @@ -184,15 +196,15 @@ 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 st m a - -> Peer ps (FlipAgency pr) 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) -> - runPeer tracerClient codec clientChannel client + (fst <$> runPeer tracerClient codec clientChannel client) `concurrently` - runPeer tracerServer codec serverChannel server + (fst <$> runPeer tracerServer codec serverChannel server) where tracerClient = contramap ((,) Client) tracer tracerServer = contramap ((,) Server) tracer @@ -202,16 +214,41 @@ runConnectedPeersPipelined :: (MonadAsync m, MonadCatch m, => m (Channel m bytes, Channel m bytes) -> Tracer m (PeerRole, TraceSendRecv ps) -> Codec ps failure m bytes - -> PeerPipelined ps pr st m a - -> Peer ps (FlipAgency pr) st m b + -> PeerPipelined ps pr st m a + -> Peer ps (FlipAgency pr) 'NonPipelined st m b -> m (a, b) runConnectedPeersPipelined createChannels tracer codec client server = createChannels >>= \(clientChannel, serverChannel) -> - runPipelinedPeer tracerClient codec clientChannel client + (fst <$> runPipelinedPeer tracerClient codec clientChannel client) `concurrently` - runPeer tracerServer codec serverChannel server + (fst <$> runPeer tracerServer codec serverChannel server) where tracerClient = contramap ((,) AsClient) tracer tracerServer = contramap ((,) AsServer) tracer + +-- Run the same protocol with different codes. This is useful for testing +-- 'Handshake' protocol which knows how to decode different versions. +-- +runConnectedPeersAsymmetric + :: ( MonadAsync m + , MonadMask m + , Exception failure + ) + => m (Channel m bytes, Channel m bytes) + -> Tracer m (Role, TraceSendRecv ps) + -> Codec ps failure m bytes + -> Codec ps failure m bytes + -> PeerPipelined ps pr st m a + -> Peer ps (FlipAgency pr) 'NonPipelined st m b + -> m (a, b) +runConnectedPeersAsymmetric createChannels tracer codec codec' client server = + createChannels >>= \(clientChannel, serverChannel) -> + + (fst <$> runPipelinedPeer tracerClient codec clientChannel client) + `concurrently` + (fst <$> runPeer tracerServer codec' serverChannel server) + where + tracerClient = contramap ((,) Client) tracer + tracerServer = contramap ((,) Server) tracer diff --git a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Client.hs b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Client.hs index f60be974..b6398428 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Client.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Client.hs @@ -1,5 +1,8 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} module Network.TypedProtocol.PingPong.Client ( -- * Normal client @@ -7,13 +10,13 @@ module Network.TypedProtocol.PingPong.Client , pingPongClientPeer -- * Pipelined client , PingPongClientPipelined (..) - , PingPongSender (..) + , PingPongClientIdle (..) , pingPongClientPeerPipelined ) where import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Client import Network.TypedProtocol.PingPong.Type -import Network.TypedProtocol.Pipelined -- | A ping-pong client, on top of some effect 'm'. -- @@ -49,33 +52,31 @@ data PingPongClient m a where -- 'PingPong' protocol. -- pingPongClientPeer - :: Monad m + :: Functor m => PingPongClient m a - -> Peer PingPong AsClient 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 -- '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 MsgDone (Done result) pingPongClientPeer (SendMsgPing next) = -- Send our message. - Yield (ClientAgency TokIdle) MsgPing $ + Yield 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 $ \MsgPong -> -- Now in this case there is only one possible response, and we have -- one corresponding continuation 'kPong' to handle that response. -- The pong reply has no content so there's nothing to pass to our -- continuation, but if there were we would. - Effect $ do - client <- next - pure $ pingPongClientPeer client + Effect $ pingPongClientPeer <$> next -- @@ -85,30 +86,31 @@ pingPongClientPeer (SendMsgPing next) = -- | A ping-pong client designed for running the 'PingPong' protocol in -- a pipelined way. -- -data PingPongClientPipelined m a where +data PingPongClientPipelined c m a where -- | A 'PingPongSender', but starting with zero outstanding pipelined -- responses, and for any internal collect type @c@. PingPongClientPipelined :: - PingPongSender Z c m a - -> PingPongClientPipelined m a + PingPongClientIdle Z c m a + -> PingPongClientPipelined c m a -data PingPongSender n c m a where - -- | - -- Send a `Ping` message but alike in `PingPongClient` do not await for the - -- resopnse, instead supply a monadic action which will run on a received +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. + -- SendMsgPingPipelined - :: m c -- pong receive action - -> PingPongSender (S n) c m a -- continuation - -> PingPongSender n c m a + :: m c + -> PingPongClientIdle (S n) c m a -- continuation + -> PingPongClientIdle n c m a -- | Collect the result of a previous pipelined receive action. -- -- This (optionally) provides two choices: -- -- * Continue without a pipelined result - -- * Continue with a pipelined result + -- * Continue with a pipelined result, which allows to run a monadic action + -- when 'MsgPong' is received. -- -- Since presenting the first choice is optional, this allows expressing -- both a blocking collect and a non-blocking collect. This allows @@ -118,58 +120,55 @@ data PingPongSender n c m a where -- eagerly. -- CollectPipelined - :: Maybe (PingPongSender (S n) c m a) - -> (c -> PingPongSender n c m a) - -> PingPongSender (S n) c m a + :: Maybe (PingPongClientIdle (S n) c m a) + -> (c -> (PingPongClientIdle n c m a)) + -> PingPongClientIdle (S n) c m a -- | Termination of the ping-pong protocol. -- -- Note that all pipelined results must be collected before terminating. -- SendMsgDonePipelined - :: a -> PingPongSender Z c m a + :: a -> PingPongClientIdle Z c m a --- | Interpret a pipelined client as a 'PeerPipelined' on the client side of +-- | Interpret a pipelined client as a pipelined 'Peer' on the client side of -- the 'PingPong' protocol. -- pingPongClientPeerPipelined - :: Monad m - => PingPongClientPipelined m a - -> PeerPipelined PingPong AsClient StIdle m a + :: Functor m + => PingPongClientPipelined c m a + -> ClientPipelined PingPong StIdle m a pingPongClientPeerPipelined (PingPongClientPipelined peer) = - PeerPipelined (pingPongClientPeerSender peer) - - -pingPongClientPeerSender - :: Monad m - => PingPongSender n c m a - -> PeerSender PingPong AsClient StIdle n c m a - -pingPongClientPeerSender (SendMsgDonePipelined result) = - -- Send `MsgDone` and complete the protocol - SenderYield - (ClientAgency TokIdle) - MsgDone - (SenderDone TokDone 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) - MsgPing - -- response handler - (ReceiverAwait (ServerAgency TokBusy) $ \MsgPong -> - ReceiverEffect $ do - x <- receive - return (ReceiverDone x)) - -- run the next step of the ping-pong protocol. - (pingPongClientPeerSender next) - -pingPongClientPeerSender (CollectPipelined mNone collect) = - SenderCollect - (fmap pingPongClientPeerSender mNone) - (pingPongClientPeerSender . collect) - + ClientPipelined $ pingPongClientPeerIdle peer + + +pingPongClientPeerIdle + :: 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' :: 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. + YieldPipelined + MsgPing + (ReceiverAwait $ \MsgPong -> + ReceiverEffect $ ReceiverDone <$> receive) + (go next) + + go (CollectPipelined mNone collect) = + Collect + (go <$> mNone) + (go . collect) + + go (SendMsgDonePipelined result) = + -- Send `MsgDone` and complete the protocol + Yield + MsgDone + (Done result) diff --git a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec.hs b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec.hs index 33ad83ca..f825dae7 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE NamedFieldPuns #-} @@ -7,6 +8,7 @@ module Network.TypedProtocol.PingPong.Codec where import Network.TypedProtocol.Codec +import Network.TypedProtocol.Core import Network.TypedProtocol.PingPong.Type @@ -16,28 +18,29 @@ 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" + encode MsgPing = "ping\n" + encode MsgDone = "done\n" + encode MsgPong = "pong\n" - decode :: forall pr (st :: PingPong) - . PeerHasAgency pr st + decode :: forall (st :: PingPong). + ActiveState st + => StateToken st -> m (DecodeStep String CodecFailure m (SomeMessage st)) decode stok = 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 + (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. @@ -66,14 +69,17 @@ codecPingPongId codecPingPongId = Codec{encode,decode} where - encode :: forall pr (st :: PingPong) (st' :: PingPong) - . PeerHasAgency pr st - -> Message PingPong st st' + encode :: forall (st :: PingPong) (st' :: PingPong) + . ( StateTokenI st + , ActiveState st + ) + => Message PingPong st st' -> AnyMessage PingPong - encode _ msg = AnyMessage msg + encode msg = AnyMessage msg - decode :: forall pr (st :: PingPong) - . PeerHasAgency pr st + decode :: forall (st :: PingPong). + ActiveState st + => StateToken st -> m (DecodeStep (AnyMessage PingPong) CodecFailure m (SomeMessage st)) decode stok = pure $ DecodePartial $ \mb -> @@ -81,13 +87,18 @@ codecPingPongId = Nothing -> return $ DecodeFail (CodecFailure "expected more data") Just (AnyMessage msg) -> return $ case (stok, msg) of - (ServerAgency TokBusy, MsgPong) -> + (SingBusy, MsgPong) -> DecodeDone (SomeMessage msg) Nothing - (ClientAgency TokIdle, MsgPing) -> + (SingIdle, MsgPing) -> DecodeDone (SomeMessage msg) Nothing - (ClientAgency TokIdle, MsgDone) -> + (SingIdle, MsgDone) -> DecodeDone (SomeMessage msg) Nothing - (ServerAgency _ , _ ) -> DecodeFail failure - where failure = CodecFailure ("unexpected server message: " ++ show msg) - (ClientAgency _ , _ ) -> DecodeFail failure - where failure = CodecFailure ("unexpected client message: " ++ show msg ) + + (SingIdle, _) -> + DecodeFail failure + where failure = CodecFailure ("unexpected client message: " ++ show msg) + (SingBusy, _) -> + DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ show msg) + + (a@SingDone, _) -> notActiveState a diff --git a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec/CBOR.hs b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec/CBOR.hs index 596bdaae..0d674a3b 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec/CBOR.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Codec/CBOR.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} @@ -25,26 +26,25 @@ 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 + encodeMsg MsgPing = CBOR.encodeWord 0 + encodeMsg MsgPong = CBOR.encodeWord 1 + encodeMsg MsgDone = CBOR.encodeWord 2 - decodeMsg :: forall (pr :: PeerRole) s (st :: PingPong). - PeerHasAgency pr st + decodeMsg :: forall s (st :: PingPong). + ActiveState st + => StateToken st -> CBOR.Decoder s (SomeMessage st) decodeMsg stok = 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 + (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" + (a@SingDone, _) -> notActiveState a diff --git a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Examples.hs b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Examples.hs index 126f5c72..efcc6ea8 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Examples.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Examples.hs @@ -1,14 +1,16 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} module Network.TypedProtocol.PingPong.Examples where import Network.TypedProtocol.PingPong.Client import Network.TypedProtocol.PingPong.Server -import Network.TypedProtocol.Pipelined +import Network.TypedProtocol.Peer.Client -- | The standard stateless ping-pong server instance. @@ -66,12 +68,12 @@ pingPongClientCount n = SendMsgPing (pure (pingPongClientCount (n-1))) pingPongClientPipelinedMax :: forall m. Monad m => Int - -> PingPongClientPipelined m [Either Int Int] + -> PingPongClientPipelined Int m [Either Int Int] pingPongClientPipelinedMax c = PingPongClientPipelined (go [] Zero 0) where go :: [Either Int Int] -> Nat o -> Int - -> PingPongSender o Int m [Either Int Int] + -> PingPongClientIdle o Int m [Either Int Int] go acc o n | n < c = SendMsgPingPipelined (return n) @@ -92,12 +94,12 @@ pingPongClientPipelinedMax c = pingPongClientPipelinedMin :: forall m. Monad m => Int - -> PingPongClientPipelined m [Either Int Int] + -> PingPongClientPipelined Int m [Either Int Int] pingPongClientPipelinedMin c = PingPongClientPipelined (go [] Zero 0) where go :: [Either Int Int] -> Nat o -> Int - -> PingPongSender o Int m [Either Int Int] + -> PingPongClientIdle o Int m [Either Int Int] go acc (Succ o) n = CollectPipelined (if n < c then Just (ping acc (Succ o) n) else Nothing) @@ -107,7 +109,7 @@ pingPongClientPipelinedMin c = go acc Zero _ = SendMsgDonePipelined (reverse acc) ping :: [Either Int Int] -> Nat o -> Int - -> PingPongSender o Int m [Either Int Int] + -> PingPongClientIdle o Int m [Either Int Int] ping acc o n = SendMsgPingPipelined (return n) (go (Left n : acc) (Succ o) (succ n)) @@ -123,12 +125,12 @@ pingPongClientPipelinedMin c = pingPongClientPipelinedLimited :: forall m. Monad m => Int -> Int - -> PingPongClientPipelined m [Either Int Int] + -> PingPongClientPipelined Int m [Either Int Int] pingPongClientPipelinedLimited omax c = PingPongClientPipelined (go [] Zero 0) where go :: [Either Int Int] -> Nat o -> Int - -> PingPongSender o Int m [Either Int Int] + -> PingPongClientIdle o Int m [Either Int Int] go acc (Succ o) n = CollectPipelined (if n < c && int (Succ o) < omax then Just (ping acc (Succ o) n) @@ -139,7 +141,7 @@ pingPongClientPipelinedLimited omax c = go acc Zero _ = SendMsgDonePipelined (reverse acc) ping :: [Either Int Int] -> Nat o -> Int - -> PingPongSender o Int m [Either Int Int] + -> PingPongClientIdle o Int m [Either Int Int] ping acc o n = SendMsgPingPipelined (return n) (go (Left n : acc) (Succ o) (succ n)) diff --git a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Server.hs b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Server.hs index 67ede8eb..768b9621 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Server.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Server.hs @@ -5,6 +5,7 @@ module Network.TypedProtocol.PingPong.Server where import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Server import Network.TypedProtocol.PingPong.Type @@ -25,11 +26,11 @@ data PingPongServer m a = PingPongServer { pingPongServerPeer :: Monad m => PingPongServer m a - -> Peer PingPong AsServer StIdle m a + -> Server PingPong NonPipelined StIdle m a pingPongServerPeer PingPongServer{..} = -- In the 'StIdle' the server is awaiting a request message - Await (ClientAgency TokIdle) $ \req -> + Await $ \req -> -- The client got to choose between two messages and we have to handle -- either of them @@ -37,10 +38,10 @@ pingPongServerPeer PingPongServer{..} = -- 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 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 MsgPong (pingPongServerPeer next) diff --git a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Type.hs b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Type.hs index 128e0f1a..5c8c5534 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Type.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Type.hs @@ -35,6 +35,17 @@ 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) + +instance StateTokenI StIdle where stateToken = SingIdle +instance StateTokenI StBusy where stateToken = SingBusy +instance StateTokenI StDone where stateToken = SingDone + instance Protocol PingPong where -- | The actual messages in our protocol. @@ -54,33 +65,11 @@ 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 + type StateAgency StIdle = ClientAgency + type StateAgency StBusy = ServerAgency + type StateAgency StDone = NobodyAgency - -- | 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 StateToken = SPingPong 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" diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Client.hs b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Client.hs index 2d9f7693..4bb1e6a4 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Client.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Client.hs @@ -1,5 +1,8 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} module Network.TypedProtocol.ReqResp.Client ( -- * Normal client @@ -7,12 +10,17 @@ module Network.TypedProtocol.ReqResp.Client , reqRespClientPeer -- * Pipelined client , ReqRespClientPipelined (..) - , ReqRespSender (..) , reqRespClientPeerPipelined + , ReqRespIdle (..) + , reqRespClientPeerIdle + -- * Request once + , requestOnce ) where import Network.TypedProtocol.Core -import Network.TypedProtocol.Pipelined +import Network.TypedProtocol.Peer.Client +import Network.TypedProtocol.Peer.Server (Server) +import Network.TypedProtocol.Proofs (connect) import Network.TypedProtocol.ReqResp.Type data ReqRespClient req resp m a where @@ -29,25 +37,24 @@ data ReqRespClient req resp m a where reqRespClientPeer :: Monad m => ReqRespClient req resp m a - -> Peer (ReqResp req resp) AsClient 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 -- 'StDone' state. Once in the 'StDone' state we can actually stop using -- 'done', with a return value. - Effect $ do - r <- result - return $ Yield (ClientAgency TokIdle) MsgDone (Done TokDone r) + Effect $ + Yield MsgDone . Done <$> result reqRespClientPeer (SendMsgReq req next) = -- Send our message. - Yield (ClientAgency TokIdle) (MsgReq req) $ + Yield (MsgReq req) $ -- 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) $ \(MsgResp resp) -> + Await $ \(MsgResp resp) -> -- Now in this case there is only one possible response, and we have -- one corresponding continuation 'kPong' to handle that response. @@ -58,6 +65,18 @@ reqRespClientPeer (SendMsgReq req next) = pure $ reqRespClientPeer client + +requestOnce :: forall req resp m. + Monad m + => (forall x. Server (ReqResp req resp) NonPipelined StIdle m x) + -> (req -> m resp) +requestOnce server req = (\(resp, _, _) -> resp) + <$> reqRespClientPeer client `connect` server + where + client :: ReqRespClient req resp m resp + client = SendMsgReq req $ \resp -> pure $ SendMsgDone (pure resp) + + -- -- Pipelined client -- @@ -69,69 +88,71 @@ data ReqRespClientPipelined req resp m a where -- | A 'PingPongSender', but starting with zero outstanding pipelined -- responses, and for any internal collect type @c@. ReqRespClientPipelined :: - ReqRespSender req resp Z c m a + ReqRespIdle req resp Z c m a -> ReqRespClientPipelined req resp m a -data ReqRespSender req resp n c 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 - -> ReqRespSender req resp (S n) c m a -- continuation - -> ReqRespSender req resp n c m a + -> (resp -> m c) -- receive action + -> ReqRespIdle req resp (S n) c m a -- continuation + -> ReqRespIdle req resp n c m a CollectPipelined - :: Maybe (ReqRespSender req resp (S n) c m a) - -> (c -> ReqRespSender req resp n c m a) - -> ReqRespSender req resp (S n) c 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 -> ReqRespSender req resp Z c m a + :: a -> ReqRespIdle req resp Z c m a --- | Interpret a pipelined client as a 'PeerPipelined' on the client side of +-- | Interpret a pipelined client as a 'Peer' on the client side of -- the 'ReqResp' protocol. -- reqRespClientPeerPipelined - :: Monad m - => ReqRespClientPipelined req resp m a - -> PeerPipelined (ReqResp req resp) AsClient StIdle m a + :: Functor m + => ReqRespClientPipelined req resp m a + -> ClientPipelined (ReqResp req resp) StIdle m a reqRespClientPeerPipelined (ReqRespClientPipelined peer) = - PeerPipelined (reqRespClientPeerSender peer) - - -reqRespClientPeerSender - :: Monad m - => ReqRespSender req resp n c m a - -> PeerSender (ReqResp req resp) AsClient StIdle n c m a - -reqRespClientPeerSender (SendMsgDonePipelined result) = - -- Send `MsgDone` and complete the protocol - SenderYield - (ClientAgency TokIdle) - MsgDone - (SenderDone TokDone result) - -reqRespClientPeerSender (SendMsgReqPipelined req receive next) = - -- Pipelined yield: send `MsgReq`, immediately follow with the next step. - -- Await for a response in a continuation. - SenderPipeline - (ClientAgency TokIdle) - (MsgReq req) - -- response handler - (ReceiverAwait (ServerAgency TokBusy) $ \(MsgResp resp) -> - ReceiverEffect $ do - x <- receive resp - return (ReceiverDone x)) - -- run the next step of the req-resp protocol. - (reqRespClientPeerSender next) - -reqRespClientPeerSender (CollectPipelined mNone collect) = - SenderCollect - (fmap reqRespClientPeerSender mNone) - (reqRespClientPeerSender . collect) - + ClientPipelined $ reqRespClientPeerIdle peer + + +reqRespClientPeerIdle + :: forall req resp n c m a. + Functor m + => 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 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. + -- Await for a response in a continuation. + YieldPipelined + (MsgReq req) + (ReceiverAwait $ \(MsgResp resp) -> + ReceiverEffect $ + ReceiverDone <$> receive resp + ) + (go next) + + go (CollectPipelined mNone collect) = + Collect + (go <$> mNone) + (\c -> Effect $ go <$> collect c) + + go (SendMsgDonePipelined result) = + -- Send `MsgDone` and complete the protocol + Yield + MsgDone + (Done result) diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec.hs b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec.hs index 1b363463..9152de55 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec.hs @@ -9,6 +9,7 @@ module Network.TypedProtocol.ReqResp.Codec where import Network.TypedProtocol.Codec +import Network.TypedProtocol.Core import Network.TypedProtocol.PingPong.Codec (decodeTerminatedFrame) import Network.TypedProtocol.ReqResp.Type import Text.Read (readMaybe) @@ -21,35 +22,33 @@ codecReqResp :: codecReqResp = Codec{encode, decode} where - encode :: forall (pr :: PeerRole) - (st :: ReqResp req resp) - (st' :: ReqResp req resp) - . PeerHasAgency pr st - -> Message (ReqResp req resp) st st' + encode :: forall req' resp' + (st :: ReqResp req' resp') + (st' :: ReqResp req' resp') + . ( Show (Message (ReqResp req' resp') st st') ) + => Message (ReqResp req' resp') st st' -> String - encode (ClientAgency TokIdle) msg = show msg ++ "\n" - encode (ServerAgency TokBusy) msg = show msg ++ "\n" + encode msg = show msg ++ "\n" - decode :: forall (pr :: PeerRole) - (st :: ReqResp req resp) - . PeerHasAgency pr st - -> m (DecodeStep String CodecFailure m (SomeMessage st)) + decode :: forall req' resp' m' + (st :: ReqResp req' resp') + . (Monad m', Read req', Read resp', ActiveState st) + => StateToken st + -> m' (DecodeStep String CodecFailure m' (SomeMessage st)) decode stok = decodeTerminatedFrame '\n' $ \str trailing -> case (stok, break (==' ') str) of - (ClientAgency TokIdle, ("MsgReq", str')) - | Just resp <- readMaybe str' - -> DecodeDone (SomeMessage (MsgReq resp)) trailing - (ClientAgency TokIdle, ("MsgDone", "")) + (SingIdle, ("MsgReq", str')) + | Just req <- readMaybe str' + -> DecodeDone (SomeMessage (MsgReq req)) trailing + (SingIdle, ("MsgDone", "")) -> DecodeDone (SomeMessage MsgDone) trailing - (ServerAgency TokBusy, ("MsgResp", str')) - | Just resp <- readMaybe str' + (SingBusy, ("MsgResp", str')) + | Just resp <- readMaybe str' -> DecodeDone (SomeMessage (MsgResp resp)) trailing - (ServerAgency _ , _ ) -> DecodeFail failure + (_ , _ ) -> DecodeFail failure where failure = CodecFailure ("unexpected server message: " ++ str) - (ClientAgency _ , _ ) -> DecodeFail failure - where failure = CodecFailure ("unexpected client message: " ++ str) codecReqRespId :: @@ -59,17 +58,17 @@ codecReqRespId :: codecReqRespId = Codec{encode, decode} where - encode :: forall (pr :: PeerRole) - (st :: ReqResp req resp) + encode :: forall (st :: ReqResp req resp) (st' :: ReqResp req resp) - . PeerHasAgency pr st - -> Message (ReqResp req resp) st st' + . StateTokenI st + => ActiveState st + => Message (ReqResp req resp) st st' -> AnyMessage (ReqResp req resp) - encode _ msg = AnyMessage msg + encode msg = AnyMessage msg - decode :: forall (pr :: PeerRole) - (st :: ReqResp req resp) - . PeerHasAgency pr st + decode :: forall (st :: ReqResp req resp) + . ActiveState st + => StateToken st -> m (DecodeStep (AnyMessage (ReqResp req resp)) CodecFailure m (SomeMessage st)) decode stok = pure $ DecodePartial $ \mb -> @@ -77,15 +76,18 @@ codecReqRespId = Nothing -> return $ DecodeFail (CodecFailure "expected more data") Just (AnyMessage msg) -> return $ case (stok, msg) of - (ClientAgency TokIdle, MsgReq{}) + (SingIdle, MsgReq{}) -> DecodeDone (SomeMessage msg) Nothing - (ClientAgency TokIdle, MsgDone) + (SingIdle, MsgDone) -> DecodeDone (SomeMessage msg) Nothing - (ServerAgency TokBusy, MsgResp{}) + (SingBusy, MsgResp{}) -> DecodeDone (SomeMessage msg) Nothing - (ServerAgency _ , _ ) -> DecodeFail failure - where failure = CodecFailure ("unexpected server message: " ++ show msg) - (ClientAgency _ , _ ) -> DecodeFail failure - where failure = CodecFailure ("unexpected client message: " ++ show msg) + (SingIdle, _) -> + DecodeFail failure + where failure = CodecFailure ("unexpected client message: " ++ show msg) + (SingBusy, _) -> + DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ show msg) + (a@SingDone, _) -> notActiveState a diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec/CBOR.hs b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec/CBOR.hs index 23fd7a95..0f12bb3b 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec/CBOR.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Codec/CBOR.hs @@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE PolyKinds #-} @@ -32,29 +33,30 @@ codecReqResp => Codec (ReqResp req resp) CBOR.DeserialiseFailure m ByteString codecReqResp = mkCodecCborLazyBS encodeMsg decodeMsg where - encodeMsg :: forall (pr :: PeerRole) st st'. - PeerHasAgency pr st - -> Message (ReqResp req resp) st st' + encodeMsg :: forall st st'. + Message (ReqResp req resp) st st' -> CBOR.Encoding - encodeMsg (ClientAgency TokIdle) (MsgReq req) = + encodeMsg (MsgReq req) = CBOR.encodeListLen 2 <> CBOR.encodeWord 0 <> CBOR.encode req - encodeMsg (ServerAgency TokBusy) (MsgResp resp) = + encodeMsg (MsgResp resp) = CBOR.encodeListLen 2 <> CBOR.encodeWord 1 <> CBOR.encode resp - encodeMsg (ClientAgency TokIdle) MsgDone = + encodeMsg MsgDone = CBOR.encodeListLen 1 <> CBOR.encodeWord 2 - decodeMsg :: forall (pr :: PeerRole) s (st :: ReqResp req resp). - PeerHasAgency pr st + decodeMsg :: forall s (st :: ReqResp req resp). + ActiveState st + => StateToken st -> CBOR.Decoder s (SomeMessage st) decodeMsg stok = do _ <- CBOR.decodeListLen key <- CBOR.decodeWord case (stok, key) of - (ClientAgency TokIdle, 0) -> SomeMessage . MsgReq <$> CBOR.decode - (ServerAgency TokBusy, 1) -> SomeMessage . MsgResp <$> CBOR.decode - (ClientAgency TokIdle, 2) -> return $ SomeMessage MsgDone + (SingIdle, 0) -> SomeMessage . MsgReq <$> CBOR.decode + (SingBusy, 1) -> SomeMessage . MsgResp <$> CBOR.decode + (SingIdle, 2) -> return $ SomeMessage MsgDone -- TODO proper exceptions - (ClientAgency TokIdle, _) -> fail "codecReqResp.StIdle: unexpected key" - (ServerAgency TokBusy, _) -> fail "codecReqResp.StBusy: unexpected key" + (SingIdle, _) -> fail "codecReqResp.StIdle: unexpected key" + (SingBusy, _) -> fail "codecReqResp.StBusy: unexpected key" + (a@SingDone, _) -> notActiveState a diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Examples.hs b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Examples.hs index c10a70ed..ecfb1932 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Examples.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Examples.hs @@ -1,6 +1,7 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} module Network.TypedProtocol.ReqResp.Examples where @@ -8,7 +9,7 @@ module Network.TypedProtocol.ReqResp.Examples where import Network.TypedProtocol.ReqResp.Client import Network.TypedProtocol.ReqResp.Server -import Network.TypedProtocol.Pipelined +import Network.TypedProtocol.Peer.Client -- | An example request\/response client which ignores received responses. -- @@ -71,7 +72,7 @@ reqRespClientMapPipelined :: forall req resp m. reqRespClientMapPipelined reqs0 = ReqRespClientPipelined (go [] Zero reqs0) where - go :: [resp] -> Nat o -> [req] -> ReqRespSender req resp o resp m [resp] + go :: [resp] -> Nat o -> [req] -> ReqRespIdle req resp o resp m [resp] go resps Zero reqs = case reqs of [] -> SendMsgDonePipelined (reverse resps) @@ -82,10 +83,10 @@ reqRespClientMapPipelined reqs0 = (case reqs of [] -> Nothing req:reqs' -> Just (sendReq resps (Succ o) req reqs')) - (\resp -> go (resp:resps) o reqs) + (\resp -> return $ go (resp:resps) o reqs) sendReq :: [resp] -> Nat o -> req -> [req] - -> ReqRespSender req resp o resp m [resp] + -> ReqRespIdle req resp o resp m [resp] sendReq resps o req reqs' = SendMsgReqPipelined req (\resp -> return resp) diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Server.hs b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Server.hs index 56c1944c..dcb91806 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Server.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Server.hs @@ -5,6 +5,7 @@ module Network.TypedProtocol.ReqResp.Server where import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Server import Network.TypedProtocol.ReqResp.Type @@ -25,11 +26,11 @@ data ReqRespServer req resp m a = ReqRespServer { reqRespServerPeer :: Monad m => ReqRespServer req resp m a - -> Peer (ReqResp req resp) AsServer StIdle m a + -> Server (ReqResp req resp) NonPipelined StIdle m a reqRespServerPeer ReqRespServer{..} = -- In the 'StIdle' the server is awaiting a request message - Await (ClientAgency TokIdle) $ \msg -> + Await $ \msg -> -- The client got to choose between two messages and we have to handle -- either of them @@ -37,10 +38,10 @@ reqRespServerPeer ReqRespServer{..} = -- 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 -> Effect $ Done TokDone <$> recvMsgDone + MsgDone -> Effect $ Done <$> 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. MsgReq req -> Effect $ do (resp, next) <- recvMsgReq req - pure $ Yield (ServerAgency TokBusy) (MsgResp resp) (reqRespServerPeer next) + pure $ Yield (MsgResp resp) (reqRespServerPeer next) diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Type.hs b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Type.hs index 059a8ed5..bd41a9f5 100644 --- a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Type.hs +++ b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Type.hs @@ -17,6 +17,21 @@ data ReqResp req resp where StBusy :: ReqResp req resp StDone :: ReqResp req resp +data SReqResp (st :: ReqResp req resp) where + SingIdle :: SReqResp StIdle + SingBusy :: SReqResp StBusy + SingDone :: SReqResp StDone + +deriving instance Show (SReqResp st) + +instance StateTokenI StIdle where + stateToken = SingIdle +instance StateTokenI StBusy where + stateToken = SingBusy +instance StateTokenI StDone where + stateToken = SingDone + + instance Protocol (ReqResp req resp) where data Message (ReqResp req resp) from to where @@ -24,18 +39,11 @@ instance Protocol (ReqResp req resp) where MsgResp :: resp -> Message (ReqResp req resp) StBusy StIdle MsgDone :: Message (ReqResp req resp) StIdle StDone - data ClientHasAgency st where - TokIdle :: ClientHasAgency StIdle + type StateAgency StIdle = ClientAgency + type StateAgency StBusy = ServerAgency + type StateAgency StDone = NobodyAgency - data ServerHasAgency st where - TokBusy :: ServerHasAgency StBusy - - 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 StateToken = SReqResp deriving instance (Show req, Show resp) @@ -43,9 +51,3 @@ deriving instance (Show req, Show resp) deriving instance (Eq req, Eq resp) => Eq (Message (ReqResp req resp) from to) - -instance Show (ClientHasAgency (st :: ReqResp req resp)) where - show TokIdle = "TokIdle" - -instance Show (ServerHasAgency (st :: ReqResp req resp)) where - show TokBusy = "TokBusy" diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Client.hs b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Client.hs new file mode 100644 index 00000000..aa2fd081 --- /dev/null +++ b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Client.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + + + +module Network.TypedProtocol.ReqResp2.Client where + +import Network.TypedProtocol.ReqResp2.Type + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer.Client + + +reqResp2Client :: forall req resp m. + () + => [Either req req] + -> 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 n (Either resp resp)) StIdle m [Either resp resp] + + send !n (Left req : reqs) = + YieldPipelined (MsgReq req) receiver (send (Succ n) reqs) + + send !n (Right req : reqs) = + YieldPipelined (MsgReq' req) receiver' (send (Succ n) reqs) + + send !n [] = collect n [] + + + receiver :: Receiver (ReqResp2 req resp) StBusy StIdle m (Either resp resp) + receiver = ReceiverAwait (\(MsgResp resp) -> ReceiverDone (Left resp)) + + + receiver' :: Receiver (ReqResp2 req resp) StBusy' StIdle m (Either resp resp) + receiver' = ReceiverAwait (\(MsgResp' resp) -> ReceiverDone (Right resp)) + + + -- collect all the responses + collect :: Nat n + -> [Either resp resp] -- all the responses received so far + -> Client (ReqResp2 req resp) (Pipelined n (Either resp resp)) StIdle m [Either resp resp] + + collect Zero !resps = Yield MsgDone (Done (reverse resps)) + + collect (Succ n) !resps = + Collect Nothing $ \c -> collect n (c : resps) + + + diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Type.hs b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Type.hs new file mode 100644 index 00000000..14a567b0 --- /dev/null +++ b/typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Type.hs @@ -0,0 +1,63 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeFamilies #-} + + +module Network.TypedProtocol.ReqResp2.Type where + +import Network.TypedProtocol.Core + + +data ReqResp2 req resp where + StIdle :: ReqResp2 req resp + StBusy :: ReqResp2 req resp + StBusy' :: ReqResp2 req resp + StDone :: ReqResp2 req resp + +data SReqResp2 (st :: ReqResp2 req resp) where + SingIdle :: SReqResp2 StIdle + SingBusy :: SReqResp2 StBusy + SingBusy' :: SReqResp2 StBusy' + SingDone :: SReqResp2 StDone + +deriving instance Show (SReqResp2 st) + +instance StateTokenI StIdle where + stateToken = SingIdle +instance StateTokenI StBusy where + stateToken = SingBusy +instance StateTokenI StBusy' where + stateToken = SingBusy' +instance StateTokenI StDone where + stateToken = SingDone + + +instance Protocol (ReqResp2 req resp) where + + data Message (ReqResp2 req resp) from to where + MsgReq :: req -> Message (ReqResp2 req resp) StIdle StBusy + MsgResp :: resp -> Message (ReqResp2 req resp) StBusy StIdle + + MsgReq' :: req -> Message (ReqResp2 req resp) StIdle StBusy' + MsgResp' :: resp -> Message (ReqResp2 req resp) StBusy' StIdle + + MsgDone :: Message (ReqResp2 req resp) StIdle StDone + + type StateAgency StIdle = ClientAgency + type StateAgency StBusy = ServerAgency + type StateAgency StBusy' = ServerAgency + type StateAgency StDone = NobodyAgency + + type StateToken = SReqResp2 + + +deriving instance (Show req, Show resp) + => Show (Message (ReqResp2 req resp) from to) + +deriving instance (Eq req, Eq resp) + => Eq (Message (ReqResp2 req resp) from to) + diff --git a/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Client.hs b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Client.hs new file mode 100644 index 00000000..31ca125c --- /dev/null +++ b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Client.hs @@ -0,0 +1,42 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Network.TypedProtocol.Stateful.ReqResp.Client + ( ReqRespClient (..) + , reqRespClientPeer + ) where + +import Data.Typeable +import Network.TypedProtocol.Stateful.Peer.Client +import Network.TypedProtocol.Stateful.ReqResp.Type + +data ReqRespClient req m a where + SendMsgReq :: Typeable resp + => req resp + -> (resp -> m (ReqRespClient req m a)) + -> ReqRespClient req m a + + SendMsgDone :: a + -> ReqRespClient req m a + + +reqRespClientPeer + :: Monad m + => ReqRespClient req m a + -> Client (ReqResp req) StIdle State m a + +reqRespClientPeer (SendMsgDone a) = + Yield StateDone MsgDone (Done a) + +reqRespClientPeer (SendMsgReq req next) = + Yield (StateBusy req) + (MsgReq req) $ + Await $ \_ (MsgResp resp) -> + let client = next resp + in ( Effect $ reqRespClientPeer <$> client + , StateIdle + ) diff --git a/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Codec.hs b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Codec.hs new file mode 100644 index 00000000..f78991a9 --- /dev/null +++ b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Codec.hs @@ -0,0 +1,114 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +module Network.TypedProtocol.Stateful.ReqResp.Codec where + +import Data.Kind (Type) +import Data.Singletons.Decide +import Data.Typeable +import Network.TypedProtocol.Core +import Network.TypedProtocol.PingPong.Codec (decodeTerminatedFrame) +import Network.TypedProtocol.Stateful.Codec +import Network.TypedProtocol.Stateful.ReqResp.Type + +data Some (f :: k -> Type) where + Some :: Typeable a => f a -> Some f + + +-- | Codec polymorphic in the RPC (e.g. `req` type) +-- +codecReqResp + :: forall req m. Monad m + => (forall resp. req resp -> String) + -- ^ encode `req resp` + -> (String -> Maybe (Some req)) + -- ^ decode `req resp` + -> (forall resp. resp -> String) + -- ^ encode resp + -> (forall resp. req resp -> String -> Maybe resp) + -- ^ decode resp + -> Codec (ReqResp req) CodecFailure State m String +codecReqResp encodeReq decodeReq encodeResp decodeResp = + Codec { encode, decode } + where + encode :: State st' + -> Message (ReqResp req) st st' + -> String + encode _ (MsgReq req) = "MsgReq " ++ encodeReq req ++ "\n" + encode _ MsgDone = "MsgDone\n" + encode _ (MsgResp resp) = "MsgResp " ++ encodeResp resp ++ "\n" + + decode :: forall (st :: ReqResp req). + ActiveState st + => StateToken st + -> State st + -> m (DecodeStep String CodecFailure m (SomeMessage st)) + decode stok state = + decodeTerminatedFrame '\n' $ \str trailing -> + case (stok, state, break (==' ') str) of + (SingIdle, StateIdle, ("MsgReq", str')) + | Just (Some req) <- decodeReq str' + -> DecodeDone (SomeMessage (MsgReq req)) trailing + (SingIdle, StateIdle, ("MsgDone", "")) + -> DecodeDone (SomeMessage MsgDone) trailing + (SingBusy, StateBusy req, ("MsgResp", str')) + -- note that we need `req` to decode response of the given type + | Just resp <- decodeResp req str' + -> DecodeDone (SomeMessage (MsgResp resp)) trailing + (_, _, _) -> DecodeFail failure + where failure = CodecFailure ("unexpected server message: " ++ str) + + +data Bytes where + Bytes :: Message (ReqResp FileAPI) st st' -> Bytes + +-- | An identity codec which wraps messages into `AnyMessage`. +-- +codecReqRespId + :: forall m. + Applicative m + => (forall (res1 :: Type) (res2 :: Type). + (Typeable res1, Typeable res2) + => Proxy res1 + -> Proxy res2 + -> Maybe (res1 :~: res2) + ) + -> Codec FileRPC String State m Bytes +codecReqRespId eqRespTypes = Codec { encode, decode } + where + encode _ = Bytes + + decode :: forall (st :: ReqResp FileAPI). + ActiveState st + => StateToken st + -> State st + -> m (DecodeStep Bytes String m (SomeMessage st)) + decode stok state = pure $ DecodePartial $ \bytes -> pure $ + case (stok, state, bytes) of + (SingIdle, StateIdle, Just (Bytes msg@MsgDone)) + -> DecodeDone (SomeMessage msg) Nothing + (SingIdle, StateIdle, Just (Bytes msg@MsgReq{})) + -> DecodeDone (SomeMessage msg) Nothing + (SingBusy, StateBusy req, Just (Bytes msg@(MsgResp _))) + -- the codec needs to verify that response type of `req` and `msg` agrees + | Just Refl <- eqRespTypes (reqRespType req) (msgRespType msg) + -> DecodeDone (SomeMessage msg) Nothing + + (SingDone, _, _) -> notActiveState stok + (_, _, Nothing) -> DecodeFail "no bytes" + (_, _, _) -> DecodeFail "no matching message" + + msgRespType :: forall resp. Message (ReqResp FileAPI) (StBusy resp) StIdle + -> Proxy resp + msgRespType (MsgResp _) = Proxy + + reqRespType :: forall resp. FileAPI resp -> Proxy resp + reqRespType _ = Proxy + + diff --git a/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Examples.hs b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Examples.hs new file mode 100644 index 00000000..7827e5a8 --- /dev/null +++ b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Examples.hs @@ -0,0 +1,33 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Network.TypedProtocol.Stateful.ReqResp.Examples where + +import Network.TypedProtocol.Stateful.ReqResp.Server +import Network.TypedProtocol.Stateful.ReqResp.Type + + +fileRPCServer :: Monad m + => (forall resp. FileAPI resp -> m resp) + -- ^ execute `FileAPI` locally + -> ReqRespServer FileAPI m () +fileRPCServer run = ReqRespServer { + reqRespServerDone = (), + reqRespHandleReq = \req -> do + resp <- run req + return (resp, fileRPCServer run) + } + +-- | Example of a file API +-- +simpleFileAPI :: Monad m => FileAPI resp -> m resp +simpleFileAPI (ReadFile filepath) = return filepath +simpleFileAPI (WriteFile _ _) = return () + +simpleFileRPCServer :: Monad m => ReqRespServer FileAPI m () +simpleFileRPCServer = fileRPCServer simpleFileAPI + diff --git a/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Server.hs b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Server.hs new file mode 100644 index 00000000..2898b6f1 --- /dev/null +++ b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Server.hs @@ -0,0 +1,36 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Network.TypedProtocol.Stateful.ReqResp.Server + ( ReqRespServer (..) + , reqRespServerPeer + ) where + +import Data.Typeable +import Network.TypedProtocol.Stateful.Peer.Server +import Network.TypedProtocol.Stateful.ReqResp.Type + + +data ReqRespServer req m a = ReqRespServer { + reqRespServerDone :: a, + reqRespHandleReq :: forall resp. Typeable resp => req resp -> m (resp, ReqRespServer req m a) + } + +reqRespServerPeer :: Functor m + => ReqRespServer req m a + -> Server (ReqResp req) StIdle State m a +reqRespServerPeer ReqRespServer { reqRespServerDone = a, + reqRespHandleReq = k } = + Await $ \_ -> \case + MsgDone -> (Done a, StateDone) + MsgReq req -> + ( Effect $ + (\(resp, k') -> Yield StateIdle (MsgResp resp) (reqRespServerPeer k')) + <$> k req + , StateBusy req + ) diff --git a/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Type.hs b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Type.hs new file mode 100644 index 00000000..bcc25153 --- /dev/null +++ b/typed-protocols-examples/src/Network/TypedProtocol/Stateful/ReqResp/Type.hs @@ -0,0 +1,101 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} + + +-- | An RPC protocol which in which request type determines respond time. +-- Unlike in the `Network.TypedProtocol.ReqResp.Type` where `req` and `resp` +-- types where statically defined, here the respond type is dynamically +-- determined by the type of request. +-- +module Network.TypedProtocol.Stateful.ReqResp.Type where + +import Data.Kind (Type) +import Data.Typeable +import Network.TypedProtocol.Core + + +type ReqResp :: (Type -> Type) -> Type +data ReqResp req where + StIdle :: ReqResp req + StBusy :: res + -> ReqResp req + StDone :: ReqResp req + +type SReqResp :: ReqResp req -> Type +data SReqResp st where + SingIdle :: SReqResp StIdle + SingBusy :: SReqResp (StBusy res :: ReqResp req) + SingDone :: SReqResp StDone + +deriving instance Show (SReqResp st) + +instance StateTokenI StIdle where stateToken = SingIdle +instance StateTokenI (StBusy res) where stateToken = SingBusy +instance StateTokenI StDone where stateToken = SingDone + + +instance Protocol (ReqResp req) where + + -- Messages for the `ReqResp` protocol. + -- + -- Typeable constraint is used to support + -- `Network.TypeProtocol.Stateful.ReqResp.Codec.codecReqRespId' - an + -- efficient encoder / decoder useful for testing purposes. + -- + data Message (ReqResp req) from to where + MsgReq :: Typeable resp + => req resp -- ^ request which expects `resp` as a result, `resp` is + -- promoted to the state `StBusy` state. + -> Message (ReqResp req) StIdle (StBusy resp) + MsgResp :: Typeable resp + => resp -- ^ respond type + -> Message (ReqResp req) (StBusy resp) StIdle + MsgDone :: Message (ReqResp req) StIdle StDone + + type StateAgency StIdle = ClientAgency + type StateAgency (StBusy _) = ServerAgency + type StateAgency StDone = NobodyAgency + + type StateToken = SReqResp + + +-- deriving instance Show req +-- => Show (Message (ReqResp req) from to) +-- +-- deriving instance Eq req +-- => Eq (Message (ReqResp req) from to) + +type State :: ReqResp req -> Type +data State st where + StateIdle :: State StIdle + -- fancy type signature is needed to help GHC infer that when pattern + -- matching on `StateBusy resp` then `resp :: Type` + StateBusy :: forall (req :: Type -> Type) + (result :: Type). + Typeable result + => req result + -> State (StBusy result :: ReqResp req) + StateDone :: State StDone + +-- +-- A simple example RPC +-- + +-- | An example RPC, e.g. the `req` type. +-- +type FileAPI :: Type -> Type +data FileAPI result where + ReadFile :: FilePath -> FileAPI String + -- read a file + + WriteFile :: FilePath -> String -> FileAPI () + -- write to a file +-- TODO: input-output-hk/typed-protocols#57 + +type FileRPC = ReqResp FileAPI diff --git a/typed-protocols-examples/src/Network/TypedProtocol/Trans/Wedge.hs b/typed-protocols-examples/src/Network/TypedProtocol/Trans/Wedge.hs new file mode 100644 index 00000000..05a628ad --- /dev/null +++ b/typed-protocols-examples/src/Network/TypedProtocol/Trans/Wedge.hs @@ -0,0 +1,164 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE InstanceSigs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Network.TypedProtocol.Trans.Wedge where + +import Network.TypedProtocol.Core + +import qualified Network.TypedProtocol.Peer.Client as Client +import qualified Network.TypedProtocol.PingPong.Type as PingPong + + +-- | A [wedge](https://hackage.haskell.org/package/smash-0.1.2/docs/Data-Wedge.html) +-- sum of two protocols. +-- +-- One can interleave both protocols using protocol pipelining. Termination +-- must be done by terminating one of the protocols. +-- +data Wedge ps (stIdle :: ps) ps' (stIdle' :: ps') where + StIdle :: Wedge ps stIdle ps' stIdle' + StFst :: ps -> Wedge ps stIdle ps' stIdle' + StSnd :: ps' -> Wedge ps stIdle ps' stIdle' + + +data SingWedge (st :: Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) where + SingStIdle :: SingWedge StIdle + SingStFst :: StateToken st + -> SingWedge (StFst st) + SingStSnd :: StateToken st' + -> SingWedge (StSnd st') + +instance Show (SingWedge StIdle) where + show SingStIdle = "SingStIdle" +instance Show (StateToken st) => Show (SingWedge (StFst st)) where + show (SingStFst s) = "SingStFst " ++ show s +instance Show (StateToken st) => Show (SingWedge (StSnd st)) where + show (SingStSnd s) = "SingStSnd " ++ show s + +instance StateTokenI StIdle where + stateToken = SingStIdle +instance StateTokenI st => StateTokenI (StFst st) where + stateToken = SingStFst (stateToken @st) +instance StateTokenI st => StateTokenI (StSnd st) where + stateToken = SingStSnd (stateToken @st) + + +-- | A Singleton type which allows to pick the starting protocol state. +-- +data SingStart (st :: Wedge ps stIdle ps' stIdle') where + AtFst :: SingStart (StFst stIdle) + AtSnd :: SingStart (StSnd stIdle) + + +-- Note: This does not require @(Protocol ps, Protocol ps')@, ghc is not +-- requiring class constraints for associated type families / data types the +-- same way as for terms. +-- +instance Protocol (Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) where + + data Message (Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) from to where + -- | Signal that starts one of the protocols. + -- + MsgStart :: SingStart st + -> Message (Wedge ps stIdle ps' stIdle') + StIdle st + + -- | Embed any @ps@ message. + -- + MsgFst :: Message ps st st' + -> Message (Wedge ps stIdle ps' stIdle') + (StFst st) (StFst st') + + + -- | Embed any @ps'@ message. + MsgSnd :: Message ps' st st' + -> Message (Wedge ps stIdle ps' stIdle') + (StSnd st) (StSnd st') + + -- | Switch from @ps@ to @ps'@. + -- + MsgFstToSnd :: Message (Wedge ps stIdle ps' stIdle') + (StFst stIdle) (StSnd stIdle') + + -- | Switch from @ps'@ to @ps@. + -- + MsgSndToFst :: Message (Wedge ps stIdle ps' stIdle') + (StSnd stIdle') (StFst stIdle) + + + type StateAgency StIdle = ClientAgency + type StateAgency (StFst st) = StateAgency st + type StateAgency (StSnd st) = StateAgency st + + type StateToken = SingWedge + + +type PingPong2 = Wedge PingPong.PingPong PingPong.StIdle + PingPong.PingPong PingPong.StIdle + + +pingPong2Client :: Client.Client PingPong2 NonPipelined StIdle m () +pingPong2Client = + Client.Yield (MsgStart AtFst) + $ Client.Yield (MsgFst PingPong.MsgPing) + $ Client.Await $ \(MsgFst PingPong.MsgPong) -> + Client.Yield MsgFstToSnd + $ Client.Yield (MsgSnd PingPong.MsgPing) + $ Client.Await $ \(MsgSnd PingPong.MsgPong) -> + -- terminate, through the second protocol + Client.Yield (MsgSnd PingPong.MsgDone) + $ Client.Done () + + +pingPong2Client' :: forall m. Client.Client PingPong2 (Pipelined Client.Z ()) StIdle m () +pingPong2Client' = + -- + -- Pipeline first protocol + -- + + Client.YieldPipelined (MsgStart AtFst) + (Client.ReceiverDone ()) + $ Client.YieldPipelined (MsgFst PingPong.MsgPing) + (Client.ReceiverAwait (\(MsgFst PingPong.MsgPong) -> Client.ReceiverDone ())) + + -- + -- Pipeline second protocol + -- + + $ Client.YieldPipelined MsgFstToSnd + (Client.ReceiverDone ()) + $ Client.YieldPipelined (MsgSnd PingPong.MsgPing) + (Client.ReceiverAwait (\(MsgSnd PingPong.MsgPong) -> Client.ReceiverDone ())) + + -- + -- Collect responses from the first protocol + -- + + $ Client.Collect Nothing $ \() -> -- collect transition pushed by `MsgStartFst` + Client.Collect Nothing $ \() -> -- collect reply received with `MsgFst MsgPong` + + -- + -- Collect responses from the second protocol + -- + + Client.Collect Nothing $ \() -> -- collect transition pushed by MsgFstToSnd + Client.Collect Nothing $ \() -> -- collect reply received with `MsgSnd MsgPong` + + -- + -- Terminate the protocol + -- + + Client.Yield (MsgSnd PingPong.MsgDone) + $ Client.Done () diff --git a/typed-protocols-examples/test/Network/TypedProtocol/PingPong/Tests.hs b/typed-protocols-examples/test/Network/TypedProtocol/PingPong/Tests.hs index 8728d5c1..65dfabaf 100644 --- a/typed-protocols-examples/test/Network/TypedProtocol/PingPong/Tests.hs +++ b/typed-protocols-examples/test/Network/TypedProtocol/PingPong/Tests.hs @@ -1,9 +1,11 @@ +{-# LANGUAGE CPP #-} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} - +-- orphaned arbitrary instances +{-# OPTIONS_GHC -Wno-orphans #-} module Network.TypedProtocol.PingPong.Tests ( tests @@ -31,11 +33,18 @@ import Control.Monad.Class.MonadSTM import Control.Monad.Class.MonadThrow import Control.Monad.IOSim (runSimOrThrow) import Control.Monad.ST (runST) -import Control.Tracer (Tracer, nullTracer) +import Control.Tracer (nullTracer) + import Data.Functor.Identity (Identity (..)) +import Data.List (inits, tails) import qualified Data.ByteString.Lazy as LBS -import Data.List (inits, tails) +#if !defined(mingw32_HOST_OS) +import qualified Network.Socket as Socket +import System.Directory (removeFile) +import System.IO +import qualified System.Posix.Files as Posix +#endif import Test.QuickCheck import Test.Tasty (TestTree, testGroup) @@ -59,6 +68,10 @@ tests = testGroup "Network.TypedProtocol.PingPong" , testProperty "connect_pipelined 5" prop_connect_pipelined5 , testProperty "channel ST" prop_channel_ST , testProperty "channel IO" prop_channel_IO +#if !defined(mingw32_HOST_OS) + , testProperty "namedPipePipelined" prop_namedPipePipelined_IO + , testProperty "socketPipelined" prop_socketPipelined_IO +#endif , testGroup "Codec" [ testProperty "codec" prop_codec_PingPong , testProperty "codec 2-splits" prop_codec_splits2_PingPong @@ -95,7 +108,7 @@ direct (SendMsgPing kPong) PingPongServer{recvMsgPing} = do directPipelined :: Monad m - => PingPongClientPipelined m a + => PingPongClientPipelined c m a -> PingPongServer m b -> m (a, b) directPipelined (PingPongClientPipelined client0) server0 = @@ -103,8 +116,8 @@ directPipelined (PingPongClientPipelined client0) server0 = where go :: Monad m => Queue n c - -> PingPongSender n c m a - -> PingPongServer m b + -> PingPongClientIdle n c m a + -> PingPongServer m b -> m (a, b) go EmptyQ (SendMsgDonePipelined clientResult) PingPongServer{recvMsgDone} = pure (clientResult, recvMsgDone) @@ -114,7 +127,7 @@ directPipelined (PingPongClientPipelined client0) server0 = x <- kPong go (enqueue x q) client' server' - go (ConsQ x q) (CollectPipelined _ k) server = + go (ConsQ x q) (CollectPipelined _ k) server = do go q (k x) server @@ -182,7 +195,7 @@ prop_connect (NonNegative n) = (pingPongClientPeer (pingPongClientCount n)) (pingPongServerPeer pingPongServerCount)) - of ((), n', TerminalStates TokDone TokDone) -> n == n' + of ((), n', TerminalStates SingDone SingDone) -> n == n' -- @@ -193,7 +206,7 @@ prop_connect (NonNegative n) = -- should return the interleaving of messages it sent and received. This -- will be used to exercise various interleavings in properties below. -- -connect_pipelined :: PingPongClientPipelined Identity [Either Int Int] +connect_pipelined :: PingPongClientPipelined Int Identity [Either Int Int] -> [Bool] -> (Int, [Either Int Int]) connect_pipelined client cs = @@ -201,8 +214,8 @@ connect_pipelined client cs = (connectPipelined cs (pingPongClientPeerPipelined client) (pingPongServerPeer pingPongServerCount)) - - of (reqResps, n, TerminalStates TokDone TokDone) -> (n, reqResps) + of (reqResps, n, TerminalStates SingDone SingDone) -> + (n, reqResps) -- | Using a client that forces maximum pipeling, show that irrespective of @@ -281,13 +294,12 @@ prop_connect_pipelined5 choices (Positive omax) (NonNegative n) = -- | Run a non-pipelined client and server over a channel using a codec. -- -prop_channel :: (MonadSTM m, MonadAsync m, MonadCatch m) +prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m) => NonNegative Int - -> Tracer m (Role, TraceSendRecv PingPong) -> m Bool -prop_channel (NonNegative n) tr = do +prop_channel (NonNegative n) = do ((), n') <- runConnectedPeers createConnectedChannels - tr + nullTracer codecPingPong client server return (n' == n) where @@ -297,22 +309,84 @@ prop_channel (NonNegative n) tr = do prop_channel_IO :: NonNegative Int -> Property prop_channel_IO n = - ioProperty (prop_channel n nullTracer) + ioProperty (prop_channel n) prop_channel_ST :: NonNegative Int -> Bool prop_channel_ST n = - runSimOrThrow (prop_channel n nullTracer) + runSimOrThrow (prop_channel n) + + +#if !defined(mingw32_HOST_OS) +prop_namedPipePipelined_IO :: NonNegative Int + -> Property +prop_namedPipePipelined_IO (NonNegative n) = ioProperty $ do + let client = pingPongClientPeer (pingPongClientCount n) + server = pingPongServerPeer pingPongServerCount + + let cliPath = "client.sock" + srvPath = "server.sock" + mode = Posix.ownerModes + + Posix.createNamedPipe cliPath mode + Posix.createNamedPipe srvPath mode + + bracket (openFile cliPath ReadWriteMode) + (\_ -> removeFile cliPath) + $ \cliHandle -> + bracket (openFile srvPath ReadWriteMode) + (\_ -> removeFile srvPath) + $ \srvHandle -> do + ((), n') <- runConnectedPeers (return ( handlesAsChannel cliHandle srvHandle + , handlesAsChannel srvHandle cliHandle + )) + nullTracer + CBOR.codecPingPong client server + return (n' == n) +#endif + + +#if !defined(mingw32_HOST_OS) +prop_socketPipelined_IO :: NonNegative Int + -> Property +prop_socketPipelined_IO (NonNegative n) = ioProperty $ do + ai : _ <- Socket.getAddrInfo (Just Socket.defaultHints + { Socket.addrFamily = Socket.AF_INET, + Socket.addrFlags = [Socket.AI_PASSIVE], + Socket.addrSocketType = Socket.Stream }) + (Just "127.0.0.1") Nothing + bracket + ((,) <$> Socket.openSocket ai + <*> Socket.openSocket ai) + ( \ (sock, sock') -> Socket.close sock + >> Socket.close sock') + $ \ (sock, sock') -> do + Socket.bind sock (Socket.addrAddress ai) + addr <- Socket.getSocketName sock + Socket.listen sock 1 + Socket.connect sock' addr + bracket (fst <$> Socket.accept sock) Socket.close + $ \sock'' -> do + let client = pingPongClientPeer (pingPongClientCount n) + server = pingPongServerPeer pingPongServerCount + + ((), n') <- runConnectedPeers (return ( socketAsChannel sock' + , socketAsChannel sock'' + )) + nullTracer + CBOR.codecPingPong client server + return (n' == n) +#endif -- -- Codec properties -- -instance Arbitrary (AnyMessageAndAgency PingPong) where +instance Arbitrary (AnyMessage PingPong) where arbitrary = elements - [ AnyMessageAndAgency (ClientAgency TokIdle) MsgPing - , AnyMessageAndAgency (ServerAgency TokBusy) MsgPong - , AnyMessageAndAgency (ClientAgency TokIdle) MsgDone + [ AnyMessage MsgPing + , AnyMessage MsgPong + , AnyMessage MsgDone ] instance Eq (AnyMessage PingPong) where @@ -321,20 +395,20 @@ instance Eq (AnyMessage PingPong) where AnyMessage MsgDone == AnyMessage MsgDone = True _ == _ = False -prop_codec_PingPong :: AnyMessageAndAgency PingPong -> Bool +prop_codec_PingPong :: AnyMessage PingPong -> Bool prop_codec_PingPong = prop_codec runIdentity codecPingPong -prop_codec_splits2_PingPong :: AnyMessageAndAgency PingPong -> Bool +prop_codec_splits2_PingPong :: AnyMessage PingPong -> Bool prop_codec_splits2_PingPong = prop_codec_splits splits2 runIdentity codecPingPong -prop_codec_splits3_PingPong :: AnyMessageAndAgency PingPong -> Bool +prop_codec_splits3_PingPong :: AnyMessage PingPong -> Bool prop_codec_splits3_PingPong = prop_codec_splits splits3 @@ -346,13 +420,13 @@ prop_codec_splits3_PingPong = -- prop_codec_cbor_PingPong - :: AnyMessageAndAgency PingPong + :: AnyMessage PingPong -> Bool prop_codec_cbor_PingPong msg = runST $ prop_codecM CBOR.codecPingPong msg prop_codec_cbor_splits2_PingPong - :: AnyMessageAndAgency PingPong + :: AnyMessage PingPong -> Bool prop_codec_cbor_splits2_PingPong msg = runST $ prop_codec_splitsM @@ -361,7 +435,7 @@ prop_codec_cbor_splits2_PingPong msg = msg prop_codec_cbor_splits3_PingPong - :: AnyMessageAndAgency PingPong + :: AnyMessage PingPong -> Bool prop_codec_cbor_splits3_PingPong msg = runST $ prop_codec_splitsM diff --git a/typed-protocols-examples/test/Network/TypedProtocol/ReqResp/Tests.hs b/typed-protocols-examples/test/Network/TypedProtocol/ReqResp/Tests.hs index 158fb825..a58c21e0 100644 --- a/typed-protocols-examples/test/Network/TypedProtocol/ReqResp/Tests.hs +++ b/typed-protocols-examples/test/Network/TypedProtocol/ReqResp/Tests.hs @@ -1,10 +1,14 @@ +{-# LANGUAGE CPP #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TupleSections #-} -{-# LANGUAGE TypeApplications #-} + +-- orphaned arbitrary instances +{-# OPTIONS_GHC -Wno-orphans #-} module Network.TypedProtocol.ReqResp.Tests (tests) where @@ -16,22 +20,33 @@ import Network.TypedProtocol.Proofs import Network.TypedProtocol.ReqResp.Client import Network.TypedProtocol.ReqResp.Codec +import qualified Network.TypedProtocol.ReqResp.Codec.CBOR as CBOR import Network.TypedProtocol.ReqResp.Examples import Network.TypedProtocol.ReqResp.Server import Network.TypedProtocol.ReqResp.Type +import Control.Exception (throw) import Control.Monad.Class.MonadAsync +import Control.Monad.Class.MonadST import Control.Monad.Class.MonadSTM import Control.Monad.Class.MonadThrow -import Control.Monad.IOSim (runSimOrThrow) +import Control.Monad.Class.MonadTimer.SI +import Control.Monad.IOSim import Control.Monad.ST (runST) import Control.Tracer (nullTracer) import Data.Functor.Identity (Identity (..)) -import Data.List (mapAccumL) +import Data.List (intercalate, mapAccumL) import Data.Tuple (swap) +#if !defined(mingw32_HOST_OS) +import qualified Network.Socket as Socket +import System.Directory (removeFile) +import System.IO +import qualified System.Posix.Files as Posix +#endif -import Network.TypedProtocol.PingPong.Tests (splits2, splits3) +import Network.TypedProtocol.PingPong.Tests (splits2, splits2BS, + splits3, splits3BS) import Test.QuickCheck import Test.Tasty (TestTree, testGroup) @@ -51,6 +66,12 @@ tests = testGroup "Network.TypedProtocol.ReqResp" , testProperty "connectPipelined" prop_connectPipelined , testProperty "channel ST" prop_channel_ST , testProperty "channel IO" prop_channel_IO + , testProperty "channelPipelined ST" prop_channelPipelined_ST + , testProperty "channelPipelined IO" prop_channelPipelined_IO +#if !defined(mingw32_HOST_OS) + , testProperty "namedPipePipelined" prop_namedPipePipelined_IO + , testProperty "socketPipelined" prop_socketPipelined_IO +#endif , testGroup "Codec" [ testProperty "codec" prop_codec_ReqResp , testProperty "codec 2-splits" prop_codec_splits2_ReqResp @@ -91,7 +112,7 @@ directPipelined (ReqRespClientPipelined client0) server0 = where go :: Monad m => Queue n c - -> ReqRespSender req resp n c m a + -> ReqRespIdle req resp n c m a -> ReqRespServer req resp m b -> m (a, b) go EmptyQ (SendMsgDonePipelined clientResult) ReqRespServer{recvMsgDone} = @@ -102,8 +123,9 @@ directPipelined (ReqRespClientPipelined client0) server0 = x <- kResp resp go (enqueue x q) client' server' - go (ConsQ x q) (CollectPipelined _ k) server = - go q (k x) server + go (ConsQ resp q) (CollectPipelined _ k) server = do + client' <- k resp + go q client' server prop_direct :: (Int -> Int -> (Int, Int)) -> [Int] -> Bool @@ -136,7 +158,7 @@ prop_connect f xs = (reqRespClientPeer (reqRespClientMap xs)) (reqRespServerPeer (reqRespServerMapAccumL (\a -> pure . f a) 0))) - of (c, s, TerminalStates TokDone TokDone) -> + of (c, s, TerminalStates SingDone SingDone) -> (s, c) == mapAccumL f 0 xs @@ -145,10 +167,10 @@ prop_connectPipelined cs f xs = case runIdentity (connectPipelined cs (reqRespClientPeerPipelined (reqRespClientMapPipelined xs)) - (reqRespServerPeer (reqRespServerMapAccumL - (\a -> pure . f a) 0))) + (reqRespServerPeer + (reqRespServerMapAccumL (\a -> pure . f a) 0))) - of (c, s, TerminalStates TokDone TokDone) -> + of (c, s, TerminalStates SingDone SingDone) -> (s, c) == mapAccumL f 0 xs @@ -156,7 +178,7 @@ prop_connectPipelined cs f xs = -- Properties using channels, codecs and drivers. -- -prop_channel :: (MonadSTM m, MonadAsync m, MonadCatch m) +prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m) => (Int -> Int -> (Int, Int)) -> [Int] -> m Bool prop_channel f xs = do @@ -169,6 +191,7 @@ prop_channel f xs = do server = reqRespServerPeer (reqRespServerMapAccumL (\a -> pure . f a) 0) + prop_channel_IO :: (Int -> Int -> (Int, Int)) -> [Int] -> Property prop_channel_IO f xs = ioProperty (prop_channel f xs) @@ -178,27 +201,122 @@ prop_channel_ST f xs = runSimOrThrow (prop_channel f xs) +prop_channelPipelined :: ( MonadLabelledSTM m, MonadAsync m, MonadCatch m + , MonadDelay m, MonadST m) + => (Int -> Int -> (Int, Int)) -> [Int] + -> m Bool +prop_channelPipelined f xs = do + (c, s) <- runConnectedPeersPipelined + (createPipelineTestChannels 100) + nullTracer + CBOR.codecReqResp + client server + return ((s, c) == mapAccumL f 0 xs) + where + client = reqRespClientPeerPipelined (reqRespClientMapPipelined xs) + server = reqRespServerPeer (reqRespServerMapAccumL + (\a -> pure . f a) 0) + +prop_channelPipelined_IO :: (Int -> Int -> (Int, Int)) -> [Int] -> Property +prop_channelPipelined_IO f xs = + ioProperty (prop_channelPipelined f xs) + +prop_channelPipelined_ST :: (Int -> Int -> (Int, Int)) -> [Int] -> Property +prop_channelPipelined_ST f xs = + let tr = runSimTrace (prop_channelPipelined f xs) in + counterexample (intercalate "\n" $ map show $ traceEvents tr) + $ case traceResult True tr of + Left err -> throw err + Right res -> res + + +#if !defined(mingw32_HOST_OS) +prop_namedPipePipelined_IO :: (Int -> Int -> (Int, Int)) -> [Int] + -> Property +prop_namedPipePipelined_IO f xs = ioProperty $ do + let client = reqRespClientPeerPipelined (reqRespClientMapPipelined xs) + server = reqRespServerPeer (reqRespServerMapAccumL + (\a -> pure . f a) 0) + let cliPath = "client.sock" + srvPath = "server.sock" + mode = Posix.ownerModes + + Posix.createNamedPipe cliPath mode + Posix.createNamedPipe srvPath mode + + bracket (openFile cliPath ReadWriteMode) + (\_ -> removeFile cliPath) + $ \cliHandle -> + bracket (openFile srvPath ReadWriteMode) + (\_ -> removeFile srvPath) + $ \srvHandle -> do + (c, s) <- runConnectedPeersPipelined + (return ( handlesAsChannel cliHandle srvHandle + , handlesAsChannel srvHandle cliHandle + )) + nullTracer + CBOR.codecReqResp + client server + return ((s, c) == mapAccumL f 0 xs) +#endif + + +#if !defined(mingw32_HOST_OS) +prop_socketPipelined_IO :: (Int -> Int -> (Int, Int)) -> [Int] + -> Property +prop_socketPipelined_IO f xs = ioProperty $ do + ai : _ <- Socket.getAddrInfo (Just Socket.defaultHints + { Socket.addrFamily = Socket.AF_INET, + Socket.addrFlags = [Socket.AI_PASSIVE], + Socket.addrSocketType = Socket.Stream }) + (Just "127.0.0.1") Nothing + bracket + ((,) <$> Socket.openSocket ai + <*> Socket.openSocket ai) + ( \ (sock, sock') -> Socket.close sock + >> Socket.close sock') + $ \ (sock, sock') -> do + Socket.bind sock (Socket.addrAddress ai) + addr <- Socket.getSocketName sock + Socket.listen sock 1 + Socket.connect sock' addr + bracket (fst <$> Socket.accept sock) Socket.close + $ \sock'' -> do + let client = reqRespClientPeerPipelined (reqRespClientMapPipelined xs) + server = reqRespServerPeer (reqRespServerMapAccumL + (\a -> pure . f a) 0) + + (c, s) <- runConnectedPeersPipelined + (return ( socketAsChannel sock' + , socketAsChannel sock'' + )) + nullTracer + CBOR.codecReqResp + client server + return ((s, c) == mapAccumL f 0 xs) +#endif + -- -- Codec properties -- instance (Arbitrary req, Arbitrary resp) => - Arbitrary (AnyMessageAndAgency (ReqResp req resp)) where + Arbitrary (AnyMessage (ReqResp req resp)) where arbitrary = oneof - [ AnyMessageAndAgency (ClientAgency TokIdle) . MsgReq <$> arbitrary - , AnyMessageAndAgency (ServerAgency TokBusy) . MsgResp <$> arbitrary - , return (AnyMessageAndAgency (ClientAgency TokIdle) MsgDone) + [ AnyMessage . MsgReq <$> arbitrary + , AnyMessage . MsgResp <$> arbitrary + , return (AnyMessage MsgDone) ] - shrink (AnyMessageAndAgency a (MsgReq r)) = - [ AnyMessageAndAgency a (MsgReq r') + shrink (AnyMessage (MsgReq r)) = + [ AnyMessage (MsgReq r') | r' <- shrink r ] - shrink (AnyMessageAndAgency a (MsgResp r)) = - [ AnyMessageAndAgency a (MsgResp r') + shrink (AnyMessage (MsgResp r)) = + [ AnyMessage (MsgResp r') | r' <- shrink r ] - shrink (AnyMessageAndAgency _ MsgDone) = [] + shrink (AnyMessage MsgDone) = [] instance (Eq req, Eq resp) => Eq (AnyMessage (ReqResp req resp)) where (AnyMessage (MsgReq r1)) == (AnyMessage (MsgReq r2)) = r1 == r2 @@ -206,13 +324,13 @@ instance (Eq req, Eq resp) => Eq (AnyMessage (ReqResp req resp)) where (AnyMessage MsgDone) == (AnyMessage MsgDone) = True _ == _ = False -prop_codec_ReqResp :: AnyMessageAndAgency (ReqResp String String) -> Bool +prop_codec_ReqResp :: AnyMessage (ReqResp String String) -> Bool prop_codec_ReqResp = prop_codec runIdentity codecReqResp -prop_codec_splits2_ReqResp :: AnyMessageAndAgency (ReqResp String String) +prop_codec_splits2_ReqResp :: AnyMessage (ReqResp String String) -> Bool prop_codec_splits2_ReqResp = prop_codec_splits @@ -220,7 +338,7 @@ prop_codec_splits2_ReqResp = runIdentity codecReqResp -prop_codec_splits3_ReqResp :: AnyMessageAndAgency (ReqResp String String) +prop_codec_splits3_ReqResp :: AnyMessage (ReqResp String String) -> Bool prop_codec_splits3_ReqResp = prop_codec_splits @@ -229,25 +347,25 @@ prop_codec_splits3_ReqResp = codecReqResp prop_codec_cbor_ReqResp - :: AnyMessageAndAgency (ReqResp String String) + :: AnyMessage (ReqResp String String) -> Bool prop_codec_cbor_ReqResp msg = - runST $ prop_codecM codecReqResp msg + runST $ prop_codecM CBOR.codecReqResp msg prop_codec_cbor_splits2_ReqResp - :: AnyMessageAndAgency (ReqResp String String) + :: AnyMessage (ReqResp String String) -> Bool prop_codec_cbor_splits2_ReqResp msg = runST $ prop_codec_splitsM - splits2 - codecReqResp + splits2BS + CBOR.codecReqResp msg prop_codec_cbor_splits3_ReqResp - :: AnyMessageAndAgency (ReqResp String String) + :: AnyMessage (ReqResp String String) -> Bool prop_codec_cbor_splits3_ReqResp msg = runST $ prop_codec_splitsM - splits3 - codecReqResp + splits3BS + CBOR.codecReqResp msg diff --git a/typed-protocols-examples/typed-protocols-examples.cabal b/typed-protocols-examples/typed-protocols-examples.cabal index 592a9817..fb2850e1 100644 --- a/typed-protocols-examples/typed-protocols-examples.cabal +++ b/typed-protocols-examples/typed-protocols-examples.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: typed-protocols-examples -version: 0.2.0.2 +version: 0.3.0.0 synopsis: Examples and tests for the typed-protocols framework -- description: license: Apache-2.0 @@ -35,6 +35,16 @@ library , Network.TypedProtocol.ReqResp.Codec.CBOR , Network.TypedProtocol.ReqResp.Examples + , Network.TypedProtocol.ReqResp2.Type + , Network.TypedProtocol.ReqResp2.Client + + , Network.TypedProtocol.Stateful.ReqResp.Type + , Network.TypedProtocol.Stateful.ReqResp.Client + , Network.TypedProtocol.Stateful.ReqResp.Server + , Network.TypedProtocol.Stateful.ReqResp.Codec + , Network.TypedProtocol.Stateful.ReqResp.Examples + + , Network.TypedProtocol.Trans.Wedge other-extensions: GADTs , RankNTypes , PolyKinds @@ -47,12 +57,15 @@ library bytestring, cborg, serialise, + singletons, contra-tracer, io-classes, si-timers, + network, time, - typed-protocols, - typed-protocols-cborg + typed-protocols ^>= 0.2, + typed-protocols-cborg, + typed-protocols-stateful hs-source-dirs: src default-language: Haskell2010 @@ -83,6 +96,12 @@ test-suite test , QuickCheck , tasty , tasty-quickcheck + + if !os(windows) + build-depends: directory + , network + , unix + default-language: Haskell2010 ghc-options: -rtsopts -Wall diff --git a/typed-protocols-stateful-cborg/ChangeLog.md b/typed-protocols-stateful-cborg/ChangeLog.md new file mode 100644 index 00000000..adaf4516 --- /dev/null +++ b/typed-protocols-stateful-cborg/ChangeLog.md @@ -0,0 +1,6 @@ +# Revision history for typed-protocols-cborg + +## 0.1.0.0 -- 2021-07-28 + +* Initial experiments and prototyping + diff --git a/typed-protocols-stateful-cborg/LICENSE b/typed-protocols-stateful-cborg/LICENSE new file mode 100644 index 00000000..f433b1a5 --- /dev/null +++ b/typed-protocols-stateful-cborg/LICENSE @@ -0,0 +1,177 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS diff --git a/typed-protocols-stateful-cborg/NOTICE b/typed-protocols-stateful-cborg/NOTICE new file mode 100644 index 00000000..d027fe3c --- /dev/null +++ b/typed-protocols-stateful-cborg/NOTICE @@ -0,0 +1,14 @@ +Copyright 2022-2024 Input Output Global Inc (IOG) + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + diff --git a/typed-protocols-stateful-cborg/README.md b/typed-protocols-stateful-cborg/README.md new file mode 100644 index 00000000..16b89de2 --- /dev/null +++ b/typed-protocols-stateful-cborg/README.md @@ -0,0 +1,6 @@ +typed-protocols-stateful-cborg +============================== + +[CBOR](https://hackage.haskell.org/package/cborg) codecs for +[typed-protocols-stateful](https://input-output-hk.github.io/ouroboros-network/typed-protocols/Network-TypedProtocol-Stateful-Peer.html) +package. diff --git a/typed-protocols-stateful-cborg/src/Network/TypedProtocol/Stateful/Codec/CBOR.hs b/typed-protocols-stateful-cborg/src/Network/TypedProtocol/Stateful/Codec/CBOR.hs new file mode 100644 index 00000000..6b159ced --- /dev/null +++ b/typed-protocols-stateful-cborg/src/Network/TypedProtocol/Stateful/Codec/CBOR.hs @@ -0,0 +1,133 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE MonoLocalBinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} + +module Network.TypedProtocol.Stateful.Codec.CBOR + ( module Network.TypedProtocol.Stateful.Codec + , DeserialiseFailure + , mkCodecCborLazyBS + , mkCodecCborStrictBS + ) where + +import Control.Monad.Class.MonadST (MonadST (..)) + +import Codec.CBOR.Decoding qualified as CBOR (Decoder) +import Codec.CBOR.Encoding qualified as CBOR (Encoding) +import Codec.CBOR.Read qualified as CBOR +import Codec.CBOR.Write qualified as CBOR +import Data.ByteString qualified as BS +import Data.ByteString.Builder qualified as BS +import Data.ByteString.Builder.Extra qualified as BS +import Data.ByteString.Lazy qualified as LBS +import Data.ByteString.Lazy.Internal qualified as LBS (smallChunkSize) + +import Network.TypedProtocol.Stateful.Codec +import Network.TypedProtocol.Codec.CBOR (DeserialiseFailure, + convertCborDecoderBS, convertCborDecoderLBS) +import Network.TypedProtocol.Core + + +-- | Construct a 'Codec' for a CBOR based serialisation format, using strict +-- 'BS.ByteString's. +-- +-- This is an adaptor between the @cborg@ library and the 'Codec' abstraction. +-- +-- It takes encode and decode functions for the protocol messages that use the +-- CBOR library encoder and decoder. +-- +-- Note that this is /less/ efficient than the 'mkCodecCborLazyBS' variant +-- because it has to copy and concatenate the result of the encoder (which +-- natively produces chunks). +-- +mkCodecCborStrictBS + :: forall ps f m. MonadST m + + => (forall (st :: ps) (st' :: ps). + StateTokenI st + =>ActiveState st + => f st' -> Message ps st st' -> CBOR.Encoding) + -- ^ cbor encoder + + -> (forall (st :: ps) s. + ActiveState st + => StateToken st + -> f st + -> CBOR.Decoder s (SomeMessage st)) + -- ^ cbor decoder + + -> Codec ps DeserialiseFailure f m BS.ByteString +mkCodecCborStrictBS cborMsgEncode cborMsgDecode = + Codec { + encode = \f msg -> convertCborEncoder (cborMsgEncode f) msg, + decode = \stok f -> convertCborDecoder (cborMsgDecode stok f) + } + where + convertCborEncoder :: (a -> CBOR.Encoding) -> a -> BS.ByteString + convertCborEncoder cborEncode = + CBOR.toStrictByteString + . cborEncode + + convertCborDecoder + :: (forall s. CBOR.Decoder s a) + -> m (DecodeStep BS.ByteString DeserialiseFailure m a) + convertCborDecoder cborDecode = + convertCborDecoderBS cborDecode stToIO + +-- | Construct a 'Codec' for a CBOR based serialisation format, using lazy +-- 'BS.ByteString's. +-- +-- This is an adaptor between the @cborg@ library and the 'Codec' abstraction. +-- +-- It takes encode and decode functions for the protocol messages that use the +-- CBOR library encoder and decoder. +-- +mkCodecCborLazyBS + :: forall ps f m. MonadST m + + => (forall (st :: ps) (st' :: ps). + StateTokenI st + => ActiveState st + => f st' + -> Message ps st st' -> CBOR.Encoding) + -- ^ cbor encoder + + -> (forall (st :: ps) s. + ActiveState st + => StateToken st + -> f st + -> CBOR.Decoder s (SomeMessage st)) + -- ^ cbor decoder + + -> Codec ps CBOR.DeserialiseFailure f m LBS.ByteString +mkCodecCborLazyBS cborMsgEncode cborMsgDecode = + Codec { + encode = \f msg -> convertCborEncoder (cborMsgEncode f) msg, + decode = \stok f -> convertCborDecoder (cborMsgDecode stok f) + } + where + convertCborEncoder :: (a -> CBOR.Encoding) -> a -> LBS.ByteString + convertCborEncoder cborEncode = + toLazyByteString + . CBOR.toBuilder + . cborEncode + + convertCborDecoder + :: (forall s. CBOR.Decoder s a) + -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m a) + convertCborDecoder cborDecode = + convertCborDecoderLBS cborDecode stToIO + +{-# NOINLINE toLazyByteString #-} +toLazyByteString :: BS.Builder -> LBS.ByteString +toLazyByteString = BS.toLazyByteStringWith strategy LBS.empty + where + -- Buffer strategy and sizes better tuned to our network protocol situation. + -- + -- The LBS.smallChunkSize is 4k - heap object overheads, so that + -- it does fit in a 4k overall. + -- + strategy = BS.untrimmedStrategy 800 LBS.smallChunkSize + diff --git a/typed-protocols-stateful-cborg/typed-protocols-stateful-cborg.cabal b/typed-protocols-stateful-cborg/typed-protocols-stateful-cborg.cabal new file mode 100644 index 00000000..8894854d --- /dev/null +++ b/typed-protocols-stateful-cborg/typed-protocols-stateful-cborg.cabal @@ -0,0 +1,42 @@ +cabal-version: 3.0 +name: typed-protocols-stateful-cborg +version: 0.2.0.0 +synopsis: CBOR codecs for typed-protocols +-- description: +license: Apache-2.0 +license-files: + LICENSE + NOTICE +copyright: 2022-2024 Input Output Global Inc (IOG) +author: Marcin Szamotulski +maintainer: marcin.szamotulski@iohk.io +category: Control +build-type: Simple + +-- These should probably be added at some point. +extra-source-files: ChangeLog.md, README.md + +library + exposed-modules: Network.TypedProtocol.Stateful.Codec.CBOR + + build-depends: base >=4.12 && <4.21, + bytestring >=0.10 && <0.13, + cborg >=0.2.1 && <0.3, + singletons, + + io-classes, + typed-protocols, + typed-protocols-cborg, + typed-protocols-stateful + + hs-source-dirs: src + default-language: Haskell2010 + default-extensions: ImportQualifiedPost + ghc-options: -Wall + -Wno-unticked-promoted-constructors + -Wcompat + -Wincomplete-uni-patterns + -Wincomplete-record-updates + -Wpartial-fields + -Widentities + -Wredundant-constraints diff --git a/typed-protocols-stateful/LICENSE b/typed-protocols-stateful/LICENSE new file mode 100644 index 00000000..f433b1a5 --- /dev/null +++ b/typed-protocols-stateful/LICENSE @@ -0,0 +1,177 @@ + + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS diff --git a/typed-protocols-stateful/NOTICE b/typed-protocols-stateful/NOTICE new file mode 100644 index 00000000..d027fe3c --- /dev/null +++ b/typed-protocols-stateful/NOTICE @@ -0,0 +1,14 @@ +Copyright 2022-2024 Input Output Global Inc (IOG) + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. + diff --git a/typed-protocols-stateful/README.md b/typed-protocols-stateful/README.md new file mode 100644 index 00000000..4a9b66e8 --- /dev/null +++ b/typed-protocols-stateful/README.md @@ -0,0 +1,6 @@ +typed-protocols-stateful +======================== + +A stateful `typed-protocols` version which allows to track state changes along +side protocol transtions. It allows to build codes depends on the current +state. diff --git a/typed-protocols-stateful/src/Network/TypedProtocol.hs b/typed-protocols-stateful/src/Network/TypedProtocol.hs new file mode 100644 index 00000000..b79a0aec --- /dev/null +++ b/typed-protocols-stateful/src/Network/TypedProtocol.hs @@ -0,0 +1,134 @@ + +-- | This package defines the typed protocol framework. This module re-exports +-- the public API. +-- +module Network.TypedProtocol + ( -- * Introduction + -- $intro + -- * Defining and implementing protocols + -- $defining + module Network.TypedProtocol.Core + -- ** Protocol proofs and tests + -- $tests + , module Network.TypedProtocol.Proofs + -- * Running protocols + -- $running + , module Network.TypedProtocol.Driver + ) where + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Driver +import Network.TypedProtocol.Proofs + + +-- $intro +-- +-- The typed protocol framework is used to define, test and execute protocols. +-- +-- It guarantees: +-- +-- * agreement on which messages can be sent and received; +-- * the absence of race conditions; and +-- * the absence of deadlock. +-- +-- The trade-off to achieve these guarantees is that it places constraints on +-- the kinds of protocol that can be expressed. In particular it requires that +-- protocols be defined as a state transition system. It requires for each +-- protocol state that exactly one of the two peers be able to send and the +-- other must be ready to receive. +-- +-- This means it is not possible to express protocols such as TCP where there +-- are protocol states where a single peer can both send and receive, however +-- it is suitable for most application-level protocols. In particular many +-- application-level protocols are completely in-order and synchronous. That +-- said, in many (but not all) cases it is possible to pipeline these protocols +-- so that network latency can be hidden and full use made of the available +-- bandwidth. Special support is provided to run protocols in a pipelined way, +-- without having to change the protocol definition. +-- +-- The protocols in this framework assume an underlying \"reliable ordered\" +-- connection. A \"reliable ordered\" connection is a term of art meaning one +-- where the receiving end receives any prefix of the messages sent by the +-- sending end. It is not reliable in the colloquial sense as it does not +-- ensure that anything actually arrives, only that /if/ any message arrives, +-- all the previous messages did too, and that they arrive in the order in +-- which they were sent. +-- +-- The framework also provides: +-- +-- * an abstraction for untyped channels; +-- * a codec abstraction for encoding and decoding protocol messages; and +-- * drivers for running protocol peers with a channel and a codec. + + +-- $defining +-- +-- The "Network.TypedProtocol.Core" module defines the core of the system. +-- +-- Start reading here to understand: +-- +-- * how to define new protocols; or +-- * to write peers that engage in a protocol. +-- +-- Typed protocol messages need to be converted to and from untyped +-- serialised forms to send over a transport channel. So part of defining a new +-- protocol is to define the message encoding and the codec for doing the +-- encoding and decoding. This is somewhat (but not significantly) more complex +-- than defining normal data type serialisation because of the need to decode +-- typed protocol messages. The "Network.TypedProtocol.Codec" module provides +-- the codec abstraction to capture this. + + +-- $tests +-- +-- There are a few proofs about the framework that we can state and implement +-- as Haskell functions (using GADTs and evaluation). A couple of these proofs +-- rely on a few lemmas that should be proved for each protocol. The +-- "Network.TypedProtocol.Proofs" module describes these proof and provides +-- the infrastructure for the simple lemmas that need to be implemented for +-- each protocol. +-- +-- This module also provides utilities helpful for testing protocols. + + +-- $running +-- +-- Typed protocols need to be able to send messages over untyped transport +-- channels. The "Network.TypedProtocol.Channel" module provides such an +-- abstraction. You can use existing example implementations of this interface +-- or define your own to run over other transports. +-- +-- Given a protocol peer, and a channel and a codec we can run the protocol +-- peer so that it engages in the protocol sending and receiving messages +-- over the channel. The "Network.TypedProtocol.Driver" module provides drivers +-- for normal and pipelined peers. + + +-- $pipelining +-- Protocol pipelining is a technique to make effective use of network +-- resources. +-- +-- <> +-- +-- As in the above diagram, instead of sending a request and waiting for the +-- response before sending the next request, pipelining involves sending all +-- three requests back-to-back and waiting for the three replies. The server +-- still simply processes the requests in order and the replies come back in +-- the same order as the requests were made. +-- +-- Not only does this save network latency, one round trip versus three in +-- the diagram above, but it also makes effective use of the bandwidth by +-- sending requests and replies back-to-back. +-- +-- In the example in the diagram it stops after three requests, but such a +-- pattern can go on indefinately with messages going in both directions, +-- which can saturate the available bandwidth. +-- +-- For many (but not all) protocols that can be defined in the @typed-protocol@ +-- framework it is possible to take the protocol, without changing the +-- protocol's state machine, and to engage in the protocol in a pipelined way. +-- Only the pipelined client has to be written specially. The server side can +-- be used unaltered and can be used with either pipelined or non-pipelined +-- clients. + + diff --git a/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Codec.hs b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Codec.hs new file mode 100644 index 00000000..27f47e6a --- /dev/null +++ b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Codec.hs @@ -0,0 +1,285 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE ViewPatterns #-} +-- @UndecidableInstances@ extension is required for defining @Show@ instance of +-- @'AnyMessage'@ and @'AnyMessage'@. +{-# LANGUAGE UndecidableInstances #-} +{-# OPTIONS_GHC -Wno-dodgy-imports #-} + +-- | Stateful codec. This module is intended to be imported qualified. +-- +module Network.TypedProtocol.Stateful.Codec + ( -- * Defining and using Codecs + Codec (..) + , hoistCodec + , isoCodec + , mapFailureCodec + , liftCodec + -- ** Incremental decoding + , DecodeStep (..) + , runDecoder + , runDecoderPure + -- ** Related types + -- *** SomeMessage + , SomeMessage (..) + -- *** StateToken + , StateToken + , StateTokenI (..) + -- *** ActiveState + , ActiveState + -- *** PeerRole + , PeerRole (..) + -- * CodecFailure + , CodecFailure (..) + -- * Testing codec properties + , AnyMessage (..) + , pattern AnyMessageAndAgency + , prop_codecM + , prop_codec + , prop_codec_splitsM + , prop_codec_splits + , prop_codecs_compatM + , prop_codecs_compat + ) where + +import Data.Kind (Type) +import Data.Monoid (All (..)) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Codec (CodecFailure (..), + DecodeStep (..), SomeMessage (..), hoistDecodeStep, + isoDecodeStep, mapFailureDecodeStep, runDecoder, + runDecoderPure) +import qualified Network.TypedProtocol.Codec as TP + + +-- | A stateful codec. +-- +data Codec ps failure (f :: ps -> Type) m bytes = Codec { + encode :: forall (st :: ps) (st' :: ps). + StateTokenI st + => ActiveState st + => f st' + -> Message ps st st' + -> bytes, + + decode :: forall (st :: ps). + ActiveState st + => StateToken st + -> f st + -> m (DecodeStep bytes failure m (SomeMessage st)) + } + +liftCodec :: TP.Codec ps failure m bytes -> Codec ps failure f m bytes +liftCodec codec = Codec { encode = \_ msg -> TP.encode codec msg + , decode = \stok _ -> TP.decode codec stok + } + +hoistCodec + :: ( Functor n ) + => (forall x . m x -> n x) + -> Codec ps failure f m bytes + -> Codec ps failure f n bytes +hoistCodec nat codec = codec + { decode = \stok f -> fmap (hoistDecodeStep nat) . nat $ decode codec stok f + } + +isoCodec :: Functor m + => (bytes -> bytes') + -> (bytes' -> bytes) + -> Codec ps failure f m bytes + -> Codec ps failure f m bytes' +isoCodec g finv Codec {encode, decode} = Codec { + encode = \f msg -> g $ encode f msg, + decode = \stok f -> isoDecodeStep g finv <$> decode stok f + } + +mapFailureCodec + :: Functor m + => (failure -> failure') + -> Codec ps failure f m bytes + -> Codec ps failure' f m bytes +mapFailureCodec g Codec {encode, decode} = Codec { + encode = encode, + decode = \stok f -> mapFailureDecodeStep g <$> decode stok f + } + + +-- +-- Codec properties +-- + +-- | Any message for a protocol, with a 'StateTokenI' constraint which gives access +-- to protocol state. +-- +-- Used where we don't know statically what the state type is, but need the +-- agency and message to match each other. +-- +data AnyMessage ps (f :: ps -> Type) where + AnyMessage :: forall ps f (st :: ps) (st' :: ps). + ( StateTokenI st + , ActiveState st + ) + => f st + -> f st' + -> Message ps (st :: ps) (st' :: ps) + -> AnyMessage ps f + +instance ( forall (st :: ps) (st' :: ps). Show (Message ps st st') + , forall (st :: ps). Show (f st) + ) + => Show (AnyMessage ps f) where + show (AnyMessage st st' msg) = concat [ "AnyMessage " + , show st + , " " + , show st' + , " " + , show msg + ] + + + +-- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the +-- singleton for the state and the message. +-- +pattern AnyMessageAndAgency :: forall ps f. () + => forall (st :: ps) (st' :: ps). + (StateTokenI st, ActiveState st) + => StateToken st + -> f st + -> f st' + -> Message ps st st' + -> AnyMessage ps f +pattern AnyMessageAndAgency stateToken f f' msg <- AnyMessage f f' (getAgency -> (msg, stateToken)) + where + AnyMessageAndAgency _ msg = AnyMessage msg +{-# COMPLETE AnyMessageAndAgency #-} + +-- | Internal view pattern for 'AnyMessageAndAgency' +-- +getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateToken st) +getAgency msg = (msg, stateToken) + +-- | The 'Codec' round-trip property: decode after encode gives the same +-- message. Every codec must satisfy this property. +-- +prop_codecM + :: forall ps failure f m bytes. + ( Monad m + , Eq (TP.AnyMessage ps) + ) + => Codec ps failure f m bytes + -> AnyMessage ps f + -> m Bool +prop_codecM Codec {encode, decode} (AnyMessage f f' (msg :: Message ps st st')) = do + r <- decode (stateToken :: StateToken st) f >>= runDecoder [encode f' msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ TP.AnyMessage msg' == TP.AnyMessage msg + Left _ -> return False + +-- | The 'Codec' round-trip property in a pure monad. +-- +prop_codec + :: forall ps failure f m bytes. + (Monad m, Eq (TP.AnyMessage ps)) + => (forall a. m a -> a) + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Bool +prop_codec runM codec msg = + runM (prop_codecM codec msg) + + +-- | A variant on the codec round-trip property: given the encoding of a +-- message, check that decode always gives the same result irrespective +-- of how the chunks of input are fed to the incremental decoder. +-- +-- This property guards against boundary errors in incremental decoders. +-- It is not necessary to check this for every message type, just for each +-- generic codec construction. For example given some binary serialisation +-- library one would write a generic adaptor to the codec interface. This +-- adaptor has to deal with the incremental decoding and this is what needs +-- to be checked. +-- +prop_codec_splitsM + :: forall ps failure f m bytes. + (Monad m, Eq (TP.AnyMessage ps)) + => (bytes -> [[bytes]]) -- ^ alternative re-chunkings of serialised form + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> m Bool +prop_codec_splitsM splits + Codec {encode, decode} (AnyMessage f f' (msg :: Message ps st st')) = do + and <$> sequence + [ do r <- decode (stateToken :: StateToken st) f >>= runDecoder bytes' + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ TP.AnyMessage msg' == TP.AnyMessage msg + Left _ -> return False + + | let bytes = encode f' msg + , bytes' <- splits bytes ] + + +-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codec_splits + :: forall ps failure f m bytes. + (Monad m, Eq (TP.AnyMessage ps)) + => (bytes -> [[bytes]]) + -> (forall a. m a -> a) + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Bool +prop_codec_splits splits runM codec msg = + runM $ prop_codec_splitsM splits codec msg + + +-- | Compatibility between two codecs of the same protocol. Encode a message +-- with one codec and decode it with the other one, then compare if the result +-- is the same as initial message. +-- +prop_codecs_compatM + :: forall ps failure f m bytes. + ( Monad m + , Eq (TP.AnyMessage ps) + , forall a. Monoid a => Monoid (m a) + ) + => Codec ps failure f m bytes + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> m Bool +prop_codecs_compatM codecA codecB + (AnyMessage f f' (msg :: Message ps st st')) = + getAll <$> do r <- decode codecB (stateToken :: StateToken st) f >>= runDecoder [encode codecA f' msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ All $ TP.AnyMessage msg' == TP.AnyMessage msg + Left _ -> return $ All False + <> do r <- decode codecA (stateToken :: StateToken st) f >>= runDecoder [encode codecB f' msg] + case r :: Either failure (SomeMessage st) of + Right (SomeMessage msg') -> return $ All $ TP.AnyMessage msg' == TP.AnyMessage msg + Left _ -> return $ All False + +-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@. +-- +prop_codecs_compat + :: forall ps failure f m bytes. + ( Monad m + , Eq (TP.AnyMessage ps) + , forall a. Monoid a => Monoid (m a) + ) + => (forall a. m a -> a) + -> Codec ps failure f m bytes + -> Codec ps failure f m bytes + -> AnyMessage ps f + -> Bool +prop_codecs_compat run codecA codecB msg = + run $ prop_codecs_compatM codecA codecB msg diff --git a/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Driver.hs b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Driver.hs new file mode 100644 index 00000000..8719e412 --- /dev/null +++ b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Driver.hs @@ -0,0 +1,102 @@ +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +-- | Actions for running 'Peer's with a 'Driver'. This module should be +-- imported qualified. +-- +module Network.TypedProtocol.Stateful.Driver + ( -- * DriverIngerface + Driver (..) + -- * Running a peer + , runPeerWithDriver + -- * Re-exports + , SomeMessage (..) + , DecodeStep (..) + ) where + +import Control.Monad.Class.MonadSTM + +import Data.Kind (Type) + +import Network.TypedProtocol.Codec (DecodeStep (..), SomeMessage (..)) +import Network.TypedProtocol.Core +import Network.TypedProtocol.Stateful.Peer + +data Driver ps (pr :: PeerRole) bytes failure dstate f m = + Driver { + -- | Send a message. + -- + sendMessage :: forall (st :: ps) (st' :: ps). + StateTokenI st + => StateTokenI st' + => ActiveState st + => ReflRelativeAgency (StateAgency st) + WeHaveAgency + (Relative pr (StateAgency st)) + -> f st' + -> Message ps st st' + -> m () + + , -- | Receive a message, a blocking action which reads from the network + -- and runs the incremental decoder until a full message is decoded. + -- + recvMessage :: forall (st :: ps). + StateTokenI st + => ActiveState st + => ReflRelativeAgency (StateAgency st) + TheyHaveAgency + (Relative pr (StateAgency st)) + -> f st + -> dstate + -> m (SomeMessage st, dstate) + + , initialDState :: dstate + } + + +-- +-- Running peers +-- + +-- | Run a peer with the given driver. +-- +-- This runs the peer to completion (if the protocol allows for termination). +-- +runPeerWithDriver + :: forall ps (st :: ps) pr bytes failure dstate (f :: ps -> Type) m a. + MonadSTM m + => Driver ps pr bytes failure dstate f m + -> f st + -> Peer ps pr st f m a + -> m (a, dstate) +runPeerWithDriver Driver{ sendMessage + , recvMessage + , initialDState + } = + go initialDState + where + go :: forall st'. + dstate + -> f st' + -> Peer ps pr st' f m a + -> m (a, dstate) + go !dstate !f (Effect k) = k >>= go dstate f + + go !dstate _ (Done _ x) = return (x, dstate) + + go !dstate _ (Yield refl !f msg k) = do + sendMessage refl f msg + go dstate f k + + go !dstate !f (Await refl k) = do + (SomeMessage msg, dstate') <- recvMessage refl f dstate + case k f msg of + (k', f') -> go dstate' f' k' diff --git a/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer.hs b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer.hs new file mode 100644 index 00000000..e228910c --- /dev/null +++ b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer.hs @@ -0,0 +1,178 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeOperators #-} +-- TODO: the 'Functor' instance of 'Peer' is undecidable +{-# LANGUAGE UndecidableInstances #-} + +-- | Protocol stateful EDSL. +-- +-- __Note__: 'Network.TypedProtocol.Peer.Client.Client' and +-- 'Network.TypedProtocol.Peer.Server.Server' patterns are easier to use. +-- +module Network.TypedProtocol.Stateful.Peer + ( Peer (..) + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core as Core + + +-- | A description of a peer that engages in a protocol. +-- +-- The protocol describes what messages peers /may/ send or /must/ accept. +-- A particular peer implementation decides what to actually do within the +-- constraints of the protocol. +-- +-- Peers engage in a protocol in either the client or server role. Of course +-- the client role can only interact with the serve role for the same protocol +-- and vice versa. +-- +-- 'Peer' has several type arguments: +-- +-- * the protocol itself; +-- * the client\/server role; +-- *.the current protocol state; +-- * the monad in which the peer operates; and +-- * the type of any final result once the peer terminates. +-- +-- For example: +-- +-- > pingPongClientExample :: Peer PingPong AsClient StIdle m () +-- > pingPongServerExample :: Peer PingPong AsServer StIdle m Int +-- +-- The actions that a peer can take are: +-- +-- * to perform local monadic effects +-- * to terminate with a result (but only in a terminal protocol state) +-- * to send a message (but only in a protocol state in which we have agency) +-- * to wait to receive a message (but only in a protocol state in which the +-- other peer has agency) +-- +-- The 'Yield', 'Await' and 'Done' constructors require to provide an evidence +-- that the appropriate peer has agency. This information is supplied using +-- one of the constructors of 'ReflRelativeAgency'. +-- +-- While this evidence must be provided, the types guarantee that it is not +-- possible to supply incorrect evidence. The +-- 'Network.TypedProtocol.Peer.Client' or 'Network.TypedProtocol.Peer.Server' +-- pattern synonyms provide this evidence automatically. +-- +-- TODO: +-- We are not exposing pipelined version, since it is not possible to write +-- a driver & proofs in a type safe which take into account the state when the +-- peer type only tracks depth of pipelining rather than pipelined transitions. +-- +type Peer :: forall ps + -> PeerRole + -> ps + -> (ps -> Type) + -- ^ protocol state + -> (Type -> Type) + -- ^ monad's kind + -> Type + -> Type +data Peer ps pr st f m a where + + -- | Perform a local monadic effect and then continue. + -- + -- Example: + -- + -- > Effect $ do + -- > ... -- actions in the monad + -- > return $ ... -- another Peer value + -- + Effect + :: forall ps pr st f m a. + m (Peer ps pr st f m a) + -- ^ monadic continuation + -> Peer ps pr st f m a + + -- | Send a message to the other peer and then continue. This takes the + -- message and the continuation. It also requires evidence that we have + -- agency for this protocol state and thus are allowed to send messages. + -- + -- Example: + -- + -- > Yield ReflClientAgency MsgPing $ ... + -- + Yield + :: forall ps pr (st :: ps) (st' :: ps) f m a. + ( StateTokenI st + , StateTokenI st' + , ActiveState st + ) + => WeHaveAgencyProof pr st + -- ^ agency singleton + -> f st' + -- ^ protocol state + -> Message ps st st' + -- ^ protocol message + -> Peer ps pr st' f m a + -- ^ continuation + -> Peer ps pr st f m a + + -- | Waits to receive a message from the other peer and then continues. + -- This takes the continuation that is supplied with the received message. It + -- also requires evidence that the other peer has agency for this protocol + -- state and thus we are expected to wait to receive messages. + -- + -- Note that the continuation that gets supplied with the message must be + -- prepared to deal with /any/ message that is allowed in /this/ protocol + -- state. This is why the continuation /must/ be polymorphic in the target + -- state of the message (the third type argument of 'Message'). + -- + -- Example: + -- + -- > Await ReflClientAgency $ \msg -> + -- > case msg of + -- > MsgDone -> ... + -- > MsgPing -> ... + -- + Await + :: forall ps pr (st :: ps) f m a. + ( StateTokenI st + , ActiveState st + ) + => TheyHaveAgencyProof pr st + -- ^ agency singleton + -> (forall (st' :: ps). + f st + -> Message ps st st' + -> ( Peer ps pr st' f m a + , f st' + ) + ) + -- ^ continuation + -> Peer ps pr st f m a + + -- | Terminate with a result. A state token must be provided from the + -- 'NobodyHasAgency' states, to show that this is a state in which we can + -- terminate. + -- + -- Example: + -- + -- > Yield ReflClientAgency + -- > MsgDone + -- > (Done ReflNobodyAgency TokDone result) + -- + Done + :: forall ps pr (st :: ps) f m a. + ( StateTokenI st + , StateAgency st ~ NobodyAgency + ) + => NobodyHasAgencyProof pr st + -- ^ (no) agency proof + -> a + -- ^ returned value + -> Peer ps pr st f m a + +deriving instance Functor m => Functor (Peer ps pr st f m) diff --git a/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer/Client.hs b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer/Client.hs new file mode 100644 index 00000000..5140c16e --- /dev/null +++ b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer/Client.hs @@ -0,0 +1,98 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +-- | Bidirectional patterns for @'Peer' ps 'AsClient'@. The advantage of +-- these patterns is that they automatically provide the 'RelativeAgencyEq' +-- singleton. +-- +module Network.TypedProtocol.Stateful.Peer.Client + ( -- * Client type alias and its pattern synonyms + Client + , pattern Effect + , pattern Yield + , pattern Await + , pattern Done + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Stateful.Peer (Peer) +import qualified Network.TypedProtocol.Stateful.Peer as TP + + +type Client :: forall ps + -> ps + -> (ps -> Type) + -> (Type -> Type) + -> Type + -> Type +type Client ps st f m a = Peer ps AsClient st f m a + + +-- | Client role pattern for 'TP.Effect'. +-- +pattern Effect :: forall ps st f m a. + m (Client ps st f m a) + -- ^ monadic continuation + -> Client ps st f m a +pattern Effect mclient = TP.Effect mclient + + +-- | Client role pattern for 'TP.Yield' +-- +pattern Yield :: forall ps st f m a. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ClientAgency + ) + => f st' + -> Message ps st st' + -- ^ protocol message + -> Client ps st' f m a + -- ^ continuation + -> Client ps st f m a +pattern Yield f msg k = TP.Yield ReflClientAgency f msg k + + +-- | Client role pattern for 'TP.Await' +-- +pattern Await :: forall ps st f m a. + () + => ( StateTokenI st + , StateAgency st ~ ServerAgency + ) + => (forall st'. + f st + -> Message ps st st' + -> ( Client ps st' f m a + , f st' + ) + ) + -- ^ continuation + -> Client ps st f m a +pattern Await k = TP.Await ReflServerAgency k + + +-- | Client role pattern for 'TP.Done' +-- +pattern Done :: forall ps st f m a. + () + => ( StateTokenI st + , StateAgency st ~ NobodyAgency + ) + => a + -- ^ protocol return value + -> Client ps st f m a +pattern Done a = TP.Done ReflNobodyAgency a + + +{-# COMPLETE Effect, Yield, Await, Done #-} diff --git a/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer/Server.hs b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer/Server.hs new file mode 100644 index 00000000..a1fbc9c8 --- /dev/null +++ b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Peer/Server.hs @@ -0,0 +1,97 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +-- | Bidirectional patterns for @'Peer' ps 'AsServer'@. The advantage of +-- these patterns is that they automatically provide the 'RelativeAgencyEq' +-- singleton. +-- +module Network.TypedProtocol.Stateful.Peer.Server + ( -- * Server type alias and its pattern synonyms + Server + , pattern Effect + , pattern Yield + , pattern Await + , pattern Done + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Stateful.Peer (Peer) +import qualified Network.TypedProtocol.Stateful.Peer as TP + + +type Server :: forall ps + -> ps + -> (ps -> Type) + -> (Type -> Type) + -> Type + -> Type +type Server ps st f m a = Peer ps AsServer st f m a + + +-- | Server role pattern for 'TP.Effect'. +-- +pattern Effect :: forall ps st f m a. + m (Server ps st f m a) + -- ^ monadic continuation + -> Server ps st f m a +pattern Effect mclient = TP.Effect mclient + + +-- | Server role pattern for 'TP.Yield' +-- +pattern Yield :: forall ps st f m a. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ServerAgency + ) + => f st' + -> Message ps st st' + -- ^ protocol message + -> Server ps st' f m a + -- ^ continuation + -> Server ps st f m a +pattern Yield f msg k = TP.Yield ReflServerAgency f msg k + + +-- | Server role pattern for 'TP.Await' +-- +pattern Await :: forall ps st f m a. + () + => ( StateTokenI st + , StateAgency st ~ ClientAgency + ) + => (forall st'. + f st + -> Message ps st st' + -> ( Server ps st' f m a + , f st' + ) + ) + -- ^ continuation + -> Server ps st f m a +pattern Await k = TP.Await ReflClientAgency k + + +-- | Server role pattern for 'TP.Done' +-- +pattern Done :: forall ps st f m a. + () + => ( StateTokenI st + , StateAgency st ~ NobodyAgency + ) + => a + -- ^ protocol return value + -> Server ps st f m a +pattern Done a = TP.Done ReflNobodyAgency a + +{-# COMPLETE Effect, Yield, Await, Done #-} diff --git a/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Proofs.hs b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Proofs.hs new file mode 100644 index 00000000..e91b399e --- /dev/null +++ b/typed-protocols-stateful/src/Network/TypedProtocol/Stateful/Proofs.hs @@ -0,0 +1,82 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} + + +-- This is already implied by the -Wall in the .cabal file, but lets just be +-- completely explicit about it too, since we rely on the completeness +-- checking in the cases below for the completeness of our proofs. +{-# OPTIONS_GHC -Wincomplete-patterns #-} + +-- | Proofs about the typed protocol framework. +-- +-- It also provides helpful testing utilities. +-- +module Network.TypedProtocol.Stateful.Proofs + ( connect + , TerminalStates (..) + , removeState + ) where + +import Control.Monad.Class.MonadSTM + +import Data.Kind (Type) +import Data.Singletons + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Stateful.Peer qualified as ST +import Network.TypedProtocol.Peer +import Network.TypedProtocol.Proofs (TerminalStates (..)) +import Network.TypedProtocol.Proofs qualified as TP + + + +-- | Remove state for non-pipelined peers. +-- +-- TODO: There's a difficulty to write `removeState` for pipelined peers which +-- is type safe. The `Peer` doesn't track all pipelined transitions, just the +-- depth of pipelining, so we cannot push `f st` to a queue which type is +-- linked to `Peer`. For a similar reason there's no way to write +-- `forgetPipelined` function. +-- +-- However, this is possible if `Peer` tracks all transitions. +-- +removeState + :: Functor m + => f st + -> ST.Peer ps pr st f m a + -> Peer ps pr NonPipelined st m a +removeState = go + where + go + :: forall ps (pr :: PeerRole) + (st :: ps) + (f :: ps -> Type) + m a. + Functor m + => f st + -> ST.Peer ps pr st f m a + -> Peer ps pr NonPipelined st m a + go f (ST.Effect k) = Effect (go f <$> k) + go _ (ST.Yield refl f msg k) = Yield refl msg (go f k) + go f (ST.Await refl k) = Await refl $ \msg -> + case k f msg of + (k', f') -> go f' k' + go _ (ST.Done refl a) = Done refl a + + +connect + :: forall ps (pr :: PeerRole) + (st :: ps) + (f :: ps -> Type) + m a b. + (MonadSTM m, SingI pr) + => f st + -> ST.Peer ps pr st f m a + -> ST.Peer ps (FlipAgency pr) st f m b + -> m (a, b, TerminalStates ps) +connect f a b = TP.connect (removeState f a) (removeState f b) diff --git a/typed-protocols-stateful/typed-protocols-stateful.cabal b/typed-protocols-stateful/typed-protocols-stateful.cabal new file mode 100644 index 00000000..1edcc1d4 --- /dev/null +++ b/typed-protocols-stateful/typed-protocols-stateful.cabal @@ -0,0 +1,52 @@ +name: typed-protocols-stateful +version: 0.2.0.0 +synopsis: A framework for strongly typed protocols +-- description: +license: Apache-2.0 +license-files: + LICENSE + NOTICE +copyright: 2022-2024 Input Output Global Inc (IOG) +author: Marcin Szamotulski +maintainer: marcin.szamotulski@iohk.io +category: Control +build-type: Simple + +-- These should probably be added at some point. +-- extra-source-files: ChangeLog.md, README.md + +cabal-version: >=1.10 + +library + exposed-modules: Network.TypedProtocol.Stateful.Peer + , Network.TypedProtocol.Stateful.Peer.Client + , Network.TypedProtocol.Stateful.Peer.Server + , Network.TypedProtocol.Stateful.Driver + , Network.TypedProtocol.Stateful.Proofs + , Network.TypedProtocol.Stateful.Codec + + other-extensions: GADTs + , RankNTypes + , PolyKinds + , DataKinds + , ScopedTypeVariables + , TypeFamilies + , TypeOperators + , BangPatterns + default-extensions: ImportQualifiedPost + build-depends: base, + contra-tracer, + singletons >= 3.0, + io-classes, + typed-protocols + + hs-source-dirs: src + default-language: Haskell2010 + ghc-options: -Wall + -Wno-unticked-promoted-constructors + -Wcompat + -Wincomplete-uni-patterns + -Wincomplete-record-updates + -Wpartial-fields + -Widentities + -Wredundant-constraints diff --git a/typed-protocols/CHANGELOG.md b/typed-protocols/CHANGELOG.md index 59c0ee18..8ad6716b 100644 --- a/typed-protocols/CHANGELOG.md +++ b/typed-protocols/CHANGELOG.md @@ -1,6 +1,24 @@ # Revision history for typed-protocols +## [Unreleased] + +- A major redesign of `typed-protocols`. `Protocol` class requires data family + `Message` and new associated type familiy instance `StateAgency`. One also + needs to define singletons and `Sing` & `SingI` instances from the + [`singletons`][singletons-3.0.1] package. + ## 0.1.1.1 * unbuildable (with `base < 0` constraint in CHaP); We cannot support `io-classes-1.{6,7}` until `Haskell.Nix` support for public sublibraries is merged. + +## 0.1.0.7 -- 2023-10-20 + +* Improved performance of `prop_codecs_splitsM` and `prop_codecs_compatM`. + +## 0.1.0.5 -- 2023-03-08 + +* Support `ghc-9.6.1`. +* Use `io-classes-1.1.0.0`. + +[singletons-3.0.1]: https://hackage.haskell.org/package/singletons diff --git a/typed-protocols/src/Network/TypedProtocol.hs b/typed-protocols/src/Network/TypedProtocol.hs index f88fe39f..b79a0aec 100644 --- a/typed-protocols/src/Network/TypedProtocol.hs +++ b/typed-protocols/src/Network/TypedProtocol.hs @@ -14,14 +14,10 @@ module Network.TypedProtocol -- * Running protocols -- $running , module Network.TypedProtocol.Driver - -- * Pipelining protocols - -- $pipelining - , module Network.TypedProtocol.Pipelined ) where import Network.TypedProtocol.Core import Network.TypedProtocol.Driver -import Network.TypedProtocol.Pipelined import Network.TypedProtocol.Proofs diff --git a/typed-protocols/src/Network/TypedProtocol/Codec.hs b/typed-protocols/src/Network/TypedProtocol/Codec.hs index 2d548395..50be7f41 100644 --- a/typed-protocols/src/Network/TypedProtocol/Codec.hs +++ b/typed-protocols/src/Network/TypedProtocol/Codec.hs @@ -1,36 +1,52 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeFamilies #-} -- @UndecidableInstances@ extension is required for defining @Show@ instance of --- @'AnyMessage'@ and @'AnyMessageAndAgency'@. +-- @'AnyMessage'@ and @'AnyMessage'@. {-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE ViewPatterns #-} module Network.TypedProtocol.Codec ( -- * Defining and using Codecs + -- ** Codec type Codec (..) , hoistCodec , isoCodec , mapFailureCodec - -- ** Related types - , PeerRole (..) - , PeerHasAgency (..) - , WeHaveAgency - , TheyHaveAgency - , SomeMessage (..) - , CodecFailure (..) -- ** Incremental decoding , DecodeStep (..) , runDecoder , runDecoderPure - -- ** Codec properties + , hoistDecodeStep + , isoDecodeStep + , mapFailureDecodeStep + -- ** Related types + -- *** SomeMessage + , SomeMessage (..) + -- *** StateToken + , StateToken + , StateTokenI (..) + -- *** ActiveState + , IsActiveState (..) + , ActiveState + , ActiveAgency + , ActiveAgency' (..) + , notActiveState + -- *** PeerRole + , PeerRole (..) + -- * CodecFailure + , CodecFailure (..) + -- * Testing codec properties , AnyMessage (..) - , AnyMessageAndAgency (..) + , pattern AnyMessageAndAgency , prop_codecM , prop_codec , prop_codec_splitsM @@ -39,17 +55,17 @@ module Network.TypedProtocol.Codec , prop_codec_binary_compat , prop_codecs_compatM , prop_codecs_compat - , SamePeerHasAgency (..) + , SomeState (..) ) where import Control.Exception (Exception) import Data.Kind (Type) import Data.Monoid (All (..)) -import Network.TypedProtocol.Core (PeerHasAgency (..), PeerRole (..), - Protocol (..), TheyHaveAgency, WeHaveAgency) +import Network.TypedProtocol.Core import Network.TypedProtocol.Driver (SomeMessage (..)) + -- | A codec for a 'Protocol' handles the encoding and decoding of typed -- protocol messages. This is typically used when sending protocol messages -- over untyped channels. The codec chooses the exact encoding, for example @@ -58,17 +74,10 @@ import Network.TypedProtocol.Driver (SomeMessage (..)) -- The codec is parametrised by: -- -- * The protocol --- * The peer role (client\/server) -- * the type of decoding failures -- * the monad in which the decoder runs -- * the type of the encoded data (typically strings or bytes) -- --- It is expected that typical codec implementations will be polymorphic in --- the peer role. For example a codec for the ping\/pong protocol might have --- type: --- --- > codecPingPong :: forall m. Monad m => Codec PingPong String m String --- -- A codec consists of a message encoder and a decoder. -- -- The encoder is supplied both with the message to encode and the current @@ -79,12 +88,12 @@ import Network.TypedProtocol.Driver (SomeMessage (..)) -- -- For example a simple text encoder for the ping\/pong protocol could be: -- --- > encode :: WeHaveAgency pr st --- > -> Message PingPong st st' +-- > encode :: SingI st +-- > => Message PingPong st st' -- > -> String --- > encode (ClientAgency TokIdle) MsgPing = "ping\n" --- > encode (ClientAgency TokIdle) MsgDone = "done\n" --- > encode (ServerAgency TokBusy) MsgPong = "pong\n" +-- > encode MsgPing = "ping\n" +-- > encode MsgDone = "done\n" +-- > encode MsgPong = "pong\n" -- -- The decoder is also given the current protocol state and it is expected to -- be able to decode /any/ message that is valid in that state, but /only/ @@ -101,60 +110,79 @@ import Network.TypedProtocol.Driver (SomeMessage (..)) -- decoder allows but does not require a format with message framing where the -- decoder input matches exactly with the message boundaries. -- --- > decode :: TheyHaveAgency pr st +-- > decode :: forall st m. SingI st +-- > => StateToken st -- > -> m (DecodeStep String String m (SomeMessage st)) -- > decode stok = -- > decodeTerminatedFrame '\n' $ \str trailing -> -- > case (stok, str) of --- > (ServerAgency TokBusy, "pong") -> +-- > (SingBusy, "pong") -> -- > DecodeDone (SomeMessage MsgPong) trailing --- > (ClientAgency TokIdle, "ping") -> +-- > (SingIdle, "ping") -> -- > DecodeDone (SomeMessage MsgPing) trailing --- > (ClientAgency TokIdle, "done") -> +-- > (SingIdle, "done") -> -- > DecodeDone (SomeMessage MsgDone) trailing -- > _ -> DecodeFail ("unexpected message: " ++ str) -- --- The main thing to note is the pattern matching on the combination of the --- message string and the protocol state. This neatly fulfils the requirement --- that we only return messages that are of the correct type for the given --- protocol state. +-- See "typed-protocols-examples" for the full example. +-- +-- Note that the pattern matching on the combination of the message string and +-- the protocol state. This neatly fulfils the requirement that we only return +-- messages that are of the correct type for the given protocol state. -- -- This toy example format uses newlines @\n@ as a framing format. See -- 'DecodeStep' for suggestions on how to use it for more realistic formats. -- data Codec ps failure m bytes = Codec { - encode :: forall (pr :: PeerRole) (st :: ps) (st' :: ps). - PeerHasAgency pr st - -> Message ps st st' + encode :: forall (st :: ps) (st' :: ps). + StateTokenI st + => ActiveState st + -- evidence that the state 'st' is active + => Message ps st st' + -- message to encode -> bytes, - decode :: forall (pr :: PeerRole) (st :: ps). - PeerHasAgency pr st + decode :: forall (st :: ps). + ActiveState st + => StateToken st + -- evidence for an active state -> m (DecodeStep bytes failure m (SomeMessage st)) } +-- TODO: input-output-hk/typed-protocols#57 +-- | Change functor in which the codec is running. +-- hoistCodec :: ( Functor n ) => (forall x . m x -> n x) + -- ^ a natural transformation -> Codec ps failure m bytes -> Codec ps failure n bytes hoistCodec nat codec = codec { decode = fmap (hoistDecodeStep nat) . nat . decode codec } +-- | Change bytes of a codec. +-- isoCodec :: Functor m - => (bytes -> bytes') + => (bytes -> bytes') + -- ^ map from 'bytes' to `bytes'` -> (bytes' -> bytes) + -- ^ its inverse -> Codec ps failure m bytes + -- ^ codec -> Codec ps failure m bytes' isoCodec f finv Codec {encode, decode} = Codec { - encode = \tok msg -> f $ encode tok msg, + encode = \msg -> f $ encode msg, decode = \tok -> isoDecodeStep f finv <$> decode tok } +-- | Modify failure type. +-- mapFailureCodec :: Functor m => (failure -> failure') + -- ^ a function to apply to failure -> Codec ps failure m bytes -> Codec ps failure' m bytes mapFailureCodec f Codec {encode, decode} = Codec { @@ -162,16 +190,6 @@ mapFailureCodec f Codec {encode, decode} = Codec { decode = \tok -> mapFailureDecodeStep f <$> decode tok } --- The types here are pretty fancy. The decode is polymorphic in the protocol --- state, but only for kinds that are the same kind as the protocol state. --- The TheyHaveAgency is a type family that resolves to a singleton, and the --- result uses existential types to hide the unknown type of the state we're --- transitioning to. --- --- Both the Message and TheyHaveAgency data families are indexed on the kind ps --- which is why it has to be a parameter here, otherwise these type functions --- are unusable. - -- | An incremental decoder with return a value of type @a@. -- @@ -199,19 +217,28 @@ data DecodeStep bytes failure m a = -- @'fail'@ or was not provided enough input. | DecodeFail failure + +-- | Change bytes of 'DecodeStep'. +-- isoDecodeStep :: Functor m => (bytes -> bytes') + -- ^ map from 'bytes' to `bytes'` -> (bytes' -> bytes) + -- its inverse -> DecodeStep bytes failure m a -> DecodeStep bytes' failure m a isoDecodeStep f finv (DecodePartial g) = DecodePartial (fmap (isoDecodeStep f finv) . g . fmap finv) isoDecodeStep f _finv (DecodeDone a bytes) = DecodeDone a (fmap f bytes) isoDecodeStep _f _finv (DecodeFail failure) = DecodeFail failure + +-- | Change functor in which the codec is running. +-- hoistDecodeStep :: ( Functor n ) => (forall x . m x -> n x) + -- ^ a natural transformation -> DecodeStep bytes failure m a -> DecodeStep bytes failure n a hoistDecodeStep nat step = case step of @@ -219,9 +246,13 @@ hoistDecodeStep nat step = case step of DecodeFail fail_AvoidNameShadow -> DecodeFail fail_AvoidNameShadow DecodePartial k -> DecodePartial (fmap (hoistDecodeStep nat) . nat . k) + +-- | Modify failure type. +-- mapFailureDecodeStep :: Functor m => (failure -> failure') + -- ^ a function to apply to failure -> DecodeStep bytes failure m a -> DecodeStep bytes failure' m a mapFailureDecodeStep f step = case step of @@ -255,7 +286,9 @@ instance Exception CodecFailure -- runDecoder :: Monad m => [bytes] + -- ^ bytes to be fed into the incremental 'DecodeStep' -> DecodeStep bytes failure m a + -- ^ decoder -> m (Either failure a) runDecoder _ (DecodeDone x _trailing) = return (Right x) runDecoder _ (DecodeFail failure) = return (Left failure) @@ -268,8 +301,10 @@ runDecoder (b:bs) (DecodePartial k) = k (Just b) >>= runDecoder bs -- runDecoderPure :: Monad m => (forall b. m b -> b) + -- ^ run monad 'm' in a pure way, e.g. 'runIdentity' -> m (DecodeStep bytes failure m a) -> [bytes] + -- ^ input bytes -> Either failure a runDecoderPure runM decoder bs = runM (runDecoder bs =<< decoder) @@ -278,35 +313,48 @@ runDecoderPure runM decoder bs = runM (runDecoder bs =<< decoder) -- Codec properties -- --- | Any message for a protocol, without knowing the protocol state. +-- | Any message for a protocol, with a 'StateTokenI' constraint which gives access to +-- protocol state. -- --- Used at least for 'Eq' instances for messages, but also as a target for an --- identity codec `Codec ps failure m (AnyMessage ps)` . +-- Used where we don't know statically what the state type is, but need the +-- agency and message to match each other. -- data AnyMessage ps where - AnyMessage :: Message ps st st' -> AnyMessage ps + AnyMessage :: forall ps (st :: ps) (st' :: ps). + ( StateTokenI st + , ActiveState st + ) + => Message ps (st :: ps) (st' :: ps) + -- ^ 'Message' between some states + -> AnyMessage ps + -- requires @UndecidableInstances@ and @QuantifiedConstraints@. -instance (forall st st'. Show (Message ps st st')) => Show (AnyMessage ps) where - show (AnyMessage msg) = show msg +instance (forall (st :: ps) (st' :: ps). Show (Message ps st st')) + => Show (AnyMessage ps) where + show (AnyMessage (msg :: Message ps st st')) = + "AnyMessage " ++ show msg --- | Used to hold the 'PeerHasAgency' state token and a corresponding 'Message'. + +-- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the +-- singleton for the state and the message. -- --- Used where we don't know statically what the state type is, but need the --- agency and message to match each other. +pattern AnyMessageAndAgency :: forall ps. () + => forall (st :: ps) (st' :: ps). + (StateTokenI st, ActiveState st) + => StateToken st + -> Message ps st st' + -> AnyMessage ps +pattern AnyMessageAndAgency stateToken msg <- AnyMessage (getAgency -> (msg, stateToken)) + where + AnyMessageAndAgency _ msg = AnyMessage msg +{-# COMPLETE AnyMessageAndAgency #-} + +-- | Internal view pattern for 'AnyMessageAndAgency' -- -data AnyMessageAndAgency ps where - AnyMessageAndAgency :: PeerHasAgency pr (st :: ps) - -> Message ps (st :: ps) (st' :: ps) - -> AnyMessageAndAgency ps +getAgency :: StateTokenI st => Message ps st st' -> (Message ps st st', StateToken st) +getAgency msg = (msg, stateToken) --- requires @UndecidableInstances@ and @QuantifiedConstraints@. -instance - ( forall (st :: ps). Show (ClientHasAgency st) - , forall (st :: ps). Show (ServerHasAgency st) - , forall (st :: ps) (st' :: ps). Show (Message ps st st') - ) => Show (AnyMessageAndAgency ps) where - show (AnyMessageAndAgency agency msg) = show (agency, msg) -- | The 'Codec' round-trip property: decode after encode gives the same -- message. Every codec must satisfy this property. @@ -317,11 +365,14 @@ prop_codecM , Eq (AnyMessage ps) ) => Codec ps failure m bytes - -> AnyMessageAndAgency ps + -- ^ codec + -> AnyMessage ps + -- ^ some message -> m Bool -prop_codecM Codec {encode, decode} (AnyMessageAndAgency stok msg) = do - r <- decode stok >>= runDecoder [encode stok msg] - case r of + -- ^ returns 'True' iff round trip returns the exact same message +prop_codecM Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do + r <- decode stateToken >>= runDecoder [encode msg] + case r :: Either failure (SomeMessage st) of Right (SomeMessage msg') -> return $ AnyMessage msg' == AnyMessage msg Left _ -> return False @@ -332,7 +383,7 @@ prop_codec (Monad m, Eq (AnyMessage ps)) => (forall a. m a -> a) -> Codec ps failure m bytes - -> AnyMessageAndAgency ps + -> AnyMessage ps -> Bool prop_codec runM codec msg = runM (prop_codecM codec msg) @@ -352,19 +403,20 @@ prop_codec runM codec msg = prop_codec_splitsM :: forall ps failure m bytes. (Monad m, Eq (AnyMessage ps)) - => (bytes -> [[bytes]]) -- ^ alternative re-chunkings of serialised form + => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form -> Codec ps failure m bytes - -> AnyMessageAndAgency ps + -> AnyMessage ps -> m Bool prop_codec_splitsM splits - Codec {encode, decode} (AnyMessageAndAgency stok msg) = do + Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do and <$> sequence - [ do r <- decode stok >>= runDecoder bytes' - case r of + [ do r <- decode stateToken >>= runDecoder bytes' + case r :: Either failure (SomeMessage st) of Right (SomeMessage msg') -> return $! AnyMessage msg' == AnyMessage msg Left _ -> return False - | let bytes = encode stok msg + | let bytes = encode msg , bytes' <- splits bytes ] @@ -374,9 +426,10 @@ prop_codec_splits :: forall ps failure m bytes. (Monad m, Eq (AnyMessage ps)) => (bytes -> [[bytes]]) + -- ^ alternative re-chunkings of serialised form -> (forall a. m a -> a) -> Codec ps failure m bytes - -> AnyMessageAndAgency ps + -> AnyMessage ps -> Bool prop_codec_splits splits runM codec msg = runM $ prop_codec_splitsM splits codec msg @@ -387,11 +440,13 @@ prop_codec_splits splits runM codec msg = -- Used for the existential @st :: ps@ parameter when expressing that for each -- value of 'PeerHasAgency' for protocol A, there is a corresponding -- 'PeerHasAgency' for protocol B of some @st :: ps@. -data SamePeerHasAgency (pr :: PeerRole) (ps :: Type) where - SamePeerHasAgency - :: forall (pr :: PeerRole) ps (st :: ps). - PeerHasAgency pr st - -> SamePeerHasAgency pr ps +data SomeState (ps :: Type) where + SomeState + :: forall ps (st :: ps). + ActiveState st + => StateToken st + -- ^ state token for some active state 'st' + -> SomeState ps -- | Binary compatibility of two protocols -- @@ -413,27 +468,29 @@ prop_codec_binary_compatM ) => Codec psA failure m bytes -> Codec psB failure m bytes - -> (forall pr (stA :: psA). PeerHasAgency pr stA -> SamePeerHasAgency pr psB) - -- ^ The states of A map directly of states of B. - -> AnyMessageAndAgency psA + -> (forall (stA :: psA). ActiveState stA => StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA -> m Bool prop_codec_binary_compatM codecA codecB stokEq - (AnyMessageAndAgency (stokA :: PeerHasAgency pr stA) msgA) = - case stokEq stokA of - SamePeerHasAgency stokB -> do + (AnyMessage (msgA :: Message psA stA stA')) = + let stokA :: StateToken stA + stokA = stateToken + in case stokEq stokA of + SomeState (stokB :: StateToken stB) -> do -- 1. - let bytesA = encode codecA stokA msgA + let bytesA = encode codecA msgA -- 2. r1 <- decode codecB stokB >>= runDecoder [bytesA] - case r1 of + case r1 :: Either failure (SomeMessage stB) of Left _ -> return False Right (SomeMessage msgB) -> do -- 3. - let bytesB = encode codecB stokB msgB + let bytesB = encode codecB msgB -- 4. - r2 <- decode codecA stokA >>= runDecoder [bytesB] - case r2 of + r2 <- decode codecA (stateToken :: StateToken stA) >>= runDecoder [bytesB] + case r2 :: Either failure (SomeMessage stA) of Left _ -> return False Right (SomeMessage msgA') -> return $ AnyMessage msgA' == AnyMessage msgA @@ -446,8 +503,9 @@ prop_codec_binary_compat => (forall a. m a -> a) -> Codec psA failure m bytes -> Codec psB failure m bytes - -> (forall pr (stA :: psA). PeerHasAgency pr stA -> SamePeerHasAgency pr psB) - -> AnyMessageAndAgency psA + -> (forall (stA :: psA). StateToken stA -> SomeState psB) + -- ^ the states of A map directly to states of B. + -> AnyMessage psA -> Bool prop_codec_binary_compat runM codecA codecB stokEq msgA = runM $ prop_codec_binary_compatM codecA codecB stokEq msgA @@ -464,17 +522,20 @@ prop_codecs_compatM , forall a. Monoid a => Monoid (m a) ) => Codec ps failure m bytes + -- ^ first codec -> Codec ps failure m bytes - -> AnyMessageAndAgency ps + -- ^ second codec + -> AnyMessage ps + -- ^ some message -> m Bool prop_codecs_compatM codecA codecB - (AnyMessageAndAgency stok msg) = - getAll <$> do r <- decode codecB stok >>= runDecoder [encode codecA stok msg] - case r of + (AnyMessage (msg :: Message ps st st')) = + getAll <$> do r <- decode codecB (stateToken :: StateToken st) >>= runDecoder [encode codecA msg] + case r :: Either failure (SomeMessage st) of Right (SomeMessage msg') -> return $! All $ AnyMessage msg' == AnyMessage msg Left _ -> return $! All False - <> do r <- decode codecA stok >>= runDecoder [encode codecB stok msg] - case r of + <> do r <- decode codecA (stateToken :: StateToken st) >>= runDecoder [encode codecB msg] + case r :: Either failure (SomeMessage st) of Right (SomeMessage msg') -> return $! All $ AnyMessage msg' == AnyMessage msg Left _ -> return $! All False @@ -489,7 +550,7 @@ prop_codecs_compat => (forall a. m a -> a) -> Codec ps failure m bytes -> Codec ps failure m bytes - -> AnyMessageAndAgency ps + -> AnyMessage ps -> Bool prop_codecs_compat run codecA codecB msg = run $ prop_codecs_compatM codecA codecB msg diff --git a/typed-protocols/src/Network/TypedProtocol/Core.hs b/typed-protocols/src/Network/TypedProtocol/Core.hs index b968ddca..e8314979 100644 --- a/typed-protocols/src/Network/TypedProtocol/Core.hs +++ b/typed-protocols/src/Network/TypedProtocol/Core.hs @@ -1,37 +1,73 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} - +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilyDependencies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} + +{-# OPTIONS_HADDOCK show-extensions #-} -- | This module defines the core of the typed protocol framework. -- - module Network.TypedProtocol.Core ( -- * Introduction -- $intro + -- * Defining protocols -- $defining Protocol (..) + , StateTokenI (..) -- $lemmas + -- * Engaging in protocols - -- $using + -- ** PeerRole , PeerRole (..) - , TokPeerRole (..) + , SingPeerRole (..) + -- ** Agency and its evidence + -- $agency + , Agency (..) + , SingAgency (..) + , RelativeAgency (..) + , Relative + , ReflRelativeAgency (..) + , WeHaveAgencyProof + , TheyHaveAgencyProof + , NobodyHasAgencyProof + -- *** FlipAgency , FlipAgency - , PeerHasAgency (..) - , WeHaveAgency - , TheyHaveAgency - , Peer (..) + -- *** ActiveState + , IsActiveState (..) + , ActiveState + , notActiveState + , ActiveAgency + , ActiveAgency' (..) + -- ** Pipelining + -- *** IsPipelined + , IsPipelined (..) + -- *** Outstanding + , Outstanding + -- *** N and Nat + , N (..) + , Nat (Succ, Zero) + , natToInt + , unsafeIntToNat ) where -import Data.Void (Void) +import Data.Kind (Constraint, Type) +import Unsafe.Coerce (unsafeCoerce) + +import Data.Singletons -- $intro -- A typed protocol between two peers is defined via a state machine: a @@ -79,7 +115,7 @@ import Data.Void (Void) -- -- The type class itself is indexed on a protocol \"tag\" type. This type -- does double duty as the /kind/ of the /types/ of the protocol states. - +-- -- We will use as a running example a simple \"ping\/pong\" protocol. (You can -- see the example in full in "Network.TypedProtocol.PingPong.Type".) In this -- example protocol the client sends a ping message and the serve must respond @@ -133,9 +169,7 @@ import Data.Void (Void) -- -- As described above, this style of protocol gives agency to only one peer at -- once. That is, in each protocol state, one peer has agency (the ability to --- send) and the other does not (it must only receive). The three associated --- data families ('ClientHasAgency', 'ServerHasAgency' and 'NobodyHasAgency') --- define which peer has agency for each state. +-- send) and the other does not (it must only receive). -- -- In the \"ping\/pong\" protocol example, the idle state is the one in which -- the client can send a message, and the busy state is the one in which the @@ -143,117 +177,234 @@ import Data.Void (Void) -- further messages. This arrangement is defined as so: -- -- > -- still within the instance Protocol PingPong --- > data ClientHasAgency st where --- > TokIdle :: ClientHasAgency StIdle --- > --- > data ServerHasAgency st where --- > TokBusy :: ServerHasAgency StBusy --- > --- > data NobodyHasAgency st where --- > TokDone :: NobodyHasAgency StDone +-- > type StateAgency StIdle = ClientAgency +-- > type StateAgency StBusy = ServerAgency +-- > type StateAgency StDone = NobodyAgency -- -- In this simple protocol there is exactly one state in each category, but in -- general for non-trivial protocols there may be several protocol states in -- each category. -- +-- Finally we need to point which singletons to use for the protocol states +-- +-- > -- still within the instance Protocol PingPong, 'SPingPong' type is what we define next. +-- > type StateToken = SPingPong +-- +-- Furthermore we use singletons to provide term level reflection of type level +-- states. One is required to provide singletons for all types of kind +-- 'PingPong'. These definitions are provided outside of the 'Protocol' type +-- class. This is as simple as providing a GADT: +-- +-- > data SingPingPong (st :: PingPong) where +-- > SingIdle :: SingPingPong StIdle +-- > SingBusy :: SingPingPong StBusy +-- > SingDone :: SingPingPong StDone +-- +-- together with 'StateTokenI' instance (similar to 'SingI' from the +-- "singletons" package): +-- +-- > instance StateTokenI StIdle where stateToken = SingIdle +-- > instance StateTokenI StBusy where stateToken = SingBusy +-- > instance StateTokenI StDone where stateToken = SingDone +-- +-- This and other example protocols are provided in "typed-protocols-examples" +-- package. --- $tests --- The mechanism for labelling each protocol state with the agency does not --- automatically prevent mislabelling, ie giving conflicting labels to a --- single state. It does in fact prevent forgetting to label states in the --- sense that it would not be possible to write protocol peers that make --- progress having entered these unlabelled states. +-- | Types for client and server peer roles. As protocol can be viewed from +-- either client or server side. +-- +-- Note that technically \"client\" and \"server\" are arbitrary labels. The +-- framework is completely symmetric between the two peers. +-- +-- This definition is only used as promoted types and kinds, never as values. -- --- This partition property is however crucial for the framework's guarantees. --- The "Network.TypedProtocol.Proofs" module provides a way to guarantee for --- each protocol that this property is not violated. It also provides utilities --- helpful for testing protocols. +data PeerRole = AsClient | AsServer --- $lemmas +-- | Singletons for 'PeerRole'. We provide 'Sing' and 'SingI' instances from +-- the "singletons" package. +-- +type SingPeerRole :: PeerRole -> Type +data SingPeerRole pr where + SingAsClient :: SingPeerRole AsClient + SingAsServer :: SingPeerRole AsServer + +deriving instance Show (SingPeerRole pr) + +type instance Sing = SingPeerRole +instance SingI AsClient where + sing = SingAsClient +instance SingI AsServer where + sing = SingAsServer + +-- $agency +-- The protocols we consider either give agency to one side (one side can send +-- a message) or the protocol terminated. Agency is a (type-level) function of +-- the protocol state, and thus uniquely determined by it. -- --- The 'connect' and 'connectPipelined' proofs rely on lemmas about the --- protocol. Specifically they rely on the property that each protocol state --- is labelled with the agency of one peer or the other, or neither, but never --- both. Or to put it another way, the protocol states should be partitioned --- into those with agency for one peer, or the other or neither. +-- The following types define the necessary type-level machinery and its +-- term-level evidence to provide type-safe API for `typed-protocols`. +-- Required proofs are hidden in an (unexposed) module +-- @Network.TypedProtocol.Lemmas@. + +-- | A promoted data type which denotes three possible agencies a protocol +-- state might be assigned. -- --- The way the labelling is encoded does not automatically enforce this --- property. It is technically possible to set up the labelling for a protocol --- so that one state is labelled as having both peers with agency, or declaring --- simultaneously that one peer has agency and that neither peer has agency --- in a particular state. +data Agency where + -- | The client has agency. + ClientAgency :: Agency + + -- | The server has agency. + ServerAgency :: Agency + + -- | Nobody has agency, terminal state. + NobodyAgency :: Agency + +type SingAgency :: Agency -> Type +data SingAgency a where + SingClientAgency :: SingAgency ClientAgency + SingServerAgency :: SingAgency ServerAgency + SingNobodyAgency :: SingAgency NobodyAgency + +deriving instance Show (SingAgency a) + +type instance Sing = SingAgency +instance SingI ClientAgency where + sing = SingClientAgency +instance SingI ServerAgency where + sing = SingServerAgency +instance SingI NobodyAgency where + sing = SingNobodyAgency + +-- | A promoted data type which indicates the effective agency (which is +-- relative to current role). It is computed by `Relative` type family. -- --- So the overall proofs rely on lemmas that say that the labelling has been --- done correctly. This type bundles up those three lemmas. +data RelativeAgency where + -- evidence that we have agency + WeHaveAgency :: RelativeAgency + -- evidence that proof the remote side has agency + TheyHaveAgency :: RelativeAgency + -- evidence of protocol termination + NobodyHasAgency :: RelativeAgency +-- TODO: input-output-hk/typed-protocols#57 + + +-- | Compute effective agency with respect to the peer role, for client role, +-- agency is preserved, while for the server role it is flipped. -- --- Specifically proofs that it is impossible for a protocol state to have: +type Relative :: PeerRole -> Agency -> RelativeAgency +type family Relative pr a where + Relative AsClient ClientAgency = WeHaveAgency + Relative AsClient ServerAgency = TheyHaveAgency + Relative AsClient NobodyAgency = NobodyHasAgency + Relative AsServer ClientAgency = TheyHaveAgency + Relative AsServer ServerAgency = WeHaveAgency + Relative AsServer NobodyAgency = NobodyHasAgency + + +-- | Type equality for 'RelativeAgency' which also carries information about +-- agency. It is isomorphic to a product of 'Agency' singleton and +-- @r :~: r'@, where both @r@ and @r'@ have kind 'RelativeAgency'. -- --- * client having agency and server having agency --- * client having agency and nobody having agency --- * server having agency and nobody having agency +-- This is a proper type with values used by the 'Peer', however they are +-- hidden by using "Network.TypedProtocol.Peer.Client" and +-- "Network.TypedProtocol.Peer.Server" APIs. -- --- These lemmas are structured as proofs by contradiction, e.g. stating --- \"if the client and the server have agency for this state then it leads to --- contradiction\". Contradiction is represented as the 'Void' type that has --- no values except ⊥. +type ReflRelativeAgency :: Agency -> RelativeAgency -> RelativeAgency -> Type +data ReflRelativeAgency a r r' where + ReflClientAgency :: ReflRelativeAgency ClientAgency r r + ReflServerAgency :: ReflRelativeAgency ServerAgency r r + ReflNobodyAgency :: ReflRelativeAgency NobodyAgency r r + +-- | Type of the proof that we have the agency. -- --- For example for the ping\/pong protocol, it has three states, and if we set --- up the labelling correctly we have: +-- 'ReflClientAgency' has this type only iff `'StateAgency' st ~ 'ClientAgency'` +-- and `pr ~ 'AsClient'`. -- --- > data PingPong where --- > StIdle :: PingPong --- > StBusy :: PingPong --- > StDone :: PingPong --- > --- > instance Protocol PingPong where --- > --- > data ClientHasAgency st where --- > TokIdle :: ClientHasAgency StIdle --- > --- > data ServerHasAgency st where --- > TokBusy :: ServerHasAgency StBusy --- > --- > data NobodyHasAgency st where --- > TokDone :: NobodyHasAgency StDone +-- 'ReflServerAgency' has this type only iff `'StateAgency' st ~ 'ServerAgency'` +-- and `pr ~ 'AsServer'` +-- +type WeHaveAgencyProof :: PeerRole -> ps -> Type +type WeHaveAgencyProof pr st = ReflRelativeAgency + (StateAgency st) + WeHaveAgency + (Relative pr (StateAgency st)) + +-- | Type of the proof that the remote side has the agency. +-- +-- 'ReflClientAgency' has this type only iff `'StateAgency' st ~ 'ClientAgency'` +-- and `pr ~ 'AsServer'`. +-- +-- 'ReflServerAgency' has this type only iff `'StateAgency' st ~ 'ServerAgency'` +-- and `pr ~ 'AsClient'` +-- +type TheyHaveAgencyProof :: PeerRole -> ps -> Type +type TheyHaveAgencyProof pr st = ReflRelativeAgency + (StateAgency st) + TheyHaveAgency + (Relative pr (StateAgency st)) + + +-- | Type of the proof that nobody has agency in this state. +-- +-- Only 'ReflNobodyAgency' can fulfil the proof obligation. -- --- So now we can prove that if the client has agency for a state then there --- are no cases in which the server has agency. +type NobodyHasAgencyProof :: PeerRole -> ps -> Type +type NobodyHasAgencyProof pr st = ReflRelativeAgency (StateAgency st) + NobodyHasAgency + (Relative pr (StateAgency st)) + +-- $lemmas -- --- > exclusionLemma_ClientAndServerHaveAgency TokIdle tok = case tok of {} +-- The 'Network.TypedProtocol.connect' proof rely on lemmas about the +-- protocol. Specifically they rely on the property that each protocol state is +-- labelled with the agency of one peer or the other, or neither, but never +-- both. This property is true by construction, since we use a type family +-- 'StateAgency' which maps states to agencies, however we still need an evince +-- that cases where both peer have the agency or neither of them has it can be +-- eliminated. -- --- For this protocol there is only one state in which the client has agency, --- the idle state. By pattern matching on the state token for the server --- agency we can list all the cases in which the server also has agency for --- the idle state. There are of course none of these so we give the empty --- set of patterns. GHC can check that we are indeed correct about this. --- This also requires the @EmptyCase@ language extension. +-- The packages defines lemmas (in a hidden module) which are structured as +-- proofs by contradiction, e.g. stating \"if the client and the server have +-- agency for this state then it leads to contradiction\". Contradiction is +-- represented as the 'Void' type that has no values except ⊥. -- --- To get this completeness checking it is important to compile modules --- containing these lemmas with @-Wincomplete-patterns@, which is implied by --- @-Wall@. +-- The framework defines protocol-agnostic proofs (in the hidden module +-- `Network.TypedProtocol.Lemmas`) which excludes that the client and server +-- have agency at the same time. -- --- All three lemmas follow the same pattern. +-- * 'exclusionLemma_ClientAndServerHaveAgency', +-- * 'terminationLemma_1', +-- * 'terminationLemma_2'. -- +-- | A type class which hides a state token / singleton inside a class +-- dictionary. +-- +-- This is similar to the 'SingI' instance, but specific to protocol state +-- singletons. +-- +class StateTokenI st where + stateToken :: StateToken st + -- | The protocol type class bundles up all the requirements for a typed -- protocol. -- --- Each protocol consists of three things: --- --- * The protocol itself, which is also expected to be the kind of the types --- of the protocol states. The class is indexed on the protocol itself. --- * The protocol messages. --- * The partition of the protocol states into those in which the client has --- agency, or the server has agency, or neither have agency. +-- Each protocol consists of four components: -- --- The labelling of each protocol state with the peer that has agency in that --- state is done by giving a definition to the data families --- 'ClientHasAgency', 'ServerHasAgency' and 'NobodyHasAgency'. These --- definitions are expected to be singleton-style GADTs with one constructor --- per protocol state. +-- * the protocol itself, which is also expected to be the kind of the types +-- of the protocol states. The class is indexed on the protocol itself; +-- * the protocol messages; +-- * a type level map from the protocol states to agency: in each state either +-- client or server or nobody has the agency. +-- * a singleton type for the protocol states (e.g. `StateToken` type family +-- instance), together with 'StateTokenI' instances. -- --- Each protocol state must be assigned to only one label. See --- "Network.TypedProtocol.Proofs" for more details on this point. +-- It is required provide 'StateToken' type family instance as well as +-- 'StateTokenI' instances for all protocol states. These singletons allow one +-- to pattern match on the state, which is useful when defining codecs, or +-- providing informative error messages, however they are not necessary for +-- proving correctness of the protocol. These type families are similar to +-- 'Sing' and 'SingI' in the "singletons" package. -- class Protocol ps where @@ -264,204 +415,146 @@ class Protocol ps where -- data Message ps (st :: ps) (st' :: ps) - -- | Tokens for those protocol states in which the client has agency. + -- | Associate an 'Agency' for each state. -- - data ClientHasAgency (st :: ps) + type StateAgency (st :: ps) :: Agency - -- | Tokens for those protocol states in which the server has agency. + -- | A type family for protocol state token, e.g. term level representation of + -- type level state (also known as singleton). -- - data ServerHasAgency (st :: ps) - - -- | Tokens for terminal protocol states in which neither the client nor - -- server has agency. + -- This type family is similar to 'Sing' type class in the "singletons" + -- package, but specific for protocol states. -- - data NobodyHasAgency (st :: ps) + type StateToken :: ps -> Type - -- | Lemma that if the client has agency for a state, there are no - -- cases in which the server has agency for the same state. - -- - exclusionLemma_ClientAndServerHaveAgency - :: forall (st :: ps). - ClientHasAgency st - -> ServerHasAgency st - -> Void - - -- | Lemma that if the nobody has agency for a state, there are no - -- cases in which the client has agency for the same state. - -- - exclusionLemma_NobodyAndClientHaveAgency - :: forall (st :: ps). - NobodyHasAgency st - -> ClientHasAgency st - -> Void - - -- | Lemma that if the nobody has agency for a state, there are no - -- cases in which the server has agency for the same state. - -- - exclusionLemma_NobodyAndServerHaveAgency - :: forall (st :: ps). - NobodyHasAgency st - -> ServerHasAgency st - -> Void --- | Types for client and server peer roles. As protocol can be viewed from --- either client or server side. +-- | Evidence that one side of the protocol has the agency, and thus that the +-- protocol hasn't yet terminated. -- --- Note that technically \"client\" and \"server\" are arbitrary labels. The --- framework is completely symmetric between the two peers. --- --- This definition is only used as promoted types and kinds, never as values. --- -data PeerRole = AsClient | AsServer +type ActiveAgency' :: ps -> Agency -> Type +data ActiveAgency' st agency where + -- | Evidence that the client has the agency. + ClientHasAgency :: StateAgency st ~ ClientAgency + => ActiveAgency' st ClientAgency + -- | Evidence that the server has the agency. + ServerHasAgency :: StateAgency st ~ ServerAgency + => ActiveAgency' st ServerAgency --- | Singletons for the promoted 'PeerRole' types. Not directly used by the --- framework, however some times useful when writing code that is shared between --- client and server. --- -data TokPeerRole (peerRole :: PeerRole) where - TokAsClient :: TokPeerRole AsClient - TokAsServer :: TokPeerRole AsServer +deriving instance Show (ActiveAgency' st agency) --- | This data type is used to hold state tokens for states with either client --- or server agency. This GADT shows up when writing protocol peers, when --- 'Yield'ing or 'Await'ing, and when writing message encoders\/decoders. +-- | Evidence that the protocol isn't in a terminal state. -- -data PeerHasAgency (pr :: PeerRole) (st :: ps) where - ClientAgency :: !(ClientHasAgency st) -> PeerHasAgency AsClient st - ServerAgency :: !(ServerHasAgency st) -> PeerHasAgency AsServer st +type ActiveAgency :: ps -> Type +type ActiveAgency st = ActiveAgency' st (StateAgency st) -instance ( forall (st' :: ps). Show (ClientHasAgency st') - , forall (st' :: ps). Show (ServerHasAgency st') - ) => Show (PeerHasAgency pr (st :: ps)) where - show (ClientAgency stok) = "ClientAgency " ++ show stok - show (ServerAgency stok) = "ServerAgency " ++ show stok --- | A synonym for an state token in which \"our\" peer has agency. This is --- parametrised over the client or server roles. In either case the peer in --- question has agency. +-- | A type class which restricts states to ones that have `ClientAgency` or +-- `ServerAgency`, excluding `NobodyAgency`. -- --- This shows up when we are sending messages, or dealing with encoding --- outgoing messages. +-- One can use `notActive' to eliminate cases for which both @'IsActiveState' +-- st@ is in scope and for which we have an evidence that the state is not +-- active (i.e. a singleton). This is useful when writing a 'Codec'. -- -type WeHaveAgency (pr :: PeerRole) st = PeerHasAgency pr st +class IsActiveState st (agency :: Agency) where + activeAgency :: ActiveAgency' st agency --- | A synonym for an state token in which the other peer has agency. This is --- parametrised over the client or server roles. In either case the other peer --- has agency. +instance ClientAgency ~ StateAgency st + => IsActiveState st ClientAgency where + activeAgency = ClientHasAgency +instance ServerAgency ~ StateAgency st + => IsActiveState st ServerAgency where + activeAgency = ServerHasAgency + +-- | A constraint which provides an evidence that the protocol isn't in +-- a terminal state. +-- +type ActiveState :: ps -> Constraint +type ActiveState st = IsActiveState st (StateAgency st) + + +-- | This is useful function to eliminate cases where the `ActiveState st` is +-- provided but we are given a state in which neither side has agency +-- (`NobodyAgency`). For example when writing a codec, we only need to encode +-- / decode messages which are in active states, but to make such functions +-- total, `notActiveState` needs to be used to eliminate the states in which +-- nobody has agency. -- --- This shows up when we are receiving messages, or dealing with decoding --- incoming messages. +-- A good analogy for this function is @'Data.Void.absurd' :: 'Void' -> a@. -- -type TheyHaveAgency (pr :: PeerRole) st = PeerHasAgency (FlipAgency pr) st +notActiveState :: forall ps (st :: ps). + StateAgency st ~ NobodyAgency + => ActiveState st + => StateToken st + -> forall a. a +notActiveState (_ :: StateToken st) = + case activeAgency :: ActiveAgency st of {} + -- | A type function to flip the client and server roles. -- -type family FlipAgency (pr :: PeerRole) where +type FlipAgency :: PeerRole -> PeerRole +type family FlipAgency pr where FlipAgency AsClient = AsServer FlipAgency AsServer = AsClient --- | A description of a peer that engages in a protocol. --- --- The protocol describes what messages peers /may/ send or /must/ accept. --- A particular peer implementation decides what to actually do within the --- constraints of the protocol. --- --- Peers engage in a protocol in either the client or server role. Of course --- the client role can only interact with the serve role for the same protocol --- and vice versa. --- --- 'Peer' has several type arguments: --- --- * the protocol itself; --- * the client\/server role; --- *.the current protocol state; --- * the monad in which the peer operates; and --- * the type of any final result once the peer terminates. --- --- For example: --- --- > pingPongClientExample :: Int -> Peer PingPong AsClient StIdle m () --- > pingPongServerExample :: Peer PingPong AsServer StIdle m Int --- --- The actions that a peer can take are: +-- | 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. -- --- * to perform local monadic effects --- * to terminate with a result (but only in a terminal protocol state) --- * to send a message (but only in a protocol state in which we have agency) --- * to wait to receive a message (but only in a protocol state in which the --- other peer has agency) +data IsPipelined where + -- | Pipelined peer which is using `c :: Type` for collecting responses + -- from a pipelined messages. 'N' indicates depth of pipelining. + 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 to +-- ensure that 'Collect' is only used when there are outstanding results to +-- collect (e.g. after 'YieldPipeliend' was used); +-- and to ensure that the non-pipelined primitives 'Yield', 'Await' and 'Done' +-- are only used when there are none unsatisfied pipelined requests. -- --- In the 'Done', 'Yield' and 'Await' cases we must provide evidence of both --- the protocol state we are in and that the appropriate peer has agency. --- This takes the form of 'ClientAgency' or 'ServerAgency' applied to a --- protocol-specific state token: either a 'ClientHasAgency' or a --- 'ServerHasAgency' token for the protocol. The 'Done' state does not need --- the extra agency information. +type Outstanding :: IsPipelined -> N +type family Outstanding pl where + Outstanding 'NonPipelined = Z + Outstanding ('Pipelined n _) = n + +-- | A value level inductive natural number, indexed by the corresponding type +-- level natural number 'N'. -- --- While this evidence must be provided, the types guarantee that it is not --- possible to supply incorrect evidence. +-- This is often needed when writing pipelined peers to be able to count the +-- number of outstanding pipelined yields, and show to the type checker that +-- 'Network.TypedProtocol.Peer.Collect' and 'Network.TypedProtocol.Peer.Done' +-- are being used correctly. -- -data Peer ps (pr :: PeerRole) (st :: ps) m a where +newtype Nat (n :: N) = UnsafeInt Int + deriving Show via Int - -- | Perform a local monadic effect and then continue. - -- - -- Example: - -- - -- > Effect $ do - -- > ... -- actions in the monad - -- > return $ ... -- another Peer value - -- - Effect :: m (Peer ps pr st m a) - -> Peer ps pr st m a +data IsNat (n :: N) where + IsZero :: IsNat Z + IsSucc :: Nat n -> IsNat (S n) - -- | Terminate with a result. A state token must be provided from the - -- 'NobodyHasAgency' states, so show that this is a state in which we can - -- terminate. - -- - -- Example: - -- - -- > Yield (ClientAgency TokIdle) - -- > MsgDone - -- > (Done TokDone result) - -- - Done :: !(NobodyHasAgency st) - -> a - -> Peer ps pr st m a +toIsNat :: Nat n -> IsNat n +toIsNat (UnsafeInt 0) = unsafeCoerce IsZero +toIsNat (UnsafeInt n) = unsafeCoerce (IsSucc (UnsafeInt (pred n))) - -- | Send a message to the other peer and then continue. This takes the - -- message and the continuation. It also requires evidence that we have - -- agency for this protocol state and thus are allowed to send messages. - -- - -- Example: - -- - -- > Yield (ClientAgency TokIdle) MsgPing $ ... - -- - Yield :: !(WeHaveAgency pr st) - -> Message ps st st' - -> Peer ps pr st' m a - -> Peer ps pr st m a - - -- | Waits to receive a message from the other peer and then continues. - -- This takes the the continuation that is supplied with the received - -- message. It also requires evidence that the other peer has agency for - -- this protocol state and thus we are expected to wait to receive messages. - -- - -- Note that the continuation that gets supplied with the message must be - -- prepared to deal with /any/ message that is allowed in /this/ protocol - -- state. This is why the continuation /must/ be polymorphic in the target - -- state of the message (the third type argument of 'Message'). - -- - -- Example: - -- - -- > Await (ClientAgency TokIdle) $ \msg -> - -- > case msg of - -- > MsgDone -> ... - -- > MsgPing -> ... - -- - Await :: !(TheyHaveAgency pr st) - -> (forall st'. Message ps st st' -> Peer ps pr st' m a) - -> Peer ps pr st m a +pattern Zero :: () => Z ~ n => Nat n +pattern Zero <- (toIsNat -> IsZero) where + Zero = UnsafeInt 0 + +pattern Succ :: () => (m ~ S n) => Nat n -> Nat m +pattern Succ n <- (toIsNat -> IsSucc n) where + Succ (UnsafeInt n) = UnsafeInt (succ n) + +{-# COMPLETE Zero, Succ #-} +natToInt :: Nat n -> Int +natToInt (UnsafeInt n) = n -deriving instance Functor m => Functor (Peer ps (pr :: PeerRole) (st :: ps) m) +unsafeIntToNat :: Int -> Nat n +unsafeIntToNat = UnsafeInt diff --git a/typed-protocols/src/Network/TypedProtocol/Driver.hs b/typed-protocols/src/Network/TypedProtocol/Driver.hs index 75cff4b5..b12d66c9 100644 --- a/typed-protocols/src/Network/TypedProtocol/Driver.hs +++ b/typed-protocols/src/Network/TypedProtocol/Driver.hs @@ -1,6 +1,7 @@ {-# LANGUAGE BangPatterns #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE NamedFieldPuns #-} {-# LANGUAGE PolyKinds #-} @@ -25,7 +26,7 @@ module Network.TypedProtocol.Driver import Data.Void (Void) import Network.TypedProtocol.Core -import Network.TypedProtocol.Pipelined +import Network.TypedProtocol.Peer import Control.Concurrent.Class.MonadSTM.TQueue import Control.Monad.Class.MonadAsync @@ -36,47 +37,70 @@ import Control.Monad.Class.MonadSTM -- $intro -- -- A 'Peer' is a particular implementation of an agent that engages in a --- typed protocol. To actually run one we need a source and sink for the typed --- protocol messages. These are provided by a 'Channel' and a 'Codec'. The --- 'Channel' represents one end of an untyped duplex message transport, and --- the 'Codec' handles conversion between the typed protocol messages and --- the untyped channel. +-- typed protocol. To actually run one we need an untyped channel representing +-- one end of an untyped duplex message transport, which allows to send and +-- receive bytes. One will also need a 'Codec' which handles conversion +-- between the typed protocol messages and the untyped channel. -- --- So given the 'Peer' and a compatible 'Codec' and 'Channel' we can run the --- peer in some appropriate monad. The peer and codec have to agree on --- the same protocol and role in that protocol. The codec and channel have to --- agree on the same untyped medium, e.g. text or bytes. All three have to --- agree on the same monad in which they will run. +-- Given the 'Peer', a compatible 'Network.TypedProtocol.Codec.Codec' and +-- an untyped channel we can run the peer in some appropriate monad (e.g. 'IO', +-- or a simulation monad for testing purposes). The peer and codec have to +-- agree on the same protocol. The codec and channel have to agree on the same +-- untyped medium, e.g. text or bytes. All three have to agree on the same +-- monad in which they will run. -- -- This module provides drivers for normal and pipelined peers. There is -- very little policy involved here so typically it should be possible to -- use these drivers, and customise things by adjusting the peer, or codec --- or channel. +-- or channel (together with an implementation of a 'Driver' based on it). -- --- It is of course possible to write custom drivers and the code for these ones --- may provide a useful starting point. The 'runDecoder' function may be a --- helpful utility for use in custom drives. +-- For implementing a 'Driver' based on some untyped channel, the +-- 'Network.TypedProtocol.Codec.runDecoder' function may be a helpful utility. -- +-- For a possible definition of an untyped channel and how to construct +-- a `Driver` from it see @typed-protocols-examples@ package. For production +-- grade examples see https://github.com/IntersectMBO/ouroboros-network +-- repository. -- -- Driver interface -- -data Driver ps dstate m = +data Driver ps (pr :: PeerRole) dstate m = Driver { - sendMessage :: forall (pr :: PeerRole) (st :: ps) (st' :: ps). - PeerHasAgency pr st + -- | Send a message; the message must transition from an active state. + -- One needs to supply agency evidence. + sendMessage :: forall (st :: ps) (st' :: ps). + StateTokenI st + => StateTokenI st' + => ActiveState st + => WeHaveAgencyProof pr st + -- agency evidence -> Message ps st st' + -- message to send -> m () - , recvMessage :: forall (pr :: PeerRole) (st :: ps). - PeerHasAgency pr st + -- | Receive some message, since we don't know the final state of + -- the protocol it is wrapped in `SomeMessage` type; the message must + -- transition from an active state. One needs to supply agency + -- evidence. + -- + , recvMessage :: forall (st :: ps). + StateTokenI st + => ActiveState st + => TheyHaveAgencyProof pr st + -- agency evidence -> dstate + -- current driver state -> m (SomeMessage st, dstate) + -- received message together with new driver state - , startDState :: dstate + , -- | Initial state of the driver + initialDState :: dstate } +-- TODO: input-output-hk/typed-protocols#57 + -- | When decoding a 'Message' we only know the expected \"from\" state. We -- cannot know the \"to\" state as this depends on the message we decode. To @@ -84,7 +108,11 @@ data Driver ps dstate m = -- type to hide the \"to"\ state. -- data SomeMessage (st :: ps) where - SomeMessage :: Message ps st st' -> SomeMessage st + SomeMessage :: ( StateTokenI st + , StateTokenI st' + , ActiveState st + ) + => Message ps st st' -> SomeMessage st -- @@ -98,26 +126,25 @@ data SomeMessage (st :: ps) where runPeerWithDriver :: forall ps (st :: ps) pr dstate m a. Monad m - => Driver ps dstate m - -> Peer ps pr st m a - -> dstate + => Driver ps pr dstate m + -> Peer ps pr NonPipelined st m a -> m (a, dstate) -runPeerWithDriver Driver{sendMessage, recvMessage} = - flip go +runPeerWithDriver Driver{sendMessage, recvMessage, initialDState} = + go initialDState where go :: forall st'. dstate - -> Peer ps pr st' m a + -> Peer ps pr 'NonPipelined st' m a -> m (a, dstate) go dstate (Effect k) = k >>= go dstate go dstate (Done _ x) = return (x, dstate) - go dstate (Yield stok msg k) = do - sendMessage stok msg + go dstate (Yield refl msg k) = do + sendMessage refl msg go dstate k - go dstate (Await stok k) = do - (SomeMessage msg, dstate') <- recvMessage stok dstate + go dstate (Await refl k) = do + (SomeMessage msg, dstate') <- recvMessage refl dstate go dstate' (k msg) -- Note that we do not complain about trailing data in any case, neither @@ -148,17 +175,16 @@ runPeerWithDriver Driver{sendMessage, recvMessage} = runPipelinedPeerWithDriver :: forall ps (st :: ps) pr dstate m a. MonadAsync m - => Driver ps dstate m + => Driver ps pr dstate m -> PeerPipelined ps pr st m a - -> dstate -> m (a, dstate) -runPipelinedPeerWithDriver driver (PeerPipelined peer) dstate0 = do +runPipelinedPeerWithDriver driver@Driver{initialDState} (PeerPipelined peer) = do receiveQueue <- atomically newTQueue collectQueue <- atomically newTQueue a <- runPipelinedPeerReceiverQueue receiveQueue collectQueue driver `withAsyncLoop` runPipelinedPeerSender receiveQueue collectQueue driver - peer dstate0 + peer initialDState return a where @@ -172,7 +198,7 @@ runPipelinedPeerWithDriver driver (PeerPipelined peer) dstate0 = do data ReceiveHandler dstate ps pr m c where ReceiveHandler :: MaybeDState dstate n - -> PeerReceiver ps pr (st :: ps) (st' :: ps) m c + -> Receiver ps pr (st :: ps) (st' :: ps) m c -> ReceiveHandler dstate ps pr m c -- | The handling of trailing data here is quite subtle. Trailing data is data @@ -228,45 +254,45 @@ runPipelinedPeerSender ) => TQueue m (ReceiveHandler dstate ps pr m c) -> TQueue m (c, dstate) - -> Driver ps dstate m - -> PeerSender ps pr st Z c m a + -> Driver ps pr dstate m + -> Peer ps pr ('Pipelined Z c) st m a -> dstate -> m (a, dstate) runPipelinedPeerSender receiveQueue collectQueue Driver{sendMessage, recvMessage} peer dstate0 = do threadId <- myThreadId - labelThread threadId "pipeliend-peer-seneder" + labelThread threadId "pipelined-peer-sender" go Zero (HasDState dstate0) peer where go :: forall st' n. Nat n -> MaybeDState dstate n - -> PeerSender ps pr st' n c m a + -> Peer ps pr ('Pipelined n c) st' m a -> m (a, dstate) - go n dstate (SenderEffect k) = k >>= go n dstate - go Zero (HasDState dstate) (SenderDone _ x) = return (x, dstate) + go n dstate (Effect k) = k >>= go n dstate + go Zero (HasDState dstate) (Done _ x) = return (x, dstate) - go Zero dstate (SenderYield stok msg k) = do - sendMessage stok msg + go Zero dstate (Yield refl msg k) = do + sendMessage refl msg go Zero dstate k - go Zero (HasDState dstate) (SenderAwait stok k) = do + go Zero (HasDState dstate) (Await stok k) = do (SomeMessage msg, dstate') <- recvMessage stok dstate go Zero (HasDState dstate') (k msg) - go n dstate (SenderPipeline stok msg receiver k) = do + go n dstate (YieldPipelined refl msg receiver k) = do atomically (writeTQueue receiveQueue (ReceiveHandler dstate receiver)) - sendMessage stok msg + sendMessage refl msg go (Succ n) NoDState k - go (Succ n) NoDState (SenderCollect Nothing k) = do + go (Succ n) NoDState (Collect Nothing k) = do (c, dstate) <- atomically (readTQueue collectQueue) case n of Zero -> go Zero (HasDState dstate) (k c) Succ n' -> go (Succ n') NoDState (k c) - go (Succ n) NoDState (SenderCollect (Just k') k) = do + go (Succ n) NoDState (Collect (Just k') k) = do mc <- atomically (tryReadTQueue collectQueue) case mc of Nothing -> go (Succ n) NoDState k' @@ -283,13 +309,13 @@ runPipelinedPeerReceiverQueue ) => TQueue m (ReceiveHandler dstate ps pr m c) -> TQueue m (c, dstate) - -> Driver ps dstate m + -> Driver ps pr dstate m -> m Void runPipelinedPeerReceiverQueue receiveQueue collectQueue - driver@Driver{startDState} = do + driver@Driver{initialDState} = do threadId <- myThreadId - labelThread threadId "pipelined-recevier-queue" - go startDState + labelThread threadId "pipelined-receiver-queue" + go initialDState where go :: dstate -> m Void go receiverDState = do @@ -306,20 +332,20 @@ runPipelinedPeerReceiverQueue receiveQueue collectQueue runPipelinedPeerReceiver :: forall ps (st :: ps) (stdone :: ps) pr dstate m c. Monad m - => Driver ps dstate m + => Driver ps pr dstate m -> dstate - -> PeerReceiver ps pr (st :: ps) (stdone :: ps) m c + -> Receiver ps pr (st :: ps) (stdone :: ps) m c -> m (c, dstate) runPipelinedPeerReceiver Driver{recvMessage} = go where go :: forall st' st''. dstate - -> PeerReceiver ps pr st' st'' m c + -> Receiver ps pr st' st'' m c -> m (c, dstate) go dstate (ReceiverEffect k) = k >>= go dstate go dstate (ReceiverDone x) = return (x, dstate) - go dstate (ReceiverAwait stok k) = do - (SomeMessage msg, dstate') <- recvMessage stok dstate + go dstate (ReceiverAwait refl k) = do + (SomeMessage msg, dstate') <- recvMessage refl dstate go dstate' (k msg) diff --git a/typed-protocols/src/Network/TypedProtocol/Lemmas.hs b/typed-protocols/src/Network/TypedProtocol/Lemmas.hs new file mode 100644 index 00000000..20bc5f0a --- /dev/null +++ b/typed-protocols/src/Network/TypedProtocol/Lemmas.hs @@ -0,0 +1,156 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeFamilies #-} + +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} +{-# HLINT ignore "Use camelCase" #-} + +-- | The module contains exclusion lemmas which are proven using ad absurdum: +-- +-- * it's impossible for both client and server have agency +-- * it's impossible for either side to be in a terminal state (no agency) and +-- the other side have agency +-- +module Network.TypedProtocol.Lemmas where + +import Data.Kind (Type) +import Network.TypedProtocol.Core + + +-- $about +-- +-- Typed languages such as Haskell can embed proofs. In total languages this +-- is straightforward: a value inhabiting a type is a proof of the property +-- corresponding to the type. +-- +-- In languages like Haskell that have ⊥ as a value of every type, things +-- are slightly more complicated. We have to demonstrate that the value that +-- inhabits the type of interest is not ⊥ which we can do by evaluation. +-- +-- This idea crops up frequently in advanced type level programming in Haskell. +-- For example @Refl@ proofs that two types are equal have to have a runtime +-- representation that is evaluated to demonstrate it is not ⊥ before it +-- can be relied upon. +-- +-- The proofs here are about the nature of typed protocols in this framework. +-- The 'connect' and 'connectPipelined' proofs rely on a few internal lemmas. + +-- | An evidence that both relative agencies are equal to 'NobodyHasAgency'. +-- +type ReflNobodyHasAgency :: RelativeAgency -> RelativeAgency -> Type +data ReflNobodyHasAgency ra ra' where + ReflNobodyHasAgency :: ReflNobodyHasAgency + NobodyHasAgency + NobodyHasAgency + + +-- | A proof that if both @Relative pr a@ and @Relative (FlipAgency pr) a@ are +-- equal then nobody has agency. In particular this lemma excludes the +-- possibility that client and server has agency at the same state. +-- +exclusionLemma_ClientAndServerHaveAgency + :: forall (pr :: PeerRole) (a :: Agency) + (ra :: RelativeAgency). + SingPeerRole pr + -> ReflRelativeAgency a ra (Relative pr a) + -- ^ evidence that `ra` is equal to `Relative pr a`, e.g. that client has + -- agency + -> ReflRelativeAgency a ra (Relative (FlipAgency pr) a) + -- ^ evidence that `ra` is equal to `Relative (FlipAgency pr) a`, e.g. that + -- the server has agency + -> ReflNobodyHasAgency (Relative pr a) + (Relative (FlipAgency pr) a) + -- ^ derived evidence that nobody has agency in that case +exclusionLemma_ClientAndServerHaveAgency + SingAsClient ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency +exclusionLemma_ClientAndServerHaveAgency + SingAsServer ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency + +exclusionLemma_ClientAndServerHaveAgency + SingAsClient ReflClientAgency x = case x of {} +exclusionLemma_ClientAndServerHaveAgency + SingAsServer ReflClientAgency x = case x of {} +exclusionLemma_ClientAndServerHaveAgency + SingAsClient ReflServerAgency x = case x of {} +exclusionLemma_ClientAndServerHaveAgency + SingAsServer ReflServerAgency x = case x of {} + + +-- | A proof that if one side has terminated, then the other side terminated as +-- well. +-- +terminationLemma_1 + :: SingPeerRole pr + -> ReflRelativeAgency a ra (Relative pr a) + -> ReflRelativeAgency a NobodyHasAgency (Relative (FlipAgency pr) a) + -> ReflNobodyHasAgency (Relative pr a) + (Relative (FlipAgency pr) a) +terminationLemma_1 + SingAsClient ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency +terminationLemma_1 + SingAsServer ReflNobodyAgency ReflNobodyAgency = ReflNobodyHasAgency +terminationLemma_1 SingAsClient ReflClientAgency x = case x of {} +terminationLemma_1 SingAsClient ReflServerAgency x = case x of {} +terminationLemma_1 SingAsServer ReflClientAgency x = case x of {} +terminationLemma_1 SingAsServer ReflServerAgency x = case x of {} + + +-- | Internal; only need to formulate auxiliary lemmas in the proof of +-- 'terminationLemma_2'. +-- +type FlipRelAgency :: RelativeAgency -> RelativeAgency +type family FlipRelAgency ra where + FlipRelAgency WeHaveAgency = TheyHaveAgency + FlipRelAgency TheyHaveAgency = WeHaveAgency + FlipRelAgency NobodyHasAgency = NobodyHasAgency + + +-- | Similar to 'terminationLemma_1'. +-- +-- Note: this could be proven the same way 'terminationLemma_1' is proved, but +-- instead we use two lemmas to reduce the assumptions (arguments) and we apply +-- 'terminationLemma_1'. +-- +terminationLemma_2 + :: SingPeerRole pr + -> ReflRelativeAgency a ra (Relative (FlipAgency pr) a) + -> ReflRelativeAgency a NobodyHasAgency (Relative pr a) + -> ReflNobodyHasAgency (Relative (FlipAgency pr) a) + (Relative pr a) + +terminationLemma_2 singPeerRole refl refl' = + case terminationLemma_1 singPeerRole + (lemma_flip singPeerRole refl) + (lemma_flip' singPeerRole refl') + of x@ReflNobodyHasAgency -> x + -- note: if we'd swap arguments of the returned @ReflNobodyHasAgency@ type, + -- we wouldn't need to pattern match on the result. But in this form the + -- lemma is a symmetric version of 'terminationLemma_1'. + where + lemma_flip + :: SingPeerRole pr + -> ReflRelativeAgency a ra (Relative (FlipAgency pr) a) + -> ReflRelativeAgency a (FlipRelAgency ra) (Relative pr a) + + lemma_flip' + :: SingPeerRole pr + -> ReflRelativeAgency a ra (Relative pr a) + -> ReflRelativeAgency a (FlipRelAgency ra) (Relative (FlipAgency pr) a) + + -- both lemmas are identity functions: + lemma_flip SingAsClient ReflClientAgency = ReflClientAgency + lemma_flip SingAsClient ReflServerAgency = ReflServerAgency + lemma_flip SingAsClient ReflNobodyAgency = ReflNobodyAgency + lemma_flip SingAsServer ReflClientAgency = ReflClientAgency + lemma_flip SingAsServer ReflServerAgency = ReflServerAgency + lemma_flip SingAsServer ReflNobodyAgency = ReflNobodyAgency + + lemma_flip' SingAsClient ReflClientAgency = ReflClientAgency + lemma_flip' SingAsClient ReflServerAgency = ReflServerAgency + lemma_flip' SingAsClient ReflNobodyAgency = ReflNobodyAgency + lemma_flip' SingAsServer ReflClientAgency = ReflClientAgency + lemma_flip' SingAsServer ReflServerAgency = ReflServerAgency + lemma_flip' SingAsServer ReflNobodyAgency = ReflNobodyAgency diff --git a/typed-protocols/src/Network/TypedProtocol/Peer.hs b/typed-protocols/src/Network/TypedProtocol/Peer.hs new file mode 100644 index 00000000..1f1097c1 --- /dev/null +++ b/typed-protocols/src/Network/TypedProtocol/Peer.hs @@ -0,0 +1,275 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +-- | Protocol EDSL. +-- +module Network.TypedProtocol.Peer + ( Peer (..) + , PeerPipelined (..) + , Receiver (..) + , Outstanding + , N (..) + , Nat (Zero, Succ) + , natToInt + , unsafeIntToNat + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core as Core + +-- | A description of a peer that engages in a protocol. +-- +-- __Note__: You should use pattern synonyms exposed in +-- "Network.TypedProtocol.Peer.Client" and "Network.TypedProtocol.Peer.Server", +-- however here we provide in-depth documentation. +-- +-- The protocol describes what messages peers /may/ send or /must/ accept. +-- A particular peer implementation decides what to actually do within the +-- constraints of the protocol. +-- +-- Peers engage in a protocol in either the client or server role. Of course +-- the client role can only interact with the serve role for the same protocol +-- and vice versa. +-- +-- 'Peer' has several type arguments: +-- +-- * the protocol itself; +-- * the client\/server role; +-- * whether the peer is using pipelining or not, if pipelined it holds the +-- depth of pipelining and a type used to collect data from pipelined +-- transitions; +-- * the current protocol state; +-- * the monad in which the peer operates (e.g. 'IO'); +-- * the type of the final result once the peer terminates. +-- +-- For example: +-- +-- > pingPongClientExample :: Peer PingPong AsClient (Pipelined Z Int) StIdle IO () +-- > pingPongServerExample :: Peer PingPong AsServer NonPipeliend StIdle IO Int +-- +-- The actions that a non-pipelining peer can take are: +-- +-- * to perform local monadic effects +-- * to terminate with a result (but only in a terminal protocol state) +-- * to send a message (but only in a protocol state in which we have agency) +-- * to wait to receive a message (but only in a protocol state in which the +-- other peer has agency) +-- +-- In addition a pipelining peer can: +-- +-- * pipeline a message, which requires upfront declaration at which state we +-- continue at and passing a receiver which will run in parallel. When +-- receiver terminates it pushes the result into the pipelining queue. +-- * collect a response from the pipelining queue. +-- +-- The 'Yield', 'Await', 'Done', 'YieldPipelined', 'Collect', +-- constructors require to provide an evidence that the +-- peer has agency in the current state. The types guarantee that it is not +-- possible to supply incorrect evidence, however the +-- pattern synonyms exposed in "Network.TypedProtocol.Peer.Client" and +-- "Network.TypedProtocol.Peer.Client" supply this evidence for you, and hence +-- are easier to use and let you avoid some kinds of type errors. +-- +type Peer :: forall ps + -> PeerRole + -> IsPipelined + -> ps + -> (Type -> Type) + -- ^ monad's kind + -> Type + -> Type +data Peer ps pr pl st m a where + + -- | Perform a local monadic effect and then continue. + -- + -- Example: + -- + -- > Effect $ do + -- > ... -- actions in the monad + -- > return $ ... -- another Peer value + -- + Effect + :: forall ps pr pl st m a. + m (Peer ps pr pl st m a) + -- ^ monadic continuation + -> Peer ps pr pl st m a + + -- | Send a message to the other peer and then continue. This takes the + -- message and the continuation. It also requires evidence that we have + -- agency for this protocol state and thus are allowed to send messages. + -- + -- Example: + -- + -- > Yield ReflClientAgency MsgPing $ ... + -- + Yield + :: forall ps pr pl (st :: ps) (st' :: ps) m a. + ( StateTokenI st + , StateTokenI st' + , ActiveState st + , Outstanding pl ~ Z + ) + => WeHaveAgencyProof pr st + -- ^ agency proof + -> Message ps st st' + -- ^ protocol message + -> Peer ps pr pl st' m a + -- ^ continuation + -> Peer ps pr pl st m a + + -- | Waits to receive a message from the other peer and then continues. + -- This takes the continuation that is supplied with the received message. It + -- also requires evidence that the other peer has agency for this protocol + -- state and thus we are expected to wait to receive messages. + -- + -- Note that the continuation that gets supplied with the message must be + -- prepared to deal with /any/ message that is allowed in /this/ protocol + -- state. This is why the continuation /must/ be polymorphic in the target + -- state of the message (the third type argument of 'Message'). + -- + -- Example: + -- + -- > Await ReflClientAgency $ \msg -> + -- > case msg of + -- > MsgDone -> ... + -- > MsgPing -> ... + -- + Await + :: forall ps pr pl (st :: ps) m a. + ( StateTokenI st + , ActiveState st + , Outstanding pl ~ Z + ) + => TheyHaveAgencyProof pr st + -- ^ agency proof + -> (forall (st' :: ps). Message ps st st' + -> Peer ps pr pl st' m a) + -- ^ continuation + -> Peer ps pr pl st m a + + -- | Terminate with a result. A state token must be provided from the + -- 'NobodyHasAgency' states, to show that this is a state in which we can + -- terminate. + -- + -- Example: + -- + -- > Yield ReflClientAgency + -- > MsgDone + -- > (Done ReflNobodyAgency TokDone result) + -- + Done + :: forall ps pr pl (st :: ps) m a. + ( StateTokenI st + , StateAgency st ~ NobodyAgency + , Outstanding pl ~ Z + ) + => NobodyHasAgencyProof pr st + -- ^ (no) agency proof + -> a + -- ^ returned value + -> Peer ps pr pl st m a + + -- + -- Pipelining primitives + -- + + -- | Pipelined send. We statically decide from which state we continue (the + -- `st''` state here), the gap (between `st'` and `st''`) must be fulfilled + -- by 'Receiver' which runs will run in parallel. + -- + YieldPipelined + :: forall ps pr (st :: ps) (st' :: ps) c n st'' m a. + ( StateTokenI st + , StateTokenI st' + , ActiveState st + ) + => WeHaveAgencyProof pr st + -- ^ agency proof + -> Message ps st st' + -- ^ protocol message + -> Receiver ps pr st' st'' m c + -- ^ receiver + -> Peer ps pr (Pipelined (S n) c) st'' m a + -- ^ continuation from state `st''` + -> Peer ps pr (Pipelined n c) st m a + + -- | Collect results returned by a `Receiver`. Results are collected in the + -- first-in-first-out way. + -- + Collect + :: forall ps pr c n st m a. + ( StateTokenI st + , ActiveState st + ) + => Maybe (Peer ps pr (Pipelined (S n) c) st m a) + -- ^ continuation, executed if no message has arrived so far + -> (c -> Peer ps pr (Pipelined n c) st m a) + -- ^ continuation + -> Peer ps pr (Pipelined (S n) c) st m a + +deriving instance Functor m => Functor (Peer ps pr pl st m) + + +-- | Receiver. It is limited to only awaiting for messages and running monadic +-- computations. This means that one can only pipeline messages if they can be +-- connected by state transitions which all have remote agency. +-- +-- The receiver runs in parallel, see `runPipelinedPeerWithDriver`. This makes +-- pipelining quite effective, since the receiver callbacks are called in +-- a separate thread which can effectively use CPU cache and can avoids +-- unnecessary context switches. +-- +type Receiver :: forall ps + -> PeerRole + -> ps + -- ^ initial state + -> ps + -- ^ final state + -> (Type -> Type) + -- ^ monad + -> Type + -- ^ returned type by the receiver + -> Type +data Receiver ps pr st stdone m c where + + -- | Execute a monadic computation. + -- + ReceiverEffect :: m (Receiver ps pr st stdone m c) + -> Receiver ps pr st stdone m c + + -- | Return value. + -- + ReceiverDone :: c -> Receiver ps pr stdone stdone m c + + -- | Await for for a remote transition. + -- + ReceiverAwait :: ( StateTokenI st + , ActiveState st + ) + => TheyHaveAgencyProof pr st + -> (forall st'. Message ps st st' + -> Receiver ps pr st' stdone m c) + -> Receiver ps pr st stdone m c + +deriving instance Functor m => Functor (Receiver ps pr st stdone m) + +-- | A description of a peer that engages in a protocol in a pipelined fashion. +-- +-- This type is useful for wrapping pipelined peers to hide information which +-- is only relevant in peer lift. It is expected by +-- `Network.TypedProtocol.Driver.runPeerPipelinedWithDriver`. +-- +data PeerPipelined ps pr (st :: ps) m a where + PeerPipelined :: { runPeerPipelined :: Peer ps pr (Pipelined Z c) st m a } + -> PeerPipelined ps pr st m a + +deriving instance Functor m => Functor (PeerPipelined ps pr st m) diff --git a/typed-protocols/src/Network/TypedProtocol/Peer/Client.hs b/typed-protocols/src/Network/TypedProtocol/Peer/Client.hs new file mode 100644 index 00000000..60c355c4 --- /dev/null +++ b/typed-protocols/src/Network/TypedProtocol/Peer/Client.hs @@ -0,0 +1,183 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +-- | Bidirectional patterns for @'Peer' ps 'AsClient'@. The advantage of +-- these patterns is that they automatically provide the 'ReflRelativeAgency' +-- evidence. +-- +module Network.TypedProtocol.Peer.Client + ( -- * Client type alias and its pattern synonyms + Client + , pattern Effect + , pattern Yield + , pattern Await + , pattern Done + , pattern YieldPipelined + , pattern Collect + -- * Receiver type alias and its pattern synonyms + , Receiver + , pattern ReceiverEffect + , pattern ReceiverAwait + , pattern ReceiverDone + -- * ClientPipelined type alias and its pattern synonym + , ClientPipelined + , TP.PeerPipelined (ClientPipelined, runClientPipelined) + -- * re-exports + , IsPipelined (..) + , Outstanding + , N (..) + , Nat (..) + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer (Peer) +import qualified Network.TypedProtocol.Peer as TP + + +type Client :: forall ps + -> IsPipelined + -> ps + -> (Type -> Type) + -> Type + -> Type +type Client ps pl st m a = Peer ps AsClient pl st m a + + +-- | A description of a peer that engages in a protocol in a pipelined fashion. +-- +type ClientPipelined ps st m a = TP.PeerPipelined ps AsClient st m a + +pattern ClientPipelined :: forall ps st m a. + () + => forall c. + () + => Client ps (Pipelined Z c) st m a + -> ClientPipelined ps st m a +pattern ClientPipelined { runClientPipelined } = TP.PeerPipelined runClientPipelined + +{-# COMPLETE ClientPipelined #-} + +-- | Client role pattern for 'TP.Effect'. +-- +pattern Effect :: forall ps pl st m a. + m (Client ps pl st m a) + -- ^ monadic continuation + -> Client ps pl st m a +pattern Effect mclient = TP.Effect mclient + + +-- | Client role pattern for 'TP.Yield' +-- +pattern Yield :: forall ps pl st m a. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ClientAgency + , Outstanding pl ~ Z + ) + => Message ps st st' + -- ^ protocol message + -> Client ps pl st' m a + -- ^ continuation + -> Client ps pl st m a +pattern Yield msg k = TP.Yield ReflClientAgency msg k + + +-- | Client role pattern for 'TP.Await' +-- +pattern Await :: forall ps pl st m a. + () + => ( StateTokenI st + , StateAgency st ~ ServerAgency + , Outstanding pl ~ Z + ) + => (forall st'. Message ps st st' + -> Client ps pl st' m a) + -- ^ continuation + -> Client ps pl st m a +pattern Await k = TP.Await ReflServerAgency k + + +-- | Client role pattern for 'TP.Done' +-- +pattern Done :: forall ps pl st m a. + () + => ( StateTokenI st + , StateAgency st ~ NobodyAgency + , Outstanding pl ~ Z + ) + => a + -- ^ protocol return value + -> Client ps pl st m a +pattern Done a = TP.Done ReflNobodyAgency a + + +-- | Client role pattern for 'TP.YieldPipelined' +-- +pattern YieldPipelined :: forall ps st n c m a. + () + => forall st' st''. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ClientAgency + ) + => Message ps st st' + -- ^ pipelined message + -> Receiver ps st' st'' m c + -> Client ps (Pipelined (S n) c) st'' m a + -- ^ continuation + -> Client ps (Pipelined n c) st m a +pattern YieldPipelined msg receiver k = TP.YieldPipelined ReflClientAgency msg receiver k + + +-- | Client role pattern for 'TP.Collect' +-- +pattern Collect :: forall ps st n c m a. + () + => ( StateTokenI st + , ActiveState st + ) + => Maybe (Client ps (Pipelined (S n) c) st m a) + -- ^ continuation, executed if no message has arrived so far + -> (c -> Client ps (Pipelined n c) st m a) + -- ^ continuation + -> Client ps (Pipelined (S n) c) st m a +pattern Collect k' k = TP.Collect k' k + +{-# COMPLETE Effect, Yield, Await, Done, YieldPipelined, Collect #-} + + +type Receiver ps st stdone m c = TP.Receiver ps AsClient st stdone m c + +pattern ReceiverEffect :: forall ps st stdone m c. + m (Receiver ps st stdone m c) + -> Receiver ps st stdone m c +pattern ReceiverEffect k = TP.ReceiverEffect k + +pattern ReceiverAwait :: forall ps st stdone m c. + () + => ( StateTokenI st + , ActiveState st + , StateAgency st ~ ServerAgency + ) + => (forall st'. Message ps st st' + -> Receiver ps st' stdone m c + ) + -> Receiver ps st stdone m c +pattern ReceiverAwait k = TP.ReceiverAwait ReflServerAgency k + +pattern ReceiverDone :: forall ps stdone m c. + c + -> Receiver ps stdone stdone m c +pattern ReceiverDone c = TP.ReceiverDone c + +{-# COMPLETE ReceiverEffect, ReceiverAwait, ReceiverDone #-} diff --git a/typed-protocols/src/Network/TypedProtocol/Peer/Server.hs b/typed-protocols/src/Network/TypedProtocol/Peer/Server.hs new file mode 100644 index 00000000..025fbf3f --- /dev/null +++ b/typed-protocols/src/Network/TypedProtocol/Peer/Server.hs @@ -0,0 +1,185 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeOperators #-} + +-- | Bidirectional patterns for @'Peer' ps 'AsServer'@. The advantage of +-- these patterns is that they automatically provide the 'ReflRelativeAgency' +-- evidence. +-- +module Network.TypedProtocol.Peer.Server + ( -- * Server type alias and its pattern synonyms + Server + , pattern Effect + , pattern Yield + , pattern Await + , pattern Done + , pattern YieldPipelined + , pattern Collect + -- * Receiver type alias and its pattern synonyms + , Receiver + , pattern ReceiverEffect + , pattern ReceiverAwait + , pattern ReceiverDone + -- * ServerPipelined type alias and its pattern synonym + , ServerPipelined + , TP.PeerPipelined (ServerPipelined, runServerPipelined) + -- * re-exports + , IsPipelined (..) + , Outstanding + , N (..) + , Nat (..) + ) where + +import Data.Kind (Type) + +import Network.TypedProtocol.Core +import Network.TypedProtocol.Peer (Peer) +import qualified Network.TypedProtocol.Peer as TP + + +type Server :: forall ps + -> IsPipelined + -> ps + -> (Type -> Type) + -> Type + -> Type +type Server ps pl st m a = Peer ps AsServer pl st m a + + +-- | A description of a peer that engages in a protocol in a pipelined fashion. +-- +type ServerPipelined ps st m a = TP.PeerPipelined ps AsServer st m a + +pattern ServerPipelined :: forall ps st m a. + () + => forall c. + () + => Server ps (Pipelined Z c) st m a + -> ServerPipelined ps st m a +pattern ServerPipelined { runServerPipelined } = TP.PeerPipelined runServerPipelined + +{-# COMPLETE ServerPipelined #-} + + +-- | Server role pattern for 'TP.Effect'. +-- +pattern Effect :: forall ps pl st m a. + m (Server ps pl st m a) + -- ^ monadic continuation + -> Server ps pl st m a +pattern Effect mclient = TP.Effect mclient + + +-- | Server role pattern for 'TP.Yield' +-- +pattern Yield :: forall ps pl st m a. + () + => forall st'. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ServerAgency + , Outstanding pl ~ Z + ) + => Message ps st st' + -- ^ protocol message + -> Server ps pl st' m a + -- ^ continuation + -> Server ps pl st m a +pattern Yield msg k = TP.Yield ReflServerAgency msg k + + +-- | Server role pattern for 'TP.Await' +-- +pattern Await :: forall ps pl st m a. + () + => ( StateTokenI st + , StateAgency st ~ ClientAgency + , Outstanding pl ~ Z + ) + => (forall st'. Message ps st st' + -> Server ps pl st' m a) + -- ^ continuation + -> Server ps pl st m a +pattern Await k = TP.Await ReflClientAgency k + + +-- | Server role pattern for 'TP.Done' +-- +pattern Done :: forall ps pl st m a. + () + => ( StateTokenI st + , StateAgency st ~ NobodyAgency + , Outstanding pl ~ Z + ) + => a + -- ^ protocol return value + -> Server ps pl st m a +pattern Done a = TP.Done ReflNobodyAgency a + + +-- | Server role pattern for 'TP.YieldPipelined' +-- +pattern YieldPipelined :: forall ps st n c m a. + () + => forall st' st''. + ( StateTokenI st + , StateTokenI st' + , StateAgency st ~ ServerAgency + ) + => Message ps st st' + -- ^ pipelined message + -> Receiver ps st' st'' m c + -> Server ps (Pipelined (S n) c) st'' m a + -- ^ continuation + -> Server ps (Pipelined n c) st m a +pattern YieldPipelined msg receiver k = TP.YieldPipelined ReflServerAgency msg receiver k + + +-- | Server role pattern for 'TP.Collect' +-- +pattern Collect :: forall ps st n c m a. + () + => ( StateTokenI st + , ActiveState st + ) + => Maybe (Server ps (Pipelined (S n) c) st m a) + -- ^ continuation, executed if no message has arrived so far + -> (c -> Server ps (Pipelined n c) st m a) + -- ^ continuation + -> Server ps (Pipelined (S n) c) st m a +pattern Collect k' k = TP.Collect k' k + + +{-# COMPLETE Effect, Yield, Await, Done, YieldPipelined, Collect #-} + + +type Receiver ps st stdone m c = TP.Receiver ps AsServer st stdone m c + +pattern ReceiverEffect :: forall ps st stdone m c. + m (Receiver ps st stdone m c) + -> Receiver ps st stdone m c +pattern ReceiverEffect k = TP.ReceiverEffect k + +pattern ReceiverAwait :: forall ps st stdone m c. + () + => ( StateTokenI st + , ActiveState st + , StateAgency st ~ ClientAgency + ) + => (forall st'. Message ps st st' + -> Receiver ps st' stdone m c + ) + -> Receiver ps st stdone m c +pattern ReceiverAwait k = TP.ReceiverAwait ReflClientAgency k + +pattern ReceiverDone :: forall ps stdone m c. + c + -> Receiver ps stdone stdone m c +pattern ReceiverDone c = TP.ReceiverDone c + +{-# COMPLETE ReceiverEffect, ReceiverAwait, ReceiverDone #-} diff --git a/typed-protocols/src/Network/TypedProtocol/Pipelined.hs b/typed-protocols/src/Network/TypedProtocol/Pipelined.hs deleted file mode 100644 index aa0a002b..00000000 --- a/typed-protocols/src/Network/TypedProtocol/Pipelined.hs +++ /dev/null @@ -1,197 +0,0 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DerivingStrategies #-} -{-# LANGUAGE DerivingVia #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PatternSynonyms #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE ViewPatterns #-} - -module Network.TypedProtocol.Pipelined - ( PeerPipelined (..) - , PeerSender (..) - , PeerReceiver (..) - , Outstanding - , N (..) - , Nat (Zero, Succ) - , natToInt - , unsafeIntToNat - , fmapPeerPipelined - ) where - -import Unsafe.Coerce (unsafeCoerce) - -import Network.TypedProtocol.Core - - --- | A description of a peer that engages in a protocol in a pipelined fashion. --- --- This is very much like 'Peer', and can work with the same protocol state --- machine descriptions, but allows the peer to pipeline the execution of --- the protocol. --- --- This wraps a 'PeerSender', but works for any internal collect type @c@, and --- with the starting condition of zero outstanding pipelined responses. --- -data PeerPipelined ps (pr :: PeerRole) (st :: ps) m a where - PeerPipelined :: PeerSender ps pr st Z c m a - -> PeerPipelined ps pr st m a - -deriving instance Functor m => Functor (PeerPipelined ps (pr :: PeerRole) (st :: ps) m) - --- | More general than 'fmap', as it allows to change the protocol. --- -fmapPeerPipelined :: (forall c. PeerSender ps pr st Z c m a -> PeerSender ps' pr st' Z c m b) - -> PeerPipelined ps pr st m a - -> PeerPipelined ps' pr st' m b -fmapPeerPipelined f (PeerPipelined peer) = PeerPipelined (f peer) - - --- | This is the pipelined variant of 'Peer'. --- --- In particular it has two extra type arguments: --- --- * @(n :: 'Outstanding')@ records the number of outstanding pipelined --- responses. Note that when this is 'Z' then we have no such outstanding --- responses, and we are in an equivalent situation to a normal --- non-pipelined 'Peer' --- --- * @c@ records the internal type of the pipelined responses. --- -data PeerSender ps (pr :: PeerRole) (st :: ps) (n :: Outstanding) c m a where - - -- | Same idea as normal 'Peer' 'Effect'. - SenderEffect :: m (PeerSender ps pr st n c m a) - -> PeerSender ps pr st n c m a - - -- | Same idea as normal 'Peer' 'Done'. - SenderDone :: !(NobodyHasAgency st) - -> a - -> PeerSender ps pr st Z c m a - - -- | A normal non-pipelined 'Yield'. - -- - -- Note that we cannot mix pipelined and normal synchronous syle, so this - -- can only be used when there are no outstanding pipelined responses. - -- - -- The @n ~ 'Z'@ constraint provides the type level guarantees that there - -- are no outstanding pipelined responses. - -- - SenderYield :: !(WeHaveAgency pr st) - -> Message ps st st' - -> PeerSender ps pr st' Z c m a - -> PeerSender ps pr st Z c m a - - -- | A normal non-pipelined 'Await'. Note that this can only be used . - -- - -- Note that we cannot mix pipelined and normal synchronous syle, so this - -- can only be used when there are no outstanding pipelined responses. - -- - -- The @n ~ 'Z'@ constraint provides the type level guarantees that there - -- are no outstanding pipelined responses. - -- - SenderAwait :: !(TheyHaveAgency pr st) - -> (forall st'. Message ps st st' - -> PeerSender ps pr st' Z c m a) - -> PeerSender ps pr st Z c m a - - -- | A pipelined equivalent of 'Yield'. The key difference is that instead - -- of moving into the immediate next state @st'@, the sender jumps directly - -- to state @st''@ and a seperate 'PeerReceiver' has to be supplied which - -- will get from @st'@ to @st''@. This sets up an outstanding pipelined - -- receive. The queue of outstanding pipelined receive actions 'PeerReceiver' - -- are executed in order, as messages arrive from the remote peer. - -- - -- The type records the fact that the number of outstanding pipelined - -- responses increases by one. - -- - SenderPipeline :: !(WeHaveAgency pr st) - -> Message ps st st' - -> PeerReceiver ps pr (st' :: ps) (st'' :: ps) m c - -> PeerSender ps pr (st'' :: ps) (S n) c m a - -> PeerSender ps pr (st :: ps) n c m a - - -- | Collect the result of a previous pipelined receive action. - -- - -- This (optionally) provides two choices: - -- - -- * Continue without a pipelined result - -- * Continue with a pipelined result - -- - -- Since presenting the first choice is optional, this allows expressing - -- both a blocking collect and a non-blocking collect. This allows - -- implementations to express policies such as sending a short sequence - -- of messages and then waiting for all replies, but also a maximum - -- pipelining policy that keeps a large number of messages in flight but - -- collects results eagerly. - -- - -- The type records the fact that when collecting a response, the number of - -- outstanding pipelined responses decreases by one. The type also guarantees - -- that it can only be used when there is at least one outstanding response. - -- - SenderCollect :: Maybe (PeerSender ps pr (st :: ps) (S n) c m a) - -> (c -> PeerSender ps pr (st :: ps) n c m a) - -> PeerSender ps pr (st :: ps) (S n) c m a - -deriving instance Functor m => Functor (PeerSender ps (pr :: PeerRole) (st :: ps) (n :: Outstanding) c m) - -data PeerReceiver ps (pr :: PeerRole) (st :: ps) (stdone :: ps) m c where - - ReceiverEffect :: m (PeerReceiver ps pr st stdone m c) - -> PeerReceiver ps pr st stdone m c - - ReceiverDone :: c -> PeerReceiver ps pr stdone stdone m c - - ReceiverAwait :: !(TheyHaveAgency pr st) - -> (forall st'. Message ps st st' - -> PeerReceiver ps pr st' stdone m c) - -> PeerReceiver ps pr st stdone m c - - --- | 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 = N - --- | A type level inductive natural number. -data N = Z | S N - --- | A value level inductive natural number, indexed by the corresponding type --- level natural number 'N'. --- --- This is often needed when writing pipelined peers to be able to count the --- number of outstanding pipelined yields, and show to the type checker that --- 'SenderCollect' and 'SenderDone' are being used correctly. --- -newtype Nat (n :: N) = UnsafeInt Int - deriving Show via Int - -data IsNat (n :: N) where - IsZero :: IsNat Z - IsSucc :: Nat n -> IsNat (S n) - -toIsNat :: Nat n -> IsNat n -toIsNat (UnsafeInt 0) = unsafeCoerce IsZero -toIsNat (UnsafeInt n) = unsafeCoerce (IsSucc (UnsafeInt (pred n))) - -pattern Zero :: () => Z ~ n => Nat n -pattern Zero <- (toIsNat -> IsZero) where - Zero = UnsafeInt 0 - -pattern Succ :: () => (m ~ S n) => Nat n -> Nat m -pattern Succ n <- (toIsNat -> IsSucc n) where - Succ (UnsafeInt n) = UnsafeInt (succ n) - -{-# COMPLETE Zero, Succ #-} - -natToInt :: Nat n -> Int -natToInt (UnsafeInt n) = n - -unsafeIntToNat :: Int -> Nat n -unsafeIntToNat = UnsafeInt diff --git a/typed-protocols/src/Network/TypedProtocol/Proofs.hs b/typed-protocols/src/Network/TypedProtocol/Proofs.hs index 289c0973..69125573 100644 --- a/typed-protocols/src/Network/TypedProtocol/Proofs.hs +++ b/typed-protocols/src/Network/TypedProtocol/Proofs.hs @@ -1,62 +1,41 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE RecordWildCards #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeFamilies #-} - +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE EmptyCase #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} -- This is already implied by the -Wall in the .cabal file, but lets just be -- completely explicit about it too, since we rely on the completeness -- checking in the cases below for the completeness of our proofs. {-# OPTIONS_GHC -Wincomplete-patterns #-} --- | Proofs about the typed protocol framework. --- --- It also provides helpful testing utilities. +-- | Proofs and helpful testing utilities. -- module Network.TypedProtocol.Proofs - ( -- * About these proofs - -- $about - -- * Connect proof + ( -- * Connect proofs connect + , connectPipelined , TerminalStates (..) -- * Pipelining proofs -- | Additional proofs specific to the pipelining features - , connectPipelined , forgetPipelined + , promoteToPipelined -- ** Pipeline proof helpers , Queue (..) , enqueue - -- ** Auxilary functions + -- ** Auxiliary functions , pipelineInterleaving ) where -import Data.Void (absurd) +import Data.Singletons import Network.TypedProtocol.Core -import Network.TypedProtocol.Pipelined - --- $about --- --- Typed languages such as Haskell can embed proofs. In total languages this --- is straightforward: a value inhabiting a type is a proof of the property --- corresponding to the type. --- --- In languages like Haskell that have ⊥ as a value of every type, things --- are slightly more complicated. We have to demonstrate that the value that --- inhabits the type of interest is not ⊥ which we can do by evaluation. --- --- This idea crops up frequently in advanced type level programming in Haskell. --- For example @Refl@ proofs that two types are equal have to have a runtime --- representation that is evaluated to demonstrate it is not ⊥ before it --- can be relied upon. --- --- The proofs here are about the nature of typed protocols in this framework. --- The 'connect' and 'connectPipelined' proofs rely on a few lemmas about --- the individual protocol. See 'AgencyProofs'. - - +import Network.TypedProtocol.Lemmas +import Network.TypedProtocol.Peer -- | The 'connect' function takes two peers that agree on a protocol and runs @@ -73,18 +52,31 @@ import Network.TypedProtocol.Pipelined -- * It is useful for testing peer implementations against each other in a -- minimalistic setting. -- -connect :: forall ps (pr :: PeerRole) (st :: ps) m a b. - (Monad m, Protocol ps) - => Peer ps pr st m a - -> Peer ps (FlipAgency pr) st m b - -> m (a, b, TerminalStates ps) +connect + :: forall ps (pr :: PeerRole) (initSt :: ps) m a b. + (Monad m, SingI pr) + => Peer ps pr NonPipelined initSt m a + -- ^ a peer + -> Peer ps (FlipAgency pr) NonPipelined initSt m b + -- ^ a peer with flipped agency + -> m (a, b, TerminalStates ps) + -- ^ peers results and an evidence of their termination connect = go where - go :: forall (st' :: ps). - Peer ps pr st' m a - -> Peer ps (FlipAgency pr) st' m b + singPeerRole :: Sing pr + singPeerRole = sing + + go :: forall (st :: ps). + Peer ps pr NonPipelined st m a + -> Peer ps (FlipAgency pr) NonPipelined st m b -> m (a, b, TerminalStates ps) - go (Done stA a) (Done stB b) = return (a, b, TerminalStates stA stB) + go (Done ReflNobodyAgency a) (Done ReflNobodyAgency b) = + return (a, b, terminals) + where + terminals :: TerminalStates ps + terminals = TerminalStates (stateToken :: StateToken st) + (stateToken :: StateToken st) + go (Effect a ) b = a >>= \a' -> go a' b go a (Effect b) = b >>= \b' -> go a b' go (Yield _ msg a) (Await _ b) = go a (b msg) @@ -92,239 +84,161 @@ connect = go -- By appealing to the proofs about agency for this protocol we can -- show that these other cases are impossible - go (Yield (ClientAgency stA) _ _) (Yield (ServerAgency stB) _ _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stA stB) - - go (Yield (ServerAgency stA) _ _) (Yield (ClientAgency stB) _ _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stB stA) - - go (Await (ServerAgency stA) _) (Await (ClientAgency stB) _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stB stA) - - go (Await (ClientAgency stA) _) (Await (ServerAgency stB) _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stA stB) - - go (Done stA _) (Yield (ServerAgency stB) _ _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stA stB) - - go (Done stA _) (Yield (ClientAgency stB) _ _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stA stB) + go (Yield reflA _ _) (Yield reflB _ _) = + case exclusionLemma_ClientAndServerHaveAgency singPeerRole reflA reflB of + ReflNobodyHasAgency -> case reflA of {} - go (Done stA _) (Await (ClientAgency stB) _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stA stB) + go (Await reflA _) (Await reflB _) = + case exclusionLemma_ClientAndServerHaveAgency singPeerRole reflA reflB of + ReflNobodyHasAgency -> case reflA of {} - go (Done stA _) (Await (ServerAgency stB) _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stA stB) + go (Done reflA _) (Yield reflB _ _) = + case terminationLemma_2 singPeerRole reflB reflA of + ReflNobodyHasAgency -> case reflB of {} - go (Yield (ClientAgency stA) _ _) (Done stB _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA) + go (Done reflA _) (Await reflB _) = + case terminationLemma_2 singPeerRole reflB reflA of + ReflNobodyHasAgency -> case reflB of {} - go (Yield (ServerAgency stA) _ _) (Done stB _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA) + go (Yield reflA _ _) (Done reflB _) = + case terminationLemma_1 singPeerRole reflA reflB of + ReflNobodyHasAgency -> case reflA of {} - go (Await (ServerAgency stA) _) (Done stB _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA) - - go (Await (ClientAgency stA) _) (Done stB _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA) + go (Await reflA _) (Done reflB _) = + case terminationLemma_1 singPeerRole reflA reflB of + ReflNobodyHasAgency -> case reflA of {} -- | The terminal states for the protocol. Used in 'connect' and -- 'connectPipelined' to return the states in which the peers terminated. -- data TerminalStates ps where - TerminalStates :: forall ps (st :: ps). - NobodyHasAgency st - -> NobodyHasAgency st - -> TerminalStates ps - + TerminalStates + :: forall ps (st :: ps). + (StateAgency st ~ NobodyAgency) + => StateToken st + -- ^ state termination evidence for the first peer + -> StateToken st + -- ^ state termination evidence for the second peer + -> TerminalStates ps --- | Analogous to 'connect' but for pipelined peers. --- --- Since pipelining allows multiple possible interleavings, we provide a --- @[Bool]@ parameter to control the choices. Each @True@ will trigger picking --- the first choice in the @SenderCollect@ construct (if possible), leading --- to more results outstanding. This can also be interpreted as a greater --- pipeline depth, or more messages in-flight. -- --- This can be exercised using a QuickCheck style generator. +-- Remove Pipelining -- -connectPipelined :: forall ps (pr :: PeerRole) (st :: ps) m a b. - (Monad m, Protocol ps) - => [Bool] -- ^ Interleaving choices. [] gives no pipelining. - -> PeerPipelined ps pr st m a - -> Peer ps (FlipAgency pr) st m b - -> m (a, b, TerminalStates ps) - -connectPipelined cs0 (PeerPipelined peerA) peerB = - goSender cs0 EmptyQ peerA peerB - where - goSender :: forall (st' :: ps) n c. - [Bool] - -> Queue n c - -> PeerSender ps pr st' n c m a - -> Peer ps (FlipAgency pr) st' m b - -> m (a, b, TerminalStates ps) - - goSender _ EmptyQ (SenderDone stA a) (Done stB b) = return (a, b, terminals) - where terminals = TerminalStates stA stB - - goSender cs q (SenderEffect a) b = a >>= \a' -> goSender cs q a' b - goSender cs q a (Effect b) = b >>= \b' -> goSender cs q a b' - - goSender cs q (SenderYield _ msg a) (Await _ b) = goSender cs q a (b msg) - goSender cs q (SenderAwait _ a) (Yield _ msg b) = goSender cs q (a msg) b - - -- This does the receiver effects immediately, as if there were no - -- pipelining. - goSender cs q (SenderPipeline _ msg r a) (Await _ b) = - goReceiver r (b msg) >>= \(b', x) -> goSender cs (enqueue x q) a b' - - -- However we make it possible to exercise the choice the environment has - -- in the non-determinism of the pipeline interleaving of collecting - -- results. Always picking the second continuation gives the fully serial - -- order. Always picking the first leads to a maximal (and possibly - -- unbounded) number of pending replies. By using a list of bools to - -- control the choices here, we can test any other order: - goSender (True:cs) q (SenderCollect (Just a) _) b = goSender cs q a b - goSender (_:cs) (ConsQ x q) (SenderCollect _ a) b = goSender cs q (a x) b - goSender [] (ConsQ x q) (SenderCollect _ a) b = goSender [] q (a x) b - - -- Proofs that the remaining cases are impossible - goSender _ _ (SenderDone stA _) (Yield (ServerAgency stB) _ _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stA stB) - - goSender _ _ (SenderDone stA _) (Yield (ClientAgency stB) _ _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stA stB) - - goSender _ _ (SenderDone stA _) (Await (ClientAgency stB) _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stA stB) - - goSender _ _ (SenderDone stA _) (Await (ServerAgency stB) _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stA stB) - - goSender _ _ (SenderYield (ClientAgency stA) _ _) (Done stB _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA) - - goSender _ _ (SenderYield (ServerAgency stA) _ _) (Done stB _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA) - - goSender _ _ (SenderYield (ClientAgency stA) _ _) (Yield (ServerAgency stB) _ _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stA stB) - - goSender _ _ (SenderYield (ServerAgency stA) _ _) (Yield (ClientAgency stB) _ _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stB stA) - - goSender _ _ (SenderAwait (ClientAgency stA) _) (Done stB _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA) - - goSender _ _ (SenderAwait (ServerAgency stA) _) (Done stB _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA) - - goSender _ _ (SenderAwait (ClientAgency stA) _) (Await (ServerAgency stB) _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stA stB) - - goSender _ _ (SenderAwait (ServerAgency stA) _) (Await (ClientAgency stB) _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stB stA) - - goSender _ _ (SenderPipeline (ClientAgency stA) _ _ _) (Done stB _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA) - - goSender _ _ (SenderPipeline (ServerAgency stA) _ _ _) (Done stB _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA) - goSender _ _ (SenderPipeline (ClientAgency stA) _ _ _) (Yield (ServerAgency stB) _ _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stA stB) - goSender _ _ (SenderPipeline (ServerAgency stA) _ _ _) (Yield (ClientAgency stB) _ _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stB stA) - - - goReceiver :: forall (st' :: ps) (stdone :: ps) c. - PeerReceiver ps pr st' stdone m c - -> Peer ps (FlipAgency pr) st' m b - -> m (Peer ps (FlipAgency pr) stdone m b, c) - - goReceiver (ReceiverDone x) b = return (b, x) - goReceiver (ReceiverEffect a) b = a >>= \a' -> goReceiver a' b - goReceiver a (Effect b) = b >>= \b' -> goReceiver a b' - - goReceiver (ReceiverAwait _ a) (Yield _ msg b) = goReceiver (a msg) b - - - -- Proofs that the remaining cases are impossible - goReceiver (ReceiverAwait (ServerAgency stA) _) (Done stB _) = - absurd (exclusionLemma_NobodyAndServerHaveAgency stB stA) - - goReceiver (ReceiverAwait (ClientAgency stA) _) (Done stB _) = - absurd (exclusionLemma_NobodyAndClientHaveAgency stB stA) - - goReceiver (ReceiverAwait (ServerAgency stA) _) (Await (ClientAgency stB) _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stB stA) +-- | A size indexed queue. This is useful for proofs, including +-- 'connectPipelined' but also as so-called @direct@ functions for running a +-- client and server wrapper directly against each other. +-- +data Queue (n :: N) a where + EmptyQ :: Queue Z a + ConsQ :: a -> Queue n a -> Queue (S n) a - goReceiver (ReceiverAwait (ClientAgency stA) _) (Await (ServerAgency stB) _) = - absurd (exclusionLemma_ClientAndServerHaveAgency stA stB) +-- | At an element to the end of a 'Queue'. This is not intended to be +-- efficient. It is only for proofs and tests. +-- +enqueue :: a -> Queue n a -> Queue (S n) a +enqueue a EmptyQ = ConsQ a EmptyQ +enqueue a (ConsQ b q) = ConsQ b (enqueue a q) --- | Prove that we have a total conversion from pipelined peers to regular +-- | Proof that we have a total conversion from pipelined peers to regular -- peers. This is a sanity property that shows that pipelining did not give -- us extra expressiveness or to break the protocol state machine. -- forgetPipelined :: forall ps (pr :: PeerRole) (st :: ps) m a. Functor m - => PeerPipelined ps pr st m a - -> Peer ps pr st m a -forgetPipelined (PeerPipelined peer) = goSender EmptyQ peer + => [Bool] + -- ^ interleaving choices for pipelining allowed by `Collect` primitive. False + -- values or `[]` give no pipelining. + -> PeerPipelined ps pr st m a + -> Peer ps pr NonPipelined st m a +forgetPipelined cs0 (PeerPipelined peer) = goSender EmptyQ cs0 peer where goSender :: forall st' n c. - Queue n c - -> PeerSender ps pr st' n c m a - -> Peer ps pr st' m a - - goSender EmptyQ (SenderDone st k) = Done st k - goSender q (SenderEffect k) = Effect (goSender q <$> k) - goSender q (SenderYield st m k) = Yield st m (goSender q k) - goSender q (SenderAwait st k) = Await st (goSender q <$> k) - goSender q (SenderPipeline st m r k) = Yield st m (goReceiver q k r) - goSender (ConsQ x q) (SenderCollect _ k) = goSender q (k x) - -- Here by picking the second continuation in Collect we resolve the - -- non-determinism by always picking the fully in-order non-pipelined - -- data flow path. + Queue n c + -> [Bool] + -> Peer ps pr ('Pipelined n c) st' m a + -> Peer ps pr 'NonPipelined st' m a + + goSender EmptyQ _cs (Done refl k) = Done refl k + goSender q cs (Effect k) = Effect (goSender q cs <$> k) + goSender q cs (Yield refl m k) = Yield refl m (goSender q cs k) + goSender q cs (Await refl k) = Await refl (goSender q cs <$> k) + goSender q cs (YieldPipelined refl m r k) = Yield refl m (goReceiver q cs k r) + goSender q (True:cs') (Collect (Just k) _) = goSender q cs' k + goSender (ConsQ x q) (_:cs) (Collect _ k) = goSender q cs (k x) + goSender (ConsQ x q) cs@[] (Collect _ k) = goSender q cs (k x) goReceiver :: forall stCurrent stNext n c. - Queue n c - -> PeerSender ps pr stNext (S n) c m a - -> PeerReceiver ps pr stCurrent stNext m c - -> Peer ps pr stCurrent m a + Queue n c + -> [Bool] + -> Peer ps pr ('Pipelined (S n) c) stNext m a + -> Receiver ps pr stCurrent stNext m c + -> Peer ps pr 'NonPipelined stCurrent m a - goReceiver q s (ReceiverDone x) = goSender (enqueue x q) s - goReceiver q s (ReceiverEffect k) = Effect (goReceiver q s <$> k) - goReceiver q s (ReceiverAwait st k) = Await st (goReceiver q s . k) + goReceiver q cs s (ReceiverDone x) = goSender (enqueue x q) cs s + goReceiver q cs s (ReceiverEffect k) = Effect (goReceiver q cs s <$> k) + goReceiver q cs s (ReceiverAwait refl k) = Await refl (goReceiver q cs s . k) --- | A size indexed queue. This is useful for proofs, including --- 'connectPipelined' but also as so-called @direct@ functions for running a --- client and server wrapper directly against each other. +-- | Promote a peer to a pipelined one. -- -data Queue (n :: N) a where - EmptyQ :: Queue Z a - ConsQ :: a -> Queue n a -> Queue (S n) a - --- | At an element to the end of a 'Queue'. This is not intended to be --- efficient. It is only for proofs and tests. +-- This is a right inverse of `forgetPipelined`, e.g. -- -enqueue :: a -> Queue n a -> Queue (S n) a -enqueue a EmptyQ = ConsQ a EmptyQ -enqueue a (ConsQ b q) = ConsQ b (enqueue a q) +-- >>> forgetPipelined . promoteToPipelined = id +-- +promoteToPipelined + :: forall ps (pr :: PeerRole) st m a. + Functor m + => Peer ps pr NonPipelined st m a + -- ^ a peer + -> PeerPipelined ps pr st m a + -- ^ a pipelined peer +promoteToPipelined p = PeerPipelined (go p) + where + go :: forall st' c. + Peer ps pr NonPipelined st' m a + -> Peer ps pr (Pipelined Z c) st' m a + go (Effect k) = Effect $ go <$> k + go (Yield refl msg k) = Yield refl msg (go k) + go (Await refl k) = Await refl (go . k) + go (Done refl k) = Done refl k + +-- | Analogous to 'connect' but also for pipelined peers. +-- +-- Since pipelining allows multiple possible interleavings, we provide a +-- @[Bool]@ parameter to control the choices. Each @True@ will trigger picking +-- the first choice in the @SenderCollect@ construct (if possible), leading +-- to more results outstanding. This can also be interpreted as a greater +-- pipeline depth, or more messages in-flight. +-- +-- This can be exercised using a QuickCheck style generator. +-- +connectPipelined + :: forall ps (pr :: PeerRole) + (st :: ps) m a b. + (Monad m, SingI pr) + => [Bool] + -- ^ an interleaving + -> PeerPipelined ps pr st m a + -- ^ a pipelined peer + -> Peer ps (FlipAgency pr) NonPipelined st m b + -- ^ a non-pipelined peer with fliped agency + -> m (a, b, TerminalStates ps) + -- ^ peers results and an evidence of their termination +connectPipelined csA a b = + connect (forgetPipelined csA a) b -- | A reference specification for interleaving of requests and responses -- with pipelining, where the environment can choose whether a response is -- available yet. -- -- This also supports bounded choice where the maximum number of outstanding --- in-flight responses is limted. +-- in-flight responses is limited. -- pipelineInterleaving :: Int -- ^ Bound on outstanding responses -> [Bool] -- ^ Pipelining choices diff --git a/typed-protocols/typed-protocols.cabal b/typed-protocols/typed-protocols.cabal index 3c0d573c..a178384e 100644 --- a/typed-protocols/typed-protocols.cabal +++ b/typed-protocols/typed-protocols.cabal @@ -1,6 +1,6 @@ cabal-version: 3.0 name: typed-protocols -version: 0.1.1.0 +version: 0.2.0.0 synopsis: A framework for strongly typed protocols -- description: license: Apache-2.0 @@ -18,10 +18,13 @@ extra-source-files: CHANGELOG.md library exposed-modules: Network.TypedProtocol , Network.TypedProtocol.Core + , Network.TypedProtocol.Peer + , Network.TypedProtocol.Peer.Client + , Network.TypedProtocol.Peer.Server , Network.TypedProtocol.Codec - , Network.TypedProtocol.Pipelined , Network.TypedProtocol.Driver , Network.TypedProtocol.Proofs + other-modules: Network.TypedProtocol.Lemmas other-extensions: GADTs , RankNTypes @@ -32,7 +35,8 @@ library , TypeOperators , BangPatterns build-depends: base, - io-classes >= 1.0 && < 1.6 + io-classes >= 1.0 && < 1.6, + singletons >= 3.0 hs-source-dirs: src default-language: Haskell2010