Skip to content

Generalize splits #76

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Generalize splits #76

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e0b22a2
Generalize splitsM property tests
crocodile-dentist Sep 26, 2025
32e1671
update changelog
crocodile-dentist Sep 30, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
11 changes: 10 additions & 1 deletion typed-protocols/CHANGELOG.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,14 @@
# Revision history for typed-protocols

## next version

### Breaking changes

### Non-breaking changes

* generalized prop_codecF_splitsM to run the decoder function provided by a client
library (instead of `runDecoder` here) to test it as well.

## 1.1.0.0 -- 05.08.2025

### Breaking changes
Expand Down Expand Up @@ -55,4 +64,4 @@
* Support `ghc-9.6.1`.
* Use `io-classes-1.1.0.0`.

[singletons-3.0.1]: https://hackage.haskell.org/package/singletons
[singletons-3.0.1]: https://hackage.haskell.org/package/singletons
129 changes: 86 additions & 43 deletions typed-protocols/properties/Network/TypedProtocol/Codec/Properties.hs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,10 @@ module Network.TypedProtocol.Codec.Properties
, SomeState (..)
) where

import Control.Monad.Class.MonadST
import Data.Maybe
import Data.STRef

import Network.TypedProtocol.Codec
import Network.TypedProtocol.Core

