Code Monkey home page Code Monkey logo

Comments (9)

sdzx-1 avatar sdzx-1 commented on September 21, 2024 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

from typed-protocols.

coot avatar coot commented on September 21, 2024 1

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).

from typed-protocols.

sdzx-1 avatar sdzx-1 commented on September 21, 2024 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.

from typed-protocols.

coot avatar coot commented on September 21, 2024

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

from typed-protocols.

sdzx-1 avatar sdzx-1 commented on September 21, 2024
  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 ()

from typed-protocols.

sdzx-1 avatar sdzx-1 commented on September 21, 2024

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

from typed-protocols.

coot avatar coot commented on September 21, 2024

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

from typed-protocols.

sdzx-1 avatar sdzx-1 commented on September 21, 2024

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

from typed-protocols.

sdzx-1 avatar sdzx-1 commented on September 21, 2024

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

from typed-protocols.

Related Issues (12)

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.