packages feed

typed-protocols (empty) → 1.0.0.0

raw patch · 47 files changed

+7246/−0 lines, 47 filesdep +QuickCheckdep +basedep +bytestring

Dependencies added: QuickCheck, base, bytestring, cborg, contra-tracer, directory, io-classes, io-sim, network, primitive, serialise, singletons, tasty, tasty-quickcheck, time, typed-protocols, unix

Files

+ CHANGELOG.md view
@@ -0,0 +1,41 @@+# Revision history for typed-protocols++## 0.3.0.0++* `AnyMessageWithAgency` pattern synonym is exported as a constructor of `AnyMessage`.+* Bumped version to agree with `typed-protocols-stateful`.++## 0.2.0.0++* A major redesign of `typed-protocols`.+  * `Protocol` class does not require to provide proof obligations for agency.+    Proofs are now provided by the framework for all protocols. Agency is now+    provided by an associated type family `StateAgency`, and evidence for it,+    in form of a singleton, by `StateToken` type family+    (similar to `Sing` from the `singletons` package).+  * `Peer` takes a different evidence type for agency,+    `Network.TypedProtocol.Peer.{Client,Server}` modules provide pattern synonyms+     which provide agency evidence and thus are easier to use.+  * One `Peer` is provided for both non- and pipelined protocol evolution.+    An extra parameter is added of kind `IsPipelined`. As a result+    `Outstanding` is now a type family rather than a type alias.+  * `ActiveAgency` type class is used to distinguish states in which one side+    has an agency (e.g. the protocol hasn't yet terminated), `nonActiveState` can+    be used in the same way as `Data.Void.absurd` - which is useful when writing+    codecs.++## 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
+ LICENSE view
@@ -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
+ NOTICE view
@@ -0,0 +1,14 @@+Copyright 2019-2025 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.+
+ README.md view
@@ -0,0 +1,39 @@+[![Haskell CI](https://img.shields.io/github/actions/workflow/status/input-output-hk/typed-protocols/haskell.yml?branch=main&label=Build&style=for-the-badge)](https://github.com/input-output-hk/typed-protocols/actions/workflows/haskell.yml)+[![handbook](https://img.shields.io/badge/policy-Cardano%20Engineering%20Handbook-informational?style=for-the-badge)](https://input-output-hk.github.io/cardano-engineering-handbook)+++typed-protocols+===============+++A robust session type framework which supports [protocol pipelining][protocol-pipelining].++Haddocks are published [here][haddocks].+++Public content+--------------++[Duncan Coutts][dcoutts] Haskell eXchange 2019 [talk][haskell-eXchange].++Monadic party workshop by Marcin Szamotulski ([coot]):+* [part 1][monadic-party-part-1]+* [part 2][monadic-party-part-2]+* [part 2][monadic-party-part-3]++Talk at [Haskell Love 2021][haskell-love] by Marcin Szamotulski ([coot]), [slides][haskell-love-slides].++An [Agda][typed-protocols-agda] implementation by Marcin Szamotulski ([coot]).+++[protocol-pipelining]: https://www.wikiwand.com/en/Protocol_pipelining+[haskell-eXchange]: https://www.youtube.com/watch?v=kkynmgwa7gE+[monadic-party-part-1]: https://www.youtube.com/watch?v=j8gza2L61nM+[monadic-party-part-2]: https://www.youtube.com/watch?v=oV6KSl1srL8+[monadic-party-part-3]: https://www.youtube.com/watch?v=nOIQCRPwmPA+[haskell-love-slides]: https://coot.me/posts/typed-protocols-at-haskell-love.html+[haskell-love]: https://www.youtube.com/watch?v=EbK6VAqYh3g+[typed-protocols-agda]: https://coot.me/agda/posts.agda.typed-protocols.html+[coot]: https://github.com/coot+[dcoutts]: https://github.com/dcoutts+[haddocks]: https://input-output-hk.github.io/typed-protocols
+ cborg/Network/TypedProtocol/Codec/CBOR.hs view
@@ -0,0 +1,174 @@+module Network.TypedProtocol.Codec.CBOR+  ( module Network.TypedProtocol.Codec+  , mkCodecCborLazyBS+  , mkCodecCborStrictBS+  , convertCborDecoderBS+  , convertCborDecoderLBS+    -- * Re-exports+  , CBOR.DeserialiseFailure (..)+  ) where++import Control.Monad.Class.MonadST (MonadST (..))+import Control.Monad.ST hiding (stToIO)++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.Codec+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 m. MonadST m++  => (forall (st :: ps) (st' :: ps).+             StateTokenI st+          => ActiveState st+          => Message ps st st' -> CBOR.Encoding)+  -- ^ cbor encoder++  -> (forall (st :: ps) s.+             ActiveState st+          => StateToken st+          -> CBOR.Decoder s (SomeMessage st))+  -- ^ cbor decoder++  -> Codec ps CBOR.DeserialiseFailure m BS.ByteString+mkCodecCborStrictBS cborMsgEncode cborMsgDecode =+    Codec {+      encode = \msg  -> convertCborEncoder cborMsgEncode msg,+      decode = \stok -> convertCborDecoder (cborMsgDecode stok)+    }+  where+    convertCborEncoder :: (a -> CBOR.Encoding) -> a -> BS.ByteString+    convertCborEncoder cborEncode =+        CBOR.toStrictByteString+      . cborEncode++    convertCborDecoder+      :: (forall s. CBOR.Decoder s 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+  -> (forall b. ST s b -> m b)+  -- ^ 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 CBOR.DeserialiseFailure m a+    go (CBOR.Done  trailing _ x)+      | BS.null trailing       = DecodeDone x Nothing+      | otherwise              = DecodeDone x (Just trailing)+    go (CBOR.Fail _ _ failure) = DecodeFail failure+    go (CBOR.Partial k)        = DecodePartial (fmap go . liftST . k)+++-- | 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 m. MonadST m++  => (forall (st :: ps) (st' :: ps).+             StateTokenI st+          => ActiveState st+          => Message ps st st' -> CBOR.Encoding)+  -- ^ cbor encoder++  -> (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 = \msg  -> convertCborEncoder cborMsgEncode msg,+      decode = \stok -> convertCborDecoder (cborMsgDecode stok)+    }+  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++convertCborDecoderLBS+  :: forall s m a. Monad m+  => 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)+  where+    -- Have to mediate between a CBOR decoder that consumes strict bytestrings+    -- and our choice here that consumes lazy bytestrings.+    go :: [BS.ByteString] -> CBOR.IDecode s a+       -> m (DecodeStep LBS.ByteString CBOR.DeserialiseFailure m a)+    go [] (CBOR.Done  trailing _ x)+      | BS.null trailing    = return (DecodeDone x Nothing)+      | otherwise           = return (DecodeDone x (Just trailing'))+                                where trailing' = LBS.fromStrict trailing+    go cs (CBOR.Done  trailing _ x) = return (DecodeDone x (Just trailing'))+                                where trailing' = LBS.fromChunks (trailing : cs)+    go _  (CBOR.Fail _ _ e) = return (DecodeFail e)++    -- 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 $ \case+                                    Nothing -> go [] =<< liftST (k Nothing)+                                    Just bs -> go cs (CBOR.Partial k)+                                      where cs = LBS.toChunks bs++{-# 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+
+ examples/Network/TypedProtocol/Channel.hs view
@@ -0,0 +1,332 @@+{-# LANGUAGE CPP #-}++module Network.TypedProtocol.Channel+  ( Channel (..)+  , hoistChannel+  , isoKleisliChannel+  , fixedInputChannel+  , mvarsAsChannel+  , handlesAsChannel+#if !defined(mingw32_HOST_OS)+  , socketAsChannel+#endif+  , createConnectedChannels+  , createConnectedBufferedChannels+  , createConnectedBufferedChannelsUnbounded+  , createPipelineTestChannels+  , channelEffect+  , delayChannel+  , loggingChannel+  ) where++import Control.Concurrent.Class.MonadSTM+import Control.Monad ((>=>))+import Control.Monad.Class.MonadSay+import Control.Monad.Class.MonadTimer.SI+import Data.ByteString qualified as BS+import Data.ByteString.Lazy qualified as LBS+import Data.ByteString.Lazy.Internal (smallChunkSize)+import Data.Proxy+import Numeric.Natural++#if !defined(mingw32_HOST_OS)+import Network.Socket (Socket)+import Network.Socket.ByteString.Lazy qualified as Socket+#endif++import System.IO qualified as IO (Handle, hFlush, hIsEOF)+++-- | One end of a duplex channel. It is a reliable, ordered channel of some+-- medium. The medium does not imply message boundaries, it can be just bytes.+--+data Channel m a = Channel {++       -- | Write output to the channel.+       --+       -- It may raise exceptions (as appropriate for the monad and kind of+       -- channel).+       --+       send :: a -> m (),++       -- | Read some input from the channel, or @Nothing@ to indicate EOF.+       --+       -- Note that having received EOF it is still possible to send.+       -- The EOF condition is however monotonic.+       --+       -- It may raise exceptions (as appropriate for the monad and kind of+       -- channel).+       --+       recv :: m (Maybe a)+     }+++-- | Given an isomorphism between @a@ and @b@ (in Kleisli category), transform+-- a @'Channel' m a@ into @'Channel' m b@.+--+isoKleisliChannel+  :: forall a b m. Monad m+  => (a -> m b)+  -> (b -> m a)+  -> Channel m a+  -> Channel m b+isoKleisliChannel f finv Channel{send, recv} = Channel {+    send = finv >=> send,+    recv = recv >>= traverse f+  }+++hoistChannel+  :: (forall x . m x -> n x)+  -> Channel m a+  -> Channel n a+hoistChannel nat channel = Channel+  { send = nat . send channel+  , recv = nat (recv channel)+  }++-- | A 'Channel' with a fixed input, and where all output is discarded.+--+-- The input is guaranteed to be supplied via 'read' with the given chunk+-- boundaries.+--+-- This is only useful for testing. In particular the fixed chunk boundaries+-- can be used to test that framing and other codecs work with any possible+-- chunking.+--+fixedInputChannel :: MonadSTM m => [a] -> m (Channel m a)+fixedInputChannel xs0 = do+    v <- atomically $ newTVar xs0+    return Channel {send, recv = recv v}+  where+    recv v = atomically $ do+               xs <- readTVar v+               case xs of+                 []      -> return Nothing+                 (x:xs') -> writeTVar v xs' >> return (Just x)++    send _ = return ()+++-- | Make a 'Channel' from a pair of 'TMVar's, one for reading and one for+-- writing.+--+mvarsAsChannel :: MonadSTM m+               => TMVar m a+               -> TMVar m a+               -> Channel m a+mvarsAsChannel bufferRead bufferWrite =+    Channel{send, recv}+  where+    send x = atomically (putTMVar bufferWrite x)+    recv   = atomically (Just <$> takeTMVar bufferRead)+++-- | Create a pair of channels that are connected via one-place buffers.+--+-- This is primarily useful for testing protocols.+--+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 $ 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)+++-- | Create a pair of channels that are connected via N-place buffers.+--+-- This variant /blocks/ when 'send' would exceed the maximum buffer size.+-- Use this variant when you want the environment rather than the 'Peer' to+-- limit the pipelining.+--+-- This is primarily useful for testing protocols.+--+createConnectedBufferedChannels :: MonadSTM m+                                => Natural -> m (Channel m a, Channel m a)+createConnectedBufferedChannels sz = do+    -- Create two TBQueues to act as the channel buffers (one for each+    -- direction) and use them to make both ends of a bidirectional channel+    bufferA <- atomically $ newTBQueue sz+    bufferB <- atomically $ newTBQueue sz++    return (queuesAsChannel bufferB bufferA,+            queuesAsChannel bufferA bufferB)+  where+    queuesAsChannel bufferRead bufferWrite =+        Channel{send, recv}+      where+        send x = atomically (writeTBQueue bufferWrite x)+        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 '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.+--+createPipelineTestChannels :: MonadSTM m+                           => Natural -> m (Channel m a, Channel m a)+createPipelineTestChannels sz = do+    -- Create two TBQueues to act as the channel buffers (one for each+    -- direction) and use them to make both ends of a bidirectional channel+    bufferA <- atomically $ newTBQueue sz+    bufferB <- atomically $ newTBQueue sz++    return (queuesAsChannel bufferB bufferA,+            queuesAsChannel bufferA bufferB)+  where+    queuesAsChannel bufferRead bufferWrite =+        Channel{send, recv}+      where+        send x = atomically $ do+                   full <- isFullTBQueue bufferWrite+                   if full then error failureMsg+                           else writeTBQueue bufferWrite x+        recv   = atomically (Just <$> readTBQueue bufferRead)++    failureMsg = "createPipelineTestChannels: "+              ++ "maximum pipeline depth exceeded: " ++ show sz+++-- | Make a 'Channel' from a pair of IO 'Handle's, one for reading and one+-- for writing.+--+-- 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.  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.+--+handlesAsChannel :: IO.Handle -- ^ Read handle+                 -> IO.Handle -- ^ Write handle+                 -> Channel IO LBS.ByteString+handlesAsChannel hndRead hndWrite =+    Channel{send, recv}+  where+    send :: LBS.ByteString -> IO ()+    send chunk = do+      LBS.hPut hndWrite chunk+      IO.hFlush hndWrite++    recv :: IO (Maybe LBS.ByteString)+    recv = do+      eof <- IO.hIsEOF hndRead+      if eof+        then return Nothing+        else Just . LBS.fromStrict <$> BS.hGetSome hndRead smallChunkSize+++-- | Transform a channel to add an extra action before /every/ send and after+-- /every/ receive.+--+channelEffect :: forall m a.+                 Monad m+              => (a -> m ())        -- ^ Action before 'send'+              -> (Maybe a -> m ())  -- ^ Action after 'recv'+              -> Channel m a+              -> Channel m a+channelEffect beforeSend afterRecv Channel{send, recv} =+    Channel{+      send = \x -> do+        beforeSend x+        send x++    , recv = do+        mx <- recv+        afterRecv mx+        return mx+    }++-- | Delay a channel on the receiver end.+--+-- This is intended for testing, as a crude approximation of network delays.+-- More accurate models along these lines are of course possible.+--+delayChannel :: MonadDelay m+             => DiffTime+             -> Channel m a+             -> Channel m a+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+                  , Show id+                  , Show a+                  )+               => id+               -> Channel m a+               -> Channel m a+loggingChannel ident Channel{send,recv} =+  Channel {+    send = loggingSend,+    recv = loggingRecv+  }+ where+  loggingSend a = do+    say (show ident ++ ":send:" ++ show a)+    send a++  loggingRecv = do+    msg <- recv+    case msg of+      Nothing -> return ()+      Just a  -> say (show ident ++ ":recv:" ++ show a)+    return msg
+ examples/Network/TypedProtocol/Driver/Simple.hs view
@@ -0,0 +1,246 @@+{-# LANGUAGE TypeFamilies         #-}+-- @UndecidableInstances@ extensions is required for defining @Show@ instance+-- of @'TraceSendRecv'@.+{-# LANGUAGE UndecidableInstances #-}++-- | Drivers for running 'Peer's with a 'Codec' and a 'Channel'.+--+module Network.TypedProtocol.Driver.Simple+  ( -- * Introduction+    -- $intro+    -- * Normal peers+    runPeer+  , TraceSendRecv (..)+  , Role (..)+    -- * Pipelined peers+  , runPipelinedPeer+    -- * Connected peers+  , runConnectedPeers+  , runConnectedPeersPipelined+  , runConnectedPeersAsymmetric+    -- * Driver utilities+    -- | This may be useful if you want to write your own driver.+  , driverSimple+  , runDecoderWithChannel+  ) where++import Network.TypedProtocol.Channel+import Network.TypedProtocol.Codec+import Network.TypedProtocol.Core+import Network.TypedProtocol.Driver+import Network.TypedProtocol.Peer++import Control.Monad.Class.MonadAsync+import Control.Monad.Class.MonadThrow+import Control.Tracer (Tracer (..), contramap, traceWith)+++-- $intro+--+-- A 'Peer' is a particular implementation of an agent that engages in a+-- typed protocol. To actualy 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.+--+-- 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.+--+-- 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.+--+-- 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.+--++-- | Structured 'Tracer' output for 'runPeer' and derivitives.+--+data TraceSendRecv ps where+     TraceSendMsg :: AnyMessage ps -> TraceSendRecv ps+     TraceRecvMsg :: AnyMessage ps -> TraceSendRecv ps++instance Show (AnyMessage ps) => Show (TraceSendRecv ps) where+  show (TraceSendMsg msg) = "Send " ++ show msg+  show (TraceRecvMsg msg) = "Recv " ++ show msg+++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 pr (Maybe bytes) m+driverSimple tracer Codec{encode, decode} channel@Channel{send} =+    Driver { sendMessage, recvMessage, initialDState = Nothing }+  where+    sendMessage :: forall (st :: ps) (st' :: ps).+                   ( StateTokenI st+                   , ActiveState st+                   )+                => ReflRelativeAgency (StateAgency st)+                                       WeHaveAgency+                                      (Relative pr (StateAgency st))+                -> Message ps st st'+                -> m ()+    sendMessage !_refl msg = do+      send (encode msg)+      traceWith tracer (TraceSendMsg (AnyMessage msg))++    recvMessage :: forall (st :: ps).+                   ( StateTokenI st+                   , ActiveState st+                   )+                => ReflRelativeAgency (StateAgency st)+                                       TheyHaveAgency+                                      (Relative pr (StateAgency st))+                -> Maybe bytes+                -> m (SomeMessage st, Maybe bytes)+    recvMessage !_refl trailing = do+      decoder <- decode stateToken+      result  <- runDecoderWithChannel channel trailing decoder+      case result of+        Right x@(SomeMessage msg, _trailing') -> do+          traceWith tracer (TraceRecvMsg (AnyMessage msg))+          return x+        Left failure ->+          throwIO failure+++-- | Run a peer with the given channel via the given codec.+--+-- This runs the peer to completion (if the protocol allows for termination).+--+runPeer+  :: 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 'NonPipelined st m a+  -> m (a, Maybe bytes)+runPeer tracer codec channel peer =+    runPeerWithDriver driver peer+  where+    driver = driverSimple tracer codec channel+++-- | Run a pipelined peer with the given channel via the given codec.+--+-- This runs the peer to completion (if the protocol allows for termination).+--+-- Unlike normal peers, running pipelined peers rely on concurrency, hence the+-- 'MonadSTM' constraint.+--+runPipelinedPeer+  :: forall ps (st :: ps) pr failure bytes m a.+     (MonadAsync m, MonadThrow m, Exception failure)+  => Tracer m (TraceSendRecv ps)+  -> Codec ps failure m bytes+  -> Channel m bytes+  -> PeerPipelined ps pr st m a+  -> m (a, Maybe bytes)+runPipelinedPeer tracer codec channel peer =+    runPipelinedPeerWithDriver driver peer+  where+    driver = driverSimple tracer codec channel+++--+-- Utils+--++-- | Run a codec incremental decoder 'DecodeStep' against a channel. It also+-- takes any extra input data and returns any unused trailing data.+--+runDecoderWithChannel :: Monad m+                      => Channel m bytes+                      -> Maybe bytes+                      -> DecodeStep bytes failure m a+                      -> m (Either failure (a, Maybe bytes))++runDecoderWithChannel Channel{recv} = go+  where+    go _ (DecodeDone x trailing)         = return (Right (x, trailing))+    go _ (DecodeFail failure)            = return (Left failure)+    go Nothing         (DecodePartial k) = recv >>= k        >>= go Nothing+    go (Just trailing) (DecodePartial k) = k (Just trailing) >>= go Nothing+++data Role = Client | Server+  deriving Show++-- | Run two 'Peer's via a pair of connected 'Channel's and a common 'Codec'.+--+-- This is useful for tests and quick experiments.+--+-- The first argument is expected to create two channels that are connected,+-- for example 'createConnectedChannels'.+--+runConnectedPeers :: (MonadAsync m, MonadCatch m,+                      Exception failure)+                  => m (Channel m bytes, Channel m bytes)+                  -> Tracer m (Role, TraceSendRecv ps)+                  -> Codec ps failure m bytes+                  -> 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) ->++    (fst <$> runPeer tracerClient codec clientChannel client)+      `concurrently`+    (fst <$> runPeer tracerServer codec serverChannel server)+  where+    tracerClient = contramap ((,) Client) tracer+    tracerServer = contramap ((,) Server) tracer++runConnectedPeersPipelined :: (MonadAsync m, MonadCatch m,+                               Exception failure)+                           => 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) 'NonPipelined st m b+                           -> m (a, b)+runConnectedPeersPipelined createChannels tracer codec client server =+    createChannels >>= \(clientChannel, serverChannel) ->++    (fst <$> runPipelinedPeer tracerClient codec clientChannel client)+      `concurrently`+    (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
+ examples/Network/TypedProtocol/PingPong/Client.hs view
@@ -0,0 +1,168 @@+module Network.TypedProtocol.PingPong.Client+  ( -- * Normal client+    PingPongClient (..)+  , pingPongClientPeer+    -- * Pipelined client+  , PingPongClientPipelined (..)+  , PingPongClientIdle (..)+  , pingPongClientPeerPipelined+  ) where++import Network.TypedProtocol.Core+import Network.TypedProtocol.Peer.Client+import Network.TypedProtocol.PingPong.Type++-- | A ping-pong client, on top of some effect 'm'.+--+-- At each step the client has a choice: ping or stop.+--+-- This type encodes the pattern of state transitions the client can go through.+-- For the ping\/pong case this is trivial. We start from one main state,+-- issue a ping and move into a state where we expect a single response,+-- bringing us back to the same main state.+--+-- If we had another state in which a different set of options were available+-- then we would need a second type like this. The two would be mutually+-- recursive if we can get in both directions, or perhaps just one way such+-- as a special initialising state or special terminating state.+--+data PingPongClient m a where+  -- | Choose to go for sending a ping message. The ping has no body so+  -- all we have to provide here is a continuation for the single legal+  -- reply message.+  --+  SendMsgPing    :: m (PingPongClient m a) -- continuation for Pong response+                 -> PingPongClient m a++  -- | Choose to terminate the protocol. This is an actual but nullary message,+  -- we terminate with the local result value. So this ends up being much like+  -- 'return' in this case, but in general the termination is a message that+  -- can communicate final information.+  --+  SendMsgDone    :: a -> PingPongClient m a+++-- | Interpret a particular client action sequence into the client side of the+-- 'PingPong' protocol.+--+pingPongClientPeer+  :: Functor m+  => PingPongClient 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 MsgDone (Done result)++pingPongClientPeer (SendMsgPing next) =++    -- Send our message.+    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 $ \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 $ pingPongClientPeer <$> next+++--+-- Pipelined client+--++-- | A ping-pong client designed for running the 'PingPong' protocol in+-- a pipelined way.+--+data PingPongClientPipelined c m a where+  -- | A 'PingPongSender', but starting with zero outstanding pipelined+  -- responses, and for any internal collect type @c@.+  PingPongClientPipelined ::+      PingPongClientIdle      Z c m a+   -> PingPongClientPipelined   c m a+++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+    -> 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, 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+  -- 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.+  --+  CollectPipelined+    :: 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 -> PingPongClientIdle Z c m a++++-- | Interpret a pipelined client as a pipelined 'Peer' on the client side of+-- the 'PingPong' protocol.+--+pingPongClientPeerPipelined+  :: Functor m+  => PingPongClientPipelined c m a+  -> ClientPipelined PingPong StIdle m a+pingPongClientPeerPipelined (PingPongClientPipelined peer) =+    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)
+ examples/Network/TypedProtocol/PingPong/Codec.hs view
@@ -0,0 +1,97 @@+module Network.TypedProtocol.PingPong.Codec where++import Network.TypedProtocol.Codec+import Network.TypedProtocol.Core+import Network.TypedProtocol.PingPong.Type+++codecPingPong+  :: forall m. Monad m+  => Codec PingPong CodecFailure m String+codecPingPong =+    Codec{encode, decode}+  where+    encode :: forall (st :: PingPong) (st' :: PingPong).+              Message PingPong st st'+           -> String+    encode MsgPing = "ping\n"+    encode MsgDone = "done\n"+    encode MsgPong = "pong\n"++    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+          (SingBusy, "pong") ->+            DecodeDone (SomeMessage MsgPong) trailing+          (SingIdle, "ping") ->+            DecodeDone (SomeMessage MsgPing) trailing+          (SingIdle, "done") ->+            DecodeDone (SomeMessage MsgDone) trailing++          (_       , _     ) -> DecodeFail failure+            where failure = CodecFailure ("unexpected server message: " ++ str)+++decodeTerminatedFrame :: forall m a.+                         Monad m+                      => Char+                      -> (String -> Maybe String -> DecodeStep String CodecFailure m a)+                      -> m (DecodeStep String CodecFailure m a)+decodeTerminatedFrame terminator k = go []+  where+    go :: [String] -> m (DecodeStep String CodecFailure m a)+    go chunks =+      return $ DecodePartial $ \mchunk ->+        case mchunk of+          Nothing    -> return $ DecodeFail CodecFailureOutOfInput+          Just chunk ->+            case break (==terminator) chunk of+              (c, _:c') -> return $ k (concat (reverse (c:chunks)))+                                      (if null c' then Nothing else Just c)+              _         -> go (chunk : chunks)++++codecPingPongId+  :: forall m. Monad m+  => Codec PingPong CodecFailure m (AnyMessage PingPong)+codecPingPongId =+    Codec{encode,decode}+  where+    encode :: forall (st :: PingPong) (st' :: PingPong)+           .  ( StateTokenI st+              , ActiveState st+              )+           => Message PingPong st st'+           -> AnyMessage PingPong+    encode msg = AnyMessage msg++    decode :: forall (st :: PingPong).+              ActiveState st+           => StateToken st+           -> m (DecodeStep (AnyMessage PingPong) CodecFailure m (SomeMessage st))+    decode stok =+      pure $ DecodePartial $ \mb ->+        case mb of+          Nothing -> return $ DecodeFail (CodecFailure "expected more data")+          Just (AnyMessage msg) -> return $+            case (stok, msg) of+              (SingBusy, MsgPong) ->+                DecodeDone (SomeMessage msg) Nothing+              (SingIdle, MsgPing) ->+                DecodeDone (SomeMessage msg) Nothing+              (SingIdle, MsgDone) ->+                DecodeDone (SomeMessage msg) Nothing++              (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
+ examples/Network/TypedProtocol/PingPong/Codec/CBOR.hs view
@@ -0,0 +1,43 @@+module Network.TypedProtocol.PingPong.Codec.CBOR where++import Control.Monad.Class.MonadST++import Data.ByteString.Lazy (ByteString)++import Codec.CBOR.Decoding qualified as CBOR (Decoder, decodeWord)+import Codec.CBOR.Encoding qualified as CBOR (Encoding, encodeWord)+import Codec.CBOR.Read qualified as CBOR++import Network.TypedProtocol.Codec+import Network.TypedProtocol.Codec.CBOR+import Network.TypedProtocol.Core+import Network.TypedProtocol.PingPong.Type++codecPingPong+  :: forall m.+     MonadST m+  => Codec PingPong CBOR.DeserialiseFailure m ByteString+codecPingPong = mkCodecCborLazyBS encodeMsg decodeMsg+ where+  encodeMsg :: forall st st'.+               Message PingPong st st'+            -> CBOR.Encoding+  encodeMsg MsgPing = CBOR.encodeWord 0+  encodeMsg MsgPong = CBOR.encodeWord 1+  encodeMsg MsgDone = CBOR.encodeWord 2++  decodeMsg :: forall s (st :: PingPong).+               ActiveState st+            => StateToken st+            -> CBOR.Decoder s (SomeMessage st)+  decodeMsg stok = do+    key <- CBOR.decodeWord+    case (stok, key) of+      (SingIdle, 0)   -> return $ SomeMessage MsgPing+      (SingBusy, 1)   -> return $ SomeMessage MsgPong+      (SingIdle, 2)   -> return $ SomeMessage MsgDone++      -- TODO proper exceptions+      (SingIdle, _)   -> fail "codecPingPong.StIdle: unexpected key"+      (SingBusy, _)   -> fail "codecPingPong.StBusy: unexpected key"+      (a@SingDone, _) -> notActiveState a
+ examples/Network/TypedProtocol/PingPong/Examples.hs view
@@ -0,0 +1,145 @@+module Network.TypedProtocol.PingPong.Examples where++import Network.TypedProtocol.PingPong.Client+import Network.TypedProtocol.PingPong.Server++import Network.TypedProtocol.Peer.Client+++-- | The standard stateless ping-pong server instance.+--+pingPongServerStandard+  :: Applicative m+  => PingPongServer m ()+pingPongServerStandard =+    PingPongServer {+      recvMsgPing = pure pingPongServerStandard,+      recvMsgDone = ()+    }+++-- | An example ping-pong server instance that counts the number of ping+-- messages.+--+pingPongServerCount+  :: Applicative m+  => PingPongServer m Int+pingPongServerCount = go 0+  where+    go !c = PingPongServer {+              recvMsgPing = pure $ go (succ c),+              recvMsgDone = c+            }+++-- | An example ping-pong client that sends pings as fast as possible forever‽+--+-- This may not be a good idea‼+--+pingPongClientFlood :: Applicative m => PingPongClient m a+pingPongClientFlood = SendMsgPing (pure pingPongClientFlood)+++-- | An example ping-pong client that sends a fixed number of ping messages+-- and then stops.+--+pingPongClientCount :: Applicative m => Int -> PingPongClient m ()+pingPongClientCount 0 = SendMsgDone ()+pingPongClientCount n = SendMsgPing (pure (pingPongClientCount (n-1)))+++--+-- Pipelined examples+--++-- | A pipelined ping-pong client that sends eagerly rather than waiting to+-- collect any replies. This is maximum pipelining in some sense, and+-- correspondingly it gives minimum choice to the environment (drivers).+--+-- It returns the interleaving of ping indexes sent, and collected.+--+pingPongClientPipelinedMax+  :: forall m. Monad m+  => Int+  -> PingPongClientPipelined Int m [Either Int Int]+pingPongClientPipelinedMax c =+    PingPongClientPipelined (go [] Zero 0)+  where+    go :: [Either Int Int] -> Nat o -> Int+       -> PingPongClientIdle o Int m [Either Int Int]+    go acc o        n | n < c+                      = SendMsgPingPipelined+                          (return n)+                          (go (Left n : acc) (Succ o) (succ n))+    go acc Zero     _ = SendMsgDonePipelined (reverse acc)+    go acc (Succ o) n = CollectPipelined+                          Nothing+                          (\n' -> go (Right n' : acc) o n)+++-- | A pipelined ping-pong client that sends eagerly but always tries to+-- collect any replies if they are available.  This allows pipelining but+-- keeps it to a minimum, and correspondingly it gives maximum choice to the+-- environment (drivers).+--+-- It returns the interleaving of ping indexes sent, and collected.+--+pingPongClientPipelinedMin+  :: forall m. Monad m+  => Int+  -> PingPongClientPipelined Int m [Either Int Int]+pingPongClientPipelinedMin c =+    PingPongClientPipelined (go [] Zero 0)+  where+    go :: [Either Int Int] -> Nat o -> 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)+                          (\n' -> go (Right n' : acc) o n)+    go acc Zero     n | n < c+                      = ping acc Zero n+    go acc Zero     _ = SendMsgDonePipelined (reverse acc)++    ping :: [Either Int Int] -> Nat o -> Int+         -> PingPongClientIdle o Int m [Either Int Int]+    ping acc o      n = SendMsgPingPipelined+                          (return n)+                          (go (Left n : acc) (Succ o) (succ n))+++-- | A pipelined ping-pong client that sends eagerly up to some maximum limit+-- of outstanding requests. It is also always ready to collect any replies if+-- they are available.  This allows limited pipelining and correspondingly+-- limited choice to the environment (drivers).+--+-- It returns the interleaving of ping indexes sent, and collected.+--+pingPongClientPipelinedLimited+  :: forall m. Monad m+  => Int -> Int+  -> PingPongClientPipelined Int m [Either Int Int]+pingPongClientPipelinedLimited omax c =+    PingPongClientPipelined (go [] Zero 0)+  where+    go :: [Either Int Int] -> Nat o -> 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)+                             else Nothing)+                          (\n' -> go (Right n' : acc) o n)+    go acc Zero     n | n < c+                      = ping acc Zero n+    go acc Zero     _ = SendMsgDonePipelined (reverse acc)++    ping :: [Either Int Int] -> Nat o -> Int+         -> PingPongClientIdle o Int m [Either Int Int]+    ping acc o      n = SendMsgPingPipelined+                          (return n)+                          (go (Left n : acc) (Succ o) (succ n))++    -- this isn't supposed to be efficient, it's just for the example+    int :: Nat n -> Int+    int Zero     = 0+    int (Succ n) = succ (int n)
+ examples/Network/TypedProtocol/PingPong/Server.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE RecordWildCards #-}++module Network.TypedProtocol.PingPong.Server where++import Network.TypedProtocol.Core+import Network.TypedProtocol.Peer.Server+import Network.TypedProtocol.PingPong.Type+++data PingPongServer m a = PingPongServer {+    -- | The client sent us a ping message. We have no choices here, and+    -- the response is nullary, all we have are local effects.+    recvMsgPing :: m (PingPongServer m a)++    -- | The client terminated. Here we have a pure return value, but we+    -- could have done another action in 'm' if we wanted to.+  , recvMsgDone :: a+  }+++-- | Interpret a particular server action sequence into the server side of the+-- 'PingPong' protocol.+--+pingPongServerPeer+  :: Monad m+  => PingPongServer m a+  -> Server PingPong NonPipelined StIdle m a+pingPongServerPeer PingPongServer{..} =++    -- In the 'StIdle' the server is awaiting a request message+    Await $ \req ->++    -- The client got to choose between two messages and we have to handle+    -- either of them+    case req of++      -- The client sent the done transition, so we're in the 'StDone' state+      -- so all we can do is stop using 'done', with a return value.+      MsgDone -> Done 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 MsgPong (pingPongServerPeer next)
+ examples/Network/TypedProtocol/PingPong/Type.hs view
@@ -0,0 +1,69 @@+{-# LANGUAGE TypeFamilies #-}++module Network.TypedProtocol.PingPong.Type where++import Network.TypedProtocol.Core+++-- | The ping\/pong protocol and the states in its protocol state machine.+--+-- This protocol serves as a simple example of the typed protocols framework+-- to help understand the framework and as a template for writing other+-- protocols.+--+-- For a slightly more realistic example, see the request\/response protocol+-- "Network.TypedProtocol.ResResp.Type".+--+-- This declares the protocol itself. It is used both as a type level tag for+-- the protocol and as the kind of the types of the states in the protocol+-- state machine. That is @PingPong@ is a kind, and @StIdle@ is a type of+-- that kind.+--+-- If the protocol needs any type parameters (e.g. for thing that end up in+-- the messages) then those type parameters go here. See the request\/response+-- protocol for an example. It is parametrised over the types of the request+-- and response.+--+data PingPong where+  StIdle :: PingPong+  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.+  --+  -- These involve transitions between different states within the 'PingPong'+  -- states. A ping request goes from idle to busy, and a pong response go from+  -- busy to idle.+  --+  -- This example is so simple that we have all the messages directly as+  -- constructors within this type. In more complex cases it may be better to+  -- factor all (or related) requests and all responses within one case (in+  -- which case the state transitions may depend on the particular message via+  -- the usual GADT tricks).+  --+  data Message PingPong from to where+    MsgPing :: Message PingPong StIdle StBusy+    MsgPong :: Message PingPong StBusy StIdle+    MsgDone :: Message PingPong StIdle StDone++  type StateAgency StIdle = ClientAgency+  type StateAgency StBusy = ServerAgency+  type StateAgency StDone = NobodyAgency++  type StateToken = SPingPong+++deriving instance Show (Message PingPong from to)
+ examples/Network/TypedProtocol/ReqResp/Client.hs view
@@ -0,0 +1,152 @@+module Network.TypedProtocol.ReqResp.Client+  ( -- * Normal client+    ReqRespClient (..)+  , reqRespClientPeer+    -- * Pipelined client+  , ReqRespClientPipelined (..)+  , reqRespClientPeerPipelined+  , ReqRespIdle (..)+  , reqRespClientPeerIdle+    -- * Request once+  , requestOnce+  ) where++import Network.TypedProtocol.Core+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+  SendMsgReq     :: req+                 -> (resp -> m (ReqRespClient req resp m a))+                 -> ReqRespClient req resp m a++  SendMsgDone    :: m a -> ReqRespClient req resp m a+++-- | Interpret a particular client action sequence into the client side of the+-- 'ReqResp' protocol.+--+reqRespClientPeer+  :: Monad m+  => ReqRespClient req resp 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 $+      Yield MsgDone . Done <$> result++reqRespClientPeer (SendMsgReq req next) =++    -- Send our message.+    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 $ \(MsgResp resp) ->++    -- 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 resp+        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+--++-- | A request-response client designed for running the 'ReqResp' protocol in+-- a pipelined way.+--+data ReqRespClientPipelined req resp m a where+  -- | A 'PingPongSender', but starting with zero outstanding pipelined+  -- responses, and for any internal collect type @c@.+  ReqRespClientPipelined ::+      ReqRespIdle            req resp Z c m a+   -> ReqRespClientPipelined req resp     m a+++data ReqRespIdle req resp n c m a where+  -- | Send a `Req` message but alike in `ReqRespClient` do not await for the+  -- resopnse, instead supply a monadic action which will run on a received+  -- `Pong` message.+  SendMsgReqPipelined+    :: req+    -> (resp -> m c)                     -- receive action+    -> ReqRespIdle req resp (S n) c m a  -- continuation+    -> ReqRespIdle req resp    n  c m a++  CollectPipelined+    :: Maybe   (ReqRespIdle req resp (S n) c m a)+    -> (c -> m (ReqRespIdle req resp    n  c m a))+    ->          ReqRespIdle req resp (S n) c m a++  -- | Termination of the req-resp protocol.+  SendMsgDonePipelined+    :: a -> ReqRespIdle req resp Z c m a+++-- | Interpret a pipelined client as a 'Peer' on the client side of+-- the 'ReqResp' protocol.+--+reqRespClientPeerPipelined+  :: Functor m+  => ReqRespClientPipelined req resp           m a+  -> ClientPipelined (ReqResp req resp) StIdle m a+reqRespClientPeerPipelined (ReqRespClientPipelined peer) =+    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)
+ examples/Network/TypedProtocol/ReqResp/Codec.hs view
@@ -0,0 +1,85 @@+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)+++codecReqResp ::+    forall req resp m+  . (Monad m, Show req, Show resp, Read req, Read resp)+  => Codec (ReqResp req resp) CodecFailure m String+codecReqResp =+    Codec{encode, decode}+  where+    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 msg = show msg ++ "\n"++    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+          (SingIdle, ("MsgReq", str'))+             | Just req <- readMaybe str'+            -> DecodeDone (SomeMessage (MsgReq req)) trailing+          (SingIdle, ("MsgDone", ""))+            -> DecodeDone (SomeMessage MsgDone) trailing+          (SingBusy, ("MsgResp", str'))+            | Just resp <- readMaybe str'+            -> DecodeDone (SomeMessage (MsgResp resp)) trailing++          (_       , _     ) -> DecodeFail failure+            where failure = CodecFailure ("unexpected server message: " ++ str)+++codecReqRespId ::+    forall req resp m+  . (Monad m, Show req, Show resp)+  => Codec (ReqResp req resp) CodecFailure m (AnyMessage (ReqResp req resp))+codecReqRespId =+    Codec{encode, decode}+  where+    encode :: forall (st  :: ReqResp req resp)+                     (st' :: ReqResp req resp)+           .  StateTokenI st+           => ActiveState st+           => Message (ReqResp req resp) st st'+           -> AnyMessage (ReqResp req resp)+    encode msg = AnyMessage msg++    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 ->+        case mb of+          Nothing -> return $ DecodeFail (CodecFailure "expected more data")+          Just (AnyMessage msg) -> return $+            case (stok, msg) of+              (SingIdle, MsgReq{})+                -> DecodeDone (SomeMessage msg) Nothing+              (SingIdle, MsgDone)+                -> DecodeDone (SomeMessage msg) Nothing+              (SingBusy, MsgResp{})+                -> DecodeDone (SomeMessage msg) Nothing++              (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
+ examples/Network/TypedProtocol/ReqResp/Codec/CBOR.hs view
@@ -0,0 +1,55 @@+module Network.TypedProtocol.ReqResp.Codec.CBOR where++import Control.Monad.Class.MonadST++import Data.ByteString.Lazy (ByteString)++import Codec.CBOR.Decoding qualified as CBOR (Decoder, decodeListLen,+           decodeWord)+import Codec.CBOR.Encoding qualified as CBOR (Encoding, encodeListLen,+           encodeWord)+import Codec.CBOR.Read qualified as CBOR+import Codec.Serialise.Class (Serialise)+import Codec.Serialise.Class qualified as CBOR++import Network.TypedProtocol.Codec+import Network.TypedProtocol.Codec.CBOR+import Network.TypedProtocol.Core+import Network.TypedProtocol.ReqResp.Type++codecReqResp+  :: forall req resp m.+     ( MonadST m+     , Serialise req+     , Serialise resp+     )+  => Codec (ReqResp req resp) CBOR.DeserialiseFailure m ByteString+codecReqResp = mkCodecCborLazyBS encodeMsg decodeMsg+ where+  encodeMsg :: forall st st'.+               Message (ReqResp req resp) st st'+            -> CBOR.Encoding+  encodeMsg (MsgReq req) =+    CBOR.encodeListLen 2 <> CBOR.encodeWord 0 <> CBOR.encode req+  encodeMsg (MsgResp resp) =+    CBOR.encodeListLen 2 <> CBOR.encodeWord 1 <> CBOR.encode resp+  encodeMsg MsgDone =+    CBOR.encodeListLen 1 <> CBOR.encodeWord 2++  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+      (SingIdle, 0)   -> SomeMessage . MsgReq  <$> CBOR.decode+      (SingBusy, 1)   -> SomeMessage . MsgResp <$> CBOR.decode+      (SingIdle, 2)   -> return $ SomeMessage MsgDone++      -- TODO proper exceptions+      (SingIdle, _)   -> fail "codecReqResp.StIdle: unexpected key"+      (SingBusy, _)   -> fail "codecReqResp.StBusy: unexpected key"+      (a@SingDone, _) -> notActiveState a+
+ examples/Network/TypedProtocol/ReqResp/Examples.hs view
@@ -0,0 +1,87 @@+module Network.TypedProtocol.ReqResp.Examples where++import Network.TypedProtocol.ReqResp.Client+import Network.TypedProtocol.ReqResp.Server++import Network.TypedProtocol.Peer.Client++-- | An example request\/response client which ignores received responses.+--+reqRespClient :: Monad m+              => [req]+              -> ReqRespClient req resp m ()+reqRespClient = go+  where+    go []         = SendMsgDone (pure ())+    go (req:reqs) = SendMsgReq req (\_resp -> return (go reqs))+++-- | A request\/response server instance that computes a 'Data.List.mapAccumL'+-- over the stream of requests.+--+reqRespServerMapAccumL :: Monad m+                       => (acc -> req -> m (acc, resp))+                       -> acc+                       -> ReqRespServer req resp m acc+reqRespServerMapAccumL f !acc =+    ReqRespServer {+      recvMsgReq  = \req -> do (acc', resp) <- f acc req+                               return (resp, reqRespServerMapAccumL f acc'),+      recvMsgDone = pure acc+    }+++-- | An example request\/response client that sends the given list of requests+-- and collects the list of responses.+--+reqRespClientMap :: Monad m+                 => [req]+                 -> ReqRespClient req resp m [resp]+reqRespClientMap = go []+  where+    go resps []         = SendMsgDone (pure $ reverse resps)+    go resps (req:reqs) =+      SendMsgReq req $ \resp ->+      return (go (resp:resps) reqs)++--+-- Pipelined example+--++-- | An example request\/response client that sends the given list of requests+-- and collects the list of responses.+--+-- It is pipelined and tries to collect any replies if they are available.+-- This allows pipelining but keeps it to a minimum, and correspondingly it+-- gives maximum choice to the environment (drivers).+--+-- In theory, with enough and large enough requests and responses, this should+-- be able to saturate any channel of any bandwidth and latency, because it+-- should be able to have both peers send essentially continuously.+--+reqRespClientMapPipelined :: forall req resp m.+                             Monad m+                          => [req]+                          -> ReqRespClientPipelined req resp m [resp]+reqRespClientMapPipelined reqs0 =+    ReqRespClientPipelined (go [] Zero reqs0)+  where+    go :: [resp] -> Nat o -> [req] -> ReqRespIdle req resp o resp m [resp]+    go resps Zero reqs =+      case reqs of+        []        -> SendMsgDonePipelined (reverse resps)+        req:reqs' -> sendReq resps Zero req reqs'++    go resps (Succ o) reqs =+      CollectPipelined+        (case reqs of+           []        -> Nothing+           req:reqs' -> Just (sendReq resps (Succ o) req reqs'))+        (\resp -> return $ go (resp:resps) o reqs)++    sendReq :: [resp] -> Nat o -> req -> [req]+            -> ReqRespIdle req resp o resp m [resp]+    sendReq resps o req reqs' =+      SendMsgReqPipelined req+        (\resp -> return resp)+        (go resps (Succ o) reqs')
+ examples/Network/TypedProtocol/ReqResp/Server.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE DataKinds       #-}+{-# LANGUAGE GADTs           #-}+{-# LANGUAGE RecordWildCards #-}++module Network.TypedProtocol.ReqResp.Server where++import Network.TypedProtocol.Core+import Network.TypedProtocol.Peer.Server+import Network.TypedProtocol.ReqResp.Type+++data ReqRespServer req resp m a = ReqRespServer {+    -- | The client sent us a ping message. We have no choices here, and+    -- the response is nullary, all we have are local effects.+    recvMsgReq  :: req -> m (resp, ReqRespServer req resp m a)++    -- | The client terminated. Here we have a pure return value, but we+    -- could have done another action in 'm' if we wanted to.+  , recvMsgDone :: m a+  }+++-- | Interpret a particular server action sequence into the server side of the+-- 'ReqResp' protocol.+--+reqRespServerPeer+  :: Monad m+  => ReqRespServer req resp m a+  -> Server (ReqResp req resp) NonPipelined StIdle m a+reqRespServerPeer ReqRespServer{..} =++    -- In the 'StIdle' the server is awaiting a request message+    Await $ \msg ->++    -- The client got to choose between two messages and we have to handle+    -- either of them+    case msg of++      -- The client sent the done transition, so we're in the 'StDone' state+      -- so all we can do is stop using 'done', with a return value.+      MsgDone -> 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 (MsgResp resp) (reqRespServerPeer next)
+ examples/Network/TypedProtocol/ReqResp/Type.hs view
@@ -0,0 +1,46 @@+{-# LANGUAGE TypeFamilies #-}++module Network.TypedProtocol.ReqResp.Type where++import Network.TypedProtocol.Core+++data ReqResp req resp where+  StIdle :: ReqResp req resp+  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+    MsgReq  :: req  -> Message (ReqResp req resp) StIdle StBusy+    MsgResp :: resp -> Message (ReqResp req resp) StBusy StIdle+    MsgDone ::         Message (ReqResp req resp) StIdle StDone++  type StateAgency StIdle = ClientAgency+  type StateAgency StBusy = ServerAgency+  type StateAgency StDone = NobodyAgency++  type StateToken = SReqResp+++deriving instance (Show req, Show resp)+               => Show (Message (ReqResp req resp) from to)++deriving instance (Eq req, Eq resp)+               => Eq (Message (ReqResp req resp) from to)
+ examples/Network/TypedProtocol/ReqResp2/Client.hs view
@@ -0,0 +1,49 @@+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)+++
+ examples/Network/TypedProtocol/ReqResp2/Type.hs view
@@ -0,0 +1,56 @@+{-# 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)+
+ examples/Network/TypedProtocol/Stateful/ReqResp/Client.hs view
@@ -0,0 +1,35 @@+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 StateIdle StateDone MsgDone (Done a)++reqRespClientPeer (SendMsgReq req next) =+    Yield StateIdle (StateBusy req)+          (MsgReq req) $+    Await $ \_ (MsgResp resp) ->+      let client = next resp+      in ( Effect $ reqRespClientPeer <$> client+         , StateIdle+         )
+ examples/Network/TypedProtocol/Stateful/ReqResp/Codec.hs view
@@ -0,0 +1,105 @@+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. req 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 (StateBusy req) (MsgResp resp) = "MsgResp " ++ encodeResp req 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++
+ examples/Network/TypedProtocol/Stateful/ReqResp/Examples.hs view
@@ -0,0 +1,26 @@+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+
+ examples/Network/TypedProtocol/Stateful/ReqResp/Server.hs view
@@ -0,0 +1,28 @@+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 (StateBusy req) StateIdle (MsgResp resp) (reqRespServerPeer  k'))+          <$> k req+      , StateBusy req+      )
+ examples/Network/TypedProtocol/Stateful/ReqResp/Type.hs view
@@ -0,0 +1,93 @@+{-# 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+            -> 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
+ examples/Network/TypedProtocol/Trans/Wedge.hs view
@@ -0,0 +1,152 @@+{-# LANGUAGE TypeFamilies         #-}+{-# LANGUAGE UndecidableInstances #-}++module Network.TypedProtocol.Trans.Wedge where++import Network.TypedProtocol.Core++import Network.TypedProtocol.Peer.Client qualified as Client+import Network.TypedProtocol.PingPong.Type qualified 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 ()
+ src/Network/TypedProtocol.hs view
@@ -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.+--+-- <<https://upload.wikimedia.org/wikipedia/commons/1/19/HTTP_pipelining2.svg>>+--+-- 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.++
+ src/Network/TypedProtocol/Codec.hs view
@@ -0,0 +1,546 @@+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE QuantifiedConstraints #-}+-- @UndecidableInstances@ extension is required for defining @Show@ instance of+-- @'AnyMessage'@ and @'AnyMessage'@.+{-# LANGUAGE UndecidableInstances  #-}+{-# LANGUAGE ViewPatterns          #-}++module Network.TypedProtocol.Codec+  ( -- * Defining and using Codecs+    -- ** Codec type+    Codec (..)+  , hoistCodec+  , isoCodec+  , mapFailureCodec+    -- ** Incremental decoding+  , DecodeStep (..)+  , runDecoder+  , runDecoderPure+  , hoistDecodeStep+  , isoDecodeStep+  , mapFailureDecodeStep+    -- ** Related types+    -- *** SomeMessage+  , SomeMessage (..)+    -- *** StateToken+  , StateToken+  , StateTokenI (..)+    -- *** ActiveState+  , IsActiveState (..)+  , ActiveState+  , ActiveAgency+  , ActiveAgency' (..)+  , notActiveState+    -- *** PeerRole+  , PeerRole (..)+    -- * CodecFailure+  , CodecFailure (..)+    -- * Testing codec properties+  , AnyMessage (AnyMessage, AnyMessageAndAgency)+  , prop_codecM+  , prop_codec+  , prop_codec_splitsM+  , prop_codec_splits+  , prop_codec_binary_compatM+  , prop_codec_binary_compat+  , prop_codecs_compatM+  , prop_codecs_compat+  , SomeState (..)+  ) where++import Control.Exception (Exception)+import Data.Kind (Type)+import Data.Monoid (All (..))++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+-- encoding in some text-based syntax, or some choice of binary format.+--+-- The codec is parametrised by:+--+-- * The protocol+-- * the type of decoding failures+-- * the monad in which the decoder runs+-- * the type of the encoded data (typically strings or bytes)+--+-- A codec consists of a message encoder and a decoder.+--+-- The encoder is supplied both with the message to encode and the current+-- protocol state (matching the message). The protocol state can be either+-- a client or server state, but for either peer role it is a protocol state+-- in which the peer has agency, since those are the only states where a+-- peer needs to encode a message to be able to send it.+--+-- For example a simple text encoder for the ping\/pong protocol could be:+--+-- > encode :: SingI st+-- >        => Message PingPong st st'+-- >        -> String+-- > 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/+-- messages that are valid in that state. Messages that are unexpected for the+-- current state should be treated like any other decoding format error.+--+-- While the current protocol state is known, the state that the message will+-- have the peer transition to is not known. For this reason the decoded+-- message is wrapped in the 'SomeMessage' constructor which hides the \"to\"+-- state.+--+-- The decoder uses an incremental decoding interface 'DecodeStep' so that+-- input can be supplied (e.g. from a Channel) bit by bit. This style of+-- decoder allows but does not require a format with message framing where the+-- decoder input matches exactly with the message boundaries.+--+-- > 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+-- >       (SingBusy, "pong") ->+-- >            DecodeDone (SomeMessage MsgPong) trailing+-- >       (SingIdle, "ping") ->+-- >            DecodeDone (SomeMessage MsgPing) trailing+-- >       (SingIdle, "done") ->+-- >            DecodeDone (SomeMessage MsgDone) trailing+-- >       _ -> DecodeFail ("unexpected message: " ++ str)+--+-- 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 (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 (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')+         -- ^ 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 = \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 {+    encode = encode,+    decode = \tok -> mapFailureDecodeStep f <$> decode tok+  }+++-- | An incremental decoder with return a value of type @a@.+--+-- This interface is not designed to be used directly for implementing+-- decoders, only for running them. In real applications it is expected to use+-- libraries for text or binary decoding and to implement appropriate wrappers+-- to match up with this incremental decoder interface.+--+-- This style of interface already closely matches that provided by libraries+-- such as @attoparsec@ for text formats, and @binary@, @cereal@ and @cborg@+-- for binary formats.+--+data DecodeStep bytes failure m a =++    -- | The decoder has consumed the available input and needs more+    -- to continue. Provide @'Just'@ if more input is available and+    -- @'Nothing'@ otherwise, and you will get a new @'DecodeStep'@.+    DecodePartial (Maybe bytes -> m (DecodeStep bytes failure m a))++    -- | The decoder has successfully finished. This provides the decoded+    -- result value plus any unused input.+  | DecodeDone a (Maybe bytes)++    -- | The decoder ran into an error. The decoder either used+    -- @'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+  DecodeDone a mb -> DecodeDone a mb+  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+  DecodeDone a mb    -> DecodeDone a mb+  DecodeFail failure -> DecodeFail (f failure)+  DecodePartial k    -> DecodePartial (fmap (mapFailureDecodeStep f) . k)+++-- | Each 'Codec' can use whatever @failure@ type is appropriate. This simple+-- exception type is provided for use by simple codecs (e.g. \"identity\") when+-- nothing more than a 'String' is needed. It is an instance of 'Exception'.+--+data CodecFailure = CodecFailureOutOfInput+                  | CodecFailure String+  deriving (Eq, Show)++-- safe instance with @UndecidableInstances@ in scope+instance Exception CodecFailure+++--+-- Running decoders+--++-- | Run a codec incremental decoder 'DecodeStep' against a list of input.+--+-- It ignores any unused trailing data. This is useful for demos, quick+-- experiments and tests.+--+-- See also 'Network.TypedProtocol.Driver.runDecoderWithChannel'+--+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)+runDecoder []     (DecodePartial k)        = k Nothing  >>= runDecoder []+runDecoder (b:bs) (DecodePartial k)        = k (Just b) >>= runDecoder bs+++-- | A variant of 'runDecoder' that is suitable for \"pure\" monads that have+-- a run function. This includes 'ST', using 'Control.Monad.ST.runST'.+--+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)+++--+-- 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 where+  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 :: ps) (st' :: ps). Show (Message ps st st'))+      => Show (AnyMessage ps) where+  show (AnyMessage (msg :: Message ps st st')) =+    "AnyMessage " ++ show msg+++-- | A convenient pattern synonym which unwrap 'AnyMessage' giving both the+-- singleton for the state and the message.+--+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'+--+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 m bytes.+     ( Monad m+     , Eq (AnyMessage ps)+     )+  => Codec ps failure m bytes+  -- ^ codec+  -> AnyMessage ps+  -- ^ some message+  -> m Bool+  -- ^ 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++-- | The 'Codec' round-trip property in a pure monad.+--+prop_codec+  :: forall ps failure m bytes.+     (Monad m, Eq (AnyMessage ps))+  => (forall a. m a -> a)+  -> Codec ps failure m bytes+  -> AnyMessage ps+  -> 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 m bytes.+     (Monad m, Eq (AnyMessage ps))+  => (bytes -> [[bytes]])+  -- ^ alternative re-chunkings of serialised form+  -> Codec ps failure m bytes+  -> AnyMessage ps+  -> m Bool+prop_codec_splitsM splits+                   Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do+    and <$> sequence+      [ 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 msg+      , bytes' <- splits bytes ]+++-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.+--+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+  -> AnyMessage ps+  -> Bool+prop_codec_splits splits runM codec msg =+    runM $ prop_codec_splitsM splits codec msg+++-- | Auxiliary definition for 'prop_codec_binary_compatM'.+--+-- 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 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+--+-- We check the following property:+--+-- 1. Using codec A, we encode a message of protocol @psA@ to @bytes@.+--+-- 2. When we decode those @bytes@ using codec B, we get a message of protocol+-- @ps@B.+--+-- 3. When we encode that message again using codec B, we get @bytes@.+--+-- 4. When we decode those @bytes@ using codec A, we get the original message+-- again.+prop_codec_binary_compatM+  :: forall psA psB failure m bytes.+     ( Monad m+     , Eq (AnyMessage psA)+     )+  => Codec psA failure m bytes+  -> Codec psB failure m bytes+  -> (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+    (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 msgA+      -- 2.+      r1 <- decode codecB stokB >>= runDecoder [bytesA]+      case r1 :: Either failure (SomeMessage stB) of+        Left _     -> return False+        Right (SomeMessage msgB) -> do+          -- 3.+          let bytesB = encode codecB msgB+          -- 4.+          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++-- | Like @'prop_codec_splitsM'@ but run in a pure monad @m@, e.g. @Identity@.+prop_codec_binary_compat+  :: forall psA psB failure m bytes.+     ( Monad m+     , Eq (AnyMessage psA)+     )+  => (forall a. m a -> a)+  -> Codec psA failure m bytes+  -> Codec psB failure m bytes+  -> (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+++-- | 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 m bytes.+     ( Monad m+     , Eq (AnyMessage ps)+     , forall a. Monoid a => Monoid (m a)+     )+  => Codec ps failure m bytes+  -- ^ first codec+  -> Codec ps failure m bytes+  -- ^ second codec+  -> AnyMessage ps+  -- ^ some message+  -> m Bool+prop_codecs_compatM codecA codecB+                    (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 (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++-- | Like @'prop_codecs_compatM'@ but run in a pure monad @m@, e.g. @Identity@.+--+prop_codecs_compat+  :: forall ps failure m bytes.+     ( Monad m+     , Eq (AnyMessage ps)+     , forall a. Monoid a => Monoid (m a)+     )+  => (forall a. m a -> a)+  -> Codec ps failure m bytes+  -> Codec ps failure m bytes+  -> AnyMessage ps+  -> Bool+prop_codecs_compat run codecA codecB msg =+    run $ prop_codecs_compatM codecA codecB msg
+ src/Network/TypedProtocol/Core.hs view
@@ -0,0 +1,547 @@+{-# LANGUAGE DerivingVia     #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TypeFamilies    #-}+{-# 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+    -- ** PeerRole+  , PeerRole (..)+  , SingPeerRole (..)+    -- ** Agency and its evidence+    -- $agency+  , Agency (..)+  , SingAgency (..)+  , RelativeAgency (..)+  , Relative+  , ReflRelativeAgency (..)+  , WeHaveAgencyProof+  , TheyHaveAgencyProof+  , NobodyHasAgencyProof+    -- *** FlipAgency+  , FlipAgency+    -- *** ActiveState+  , IsActiveState (..)+  , ActiveState+  , notActiveState+  , ActiveAgency+  , ActiveAgency' (..)+    -- ** Pipelining+    -- *** IsPipelined+  , IsPipelined (..)+    -- *** Outstanding+  , Outstanding+    -- *** N and Nat+  , N (..)+  , Nat (Succ, Zero)+  , natToInt+  , unsafeIntToNat+  ) where++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+-- collection of protocol states and protocol messages which are transitions+-- between those states.+--+-- Start from the idea that a protocol is some language of messages sent+-- between two peers. To specify a protocol is to describe what possible+-- sequences of messages are valid. One simple but still relatively expressive+-- way to do this is via a state machine: starting from some initial state,+-- all possible paths through the state machine gives the set of valid protocol+-- traces. This then dictates what a peer participating in a protocol may+-- produce and what it must accept.+--+-- In this style we have a fixed number of states and in each state there is+-- some number of valid messages that move us on to the next state. This can be+-- illustrated as a graph, which can be a helpful form of documentation.+--+-- We further constrain this idea by saying that the two peers will use the+-- same state machine and change states in lock-step by sending\/receiving+-- messages. In this approach, for each protocol state, the description+-- dictates which peer has the agency to choose to send a message, while+-- correspondingly the other must be prepared to receive the message.+--+-- The views of the two peers are dual. In each state one peer can send any+-- message that is valid for the current protocol state while the other+-- must be prepared to receive any valid message for current protocol state.+--+-- We can also have terminal protocol states in which neither peer has agency.+--+-- So part of the protocol description is to label each protocol state with+-- the peer that has the agency in that state, or none for terminal states.+-- We use the labels \"client\" and \"server\" for the two peers, but they are+-- in fact symmetric.+++-- $defining+--+-- The 'Protocol' type class bundles up all the requirements for a typed+-- protocol, which are in fact all type level constructs. Defining a new+-- protocol and making it an instance of the 'Protocol' class requires the+-- following language extensions:+--+-- > {-# LANGUAGE GADTs, TypeFamilies, DataKinds #-}+--+-- 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+-- with a pong message. The client can also terminate the protocol. So modelled+-- as a state machine this protocol has three states, the one in which the+-- client can send a ping or terminate message, the one in which the server+-- must send a pong, and the terminal state where neither can send anything.+-- We somewhat arbitrarily choose label these protocol states as \"idle\"+-- \"busy\" and \"done\".+--+-- For this ping pong example the protocol tag and the protocol state types+-- would be defined (via promoted data kinds) as:+--+-- > data PingPong where+-- >   StIdle :: PingPong+-- >   StBusy :: PingPong+-- >   StDone :: PingPong+--+-- We use @DataKinds@ promotion here so @StIdle@, @StBusy@ and @StDone@ are+-- /types/ (of /kind/ @PingPong@) representing the three states in this+-- protocol's state machine. @PingPong@ itself is both the kind of these types+-- and is also the tag for protocol. We only ever use these as types, via the+-- @DataKinds@ promotion, never as value level data constructors.+--+-- Having defined our protocol tag and states we can instantiate the 'Protocol'+-- type class and fill out the other details.+--+-- The protocol must define what its messages are. These form the state+-- transitions in the protocol state machine. Each transition specifies a+-- \"from\" and \"to\" state as type parameters. This of course determines in+-- which protocol states each message can appear.+--+-- In the \"ping\/pong\" protocol example, the messages are of course ping and+-- pong, which transition between the two main states. There is also a done+-- message that moves the system into a terminal state.+--+-- > instance Protocol PingPong where+-- >   data Message PingPong from to where+-- >     MsgPing :: Message PingPong StIdle StBusy+-- >     MsgPong :: Message PingPong StBusy StIdle+-- >     MsgDone :: Message PingPong StIdle StDone+--+-- This says that in the idle state a ping message takes us to the busy state,+-- while a pong message takes us back to idle. Also in the idle state a done+-- message takes us to the done state.+--+-- It is not required that protocols have any terminal states or corresponding+-- transitions, as in this example, but it is often useful and it aids testing+-- to have protocols that terminate cleanly as it allows them to return a+-- result.+--+-- 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).+--+-- 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+-- server must respond. Finally in the done state, neither peer can send any+-- further messages. This arrangement is defined as so:+--+-- >    -- still within the instance Protocol PingPong+-- >    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.++-- | 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.+--+data PeerRole = AsClient | AsServer++-- | 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 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.+--+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.+--+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.+--+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'.+--+-- 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.+--+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.+--+-- 'ReflClientAgency' has this type only iff `'StateAgency' st ~ 'ClientAgency'`+-- and `pr ~ 'AsClient'`.+--+-- '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.+--+type NobodyHasAgencyProof :: PeerRole -> ps -> Type+type NobodyHasAgencyProof pr st = ReflRelativeAgency (StateAgency st)+                                                      NobodyHasAgency+                                                     (Relative pr (StateAgency st))++-- $lemmas+--+-- 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.+--+-- 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 ⊥.+--+-- 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.+--+-- * '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 four components:+--+-- * 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.+--+-- 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++  -- | The messages for this protocol. It is expected to be a GADT that is+  -- indexed by the @from@ and @to@ protocol states. That is the protocol state+  -- the message transitions from, and the protocol state it transitions into.+  -- These are the edges of the protocol state transition system.+  --+  data Message ps (st :: ps) (st' :: ps)++  -- | Associate an 'Agency' for each state.+  --+  type StateAgency (st :: ps) :: Agency++  -- | A type family for protocol state token, e.g. term level representation of+  -- type level state (also known as singleton).+  --+  -- This type family is similar to 'Sing' type class in the "singletons"+  -- package, but specific for protocol states.+  --+  type StateToken :: ps -> Type+++-- | Evidence that one side of the protocol has the agency, and thus that the+-- protocol hasn't yet terminated.+--+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++deriving instance Show (ActiveAgency' st agency)++-- | Evidence that the protocol isn't in a terminal state.+--+type ActiveAgency :: ps -> Type+type ActiveAgency st = ActiveAgency' st (StateAgency st)+++-- | A type class which restricts states to ones that have `ClientAgency` or+-- `ServerAgency`, excluding `NobodyAgency`.+--+-- 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'.+--+class IsActiveState st (agency :: Agency) where+  activeAgency :: ActiveAgency' st 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.+--+-- A good analogy for this function is @'Data.Void.absurd' :: 'Void' -> a@.+--+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        FlipAgency :: PeerRole -> PeerRole+type family FlipAgency pr where+  FlipAgency AsClient = AsServer+  FlipAgency AsServer = AsClient+++-- | A type level inductive natural number.+data N = Z | S N++-- | Promoted data type which indicates if 'Peer' is used in+-- pipelined mode or not.+--+data IsPipelined where+    -- | Pipelined peer which is using `c :: Type` for collecting responses+    -- from a pipelined messages. '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.+--+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'.+--+-- 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.+--+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
+ src/Network/TypedProtocol/Driver.hs view
@@ -0,0 +1,342 @@+{-# LANGUAGE TypeFamilies #-}++-- | Actions for running 'Peer's with a 'Driver'+--+module Network.TypedProtocol.Driver+  ( -- * Introduction+    -- $intro+    -- * Driver interface+    Driver (..)+  , SomeMessage (..)+    -- * Normal peers+  , runPeerWithDriver+    -- * Pipelined peers+  , runPipelinedPeerWithDriver+  ) where++import Data.Void (Void)++import Network.TypedProtocol.Core+import Network.TypedProtocol.Peer++import Control.Concurrent.Class.MonadSTM.TQueue+import Control.Monad.Class.MonadAsync+import Control.Monad.Class.MonadFork+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 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.+--+-- 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 (together with an implementation of a 'Driver' based on it).+--+-- 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 (pr :: PeerRole) dstate m =+        Driver {+          -- | 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 ()++        -- | 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++        , -- | 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+-- resolve this we use the 'SomeMessage' wrapper which uses an existential+-- type to hide the \"to"\ state.+--+data SomeMessage (st :: ps) where+     SomeMessage :: ( StateTokenI st+                    , StateTokenI st'+                    , ActiveState st+                    )+                 => Message ps st st' -> SomeMessage st+++--+-- Running normal non-pipelined 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 dstate m a.+     Monad m+  => Driver ps pr dstate m+  -> Peer ps pr NonPipelined st m a+  -> m (a, dstate)+runPeerWithDriver Driver{sendMessage, recvMessage, initialDState} =+    go initialDState+  where+    go :: forall st'.+          dstate+       -> 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 refl msg k) = do+      sendMessage refl msg+      go dstate k++    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+    -- the 'Await' nor 'Done' cases.+    --+    -- We want to be able to use a non-pipelined peer in communication with+    -- a pipelined peer, and in that case the non-pipelined peer will in+    -- general see trailing data after an 'Await' which is the next incoming+    -- message.+    --+    -- Likewise for 'Done', we want to allow for one protocols to be run after+    -- another on the same channel. It would be legal for the opening message+    -- of the next protocol arrives in the same data chunk as the final+    -- message of the previous protocol.+++--+-- Running pipelined peers+--++-- | Run a pipelined peer with the given driver.+--+-- This runs the peer to completion (if the protocol allows for termination).+--+-- Unlike normal peers, running pipelined peers rely on concurrency, hence the+-- 'MonadAsync' constraint.+--+runPipelinedPeerWithDriver+  :: forall ps (st :: ps) pr dstate m a.+     MonadAsync m+  => Driver ps pr dstate m+  -> PeerPipelined ps pr st m a+  -> m (a, dstate)+runPipelinedPeerWithDriver driver@Driver{initialDState} (PeerPipelined peer) = do+    receiveQueue <- atomically newTQueue+    collectQueue <- atomically newTQueue+    a <- runPipelinedPeerReceiverQueue receiveQueue collectQueue driver+           `withAsyncLoop`+         runPipelinedPeerSender        receiveQueue collectQueue driver+                                       peer initialDState+    return a++  where+    withAsyncLoop :: m Void -> m x -> m x+    withAsyncLoop left right = do+      -- race will throw if either of the threads throw+      res <- race left right+      case res of+        Left v  -> case v of {}+        Right a -> return a++data ReceiveHandler dstate ps pr m c where+     ReceiveHandler :: MaybeDState dstate n+                    -> 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+-- we have read from the channel but the decoder has told us that it comes+-- after the message we decoded. So it potentially belongs to the next message+-- to decode.+--+-- We read from the channel on both the 'runPipelinedPeerSender' and the+-- 'runPipelinedPeerReceiver', and we synchronise our use of trailing data+-- between the two. The scheme for the sender and receiver threads using the+-- channel ensures that only one can use it at once:+--+-- * When there are zero outstanding pipelined receiver handlers then the+--   sending side is allowed to access the channel directly (to do synchronous+--   yield\/awaits). Correspondingly the receiver side is idle and not+--   accessing the channel.+-- * When there are non-zero outstanding pipelined receiver handlers then+--   the receiver side can access the channel, but the sending side is not+--   permitted to do operations that access the channel.+--+-- So the only times we need to synchronise the trailing data are the times+-- when the right to access the channel passes from one side to the other.+--+-- The transitions are as follows:+--+-- * There having been Zero outstanding pipelined requests there is now a+--   new pipelined yield. In this case we must pass the trailing data from+--   the sender thread to the receiver thread. We pass it with the+--   'ReceiveHandler'.+--+-- * When the last pipelined request is collected. In this case we must pass+--   the trailing data from the receiver thread to the sender thread. We pass+--   it with the collected result.+--+-- Note that the receiver thread cannot know what the last pipelined request+-- is, that is tracked on the sender side. So the receiver thread always+-- returns the trailing data with every collected result. It is for the sender+-- thread to decide if it needs to use it. For the same reason, the receiver+-- thread ends up retaining the last trailing data (as well as passing it to+-- the sender). So correspondingly when new trailing data is passed to the+-- receiver thread, it simply overrides any trailing data it already had, since+-- we now know that copy to be stale.+--+data MaybeDState dstate (n :: N) where+     HasDState :: dstate -> MaybeDState dstate Z+     NoDState  ::           MaybeDState dstate (S n)+++runPipelinedPeerSender+  :: forall ps (st :: ps) pr dstate c m a.+     ( MonadSTM    m+     , MonadThread m+     )+  => TQueue m (ReceiveHandler dstate ps pr m c)+  -> TQueue m (c, dstate)+  -> 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 "pipelined-peer-sender"+    go Zero (HasDState dstate0) peer+  where+    go :: forall st' n.+          Nat n+       -> MaybeDState dstate n+       -> Peer ps pr ('Pipelined n c) st' m a+       -> m (a, dstate)+    go n    dstate             (Effect k) = k >>= go n dstate+    go Zero (HasDState dstate) (Done _ x) = return (x, dstate)++    go Zero dstate (Yield refl msg k) = do+      sendMessage refl msg+      go Zero dstate k++    go Zero (HasDState dstate) (Await stok k) = do+      (SomeMessage msg, dstate') <- recvMessage stok dstate+      go Zero (HasDState dstate') (k msg)++    go n dstate (YieldPipelined refl msg receiver k) = do+      atomically (writeTQueue receiveQueue (ReceiveHandler dstate receiver))+      sendMessage refl msg+      go (Succ n) NoDState k++    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 (Collect (Just k') k) = do+      mc <- atomically (tryReadTQueue collectQueue)+      case mc of+        Nothing  -> go (Succ n) NoDState  k'+        Just (c, dstate) ->+          case n of+            Zero    -> go Zero      (HasDState dstate) (k c)+            Succ n' -> go (Succ n')  NoDState          (k c)+++runPipelinedPeerReceiverQueue+  :: forall ps pr dstate m c.+     ( MonadSTM    m+     , MonadThread m+     )+  => TQueue m (ReceiveHandler dstate ps pr m c)+  -> TQueue m (c, dstate)+  -> Driver ps pr dstate m+  -> m Void+runPipelinedPeerReceiverQueue receiveQueue collectQueue+                              driver@Driver{initialDState} = do+    threadId <- myThreadId+    labelThread threadId "pipelined-receiver-queue"+    go initialDState+  where+    go :: dstate -> m Void+    go receiverDState = do+      ReceiveHandler senderDState receiver+        <- atomically (readTQueue receiveQueue)+      let dstate = case (senderDState, receiverDState) of+                       (HasDState t, _) -> t+                       (NoDState,    t) -> t+      x@(!_c, !dstate') <- runPipelinedPeerReceiver driver dstate receiver+      atomically (writeTQueue collectQueue x)+      go dstate'+++runPipelinedPeerReceiver+  :: forall ps (st :: ps) (stdone :: ps) pr dstate m c.+     Monad m+  => Driver ps pr dstate m+  -> dstate+  -> Receiver ps pr (st :: ps) (stdone :: ps) m c+  -> m (c, dstate)+runPipelinedPeerReceiver Driver{recvMessage} = go+  where+    go :: forall st' st''.+          dstate+       -> 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 refl k) = do+      (SomeMessage msg, dstate') <- recvMessage refl dstate+      go dstate' (k msg)
+ src/Network/TypedProtocol/Lemmas.hs view
@@ -0,0 +1,151 @@+{-# 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
+ src/Network/TypedProtocol/Peer.hs view
@@ -0,0 +1,273 @@+{-# LANGUAGE DerivingVia #-}++-- | 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.+--+-- __NOTE__:+-- one should not allocate resources within a `Peer` since there's no way to+-- safely clean-up resources in case of an asynchronous exception.  The proper+-- way to allocate resources is to call+-- `Network.TypedProtocol.Driver.runPeerWithDriver` (or `runPeer`,+-- `runPipelinedPeer`) within a `Control.Exception.bracket`.+--+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)
+ src/Network/TypedProtocol/Peer/Client.hs view
@@ -0,0 +1,176 @@+{-# LANGUAGE PatternSynonyms #-}++-- | 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 Network.TypedProtocol.Peer qualified 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 #-}
+ src/Network/TypedProtocol/Peer/Server.hs view
@@ -0,0 +1,179 @@+{-# LANGUAGE PatternSynonyms #-}+{-# 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 Network.TypedProtocol.Peer qualified 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 #-}
+ src/Network/TypedProtocol/Proofs.hs view
@@ -0,0 +1,254 @@+{-# LANGUAGE QuantifiedConstraints #-}+{-# 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 and helpful testing utilities.+--+module Network.TypedProtocol.Proofs+  ( -- * Connect proofs+    connect+  , connectPipelined+  , TerminalStates (..)+    -- * Pipelining proofs+    -- | Additional proofs specific to the pipelining features+  , forgetPipelined+  , promoteToPipelined+    -- ** Pipeline proof helpers+  , Queue (..)+  , enqueue+    -- ** Auxiliary functions+  , pipelineInterleaving+  ) where++import Data.Singletons+import Network.TypedProtocol.Core+import Network.TypedProtocol.Lemmas+import Network.TypedProtocol.Peer+++-- | The 'connect' function takes two peers that agree on a protocol and runs+-- them in lock step, until (and if) they complete.+--+-- The 'connect' function serves a few purposes.+--+-- * The fact we can define this function at at all proves some minimal+-- sanity property of the typed protocol framework.+--+-- * It demonstrates that all protocols defined in the framework can be run+-- with synchronous communication rather than requiring buffered communication.+--+-- * It is useful for testing peer implementations against each other in a+-- minimalistic setting.+--+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+    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 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)+    go (Await _ a)     (Yield _ msg b) = go (a msg) b++    -- By appealing to the proofs about agency for this protocol we can+    -- show that these other cases are impossible+    go (Yield reflA _ _) (Yield reflB _ _) =+      case exclusionLemma_ClientAndServerHaveAgency singPeerRole reflA reflB of+        ReflNobodyHasAgency -> case reflA of {}++    go (Await reflA _)   (Await reflB _)   =+      case exclusionLemma_ClientAndServerHaveAgency singPeerRole reflA reflB of+        ReflNobodyHasAgency -> case reflA of {}++    go (Done  reflA _) (Yield reflB _ _)   =+      case terminationLemma_2 singPeerRole reflB reflA of+        ReflNobodyHasAgency -> case reflB of {}++    go (Done  reflA _) (Await reflB _)     =+      case terminationLemma_2 singPeerRole reflB reflA of+        ReflNobodyHasAgency -> case reflB of {}++    go (Yield reflA _ _) (Done reflB _)    =+      case terminationLemma_1 singPeerRole reflA reflB of+        ReflNobodyHasAgency -> case reflA of {}++    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).+          (StateAgency st  ~ NobodyAgency)+       => StateToken st+       -- ^ state termination evidence for the first peer+       -> StateToken st+       -- ^ state termination evidence for the second peer+       -> TerminalStates ps++--+-- Remove Pipelining+--+++-- | 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++-- | 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)+++-- | 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+  => [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+             -> [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+               -> [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 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)+++-- | Promote a peer to a pipelined one.+--+-- This is a right inverse of `forgetPipelined`, e.g.+--+-- >>> 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 limited.+--+pipelineInterleaving :: Int    -- ^ Bound on outstanding responses+                     -> [Bool] -- ^ Pipelining choices+                     -> [req] -> [resp] -> [Either req resp]+pipelineInterleaving omax cs0 reqs0 resps0 =+    go 0 cs0 (zip [0 :: Int ..] reqs0)+             (zip [0 :: Int ..] resps0)+  where+    go o (c:cs) reqs@((reqNo, req) :reqs')+               resps@((respNo,resp):resps')+      | respNo == reqNo = Left  req   : go (o+1) (c:cs) reqs' resps+      | c && o < omax   = Left  req   : go (o+1)    cs  reqs' resps+      | otherwise       = Right resp  : go (o-1)    cs  reqs  resps'++    go o []     reqs@((reqNo, req) :reqs')+               resps@((respNo,resp):resps')+      | respNo == reqNo = Left  req   : go (o+1) [] reqs' resps+      | otherwise       = Right resp  : go (o-1) [] reqs  resps'++    go _ _ [] resps     = map (Right . snd) resps+    go _ _ (_:_) []     = error "pipelineInterleaving: not enough responses"
+ stateful-cborg/Network/TypedProtocol/Stateful/Codec/CBOR.hs view
@@ -0,0 +1,126 @@+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.Codec.CBOR (DeserialiseFailure,+           convertCborDecoderBS, convertCborDecoderLBS)+import Network.TypedProtocol.Core+import Network.TypedProtocol.Stateful.Codec+++-- | 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+
+ stateful/Network/TypedProtocol/Stateful/Codec.hs view
@@ -0,0 +1,295 @@+{-# LANGUAGE PatternSynonyms       #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# 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 (.., AnyMessageAndAgency)+  , showAnyMessage+  , 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.Codec (CodecFailure (..), DecodeStep (..),+           SomeMessage (..), hoistDecodeStep, isoDecodeStep,+           mapFailureDecodeStep, runDecoder, runDecoderPure)+import Network.TypedProtocol.Codec qualified as TP hiding (AnyMessageAndAgency)+import Network.TypedProtocol.Core+++-- | 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+              -- local state, which contain extra context for the encoding+              -- process.+              --+              -- TODO: input-output-hk/typed-protocols#57+              -> Message ps st st'+              -- message to be encoded+              -> bytes,++       decode :: forall (st :: ps).+                 ActiveState st+              => StateToken st+              -> f st+              -- local state, which can contain extra context from the+              -- previous message.+              --+              -- TODO: input-output-hk/typed-protocols#57+              -> 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+             -- ^ local state+             -> Message ps (st :: ps) (st' :: ps)+             -- ^ protocol messsage+             -> AnyMessage ps f+++-- | `showAnyMessage` is can be used to provide `Show` instance for+-- `AnyMessage` if showing `Message` is independent of the state or one accepts+-- showing only partial information included in message constructors or accepts+-- message constructors to carry `Show` instances for its arguments.  Note that+-- the proper solution is to define a custom `Show (AnyMessage ps f)` instance+-- for a protocol `ps`, which give access to the state functor `f` in scope of+-- `show`.+--+showAnyMessage :: forall ps f.+                  ( forall st st'. Show (Message ps st st')+                  , forall st. Show (f st)+                  )+               => AnyMessage ps f+               -> String+showAnyMessage (AnyMessage st msg) =+    concat [ "AnyMessage "+           , 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+                            -> Message ps st st'+                            -> AnyMessage ps f+pattern AnyMessageAndAgency stateToken f msg <- AnyMessage 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 (AnyMessage ps f)+     )+  => Codec ps failure f m bytes+  -> AnyMessage ps f+  -> m Bool+prop_codecM Codec {encode, decode} a@(AnyMessage 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 $ AnyMessage f msg' == a+      Left _                   -> return False++-- | The 'Codec' round-trip property in a pure monad.+--+prop_codec+  :: forall ps failure f m bytes.+     (Monad m, Eq (AnyMessage ps f))+  => (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 (AnyMessage ps f))+  => (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} a@(AnyMessage 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 $ AnyMessage f msg' == a+             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 (AnyMessage ps f))+  => (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 (AnyMessage ps f)+     , 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+                    a@(AnyMessage 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 $ AnyMessage f msg' == a+                    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 $ AnyMessage f msg' == a+                    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 (AnyMessage ps f)+     , 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
+ stateful/Network/TypedProtocol/Stateful/Driver.hs view
@@ -0,0 +1,112 @@+-- | 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+                        -- local state associated to protocol state `st`;+                        -- local state should not be sent to the remote side.+                        -- However it provide extra context for the encoder.+                        --+                        -- TODO: input-output-hk/typed-protocols#57+                        -> Message ps st st'+                        -- message to send+                        --+                        -- TODO: input-output-hk/typed-protocols#57+                        -> 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+                        -- local state which provides extra context for the+                        -- decoder.+                        --+                        -- TODO: input-output-hk/typed-protocols#57+                        -> dstate+                        -- decoder state, e.g. bytes left from decoding of+                        -- a previous message.+                        --+                        -- TODO: input-output-hk/typed-protocols#57+                        -> m (SomeMessage st, dstate)++        , -- | Initial decoder state.+          --+          initialDState :: dstate+        }+++--+-- Running peers+--++-- | Run a peer with the given driver.+--+-- This runs the peer to completion (if the protocol allows for termination).+--+-- NOTE: this function threads local state (i.e. `f`) through evolution of+-- a protocol (i.e. `Peer`).+--+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 !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'
+ stateful/Network/TypedProtocol/Stateful/Peer.hs view
@@ -0,0 +1,195 @@+-- 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 local state type;+-- * the monad in which the peer operates; and+-- * the type of any final result once the peer terminates.+--+-- For example:+--+-- > reqRespClientExample :: Peer (ReqResp FileAPI) AsClient StIdle State m ()+-- > reqRespServerExample :: Peer (ReqResp FileAPI) AsServer StIdle State m Int+--+-- The actions that a peer can take are:+--+-- * perform a local monadic effect,+-- * terminate with a result (but only in a terminal protocol state),+-- * send a message (but only in a protocol state in which we have agency),+-- * 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.+--+-- __NOTE__:+-- one should not allocate resources within a `Peer` since there's no way to+-- safely clean-up resources in case of an asynchronous exception.  The proper+-- way to allocate resources is to call+-- `Network.TypedProtocol.Stateful.Driver.runPeerWithDriver` within+-- a `Control.Exception.bracket`.+--+-- __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. The constructor+  -- requires evidence that we have agency for this protocol state and thus are+  -- allowed to send messages.  It takes local state associated to the source+  -- and target protocol state of the message that is sent.  This state is only+  -- maintained locally, never shared remotely.  It also 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 (StateBusy (ReadFile /etc/os-release))+  -- >                        StateIdle+  -- >                      $ MsgResp "..."+  --+  Yield+    :: forall ps pr (st :: ps) (st' :: ps) f m a.+       ( StateTokenI st+       , StateTokenI st'+       , ActiveState st+       )+    => WeHaveAgencyProof pr st+    -- ^ agency singleton+    -> f st+    -- ^ associated local state to the source protocol state 'st'+    -> f st'+    -- ^ associated local state to the target protocol state `st'`+    -> 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 $ \f msg ->+  -- > case (f, msg) of+  -- >   (StateBusy (ReadFile path), MsgResp resp) ->+  -- >     ( _continuation+  -- >     , StateIdle+  -- >     )+  --+  --+  Await+    :: forall ps pr (st :: ps) f m a.+       ( StateTokenI st+       , ActiveState st+       )+    => TheyHaveAgencyProof pr st+    -- ^ agency singleton+    -> (forall (st' :: ps).+           f st+        -- associated local state to the source protocol state 'st'+        --+        -- TODO: input-output-hk/typed-protocols#57+        -> Message ps st st'+        -> ( Peer ps pr st' f m a+           , f st'+           )+         -- continuation and associated local state to the target protocol+         -- state `st'`+         --+         -- NOTE: the API is limited to pure transition of local state e.g.+         -- `f st -> Message ps st st' -> f st'`,+         -- see https://github.com/input-output-hk/typed-protocols/discussions/63+         --+         -- TODO: input-output-hk/typed-protocols#57+       )+    -- ^ 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)
+ stateful/Network/TypedProtocol/Stateful/Peer/Client.hs view
@@ -0,0 +1,92 @@+{-# LANGUAGE PatternSynonyms #-}++-- | 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 Network.TypedProtocol.Stateful.Peer qualified 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+              -> f st'+              -> Message ps st st'+              -- ^ protocol message+              -> Client ps st' f m a+              -- ^ continuation+              -> Client ps st  f m a+pattern Yield f f' msg k = TP.Yield ReflClientAgency f 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 #-}
+ stateful/Network/TypedProtocol/Stateful/Peer/Server.hs view
@@ -0,0 +1,91 @@+{-# LANGUAGE PatternSynonyms #-}++-- | 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 Network.TypedProtocol.Stateful.Peer qualified 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+              -> f st'+              -> Message ps st st'+              -- ^ protocol message+              -> Server ps st' f m a+              -- ^ continuation+              -> Server ps st  f m a+pattern Yield f f' msg k = TP.Yield ReflServerAgency f 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 #-}
+ stateful/Network/TypedProtocol/Stateful/Proofs.hs view
@@ -0,0 +1,75 @@+{-# 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.Peer+import Network.TypedProtocol.Proofs (TerminalStates (..))+import Network.TypedProtocol.Proofs qualified as TP+import Network.TypedProtocol.Stateful.Peer qualified as ST++++-- | 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 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)
+ test/Main.hs view
@@ -0,0 +1,17 @@+module Main (main) where++import Test.Tasty++import Network.TypedProtocol.PingPong.Tests qualified as PingPong+import Network.TypedProtocol.ReqResp.Tests qualified as ReqResp++main :: IO ()+main = defaultMain tests++tests :: TestTree+tests =+  testGroup "typed-protocols"+  [ PingPong.tests+  , ReqResp.tests+  ]+
+ test/Network/TypedProtocol/PingPong/Tests.hs view
@@ -0,0 +1,469 @@+{-# LANGUAGE CPP #-}+-- orphaned arbitrary instances+{-# OPTIONS_GHC -Wno-orphans #-}++module Network.TypedProtocol.PingPong.Tests+  ( tests+  , splits2+  , splits3+  , splits2BS+  , splits3BS+  ) where+++import Network.TypedProtocol.Channel+import Network.TypedProtocol.Codec+import Network.TypedProtocol.Driver.Simple+import Network.TypedProtocol.Proofs++import Network.TypedProtocol.PingPong.Client+import Network.TypedProtocol.PingPong.Codec+import Network.TypedProtocol.PingPong.Codec.CBOR qualified as CBOR+import Network.TypedProtocol.PingPong.Examples+import Network.TypedProtocol.PingPong.Server+import Network.TypedProtocol.PingPong.Type++import Control.Monad.Class.MonadAsync+import Control.Monad.Class.MonadSTM+import Control.Monad.Class.MonadThrow+import Control.Monad.IOSim (runSimOrThrow)+import Control.Monad.ST (runST)+import Control.Tracer (nullTracer)++import Data.Functor.Identity (Identity (..))+import Data.List (inits, tails)++import Data.ByteString.Lazy qualified as LBS+#if !defined(mingw32_HOST_OS)+import Network.Socket qualified as Socket+import System.Directory (removeFile)+import System.IO+import System.Posix.Files qualified as Posix+#endif++import Test.QuickCheck+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.QuickCheck (testProperty)+++--+-- The list of all properties+--++tests :: TestTree+tests = testGroup "Network.TypedProtocol.PingPong"+  [ testProperty "direct"              prop_direct+  , testProperty "directPipelined 1"   prop_directPipelined1+  , testProperty "directPipelined 2"   prop_directPipelined2+  , testProperty "connect"             prop_connect+  , testProperty "connect_pipelined 1" prop_connect_pipelined1+  , testProperty "connect_pipelined 2" prop_connect_pipelined2+  , testProperty "connect_pipelined 3" prop_connect_pipelined3+  , testProperty "connect_pipelined 4" prop_connect_pipelined4+  , 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+    , testProperty "codec 3-splits"    prop_codec_splits3_PingPong+    , testGroup "CBOR"+      [ testProperty "codec"           prop_codec_cbor_PingPong+      , testProperty "codec 2-splits"  prop_codec_cbor_splits2_PingPong+      , testProperty "codec 3-splits"  $ withMaxSuccess 30 prop_codec_cbor_splits3_PingPong+      ]+    ]+  ]+++--+-- Properties going directly, not via Peer.+--++-- | The 'PingPongClient m' and 'PingPongServer m' types are complementary.+-- The former can be used to feed the latter directly, in the same thread.+-- That's demonstrated here by constructing 'direct'.+--+direct :: Monad m+       => PingPongClient m a+       -> PingPongServer m b+       -> m (a, b)++direct (SendMsgDone clientResult) PingPongServer{recvMsgDone} =+    pure (clientResult, recvMsgDone)++direct (SendMsgPing kPong) PingPongServer{recvMsgPing} = do+    server' <- recvMsgPing+    client' <- kPong+    direct client' server'+++directPipelined :: Monad m+                => PingPongClientPipelined c m a+                -> PingPongServer          m b+                -> m (a, b)+directPipelined (PingPongClientPipelined client0) server0 =+    go EmptyQ client0 server0+  where+    go :: Monad m+       => Queue n c+       -> PingPongClientIdle n c m a+       -> PingPongServer         m b+       -> m (a, b)+    go EmptyQ (SendMsgDonePipelined clientResult) PingPongServer{recvMsgDone} =+      pure (clientResult, recvMsgDone)++    go q (SendMsgPingPipelined kPong client') PingPongServer{recvMsgPing} = do+      server' <- recvMsgPing+      x       <- kPong+      go (enqueue x q) client' server'++    go (ConsQ x q) (CollectPipelined _ k) server = do+      go q (k x) server+++-- | Run a simple ping\/pong client and server, without going via the 'Peer'+-- representation at all.+--+prop_direct :: NonNegative Int -> Bool+prop_direct (NonNegative n) =+    runIdentity+      (direct (pingPongClientCount n)+               pingPongServerCount)+ ==+    ((), n)+++-- | Run a ping\/pong server and pipelined client, without going via the 'Peer'+-- representation.+--+-- This uses a client that forces maximum pipeling. It shows that irrespective+-- of the envronment's choices, the interleaving we get is all requests+-- followed by all responses+--+prop_directPipelined1 :: NonNegative Int -> Bool+prop_directPipelined1 (NonNegative n) =+    runIdentity+      (directPipelined+        (pingPongClientPipelinedMax n)+         pingPongServerCount)+ ==+    (reqResps, n)+  where+    reqResps = map Left [0..n-1] ++ map Right [0..n-1]+++-- | Run a ping\/pong server and pipelined client, without going via the 'Peer'+-- representation.+--+-- This uses a client that collects eagerly. It shows that when the environment+-- chooses minimum pipelining, then the interleaving we get is the in-order+-- non-pipelined interleaving of each request followed by its response.+--+prop_directPipelined2 :: NonNegative Int -> Bool+prop_directPipelined2 (NonNegative n) =+    runIdentity+      (directPipelined+        (pingPongClientPipelinedMin n)+         pingPongServerCount)+ ==+    (reqResps, n)+  where+    reqResps = concat [ [Left n', Right n'] | n' <- [0..n-1] ]+++--+-- Properties using connect, without pipelining.+--++-- | Run a simple ping\/pong client and server, going via the 'Peer'+-- representation, but without going via a channel.+--+prop_connect :: NonNegative Int -> Bool+prop_connect (NonNegative n) =+  case runIdentity+         (connect+           (pingPongClientPeer (pingPongClientCount n))+           (pingPongServerPeer  pingPongServerCount))++    of ((), n', TerminalStates SingDone SingDone) -> n == n'+++--+-- Properties using connect, with pipelining.+--++-- | Run a pipelined ping\/pong client with a normal server. The client+-- should return the interleaving of messages it sent and received. This+-- will be used to exercise various interleavings in properties below.+--+connect_pipelined :: PingPongClientPipelined Int Identity [Either Int Int]+                  -> [Bool]+                  -> (Int, [Either Int Int])+connect_pipelined client cs =+  case runIdentity+         (connectPipelined cs+            (pingPongClientPeerPipelined client)+            (pingPongServerPeer pingPongServerCount))+    of (reqResps, n, TerminalStates SingDone SingDone) ->+         (n, reqResps)+++-- | Using a client that forces maximum pipeling, show that irrespective of+-- the envronment's choices, the interleaving we get is all requests followed+-- by all responses.+--+prop_connect_pipelined1 :: [Bool] -> NonNegative Int -> Bool+prop_connect_pipelined1 choices (NonNegative n) =+    connect_pipelined (pingPongClientPipelinedMax n) choices+ ==+    (n, reqResps)+  where+    reqResps = map Left [0..n-1] ++ map Right [0..n-1]+++-- | Using a client that collects eagerly, show that when the environment+-- chooses maximum pipelining, then the interleaving we get is all requests+-- followed by all responses.+--+prop_connect_pipelined2 :: NonNegative Int -> Bool+prop_connect_pipelined2 (NonNegative n) =+    connect_pipelined (pingPongClientPipelinedMin n) choices+ ==+    (n, reqResps)+  where+    choices  = repeat True+    reqResps = map Left [0..n-1] ++ map Right [0..n-1]+++-- | Using a client that collects eagerly, show that when the environment+-- chooses minimum pipelining, then the interleaving we get is the in-order+-- non-pipelined interleaving of each request followed by its response.+--+prop_connect_pipelined3 :: NonNegative Int -> Bool+prop_connect_pipelined3 (NonNegative n) =+    connect_pipelined (pingPongClientPipelinedMin n) choices+ ==+    (n, reqResps)+  where+    choices  = repeat False+    reqResps = concat [ [Left n', Right n'] | n' <- [0..n-1] ]+++-- | Using a client that collects eagerly, but otherwise is always willing+-- to send new messages, show that when the environment chooses arbitrary+-- pipelining, then we get complex interleavings given by the reference+-- specification 'pipelineInterleaving'.+--+prop_connect_pipelined4 :: [Bool] -> NonNegative Int -> Bool+prop_connect_pipelined4 choices (NonNegative n) =+    connect_pipelined (pingPongClientPipelinedMin n) choices+ ==+    (n, reqResps)+  where+    reqResps = pipelineInterleaving maxBound choices [0..n-1] [0..n-1]+++-- | Using a client that collects eagerly, and is willing to send new messages+-- up to a fixed limit of outstanding messages, show that when the environment+-- chooses arbitrary pipelining, then we get complex interleavings given by+-- the reference specification 'pipelineInterleaving', for that limit of+-- outstanding messages.+--+prop_connect_pipelined5 :: [Bool] -> Positive Int -> NonNegative Int -> Bool+prop_connect_pipelined5 choices (Positive omax) (NonNegative n) =+    connect_pipelined (pingPongClientPipelinedLimited omax n) choices+ ==+    (n, reqResps)+  where+    reqResps = pipelineInterleaving omax choices [0..n-1] [0..n-1]+++--+-- Properties using channels, codecs and drivers.+--++-- | Run a non-pipelined client and server over a channel using a codec.+--+prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m)+             => NonNegative Int+             -> m Bool+prop_channel (NonNegative n) = do+    ((), n') <- runConnectedPeers createConnectedChannels+                                  nullTracer+                                  codecPingPong client server+    return (n' == n)+  where+    client = pingPongClientPeer (pingPongClientCount n)+    server = pingPongServerPeer  pingPongServerCount+++prop_channel_IO :: NonNegative Int -> Property+prop_channel_IO n =+    ioProperty (prop_channel n)++prop_channel_ST :: NonNegative Int -> Bool+prop_channel_ST n =+    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 (AnyMessage PingPong) where+  arbitrary = elements+    [ AnyMessage MsgPing+    , AnyMessage MsgPong+    , AnyMessage MsgDone+    ]++instance Eq (AnyMessage PingPong) where+  AnyMessage MsgPing == AnyMessage MsgPing = True+  AnyMessage MsgPong == AnyMessage MsgPong = True+  AnyMessage MsgDone == AnyMessage MsgDone = True+  _                  ==                  _ = False++prop_codec_PingPong :: AnyMessage PingPong -> Bool+prop_codec_PingPong =+    prop_codec+      runIdentity+      codecPingPong++prop_codec_splits2_PingPong :: AnyMessage PingPong -> Bool+prop_codec_splits2_PingPong =+    prop_codec_splits+      splits2+      runIdentity+      codecPingPong++prop_codec_splits3_PingPong :: AnyMessage PingPong -> Bool+prop_codec_splits3_PingPong =+    prop_codec_splits+      splits3+      runIdentity+      codecPingPong++--+-- CBOR codec properties+--++prop_codec_cbor_PingPong+  :: AnyMessage PingPong+  -> Bool+prop_codec_cbor_PingPong msg =+  runST $ prop_codecM CBOR.codecPingPong msg++prop_codec_cbor_splits2_PingPong+  :: AnyMessage PingPong+  -> Bool+prop_codec_cbor_splits2_PingPong msg =+  runST $ prop_codec_splitsM+      splits2BS+      CBOR.codecPingPong+      msg++prop_codec_cbor_splits3_PingPong+  :: AnyMessage PingPong+  -> Bool+prop_codec_cbor_splits3_PingPong msg =+  runST $ prop_codec_splitsM+      splits3BS+      CBOR.codecPingPong+      msg++--+-- Utils+--++-- | Generate all 2-splits of a string.+--+splits2 :: String -> [[String]]+splits2 str = zipWith (\a b -> [a,b]) (inits str) (tails str)++-- | Generate all 3-splits of a string.+--+splits3 :: String -> [[String]]+splits3 str =+    [ [a,b,c]+    | (a,str') <- zip (inits str)  (tails str)+    , (b,c)    <- zip (inits str') (tails str') ]++-- | Generate all 2-splits of a 'LBS.ByteString'.+--+splits2BS :: LBS.ByteString -> [[LBS.ByteString]]+splits2BS bs = zipWith (\a b -> [a,b]) (LBS.inits bs) (LBS.tails bs)++-- | Generate all 3-splits of a 'LBS.ByteString'.+--+splits3BS :: LBS.ByteString -> [[LBS.ByteString]]+splits3BS bs =+    [ [a,b,c]+    | (a,bs') <- zip (LBS.inits bs)  (LBS.tails bs)+    , (b,c)   <- zip (LBS.inits bs') (LBS.tails bs') ]
+ test/Network/TypedProtocol/ReqResp/Tests.hs view
@@ -0,0 +1,362 @@+{-# LANGUAGE CPP #-}+-- orphaned arbitrary instances+{-# OPTIONS_GHC -Wno-orphans #-}++module Network.TypedProtocol.ReqResp.Tests (tests) where++import Network.TypedProtocol.Channel+import Network.TypedProtocol.Codec+import Network.TypedProtocol.Driver.Simple+import Network.TypedProtocol.Proofs++import Network.TypedProtocol.ReqResp.Client+import Network.TypedProtocol.ReqResp.Codec+import Network.TypedProtocol.ReqResp.Codec.CBOR qualified 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.Class.MonadTimer.SI+import Control.Monad.IOSim+import Control.Monad.ST (runST)+import Control.Tracer (nullTracer)++import Data.Functor.Identity (Identity (..))+import Data.List (intercalate, mapAccumL)+import Data.Tuple (swap)+#if !defined(mingw32_HOST_OS)+import Network.Socket qualified as Socket+import System.Directory (removeFile)+import System.IO+import System.Posix.Files qualified as Posix+#endif++import Network.TypedProtocol.PingPong.Tests (splits2, splits2BS, splits3,+           splits3BS)++import Test.QuickCheck+import Test.Tasty (TestTree, testGroup)+import Test.Tasty.QuickCheck (testProperty)+import Text.Show.Functions ()+++--+-- The list of all properties+--++tests :: TestTree+tests = testGroup "Network.TypedProtocol.ReqResp"+  [ testProperty "direct"              prop_direct+  , testProperty "directPipelined"     prop_directPipelined+  , testProperty "connect"             prop_connect+  , 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+    , testProperty "codec 3-splits"    (withMaxSuccess 33 prop_codec_splits3_ReqResp)+    , testGroup "CBOR"+      [ testProperty "codec"           prop_codec_cbor_ReqResp+      , testProperty "codec 2-splits"  prop_codec_cbor_splits2_ReqResp+      , testProperty "codec 3-splits"  $ withMaxSuccess 30 prop_codec_cbor_splits3_ReqResp+      ]+    ]+  ]+++--+-- Properties going directly, not via Peer.+--++direct :: Monad m+       => ReqRespClient req resp m a+       -> ReqRespServer req resp m b+       -> m (a, b)++direct (SendMsgDone clientResult) ReqRespServer{recvMsgDone} =+    (,) <$> clientResult <*> recvMsgDone++direct (SendMsgReq req kResp) ReqRespServer{recvMsgReq} = do+    (resp, server') <- recvMsgReq req+    client' <- kResp resp+    direct client' server'+++directPipelined :: Monad m+                => ReqRespClientPipelined req resp m a+                -> ReqRespServer          req resp m b+                -> m (a, b)+directPipelined (ReqRespClientPipelined client0) server0 =+    go EmptyQ client0 server0+  where+    go :: Monad m+       => Queue n c+       -> ReqRespIdle   req resp n c m a+       -> ReqRespServer req resp     m b+       -> m (a, b)+    go EmptyQ (SendMsgDonePipelined clientResult) ReqRespServer{recvMsgDone} =+      (clientResult,) <$> recvMsgDone++    go q (SendMsgReqPipelined req kResp client') ReqRespServer{recvMsgReq} = do+      (resp, server') <- recvMsgReq req+      x               <- kResp resp+      go (enqueue x q) client' server'++    go (ConsQ resp q) (CollectPipelined _ k) server = do+      client' <- k resp+      go q client' server+++prop_direct :: (Int -> Int -> (Int, Int)) -> [Int] -> Bool+prop_direct f xs =+    runIdentity+      (direct+        (reqRespClientMap xs)+        (reqRespServerMapAccumL (\a -> pure . f a) 0))+ ==+    swap (mapAccumL f 0 xs)++prop_directPipelined :: (Int -> Int -> (Int, Int)) -> [Int] -> Bool+prop_directPipelined f xs =+    runIdentity+      (directPipelined+        (reqRespClientMapPipelined xs)+        (reqRespServerMapAccumL (\a -> pure . f a) 0))+ ==+    swap (mapAccumL f 0 xs)+++--+-- Properties using connect+--++prop_connect :: (Int -> Int -> (Int, Int)) -> [Int] -> Bool+prop_connect f xs =+    case runIdentity+           (connect+             (reqRespClientPeer (reqRespClientMap xs))+             (reqRespServerPeer (reqRespServerMapAccumL (\a -> pure . f a) 0)))++      of (c, s, TerminalStates SingDone SingDone) ->+           (s, c) == mapAccumL f 0 xs+++prop_connectPipelined :: [Bool] -> (Int -> Int -> (Int, Int)) -> [Int] -> Bool+prop_connectPipelined cs f xs =+    case runIdentity+           (connectPipelined cs+             (reqRespClientPeerPipelined (reqRespClientMapPipelined xs))+             (reqRespServerPeer+               (reqRespServerMapAccumL (\a -> pure . f a) 0)))++      of (c, s, TerminalStates SingDone SingDone) ->+           (s, c) == mapAccumL f 0 xs+++--+-- Properties using channels, codecs and drivers.+--++prop_channel :: (MonadLabelledSTM m, MonadTraceSTM m, MonadAsync m, MonadCatch m)+             => (Int -> Int -> (Int, Int)) -> [Int]+             -> m Bool+prop_channel f xs = do+    (c, s) <- runConnectedPeers createConnectedChannels+                                nullTracer+                                codecReqResp client server+    return ((s, c) == mapAccumL f 0 xs)+  where+    client = reqRespClientPeer (reqRespClientMap xs)+    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)++prop_channel_ST :: (Int -> Int -> (Int, Int)) -> [Int] -> Bool+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 (AnyMessage (ReqResp req resp)) where+  arbitrary = oneof+    [ AnyMessage . MsgReq <$> arbitrary+    , AnyMessage . MsgResp <$> arbitrary+    , return (AnyMessage MsgDone)+    ]++  shrink (AnyMessage (MsgReq r))  =+    [ AnyMessage (MsgReq r')+    | r' <- shrink r ]++  shrink (AnyMessage (MsgResp r)) =+    [ AnyMessage (MsgResp r')+    | r' <- shrink r ]++  shrink (AnyMessage MsgDone)     = []++instance (Eq req, Eq resp) => Eq (AnyMessage (ReqResp req resp)) where+  (AnyMessage (MsgReq  r1)) == (AnyMessage (MsgReq  r2)) = r1 == r2+  (AnyMessage (MsgResp r1)) == (AnyMessage (MsgResp r2)) = r1 == r2+  (AnyMessage MsgDone)      == (AnyMessage MsgDone)      = True+  _                         == _                         = False++prop_codec_ReqResp :: AnyMessage (ReqResp String String) -> Bool+prop_codec_ReqResp =+    prop_codec+      runIdentity+      codecReqResp++prop_codec_splits2_ReqResp :: AnyMessage (ReqResp String String)+                           -> Bool+prop_codec_splits2_ReqResp =+    prop_codec_splits+      splits2+      runIdentity+      codecReqResp++prop_codec_splits3_ReqResp :: AnyMessage (ReqResp String String)+                           -> Bool+prop_codec_splits3_ReqResp =+    prop_codec_splits+      splits3+      runIdentity+      codecReqResp++prop_codec_cbor_ReqResp+  :: AnyMessage (ReqResp String String)+  -> Bool+prop_codec_cbor_ReqResp msg =+  runST $ prop_codecM CBOR.codecReqResp msg++prop_codec_cbor_splits2_ReqResp+  :: AnyMessage (ReqResp String String)+  -> Bool+prop_codec_cbor_splits2_ReqResp msg =+  runST $ prop_codec_splitsM+      splits2BS+      CBOR.codecReqResp+      msg++prop_codec_cbor_splits3_ReqResp+  :: AnyMessage (ReqResp String String)+  -> Bool+prop_codec_cbor_splits3_ReqResp msg =+  runST $ prop_codec_splitsM+      splits3BS+      CBOR.codecReqResp+      msg
+ typed-protocols.cabal view
@@ -0,0 +1,204 @@+cabal-version:       3.4+name:                typed-protocols+version:             1.0.0.0+synopsis:            A framework for strongly typed protocols+description:         A robust session type framework which supports protocol pipelining.+license:             Apache-2.0+license-files:+  LICENSE+  NOTICE+copyright:           2019-2025 Input Output Global Inc (IOG)+author:              Alexander Vieth, Duncan Coutts, Marcin Szamotulski+maintainer:          alex@well-typed.com, duncan@well-typed.com, marcin.szamotulski@iohk.io+category:            Control+build-type:          Simple+tested-with:         GHC == {9.6, 9.8, 9.10, 9.12}+extra-doc-files:     CHANGELOG.md+                     README.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.Driver+                   , Network.TypedProtocol.Proofs+  other-modules:     Network.TypedProtocol.Lemmas+  build-depends:     base >=4.12 && <4.22,+                     io-classes:io-classes ^>= 1.8,+                     singletons ^>= 3.0++  hs-source-dirs:    src+  default-language:  GHC2021+  default-extensions: DataKinds+                      GADTs+                      LambdaCase+  ghc-options:       -Wall+                     -Wno-unticked-promoted-constructors+                     -Wcompat+                     -Wincomplete-uni-patterns+                     -Wincomplete-record-updates+                     -Wpartial-fields+                     -Widentities+                     -Wredundant-constraints++library cborg+  visibility:        public+  exposed-modules:   Network.TypedProtocol.Codec.CBOR++  build-depends:     base,+                     bytestring      >=0.10  && <0.13,+                     cborg           >=0.2.1 && <0.3,+                     singletons,       +                     primitive,++                     io-classes:io-classes,+                     typed-protocols:typed-protocols++  hs-source-dirs:    cborg+  default-language:  GHC2021+  default-extensions: LambdaCase+  ghc-options:       -Wall+                     -Wno-unticked-promoted-constructors+                     -Wcompat+                     -Wincomplete-uni-patterns+                     -Wincomplete-record-updates+                     -Wpartial-fields+                     -Widentities+                     -Wredundant-constraints++library stateful+  visibility:         public+  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+  build-depends:      base,+                      singletons,+                      io-classes:io-classes,+                      typed-protocols:typed-protocols++  hs-source-dirs:     stateful+  default-language:   GHC2021+  default-extensions: DataKinds+                      GADTs+                      ImportQualifiedPost+  ghc-options:        -Wall+                      -Wno-unticked-promoted-constructors+                      -Wcompat+                      -Wincomplete-uni-patterns+                      -Wincomplete-record-updates+                      -Wpartial-fields+                      -Widentities+                      -Wredundant-constraints++library stateful-cborg+  visibility:        public+  exposed-modules:   Network.TypedProtocol.Stateful.Codec.CBOR++  build-depends:     base,+                     bytestring,+                     cborg,+                     singletons,       ++                     io-classes:io-classes,+                     typed-protocols:{typed-protocols,cborg,stateful}++  hs-source-dirs:    stateful-cborg+  default-language:  GHC2021+  default-extensions: ImportQualifiedPost+  ghc-options:       -Wall+                     -Wno-unticked-promoted-constructors+                     -Wcompat+                     -Wincomplete-uni-patterns+                     -Wincomplete-record-updates+                     -Wpartial-fields+                     -Widentities+                     -Wredundant-constraints++library examples+  visibility:        public+  exposed-modules:   Network.TypedProtocol.Channel+                   , Network.TypedProtocol.Driver.Simple++                   , Network.TypedProtocol.PingPong.Type+                   , Network.TypedProtocol.PingPong.Client+                   , Network.TypedProtocol.PingPong.Server+                   , Network.TypedProtocol.PingPong.Codec+                   , Network.TypedProtocol.PingPong.Codec.CBOR+                   , Network.TypedProtocol.PingPong.Examples++                   , Network.TypedProtocol.ReqResp.Type+                   , Network.TypedProtocol.ReqResp.Client+                   , Network.TypedProtocol.ReqResp.Server+                   , Network.TypedProtocol.ReqResp.Codec+                   , 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+  build-depends:     base,+                     bytestring,+                     cborg,+                     serialise,+                     singletons,+                     contra-tracer,+                     io-classes:{io-classes, si-timers},+                     network,+                     time,+                     typed-protocols:{typed-protocols,cborg,stateful}++  hs-source-dirs:    examples+  default-language:  GHC2021+  default-extensions: DataKinds+                      GADTs+                      LambdaCase+  ghc-options:       -Wall+                     -Wno-unticked-promoted-constructors+                     -Wcompat+                     -Wincomplete-uni-patterns+                     -Wincomplete-record-updates+                     -Wpartial-fields+                     -Widentities+                     -Wredundant-constraints++test-suite test+  type:              exitcode-stdio-1.0+  main-is:           Main.hs+  hs-source-dirs:    test+  default-language:  GHC2021+  default-extensions: GADTs+                      LambdaCase+  other-modules:     Network.TypedProtocol.PingPong.Tests+                   , Network.TypedProtocol.ReqResp.Tests+  build-depends:     base+                   , bytestring+                   , contra-tracer+                   , typed-protocols:{typed-protocols,cborg,examples}+                   , io-classes:{io-classes,si-timers}+                   , io-sim+                   , QuickCheck+                   , tasty+                   , tasty-quickcheck++  if !os(windows)+      build-depends: directory+                   , network+                   , unix++  ghc-options:       -rtsopts+                     -Wall+                     -Wno-unticked-promoted-constructors+                     -Wno-orphans