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