New API for typed-protocols #52

coot · 2024-08-20T14:00:38Z

Takes lessons learned in #3, but preserving original (parallel) pipelining design.

The original pipelining is limited to transitions which can be fulfilled by remote transitions, this could be lifted by the more general scheme of tracking pipelined transition at type level done in #3 in the future. But what's important we run the receiver for pipelined transition in parallel, which preserves performance. Below is the comparison of plain and modified cardano-node-9.1.0 syncing mainet:

coot · 2024-08-22T19:10:46Z

I removed typed-protocols-doc from GHA for now, since it doesn't build against typed-protocols-0.2.0.0.

bolt12 · 2024-08-26T14:51:16Z

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

 runPeer
-  :: forall ps (st :: ps) pr failure bytes m a .
+  :: forall ps (st :: ps) pr failure bytes m a.
     (MonadThrow m, Exception failure)
  => Tracer m (TraceSendRecv ps)
  -> Codec ps failure m bytes
  -> Channel m bytes
-  -> Peer ps pr st m a
-  -> m a
+  -> Peer ps pr 'NonPipelined Z st m a
+  -> m (a, Maybe bytes)
 runPeer tracer codec channel peer =
-    fst <$> runPeerWithDriver driver peer (startDState driver)
+    runPeerWithDriver driver peer Nothing


want to do: IntersectMBO/ouroboros-network#594 here?

This is in typed-protocols-examples, it doesn't matter than match, does it?

In typed-protocols we anyway need io-classes dependency for Monad{STM,Async} to implement runPipelinedPeerWithDriver.

Looking more closely, this will require to annotate Driver with a failure type, which runPeer will return, so it will be quite substantial change.

I'd leave it for later, when we also include implementation of Driver.Simple and Driver.WithLimits in typed-protocols. This way we wouldn't pull a dependency on a logging framework - error handling will be up to the user.

bolt12

Very clean! I looked through most of it except tests which I only skimmed, the API looks much more polished! :) I just made a some comments, which don't impact the design at all.

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

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

bolt12 · 2024-09-12T15:06:08Z

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

+-- | A proof that if one side has terminated, then the other side terminated as
+-- well.
+--


Same here:

forall (pr :: PeerRole) (a :: Agency) (ra :: RelativeAgency). ra == Relative pr a -> NobodyHasAgency == Relative (FlipAgency pr) a -> Relative pr a == NobodyHasAgency && Relative (FlipAgency pr) a == NobodyHasAgency

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

bolt12 · 2024-09-16T09:28:17Z

typed-protocols-stateful/src/Data/Type/Queue.hs

+                   -> ![SomeF f] -- ^ head
+                   -> ![SomeF f] -- ^ tail
+                   -> SingQueueF f q


Why do you need SomeF ? can't you "monomorphise" it to f st st' since it is what is going to be used for? This would avoid unsafeCoerce usage

This whole module is not needed. It's an artifact of the previous approach.

Why dont we remove it then?

That's what I did 😄

typed-protocols-stateful/src/Data/Type/Queue.hs

The new API provides proofs for all protocols, and thus proof obligations are not part of `Protocol` type class but instead an internal detail of the library.

The client / server 'Peer's pattern synonyms make it easier to write a 'Peer'. They automatically provide the 'RelativeAgencyEq' singleton. See "Network.TypedProtocol.PingPong.Client".

The 'IsActiveAgency' type class allows to limit cases in codecs. We don't need to write decoders for inactive states, ``notActiveState` allows to reduce them. Note that the advantage of the new approach to typed-protocols is that we have access to protocol state singleton in the decoder, without distinguishing which side has the agency. This simplifies writing codecs.

There's no need to to pass initial `dstate` it is already passed inside `Driver` record.

* WeHaveAgencyProof * TheyHaveAgencyProof * NobodyHasAgencyProof

Illustrative example how to define a 'Channel' for a socket. The implementation is only given for posix platforms. It is using a non-blocking `recv` foreign call to provide `tryRecv`.

An example which demonstrates that one can pipeline two kinds of requests, and collect all the responses.

We don't provide pipelined stateful peer, as safe API requires tracking of pipelined transitions rather than just the depth of pipelining at the type level of a `Peer`. See the `coot/typed-protocols-rewrite` branch how this can be done.

coot · 2024-09-16T13:24:10Z

^ I rebased the branch on top of recent main branch (which requires some rather simple conflict resultion).

This is because stylish-parser cannot parse the export list which starts with ```hs module Network.TypedProtocol.Core ( -- * Introduction -- $intro -- * Defining protocols -- $defining Protocol (..) ``` But this is required by haddock, to include the next section.

New API for typed-protocols

# Description Use `typed-protocols-0.3.0.0`. Depends on: * [x] input-output-hk/typed-protocols#52 * [x] input-output-hk/typed-protocols#61 * [x] IntersectMBO/ouroboros-network#4935 - **Updated to use typed-protocols-0.3.0.0** - **Added KeepAlive tracer**

This was referenced Aug 21, 2024

Typed Protocols: new API IntersectMBO/ouroboros-network#4935

Merged

New Typed-Protocols API IntersectMBO/ouroboros-network#4936

Open

coot force-pushed the coot/typed-protocols-new-api branch 3 times, most recently from 30e4c45 to 5741f30 Compare August 22, 2024 16:06

