Using IndexMonad to improve typed-protocols #25

sdzx-1 · 2023-01-17T22:38:17Z

Is your feature request related to a problem? Please describe.

Peer is essentially a McBride style indexed monad.
With a slight modification to Peer, we can use do syntax to describe Peer.

new Peer implement:

https://github.com/sdzx-1/typed-protocols-i/blob/685fb27ec0b57bab508874127c578ead22807a28/src/Network/TypedProtocol/Core.hs#L67

use do syntax to describe Peer:
https://github.com/sdzx-1/typed-protocols-i/blob/685fb27ec0b57bab508874127c578ead22807a28/test/Network/Core.hs#L46

pingPongClientPeer :: Has (State Int) sig m 
                   => Peer PingPong AsClient m (At () StDone) StIdle
pingPongClientPeer = I.do
    -- ghc bug: https://gitlab.haskell.org/ghc/ghc/-/issues/22788 
    -- we can't use this: 
    -- i <- effect (get @Int) 
    -- if i > 10 
    --   then  ...
    --   else ...
    --
    effect (get @Int) I.>>= 
      \(At i ) ->
         if i > 10 
          then I.do
            yield (ClientAgency TokIdle) MsgDone
            done TokDone ()
          else I.do
            yield (ClientAgency TokIdle) MsgPing 
            effect $ modify @Int (+1)
            await (ServerAgency TokBusy) I.>>= \case
              MsgPong -> pingPongClientPeer

pingPongServerPeer :: Has (Lift IO ) sig m 
                   => Peer PingPong AsServer m (At () StDone) StIdle
pingPongServerPeer = Indexed.do 
    await (ClientAgency TokIdle) I.>>= \case
      MsgDone -> I.do 
        effect $ sendIO (print "recv MsgDone, finish")
        done TokDone ()
      MsgPing -> I.do 
        effect $ sendIO (print "recv MsgPing, send MsgPong")
        yield (ServerAgency TokBusy) MsgPong
        pingPongServerPeer

Describe the solution you'd like

Describe alternatives you've considered

Additional context

ghc currently has a bug in the QualifiedDo syntax, sometimes makes the code look weird.
https://gitlab.haskell.org/ghc/ghc/-/issues/22788

the code I expect：

pingPongClientPeer' :: Has (State Int) sig m 
                   => Peer PingPong AsClient m (At () StDone) StIdle
pingPongClientPeer' = I.do
  At i <- effect (get @Int) 
  if i > 10 
   then I.do
     yield (ClientAgency TokIdle) MsgDone
     done TokDone ()
   else I.do
     yield (ClientAgency TokIdle) MsgPing 
     effect $ modify @Int (+1)
     await (ServerAgency TokBusy) I.>>= \case
       MsgPong -> pingPongClientPeer

Are you willing to implement it?

Are you? yes

@coot

coot · 2023-01-19T13:15:25Z

That's an interesting idea. Will this also work with our redesign in #3? It tracks even more than just the state at the type level, also the pipelining queue?

The Peer in the current implementation is non pipelined one, and probably the pipelined one does not fit into this scheme. The new Peer in #3 can also be limited to just non-pipelined version, and this will probably work too. If so then your example will become even simpler:

pingPongClientPeer' :: Has (State Int) sig m 
                    => Client PingPong NotPipelined ...
pingPongClientPeer' = I.do
  At i <- effect (get @Int) 
  if i > 10 
   then I.do
     yield MsgDone
     done ()
   else I.do
     yield MsgPing 
     effect $ modify @Int (+1)
     await I.>>= \case
       MsgPong -> pingPongClientPeer

sdzx-1 · 2023-01-20T03:28:45Z

After a brief look at the new design, I feel that the new Peer is also an Indexed Monad, and it tracks more states.
I have also tried to simplify Peer.

