Closed sdzx-1 closed 2 months ago
@coot @dcoutts @mrBliss @edsko
I'm trying to improve typed-protocols. typed-protocols only allows communication between client-server, but typed-communication-protocol allows communication between any number of roles.
typed-communication-protocol uses Mcbride Indexed Monad.
This library requires the latest ghc 9.10.1!
Here is a examples:TheBug-ProneBookseller The example comes from HasChor: Functional Choreographic Programming for All
Detailed description:
{- ----------------------------------------------- role: Buyer Seller Buyer Seller title -> <- price checkPrice CheckTrue Afford -> data <- CheckFalse NotBuy -> ------------------- Add State --------------------------- Buyer Seller :S0 :S0 Title -> :S1 :S1 <- Price :S12 :S2 s [S2 True] Afford -> :S3 :S3 Data <- :End :End [S2 False] NotBuy -> :End :End - -}
Code:
data Role = Buyer | Seller data BookSt = S0 | S1 | S12 | S2 Bool | S3 | End type Date = Int instance Protocol Role BookSt where type Done Buyer = End type Done Seller = End data Msg Role BookSt send recv from to where Title :: String -> Msg Role BookSt Buyer Seller S0 '(S1, S1) Price :: Int -> Msg Role BookSt Seller Buyer S1 '(S2 s, S12) Afford :: Msg Role BookSt Buyer Seller (S2 True) '(S3, S3) Date :: Date -> Msg Role BookSt Seller Buyer S3 '(End, End) NotBuy :: Msg Role BookSt Buyer Seller (S2 False) '(End, End) data CheckPriceResult :: BookSt -> Type where CheckTrue :: CheckPriceResult (S2 True) CheckFalse :: CheckPriceResult (S2 False) checkPrice :: Int -> Peer Role BookSt Buyer IO CheckPriceResult S12 checkPrice i = if i < 100 then LiftM $ pure (ireturn CheckTrue) else LiftM $ pure (ireturn CheckFalse) buyerPeer :: Peer Role BookSt Buyer IO (At (Maybe Date) (Done Buyer)) S0 buyerPeer = I.do yield (Title "haskell book") Recv (Price i) <- await res <- checkPrice i case res of CheckTrue -> I.do yield Afford Recv (Date d) <- await returnAt (Just d) CheckFalse -> I.do yield NotBuy returnAt Nothing 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 -> yield (Date 100) NotBuy -> returnAt ()
two-buyer bookseller protocol
{- ----------------------------------------------- Buyer Seller Buyer2 :S0 :S0 Title -> :S1 :S1 <- Price :S11 :S11 -> PriceToB2 :S110 :S110 <- HalePrice :S12 :End :S2 s [S2 True] Afford -> :S3 :S3 Data <- :End :End [S2 False] NotBuy -> :End :End - -}
data Role = Buyer | Seller | Buyer2 data BookSt = S0 | S1 | S11 | S110 | S12 | S2 Bool | 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 send recv from to where Title :: String -> Msg Role BookSt Buyer Seller S0 '(S1, S1) Price :: Int -> Msg Role BookSt Seller Buyer S1 '(S2 s, S11) PriceToB2 :: Int -> Msg Role BookSt Buyer Buyer2 S11 '(S110, S110) HalfPrice :: Int -> Msg Role BookSt Buyer2 Buyer S110 '(End, S12) Afford :: Msg Role BookSt Buyer Seller (S2 True) '(S3, S3) Date :: Date -> Msg Role BookSt Seller Buyer S3 '(End, End) NotBuy :: Msg Role BookSt Buyer Seller (S2 False) '(End, End) data CheckPriceResult :: BookSt -> Type where CheckTrue :: CheckPriceResult (S2 True) CheckFalse :: CheckPriceResult (S2 False) budget :: Int budget = 100 checkPrice :: Int -> Int -> Peer Role BookSt Buyer IO CheckPriceResult S12 checkPrice i hv = if i < budget + hv then LiftM $ pure (ireturn CheckTrue) else LiftM $ pure (ireturn CheckFalse) 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 CheckTrue -> I.do yield Afford Recv (Date d) <- await returnAt (Just d) CheckFalse -> 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 -> yield (Date 100) NotBuy -> returnAt ()
Now my question is how to design Driver & Codec? This seems complicated and I have no idea. Do you have any suggestions?
Maybe I've solved this problem!
@coot @dcoutts @mrBliss @edsko
I'm trying to improve typed-protocols. typed-protocols only allows communication between client-server, but typed-communication-protocol allows communication between any number of roles.
typed-communication-protocol uses Mcbride Indexed Monad.
This library requires the latest ghc 9.10.1!
Here is a examples:TheBug-ProneBookseller The example comes from HasChor: Functional Choreographic Programming for All
Detailed description:
Code:
two-buyer bookseller protocol
Code:
Now my question is how to design Driver & Codec? This seems complicated and I have no idea. Do you have any suggestions?