Using IndexMonad to improve typed-protocols

[sdzx-1]

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]

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]

1. After a brief look at the new design, I feel that the new Peer is also an Indexed Monad, and it tracks more states.
2. 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]

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]

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

[sdzx-1]

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]

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]

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

[coot]

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]

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.