Expand Down Expand Up @@ -161,28 +165,40 @@ prop_anncodec = prop_codecF runAnnotator
-- | A more general version of 'prop_codec_splitsM' for 'CodecF'.
--
prop_codecF_splitsM
:: forall ps failure m f bytes.
( Monad m
, Eq (AnyMessage ps)
:: forall ps failure m annotator f bytes channel.
( Eq (AnyMessage ps)
, Show (AnyMessage ps)
, Show failure
, Monoid bytes
, MonadST m
)
=> (forall (st :: ps). f st -> bytes -> SomeMessage st)
=> (forall (st :: ps). annotator st -> f (SomeMessage st))
-> (m (Maybe bytes) -> channel)
-> (forall (st :: ps).
channel
-> Maybe bytes
-> DecodeStep bytes failure m (f (SomeMessage st))
-> m (Either failure (SomeMessage st)))
Comment on lines +174 to +180
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

One problem is that we don't have a function which fits into this type in typed-protocols (running an incremental decoder against a channel), so it makes it a little bit awkward to have this type signature here.

There's no notion of channel in typed-protocols, that's why you had to have a polymorphic channel. I never fully agreed with it, but the point was that this part pulls some dependencies that are custom (e.g. contra-tracing, cborg).
With how things are right now, this fits more into some testing library in ouroboros-newtork. If we move various drivers and channels to some typed-protocols sublibrary, then this will fit here as well.

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I had similar thoughts about this and I think copying this test to o-n like you say makes more sense. We can leave this here as-is because the examples depend on it and it gives other users a starting point to making their own tests based on those.

Copy link
Collaborator

@coot coot Oct 4, 2025 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The typed-protocols:examples sublibrary does not depend on typed-protocols:codec-properties.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The test depends on it, though, that's why there are a bunch of compilation errors.

Is it possible to implement the old API with the new one?

-> (bytes -> [[bytes]])
-- ^ alternative re-chunkings of serialised form
-> CodecF ps failure m f bytes
-> CodecF ps failure m annotator bytes
-> AnyMessage ps
-> m Property
prop_codecF_splitsM runF splits
prop_codecF_splitsM conv mkChannel runDecoder' splits
Codec {encode, decode} (AnyMessage (msg :: Message ps st st')) = do
property . foldMap Every <$> sequence
[ do r <- decode stateToken >>= runDecoder bytes'
case r :: Either failure (f st) of
Right f -> case runF f (mconcat bytes') of
SomeMessage msg' ->
return $! AnyMessage msg' === AnyMessage msg
Left err -> return $ counterexample (show err) False
[ do
stateRef <- stToIO . newSTRef $ tail bytes'
let channelAction = stToIO $ do
chunksRemaining <- readSTRef stateRef
modifySTRef' stateRef (drop 1)
return $! listToMaybe chunksRemaining
channel = mkChannel channelAction
decoder <- decode @st stateToken
r <- runDecoder' channel (listToMaybe bytes') (conv <$> decoder)
case r of
Right (SomeMessage msg') ->
return $! AnyMessage msg' === AnyMessage msg
Left err -> return $ counterexample (show err) False

| let bytes = encode msg
, bytes' <- splits bytes ]
Expand All @@ -200,31 +216,42 @@ prop_codecF_splitsM runF splits
-- to be checked.
--
prop_codec_splitsM
:: forall ps failure m bytes.
( Monad m
, Eq (AnyMessage ps)
:: forall ps failure m f bytes channel.
( Eq (AnyMessage ps)
, Show (AnyMessage ps)
, Show failure
, Monoid bytes
, Applicative f
, MonadST m
)
=> (bytes -> [[bytes]])
=> (m (Maybe bytes) -> channel)
-> (forall (st :: ps).
channel
-> Maybe bytes
-> DecodeStep bytes failure m (f (SomeMessage st))
-> m (Either failure (SomeMessage st)))
-> (bytes -> [[bytes]])
-- ^ alternative re-chunkings of serialised form
-> Codec ps failure m bytes
-> AnyMessage ps
-> m Property
prop_codec_splitsM = prop_codecF_splitsM const
prop_codec_splitsM = prop_codecF_splitsM pure

-- | A variant of 'prop_codec_splitsM' for 'AnnotatedCodec'.
--
prop_anncodec_splitsM
:: forall ps failure m bytes.
( Monad m
, Eq (AnyMessage ps)
:: forall ps failure m bytes channel.
( Eq (AnyMessage ps)
, Show (AnyMessage ps)
, Show failure
, Monoid bytes
, MonadST m
)
=> (bytes -> [[bytes]])
=> (m (Maybe bytes) -> channel)
-> (forall (st :: ps).
channel
-> Maybe bytes
-> DecodeStep bytes failure m (bytes -> SomeMessage st)
-> m (Either failure (SomeMessage st)))
-> (bytes -> [[bytes]])
-- ^ alternative re-chunkings of serialised form
-> AnnotatedCodec ps failure m bytes
-> AnyMessage ps
Expand All @@ -235,51 +262,67 @@ prop_anncodec_splitsM = prop_codecF_splitsM runAnnotator
-- | A more general version of 'prop_codec_splits' for 'CodecF'.
--
prop_codecF_splits
:: forall ps failure m f bytes.
( Monad m
, Eq (AnyMessage ps)
:: forall ps failure m annotator f bytes channel.
( Eq (AnyMessage ps)
, Show (AnyMessage ps)
, Show failure
, Monoid bytes
, MonadST m
)
=> (forall (st :: ps). f st -> bytes -> SomeMessage st)
=> (forall (st :: ps). annotator st -> f (SomeMessage st))
-> (m (Maybe bytes) -> channel)
-> (forall (st :: ps).
channel
-> Maybe bytes
-> DecodeStep bytes failure m (f (SomeMessage st))
-> m (Either failure (SomeMessage st)))
-> (bytes -> [[bytes]])
-- ^ alternative re-chunkings of serialised form
-> (forall a. m a -> a)
-> CodecF ps failure m f bytes
-> CodecF ps failure m annotator bytes
-> AnyMessage ps
-> Property
prop_codecF_splits runF splits runM codec msg =
runM $ prop_codecF_splitsM runF splits codec msg
prop_codecF_splits runF mkChannel runDecoder' splits runM codec msg =
runM $ prop_codecF_splitsM runF mkChannel runDecoder' splits codec msg

-- | 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)
:: forall ps failure m f bytes channel.
( Eq (AnyMessage ps)
, Show (AnyMessage ps)
, Show failure
, Monoid bytes
, Applicative f
, MonadST m
)
=> (bytes -> [[bytes]])
=> (m (Maybe bytes) -> channel)
-> (forall (st :: ps).
channel
-> Maybe bytes
-> DecodeStep bytes failure m (f (SomeMessage st))
-> m (Either failure (SomeMessage st)))
-> (bytes -> [[bytes]])
-- ^ alternative re-chunkings of serialised form
-> (forall a. m a -> a)
-> Codec ps failure m bytes
-> AnyMessage ps
-> Property
prop_codec_splits = prop_codecF_splits const
prop_codec_splits = prop_codecF_splits pure

-- | Like 'prop_codec_splits' but for 'AnnotatorCodec'.
prop_anncodec_splits
:: forall ps failure m bytes.
( Monad m
, Eq (AnyMessage ps)
:: forall ps failure m bytes channel.
( Eq (AnyMessage ps)
, Show (AnyMessage ps)
, Show failure
, Monoid bytes
, MonadST m
)
=> (bytes -> [[bytes]])
=> (m (Maybe bytes) -> channel)
-> (forall (st :: ps).
channel
-> Maybe bytes
-> DecodeStep bytes failure m (bytes -> SomeMessage st)
-> m (Either failure (SomeMessage st)))
-> (bytes -> [[bytes]])
-- ^ alternative re-chunkings of serialised form
-> (forall a. m a -> a)
-> AnnotatedCodec ps failure m bytes
Expand Down
1 change: 1 addition & 0 deletions typed-protocols/typed-protocols.cabal
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,7 @@ library codec-properties
exposed-modules: Network.TypedProtocol.Codec.Properties
Network.TypedProtocol.Stateful.Codec.Properties
build-depends: base >=4.12 && <4.22,
io-classes,
typed-protocols:{stateful, typed-protocols},
QuickCheck >= 2.16
hs-source-dirs: properties
Expand Down
Loading