coot self-assigned this Aug 23, 2024

coot requested review from dcoutts, bolt12 and crocodile-dentist August 23, 2024 05:27

coot changed the title ~~New API for typed-protocols.~~ New API for typed-protocols Aug 23, 2024

coot force-pushed the coot/typed-protocols-new-api branch from 516b253 to cdb6259 Compare August 23, 2024 14:56

bolt12 reviewed Aug 26, 2024

View reviewed changes

coot force-pushed the coot/typed-protocols-new-api branch from cdb6259 to 304b101 Compare August 27, 2024 12:39

coot force-pushed the coot/typed-protocols-new-api branch 3 times, most recently from 9e162be to ea29919 Compare September 6, 2024 04:58

coot force-pushed the coot/typed-protocols-new-api branch from ea29919 to f360046 Compare September 14, 2024 19:07

bolt12 requested changes Sep 16, 2024

View reviewed changes

coot force-pushed the coot/typed-protocols-new-api branch from f360046 to c7b34a4 Compare September 16, 2024 13:10

coot and others added 10 commits September 16, 2024 15:15

typed-protocols: new API

08ee7c4

The new API provides proofs for all protocols, and thus proof obligations are not part of `Protocol` type class but instead an internal detail of the library.

typed-protocols: Peer pattern synonyms

81f2fbe

The client / server 'Peer's pattern synonyms make it easier to write a 'Peer'. They automatically provide the 'RelativeAgencyEq' singleton. See "Network.TypedProtocol.PingPong.Client".

typed-protocols-examples: updated

fe36759

typed-protocols: simplify runPeerWithDriver

b121a80

There's no need to to pass initial `dstate` it is already passed inside `Driver` record.

typed-protocols: internal lemmas module

bdf8100

typed-protocols: provide ReflRelativeAgency type aliases

564da48

* WeHaveAgencyProof * TheyHaveAgencyProof * NobodyHasAgencyProof

typed-protocols-examples: socketAsChannel

6f5ce41

Illustrative example how to define a 'Channel' for a socket. The implementation is only given for posix platforms. It is using a non-blocking `recv` foreign call to provide `tryRecv`.

typed-protocols-examples: ReqResp2 example

c69993a

An example which demonstrates that one can pipeline two kinds of requests, and collect all the responses.

typed-protocols-examples: Wedge

e4bcf98

coot added 10 commits September 16, 2024 15:21

typed-protocols: moved outstanding counter into IsPipelined kind

6c6a8ce

typed-protocols: moved types to Core module

0d9cb77

typed-protocols: connectPipelined type signature

5ec9a8c

typed-protocols: added PeerPipelined newtype wrapper

8d31814

Support io-classes-1.7

b3ba779

typed-protocols: added haddocks

b23f327

disabled typed-protocols-doc in GHA

72a799c

stylish-haskell: fixes

5cf79f3

typed-protocols: removed unused extensions

b9e71bb

coot force-pushed the coot/typed-protocols-new-api branch from c7b34a4 to 2fa9364 Compare September 16, 2024 13:23

bolt12 approved these changes Sep 16, 2024

View reviewed changes

coot force-pushed the coot/typed-protocols-new-api branch 2 times, most recently from 3a117a2 to 9fec582 Compare September 16, 2024 14:30

coot and others added 5 commits September 16, 2024 16:50

Improved haddocks, removed unused pragmas (extensions)

20aa2fe

Removed Stateful PingPong example

0042b72

Stateful RPC example

b195c92

typed-protocols: fixed typos

f451040

coot force-pushed the coot/typed-protocols-new-api branch from 9fec582 to f451040 Compare September 16, 2024 14:51

coot added this pull request to the merge queue Sep 16, 2024

github-merge-queue bot pushed a commit that referenced this pull request Sep 16, 2024

Merge pull request #52 from input-output-hk/coot/typed-protocols-new-api

52a4afd

New API for typed-protocols

coot removed this pull request from the merge queue due to a manual request Sep 16, 2024

coot added this pull request to the merge queue Sep 16, 2024

Merged via the queue into main with commit e216a0a Sep 16, 2024
16 checks passed

coot deleted the coot/typed-protocols-new-api branch September 16, 2024 15:15

coot mentioned this pull request Sep 27, 2024

Typed Protocols: new API IntersectMBO/ouroboros-consensus#1223

Merged

3 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

New API for typed-protocols #52

New API for typed-protocols #52

coot commented Aug 20, 2024 •

edited

Loading

coot commented Aug 22, 2024

bolt12 Aug 26, 2024

coot Sep 3, 2024

coot Sep 3, 2024

coot Sep 3, 2024

bolt12 left a comment

bolt12 Sep 12, 2024

bolt12 Sep 16, 2024

coot Sep 16, 2024

bolt12 Sep 16, 2024

coot Sep 16, 2024

coot commented Sep 16, 2024 •

edited

Loading

New API for typed-protocols #52

New API for typed-protocols #52

Conversation

coot commented Aug 20, 2024 • edited Loading

coot commented Aug 22, 2024

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

bolt12 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

coot commented Sep 16, 2024 • edited Loading

coot commented Aug 20, 2024 •

edited

Loading

coot commented Sep 16, 2024 •

edited

Loading