h,(V&      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQ0.3.0.1 Safe-Inferred )*0 McBride Indexed MonadsHere's Edward Kmett's  https://stackoverflow.com/questions/28690448/what-is-indexed-monadintroduction to Indexed Monads.4As he said, there are at least three indexed monads: Bob Atkey class IMonad m where ireturn :: a -> m i i a ibind :: m i j a -> (a -> m j k b) -> m i k b  Conor McBride type a ~> b = forall i. a i -> b i class IMonad m where ireturn :: a ~> m a ibind :: (a ~> m b) -> (m a ~> m b) Dominic Orchard-No detailed description, just a link to this  https://github.com/dorchard/effect-monad/blob/master/docs/ixmonad-fita14.pdflecture`5I use the McBride Indexed Monad, the earliest paper  ;https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdfhere.The following is my understanding of (~>): through GADT, let the value contain type information, and then use ((~>), pattern match) to pass the type to subsequent functions data V = A | B data SV :: V -> Type where -- GADT, let the value contain type information SA :: SV A SB :: SV B data SV1 :: V -> Type where SA1 :: SV1 A SB1 :: SV1 B fun :: SV ~> SV1 -- type f ~> g = forall x. f x -> g x fun sv = case sv of -- x is arbitrary but f, g must have the same x SA -> SA1 -- Pass concrete type state to subsequent functions via pattern matching SB -> SB1 class (IFunctor m) => IMonad m where ireturn :: a ~> m a ibind :: (a ~> m b) -- The type information contained in a will be passed to (m b), -- which is exactly what we need: external input has an impact on the type! -> m a ~> m b examplePing-Pong type instance Sing = SPingPong instance SingI (S0 b) where sing = SS0 instance SingI S1 where sing = SS1 instance SingI (S2 b) where sing = SS2 instance SingI End where sing = SEnd Singletons are not used here. I am not sure if singletons can generate the instances I need.Here is an example: Ping-Pong data PingPong = S0 [Bool] | S1 | S2 [Bool] | End data SPingPong :: PingPong -> Type where SS0 :: SPingPong (S0 b) SS1 :: SPingPong S1 SS2 :: SPingPong (S2 b) SEnd :: SPingPong End  Note here SS0 :: SPingPong (S0 b)Using singletons will generate !SS0 :: Sing b -> SPingPong (S0 b) which is not what I need."Please note the following example: serverPeer :: (Monad m) => Peer Role PingPong Server m (At () (Done Server)) (S0 s) serverPeer = I.do -- The server is in a state (S0 s) while it is awaiting a message, -- and its state is indeterminate until it receives a message. -- SS0 :: SPingPong (S0 b) correctly indicates this indeterminacy. Recv msg <- await case msg of Ping -> I.do yield Pong serverPeer Stop -> returnAt ()      None)*01P Peer role' ps r m ia st 6IReturn indicates the termination of the continuation. LiftM :: m (Peer role' ps r m ia st') -> Peer role' ps r m ia st Liftm can transform state st to any state st'. It looks a bit strange, as if it is a constructor that is not constrained by the Msg type. Be careful when using it, it is a type breakpoint. But some state transition functions need it, which can make the code more flexible. Be very careful when using it! Yield :: ( SingI recv , SingI from , SingToInt ps ) => Msg role' ps from '(send, sps) '(recv, rps) -> Peer role' ps send m ia sps -> Peer role' ps send m ia from Yield represents sending a message. Note that the Peer status changes from from to sps. Await :: ( SingI recv , SingI from , SingToInt ps ) => (Msg role' ps from send sps recv ~> Peer role' ps recv m ia) -> Peer role' ps recv m ia from Await represents receiving messages. Different messages will lead to different states. The state is passed to the next behavior through (~>).Packaging of Msg, shielding part of the type information, mainly used for serialization.Messages received from the outside are placed in MsgCache. When interpreting Peer will use the Msg in MsgCache.;Describes the type class of Msg. The core of typed-session. type Done (sr :: role') :: ps 3Describe the state of each role when it terminates. data Msg role' ps (fromSt :: ps) (sender :: role') (senderNewSt :: ps) (receiver :: role') (receiverNewSt :: ps) role': the type of the role."ps: the type of the state machine.@@fromSt: when sending a message, the sender is in this state, where the receiver may be in this state, or a more generalized state related to this state. For example, the sender is in state (S1 [True]), and the receiver is in state (S1 s).'sender: the role that sends the message b) and (b -> c), which is wrong. :s1 s1 s1 a -> b s2 s1 s1 b -> c s2 s4 s5 typed-session is a communication framework. The messages received from the outside will be placed in MsgCache. When interpreting the Peer, (Sing (r :: s)) will be generated according to the Peer's status. SingToInt can convert Sing (r :: s) to Int. Depending on this Int value, the required Msg is finally found from MsgCache.In the process of multi-role communication, a message cache structure like MsgCache is needed.Consider the following scenario s1 s1 s2 Initial state ------------ a -> b a sends message MsgA to b ------------ s3 s2 s2 State after sending ------------ b <- c c sends message MsgC to b ------------ s3 s4 s5 State after sending For b, due to the influence of network transmission, it cannot guarantee that it can receive MsgA first and then MsgC. If it receives MsgC first, it will directly put it in MsgCache and continue to wait until MsgA arrives, then it will start to process MsgA first and then MsgC.-In general, dataToTag# is used directly here.Example: instance SingToInt Role where singToInt x = I# (dataToTag# x) instance SingToInt PingPong where singToInt x = I# (dataToTag# x) -Send a message, the Peer status changes from from to sps.Receiving Messages. Lift any m to Peer role' ps r m, which is an application of LiftM. Note that the state of ts has not changed.!  !None')*01%1Bottom functions for sending and receiving bytes.,Generic incremental decoder constructor, you need to convert specific incremental decoders to it.0Incremental decoding function.3"Function to encode Msg into bytes.6&Generic incremental decoding function.6%&'()+*012,./-345345012,/.-)*+%&'(6None')*01&N>?ConnChannels aggregates the multiple connect channels together.?Similar to the log function, used to print received or sent messages.@A wrapper around AnyMsg that represents sending and receiving Msg.CContains two functions sendMsg, recvMsg. runPeerWithDriver uses them to send and receive Msg.HInterpret Peer.I9The default trace function. It simply ignores everything.JBuild Driver through ConnChannels. Here we need some help from other functions: `Tracer role' ps n` is similar to the log function, used to print received or sent messages.`Encode role' ps` bytes encoding function, converts Msg into bytes.`Decode role' ps failure bytes` bytes decode function, converts bytes into Msg.`forall a. n a -> m a` This is a bit complicated, I will explain it in detail below.I see Peer as three layers:  upper layer, meets the requirements of McBride Indexed Monad, uses do syntax construction, has semantic checks, and is interpreted to the second layer m through runPeerWithDriver.m middle layer, describes the business requirements in this layer, and converts the received Msg into specific business actions.n bottom layer, responsible for receiving and sending bytes. It can have multiple options such as IO or IOSim. Using IOSim can easily test the code.K*decode loop, usually in a separate thread.&The decoded Msg is placed in MsgCache. data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', ps)) Note that when placing a new Msg in MsgCache, if a Msg with the same from already exists in MsgCache, the decoding process will be blocked, until that Msg is consumed before placing the new Msg in MsgCache.This usually happens when the efficiency of Msg generation is greater than the efficiency of consumption.KJLIH>CDFGE<=:;@BA?CEFGDH@BA?I><=:;JKLNone')*01&QPQP      !"#$%&'()*+++,+-./.01234445666789:;<<==>?@ABCCCDCECFGHIJKLMNOPtyped-session-0.3.0.1-inplace Data.IFunctorTypedSession.CoreTypedSession.CodecTypedSession.DriverTypedSession.TH typed-session0At IMonadFailfailIMonadireturnibindIFunctorimap~>SingIsingSing>>=>>returnAtPeerIReturnLiftMYieldAwaitAnyMsgMsgCacheProtocolDoneMsg SingToInt singToInt msgFromStSingyieldawaitliftmliftConstructor$fIMonadpsPeer$fIFunctorpspsPeer$fIMonadFailpsPeerChannelrecvsend CodecFailureCodecFailureOutOfInput DecodeStep DecodePartial DecodeDone DecodeFailDecodedecodeEncodeencoderunDecoderWithChannel$fExceptionCodecFailure$fEqCodecFailure$fShowCodecFailureSomeRole NotConnect ConnChannelsTracer TraceSendRecv TraceSendMsg TraceRecvMsgDriverterminalDecodeThreadsrecvMsgsendMsgrunPeerWithDriver nullTracer driverSimple decodeLooplocalDriverSimple$fShowTraceSendRecv$fExceptionNotConnect$fShowNotConnect protocol'protocol