class Protocol ps where
  data Message ps (st :: ps) (st' :: ps)
  data Sig ps (st :: ps)
  type NobodyAgencyList ps :: [ps]
  type ClientAgencyList ps :: [ps]
  type ServerAgencyList ps :: [ps]
  encode :: Message ps (st :: ps) (st' :: ps) -> CBOR.Encoding
  decode :: Sig ps (st :: ps) -> CBOR.Decoder s (SomeMessage st)

class ToSig ps (st :: ps) where
  toSig :: Sig ps st

pingPong example

ppServer
  :: forall m n sig
   . ( Monad n
     , MonadSay n
     , MonadTime n
     , Has (State Int) sig m
     , HasLabelledLift n sig m
     )
  => Peer PingPong Server StIdle m ()
ppServer = await $ \case
  MsgPing i -> effect $ do
    modify (+ i)
    lift $ say $ "s MsgPing " ++ show i
    i' <- get @Int
    pure $ yield (MsgPong i') ppServer
  MsgDone -> Effect $ do
    lift $ say "server done"
    pure $ done ()

sdzx-1 · 2023-01-23T08:47:21Z

Some thoughts on pipeplined

data K ps ::  (n, st) -> (n, st) -> Type where
    K :: Message ps st st' -> K ps '(n, st) '(n, st')

data PS ps pr c m q (k :: (N, st)) where

    SReturn :: q k -> PS ps pr c m q k

    SEffect :: m (PS ps pr c m q k) -> PS ps pr c m q k

    SYield :: (WeHaveAgency pr st) 
           -> K ps '(any, st) '(any, st')
           -> PS ps pr c m q '(Z, st')
           -> PS ps pr c m q '(Z, st)

    SAwait :: TheyHaveAgency pr st 
           -> (K ps '(any, st) ~> PS ps pr c m q )
           -> PS ps pr c m q '(Z, st)

    SPipeline :: WeHaveAgency pr st  
              -> K ps '(any, st) '(any, st')
              -> PeerReceiver ps pr st' st'' m c 
              -> PS ps pr  c m q '(S n , st'')
              -> PS ps pr c m q '(n, st)

    -- SCollect :: Maybe (PS ps pr c m q '(S n, st))
    --               -> (c -> PS ps pr c m q '(n, st))
    --               -> PS ps pr c m q '(S n , st)


ppClientPeerSender :: Functor m 
                   => PS PingPong AsClient c m (At () '(Z, StDone)) '(Z, StIdle)
ppClientPeerSender = I.do
    sYield (ClientAgency TokIdle) (K MsgPing)
    K v <- sAwait (ServerAgency TokBusy)
    case v of 
        MsgPong -> 
            sYield (ClientAgency TokIdle) (K MsgDone)


ppSender :: Functor m 
         => PS PingPong AsClient c m (At () '(Z, StDone)) '(Z, StIdle)
ppSender = I.do 
    sPipeline (ClientAgency TokIdle) (K MsgPing) (ReceiverAwait (ServerAgency TokBusy) $ \MsgPong -> undefined)
    sPipeline (ClientAgency TokIdle) (K MsgPing) (ReceiverAwait (ServerAgency TokBusy) $ \MsgPong -> undefined)
    sPipeline (ClientAgency TokIdle) (K MsgPing) (ReceiverAwait (ServerAgency TokBusy) $ \MsgPong -> undefined)
    sPipeline (ClientAgency TokIdle) (K MsgPing) (ReceiverAwait (ServerAgency TokBusy) $ \MsgPong -> undefined)
    undefined

This is not comprehensive. But I think pipeliened can be Indexed Monad.

I don't understand the meaning here.

  SenderCollect  :: Maybe (PeerSender ps pr (st :: ps) (S n) c m a)  --I don't know what it means here？
                          -> (c ->  PeerSender ps pr (st :: ps)    n  c m a)
                          ->        PeerSender ps pr (st :: ps) (S n) c m a

@coot

coot · 2023-01-27T22:00:52Z

Consider the case when nothing is yet available from the channel, then Just pipelineMore allows one to pipeline more messages

sdzx-1 · 2023-02-03T10:41:35Z

A more complete idea about pipelined

data K ps :: (N, st) -> (N, st) -> Type where
  K :: Message ps st st' -> K ps '(n, st) '(n, st')

data PS ps pr c m q (k :: (N, st)) where
  SReturn :: q k -> PS ps pr c m q k
  SEffect :: m (PS ps pr c m q k) -> PS ps pr c m q k
  SYield ::
    (WeHaveAgency pr st) ->
    Message ps st st' ->
    PS ps pr c m q '(Z, st') ->
    PS ps pr c m q '(Z, st)
  SAwait ::
    TheyHaveAgency pr st ->
    (K ps '(Z, st) ~> PS ps pr c m q) ->
    PS ps pr c m q '(Z, st)
  SPipeline ::
    WeHaveAgency pr st ->
    Message ps st st' ->
    PeerReceiver ps pr st' st'' m c ->
    PS ps pr c m q '(S n, st'') ->
    PS ps pr c m q '(n, st)
  SCollect ::
    (At c '(n, st) ~> PS ps pr c m q) ->
    PS ps pr c m q '(S n, st)

Two pingpong client examples:

ppClientPeerSender ::
  Functor m =>
  PS PingPong AsClient c m (At () '(Z, StDone)) '(Z, StIdle)
ppClientPeerSender = I.do
  sYield (ClientAgency TokIdle) MsgPing
  K v <- sAwait (ServerAgency TokBusy)
  case v of
    MsgPong -> sYield (ClientAgency TokIdle) MsgDone

ppSender ::
  Functor m =>
  PS PingPong AsClient () m (At () '(Z, StDone)) '(Z, StIdle)
ppSender = I.do
  sYield (ClientAgency TokIdle) MsgPing
  K v <- sAwait (ServerAgency TokBusy)
  case v of
    MsgPong -> I.do
      sPipeline (ClientAgency TokIdle) MsgPing (ReceiverAwait (ServerAgency TokBusy) $ \MsgPong -> ReceiverDone ())
      sPipeline (ClientAgency TokIdle) MsgPing (ReceiverAwait (ServerAgency TokBusy) $ \MsgPong -> ReceiverDone ())
      sCollect
      sCollect
      sPipeline (ClientAgency TokIdle) MsgPing (ReceiverAwait (ServerAgency TokBusy) $ \MsgPong -> ReceiverDone ())
      sCollect
      sYield (ClientAgency TokIdle) MsgDone

I think it's time to start thinking about #3 redesign.
@coot

sdzx-1 · 2023-02-05T12:42:07Z

Thinking about #3 redesign.
After fixing the QualifiedQo bug, we finally got here.

ppClient1 ::
  (Functor m, IMonadFail (Peer PingPong 'AsClient m)) =>
  Peer
    PingPong
    AsClient
    m
    (At () '(Pipelined, Empty, StDone))
    '(Pipelined, Empty, StIdle)
ppClient1 = I.do
  sYieldPipelined MsgPing
  sYieldPipelined MsgPing
  sYieldPipelined MsgPing
  sYieldPipelined @_ @StDone MsgDone
  C MsgPong <- sCollect
  sCollectDone
  C MsgPong <- sCollect
  sCollectDone
  C MsgPong <- sCollect
  sCollectDone
  sCollectDone

sdzx-1 · 2024-02-06T09:17:00Z

The issue with QualifiedQo seems to have been resolved, maybe it can be continued from here.

coot · 2024-02-07T12:33:00Z

Yes, that's fine.

We also discovered that the new pipelining API (asynchronious rather than parallel) is quite a bit slower, so we will not continue that approach - at least right away, the possible fix would require substantial changes. We might bring just API improvements but we can figure that later once we'll have time for it (probably somewhere in Q2 or Q3 2024).

sdzx-1 · 2024-04-24T06:20:10Z

I'm developing this library typed-communication-protocol. It is inspired by typed-protocols. It can describe communication protocols for any number of roles, not just client-server.

sdzx-1 added the enhancement New feature or request label Jan 17, 2023

coot added this to Ouroboros Network Jan 19, 2023

amesgen mentioned this issue Jan 29, 2024

Allow the pipelined ChainSync client to observe MsgAwaitReply messages IntersectMBO/ouroboros-network#4791

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Using IndexMonad to improve typed-protocols #25

Using IndexMonad to improve typed-protocols #25

sdzx-1 commented Jan 17, 2023 •

edited

Loading

coot commented Jan 19, 2023

sdzx-1 commented Jan 20, 2023

sdzx-1 commented Jan 23, 2023 •

edited

Loading

coot commented Jan 27, 2023

sdzx-1 commented Feb 3, 2023 •

edited

Loading

sdzx-1 commented Feb 5, 2023 •

edited

Loading

sdzx-1 commented Feb 6, 2024

coot commented Feb 7, 2024

sdzx-1 commented Apr 24, 2024

Using IndexMonad to improve typed-protocols #25

Using IndexMonad to improve typed-protocols #25

Comments

sdzx-1 commented Jan 17, 2023 • edited Loading

coot commented Jan 19, 2023

sdzx-1 commented Jan 20, 2023

sdzx-1 commented Jan 23, 2023 • edited Loading

coot commented Jan 27, 2023

sdzx-1 commented Feb 3, 2023 • edited Loading

sdzx-1 commented Feb 5, 2023 • edited Loading

sdzx-1 commented Feb 6, 2024

coot commented Feb 7, 2024

sdzx-1 commented Apr 24, 2024

sdzx-1 commented Jan 17, 2023 •

edited

Loading

sdzx-1 commented Jan 23, 2023 •

edited

Loading

sdzx-1 commented Feb 3, 2023 •

edited

Loading

sdzx-1 commented Feb 5, 2023 •

edited

Loading