Typed-communication-protocol

[sdzx-1]

Typed communication protocol allows communication between any number of roles.It is inspired by typed-protocols.

Here is a examples：Two-buyer bookseller protocol. The example comes from HasChor: Functional Choreographic Programming for All.

Code:

data Role = Buyer | Seller | Buyer2
  deriving (Show, Eq, Ord)

data BudgetSt
  = EnoughBudget
  | NotEnoughBuget

data BookSt
  = S0
  | S1
  | S11
  | S110
  | S12'
  | S12 BudgetSt
  | S3
  | End

type Date = Int

instance Protocol Role BookSt where
  type Done Buyer = End
  type Done Seller = End
  type Done Buyer2 = End
  data Msg Role BookSt from send recv  where
    Title     :: String -> Msg Role BookSt S0                   '(Buyer, S1)       '(Seller, S1) 
    Price     :: Int ->    Msg Role BookSt S1                   '(Seller, S12 s)   '(Buyer, S11) 
    PriceToB2 :: Int ->    Msg Role BookSt S11                  '(Buyer  ,S110)    '(Buyer2 ,S110) 
    HalfPrice :: Int ->    Msg Role BookSt S110                 '(Buyer2 ,End)     '(Buyer  ,S12') 
    Afford    ::           Msg Role BookSt (S12 EnoughBudget)   '(Buyer  ,S3)      '(Seller ,S3) 
    Date      :: Date ->   Msg Role BookSt S3                   '(Seller ,End)     '(Buyer  ,End)
    NotBuy    ::           Msg Role BookSt (S12 NotEnoughBuget) '(Buyer  ,End)     '(Seller ,End)

budget :: Int
budget = 16

data CheckPriceResult :: BookSt -> Type where
  Yes :: CheckPriceResult (S12 EnoughBudget)
  No :: CheckPriceResult (S12 NotEnoughBuget)

checkPrice :: Int -> Int -> Peer Role BookSt Buyer IO CheckPriceResult S12'
checkPrice i h = 
  if i <= budget + h
  then LiftM $ pure (ireturn Yes)
  else LiftM $ pure (ireturn No)

buyerPeer
  :: Peer Role BookSt Buyer IO (At (Maybe Date) (Done Buyer)) S0
buyerPeer = I.do
  yield (Title "haskell book")
  Recv (Price i) <- await
  yield (PriceToB2 i)
  Recv (HalfPrice hv) <- await
  res <- checkPrice i hv
  case res of
    Yes -> I.do
      yield Afford
      Recv (Date d) <- await
      returnAt (Just d)
    No -> I.do
      yield NotBuy
      returnAt Nothing

buyerPeer2
  :: Peer Role BookSt Buyer2 IO (At () (Done Buyer2)) S11
buyerPeer2 = I.do
  Recv (PriceToB2 i) <- await
  yield (HalfPrice (i `div` 2))

sellerPeer :: Peer Role BookSt Seller IO (At () (Done Seller)) S0
sellerPeer = I.do
  Recv (Title _name) <- await
  yield (Price 30)
  Recv msg <- await
  case msg of
    Afford -> I.do
      yield (Date 100)
    NotBuy -> I.do
      returnAt ()

[blamario]

I’m not fond of QualifiedDo, but I must admit it makes this example very readable. I wish we had a more principled solution for indexed monads.

[sdzx-1]

You may also be interested in this library: typed-fsm.I think Mcbride Indexed Monad has huge potential. There is currently too little discussion and use of it. I’m trying to find its value. I hope more people use it.

[Ambrose]

I kind of want to use this to define video game logic! Just gotta find the time.

[sdzx-1]

I’m developing an algorithm communication-protocol-state-algorithm : automatically generate status for typed-communication-protocol.

data BookRole
  = Buyer
  | Seller
  | Buyer2
  deriving (Show)

bookRoleToInt :: BookRole -> Int
bookRoleToInt = \case
  Buyer -> 0
  Seller -> 1
  Buyer2 -> 2

p :: R BookRole ()
p =
  (Buyer --> Seller) "Title"
    :> branch
      [ branchVal "BookNotFound" $
          (Buyer <-- Seller) "BookNotFoun"
            :> (Buyer --> Buyer2) "SellerNotFoundBook"
            :> terminal
      , branchVal "BookFound" $
          (Buyer <-- Seller) "Price"
            :> (Buyer --> Buyer2) "PriceToBuyer2"
            :> (Buyer <-- Buyer2) "HalfPrice"
            :> branch
              [ branchVal "EnoughBudget" $
                  ( (Buyer --> Seller) "Afford"
                      :> (Buyer <-- Seller) "Data"
                      :> (Buyer --> Buyer2) "Success"
                      :> terminal
                  )
              , branchVal "NotEnoughBudget" $
                  ( (Buyer --> Seller) "NotBuy"
                      :> (Buyer --> Buyer2) "Failed"
                      :> terminal
                  )
              ]
      ]

v2 :: [Char]
v2 =
  pipleR
    [Buyer, Seller, Buyer2]
    bookRoleToInt
    p

It can automatically generate the following status:

{-

>>> error v2
-----------------Buyer---------------Seller--------------Buyer2-----------------
                   S0                  S0                 S1 s
       Title       |        --->       |
                  S2 s                S2 s                S1 s
    ------------------------------BookNotFound------------------------------
                  S2 s          S2 BookNotFound           S1 s
    BookNotFoun    |        <---       |
            S1 BookNotFound           End                 S1 s
  SellerNotFoundB  |                  --->                 |
                  End                 End                 End
                                    Terminal

    -------------------------------BookFound--------------------------------
                  S2 s            S2 BookFound            S1 s
       Price       |        <---       |
              S1 BookFound            S3 s                S1 s
   PriceToBuyer2   |                  --->                 |
                   S4                 S3 s                 S4
     HalfPrice     |                  <---                 |
                  S3 s                S3 s                S5 s
        --------------------------EnoughBudget--------------------------
            S3 EnoughBudget           S3 s                S5 s
       Afford      |        --->       |
                   S6                  S6                 S5 s
        Data       |        <---       |
            S5 EnoughBudget           End                 S5 s
      Success      |                  --->                 |
                  End                 End                 End
                                    Terminal

        ------------------------NotEnoughBudget-------------------------
           S3 NotEnoughBudget         S3 s                S5 s
       NotBuy      |        --->       |
           S5 NotEnoughBudget         End                 S5 s
       Failed      |                  --->                 |
                  End                 End                 End
                                    Terminal

-}

Is anyone interested in it?