TypedSession.Core

Documentation

class SingToInt s where

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)

Methods

singToInt :: forall (r :: s). Sing r -> Int

class (SingToInt role', SingToInt ps) => Protocol role' ps

Describes the type class of Msg. The core of typed-session.

type Done (sr :: role') :: ps

Describe 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
• senderNewSt: the state of the role after sending the message
• receiver: the role that receives the message
• receiverNewSt: the state of the role after receiving the message

There are two principles to follow when designing the state of Msg:

1. When sending a message, the sender and receiver must be in the same state. Here the receiver may be in a more generalized state related to the state. For example, the sender is in state (S1 [True]), and the receiver is in state (S1 s).
2. The same state can only be used for the same pair of receiver and sender.

For example, in the following example, state s1 is used for both (a -> b) and (b -> c), which is wrong.

s1   s1   s1
a -> b
s2   s1   s1
     b -> c
s2   s4   s5

Associated Types

type Done (sr :: role') :: ps

data Msg role' ps (fromSt :: ps) (sender :: role') (senderNewSt :: ps) (receiver :: role') (receiverNewSt :: ps)

type MsgCache role' ps (n :: Type -> Type) = TVar n (IntMap (AnyMsg role' ps))

Messages received from the outside are placed in MsgCache. When interpreting Peer will use the Msg in MsgCache.

data AnyMsg role' ps where

Packaging of Msg, shielding part of the type information, mainly used for serialization.

Constructors

AnyMsg :: forall role' (recv :: role') ps (st :: ps) (send :: role') (st' :: ps) (st'' :: ps). (SingI recv, SingI st, SingToInt role', SingToInt ps) => Msg role' ps st send st' recv st'' -> AnyMsg role' ps

msgFromStSing :: forall role' ps (st :: ps) (send :: role') (recv :: role') (st' :: ps) (st'' :: ps). (SingI recv, SingI st) => Msg role' ps st send st' recv st'' -> Sing st

data Peer role' ps (r :: role') (m :: Type -> Type) (ia :: ps -> Type) (st :: ps) where

Core Ast, all we do is build this Ast and then interpret it.

IReturn :: ia st -> Peer role' ps r m ia st

IReturn 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 (~>).

Constructors

IReturn :: forall ps (ia :: ps -> Type) (st :: ps) role' (r :: role') (m :: Type -> Type). ia st -> Peer role' ps r m ia st

LiftM :: forall (m :: Type -> Type) role' ps (r :: role') (ia :: ps -> Type) (st' :: ps) (st :: ps). m (Peer role' ps r m ia st') -> Peer role' ps r m ia st

Yield :: forall role' (recv :: role') ps (st :: ps) (r :: role') (sps :: ps) (rps :: ps) (m :: Type -> Type) (ia :: ps -> Type). (SingI recv, SingI st, SingToInt ps) => Msg role' ps st r sps recv rps -> Peer role' ps r m ia sps -> Peer role' ps r m ia st

Await :: forall role' (r :: role') ps (st :: ps) (send :: role') (sps :: ps) (m :: Type -> Type) (ia :: ps -> Type). (SingI r, SingI st, SingToInt ps) => (Msg role' ps st send sps r ~> Peer role' ps r m ia) -> Peer role' ps r m ia st

Instances

Functor m => IFunctor (Peer role' ps r m :: (ps -> Type) -> ps -> Type)

Defined in TypedSession.Core

Methods

imap :: forall (a :: ps -> Type) (b :: ps -> Type). (a ~> b) -> Peer role' ps r m a ~> Peer role' ps r m b

Functor m => IMonad (Peer role' ps r m :: (ps -> Type) -> ps -> Type)

Defined in TypedSession.Core

Methods

ireturn :: forall (a :: ps -> Type). a ~> Peer role' ps r m a

ibind :: forall (a :: ps -> Type) (b :: ps -> Type). (a ~> Peer role' ps r m b) -> Peer role' ps r m a ~> Peer role' ps r m b

Functor m => IMonadFail (Peer role' ps r m :: (ps -> Type) -> ps -> Type)

Defined in TypedSession.Core

Methods

fail :: forall (a :: ps -> Type) (ix :: ps). String -> Peer role' ps r m a ix

yield :: forall (m :: Type -> Type) role' (recv :: role') ps (from :: ps) (send :: role') (sps :: ps) (rps :: ps). (Functor m, SingI recv, SingI from, SingToInt ps) => Msg role' ps from send sps recv rps -> Peer role' ps send m (At () sps) from

Send a message, the Peer status changes from from to sps.

await :: forall (m :: Type -> Type) role' (recv :: role') ps (from :: ps) (send :: role') (sps :: ps). (Functor m, SingI recv, SingI from, SingToInt ps) => Peer role' ps recv m (Msg role' ps from send sps recv) from

Receiving Messages.

liftm :: forall m a role' ps (r :: role') (ts :: ps). Functor m => m a -> Peer role' ps r m (At a ts) ts

Lift any m to Peer role' ps r m, which is an application of LiftM. Note that the state of ts has not changed.

liftConstructor :: forall (m :: Type -> Type) k ia (st' :: k) role' (r :: role') (st :: k). Applicative m => ia st' -> Peer role' k r m ia st