typed-session (empty) → 0.1.0.0
raw patch · 16 files changed
+2453/−0 lines, 16 filesdep +basedep +containersdep +fused-effectsbinary-added
Dependencies added: base, containers, fused-effects, fused-effects-random, io-classes, io-sim, random, typed-session
Files
- CHANGELOG.md +3/−0
- LICENSE +21/−0
- data/fm.png binary
- src/Data/IFunctor.hs +163/−0
- src/TypedProtocol/Codec.hs +72/−0
- src/TypedProtocol/Core.hs +254/−0
- src/TypedProtocol/Driver.hs +216/−0
- test/Book.hs +231/−0
- test/Book1.hs +280/−0
- test/Book2.hs +341/−0
- test/Book3/Main.hs +118/−0
- test/Book3/Peer.hs +159/−0
- test/Book3/Type.hs +256/−0
- test/Main.hs +15/−0
- test/PingPong.hs +195/−0
- typed-session.cabal +129/−0
+ CHANGELOG.md view
@@ -0,0 +1,3 @@+# Revision history for typed-session++## 0.1.0.0-- 2024-8-6
+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2024 Yang Miao++Permission is hereby granted, free of charge, to any person obtaining a copy+of this software and associated documentation files (the "Software"), to deal+in the Software without restriction, including without limitation the rights+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell+copies of the Software, and to permit persons to whom the Software is+furnished to do so, subject to the following conditions:++The above copyright notice and this permission notice shall be included in all+copies or substantial portions of the Software.++THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE+SOFTWARE.
+ data/fm.png view
binary file changed (absent → 95345 bytes)
+ src/Data/IFunctor.hs view
@@ -0,0 +1,163 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE StandaloneKindSignatures #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++module Data.IFunctor where++import Data.Data+import Data.Kind++{- |+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 ()+@+-}+type family Sing :: k -> Type++type SingI :: forall {k}. k -> Constraint++{- |++example：Ping-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+@+-}+class SingI a where+ sing :: Sing a++infixr 0 ~>++type f ~> g = forall x. f x -> g x++class IFunctor f where+ imap :: (a ~> b) -> f a ~> f b++{- | McBride Indexed Monads++Here's Edward Kmett's [introduction to Indexed Monads](https://stackoverflow.com/questions/28690448/what-is-indexed-monad).++As 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 [lecture](https://github.com/dorchard/effect-monad/blob/master/docs/ixmonad-fita14.pdf)。++I use the McBride Indexed Monad, the earliest paper [here](https://personal.cis.strath.ac.uk/conor.mcbride/Kleisli.pdf).++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+@+-}+class (IFunctor m) => IMonad m where+ ireturn :: a ~> m a+ ibind :: (a ~> m b) -> m a ~> m b++class (IMonad m) => IMonadFail m where+ fail :: String -> m a ix++data At :: Type -> k -> k -> Type where+ At :: a -> At a k k+ deriving (Typeable)++(>>=) :: (IMonad (m :: (x -> Type) -> x -> Type)) => m a ix -> (a ~> m b) -> m b ix+m >>= f = ibind f m++(>>) :: (IMonad (m :: (x -> Type) -> x -> Type)) => m (At a j) i -> m b j -> m b i+m >> f = ibind (\(At _) -> f) m++returnAt :: (IMonad m) => a -> m (At a k) k+returnAt = ireturn . At
+ src/TypedProtocol/Codec.hs view
@@ -0,0 +1,72 @@+-- This part of the code comes from typed-protocols, I modified a few things.+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE UndecidableInstances #-}++module TypedProtocol.Codec where++import Control.Exception (Exception)+import TypedProtocol.Core++{- |+Function to encode Msg into bytes.+-}+newtype Encode role' ps bytes = Encode+ { encode+ :: forall (send :: role') (recv :: role') (st :: ps) (st' :: ps) (st'' :: ps)+ . Msg role' ps st '(send, st') '(recv, st'')+ -> bytes+ }++{- |+Incremental decoding function.+-}+newtype Decode role' ps failure bytes = Decode+ { decode :: DecodeStep bytes failure (AnyMsg role' ps)+ }++{- |+Generic incremental decoder constructor, you need to convert specific incremental decoders to it.+-}+data DecodeStep bytes failure a+ = DecodePartial (Maybe bytes -> (DecodeStep bytes failure a))+ | DecodeDone a (Maybe bytes)+ | DecodeFail failure++data CodecFailure+ = CodecFailureOutOfInput+ | CodecFailure String+ deriving (Eq, Show)++instance Exception CodecFailure++{- |+Bottom functions for sending and receiving bytes.+-}+data Channel m bytes = Channel+ { send :: bytes -> m ()+ , recv :: m (Maybe bytes)+ }++{- |+Generic incremental decoding function.+-}+runDecoderWithChannel+ :: (Monad m)+ => Channel m bytes+ -> Maybe bytes+ -> DecodeStep bytes failure a+ -> m (Either failure (a, Maybe bytes))+runDecoderWithChannel Channel{recv} = go+ where+ go _ (DecodeDone x trailing) = return (Right (x, trailing))+ go _ (DecodeFail failure) = return (Left failure)+ go Nothing (DecodePartial k) = recv >>= pure . k >>= go Nothing+ go (Just trailing) (DecodePartial k) = (pure . k) (Just trailing) >>= go Nothing
+ src/TypedProtocol/Core.hs view
@@ -0,0 +1,254 @@+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-}++module TypedProtocol.Core where++import Data.IFunctor+import Data.IntMap (IntMap)+import Data.Kind++{- |++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)+@+-}+class SingToInt s where+ singToInt :: Sing (r :: s) -> Int++{- |++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 (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', ps))+@+* role': the type of the role.+* ps: the type of the state machine.+* from: 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).+* sendAndSt: the role that sends the message and the state of the role after sending the message.+* recvAndSt: the role that receives the message and 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+@+-}+class (SingToInt role', SingToInt ps) => Protocol role' ps where+ type Done (sr :: role') :: ps+ data Msg role' ps (from :: ps) (sendAndSt :: (role', ps)) (recvAndSt :: (role', ps))++{- |+Package Msg and extract the required type.++@+Msg role' ps from '(send, sps) '(recv, rps)+Recv role' ps recv from rps+@+-}+data Recv role' ps recv from to where+ Recv+ :: Msg role' ps from '(send, sps) '(recv, rps)+ -> Recv role' ps recv from rps++{- |+Messages received from the outside are placed in MsgCache. When interpreting+Peer will use the Msg in MsgCache.+-}+type MsgCache role' ps = IntMap (AnyMsg role' ps)++{- |+Packaging of Msg, shielding part of the type information, mainly used for serialization.+-}+data AnyMsg role' ps where+ AnyMsg+ :: ( SingI recv+ , SingI st+ , SingToInt role'+ , SingToInt ps+ )+ => Msg role' ps st '(send, st') '(recv, st'')+ -> AnyMsg role' ps++msgFromStSing+ :: forall role' ps st send recv st' st''+ . (SingI recv, SingI st)+ => Msg role' ps st '(send, st') '(recv, st'')+ -> Sing st+msgFromStSing _ = sing @st++{- |+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+ )+ => (Recv role' ps recv from ~> 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 (~>).+-}+data Peer role' ps (r :: role') (m :: Type -> Type) (ia :: ps -> Type) (st :: ps) where+ IReturn :: ia st -> Peer role' ps r m ia st+ LiftM :: m (Peer role' ps r m ia st') -> Peer role' ps r m ia st+ 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+ Await+ :: ( SingI recv+ , SingI from+ , SingToInt ps+ )+ => (Recv role' ps recv from ~> Peer role' ps recv m ia)+ -> Peer role' ps recv m ia from++instance (Functor m) => IMonadFail (Peer role' ps r m) where+ fail = error++instance (Functor m) => IFunctor (Peer role' ps r m) where+ imap f = \case+ IReturn ia -> IReturn (f ia)+ LiftM f' -> LiftM (fmap (imap f) f')+ Yield ms cont -> Yield ms (imap f cont)+ Await cont -> Await (imap f . cont)++instance (Functor m) => IMonad (Peer role' ps r m) where+ ireturn = IReturn+ ibind f = \case+ IReturn ia -> (f ia)+ LiftM f' -> LiftM (fmap (ibind f) f')+ Yield ms cont -> Yield ms (ibind f cont)+ Await cont -> Await (ibind f . cont)++{- |+Send a message, the Peer status changes from `from` to `sps`.+-}+yield+ :: ( Functor m+ , SingI recv+ , SingI from+ , SingToInt ps+ )+ => Msg role' ps from '(send, sps) '(recv, rps)+ -> Peer role' ps send m (At () sps) from+yield msg = Yield msg (returnAt ())++{- |+Receiving Messages.+-}+await+ :: ( Functor m+ , SingI recv+ , SingI from+ , SingToInt ps+ )+ => Peer role' ps recv m (Recv role' ps recv from) from+await = Await ireturn++{- |+Lift any m to Peer role' ps r m, which is an application of LiftM. +Note that the state of `ts` has not changed.+-}+liftm :: (Functor m) => m a -> Peer role' ps r m (At a ts) ts+liftm m = LiftM (returnAt <$> m)
+ src/TypedProtocol/Driver.hs view
@@ -0,0 +1,216 @@+-- This part of the code comes from typed-protocols, I modified a few things.+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++{- |+Schematic diagram of the communication structure of three roles through typed-session:+++Some explanations for this diagram:++1. Roles are connected through channels, and there are many types of channels, such as channels established through TCP or channels established through TMVar.++2. Each role has a Peer thread, in which the Peer runs.++3. Each role has one or more decode threads, and the decoded Msgs are placed in the MsgCache.++4. SendMap aggregates the send functions of multiple Channels together.+When sending a message, the send function of the receiver is searched from SendMap.+-}+module TypedProtocol.Driver where++import Control.Concurrent.Class.MonadSTM+import Control.Monad.Class.MonadThrow (MonadThrow, throwIO)+import Data.IFunctor (At (..), Sing, SingI (sing))+import qualified Data.IFunctor as I+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import GHC.Exception (Exception)+import TypedProtocol.Codec+import TypedProtocol.Core+import Unsafe.Coerce (unsafeCoerce)++{- |+Contains two functions sendMsg, recvMsg.+runPeerWithDriver uses them to send and receive Msg.+-}+data Driver role' ps m+ = Driver+ { sendMsg+ :: forall (send :: role') (recv :: role') (st :: ps) (st' :: ps) (st'' :: ps)+ . ( SingI recv+ , SingI st+ , SingToInt ps+ , SingToInt role'+ )+ => Sing recv+ -> Msg role' ps st '(send, st') '(recv, st'')+ -> m ()+ , recvMsg+ :: forall (st' :: ps)+ . (SingToInt ps)+ => Sing st'+ -> m (AnyMsg role' ps)+ }++{- |+Interpret Peer.+-}+runPeerWithDriver+ :: forall role' ps (r :: role') (st :: ps) m a+ . ( Monad m+ , (SingToInt role')+ )+ => Driver role' ps m+ -> Peer role' ps r m (At a (Done r)) st+ -> m a+runPeerWithDriver Driver{sendMsg, recvMsg} =+ go+ where+ go+ :: forall st'+ . Peer role' ps r m (At a (Done r)) st'+ -> m a+ go (IReturn (At a)) = pure a+ go (LiftM k) = k >>= go+ go (Yield (msg :: Msg role' ps (st' :: ps) '(r, sps) '(recv :: role', rps)) k) = do+ sendMsg (sing @recv) msg+ go k+ go (Await (k :: (Recv role' ps r st' I.~> Peer role' ps r m ia))) = do+ AnyMsg msg <- recvMsg (sing @st')+ go (k $ unsafeCoerce (Recv msg))++{- |+A wrapper around AnyMsg that represents sending and receiving Msg.+-}+data TraceSendRecv role' ps where+ TraceSendMsg :: AnyMsg role' ps -> TraceSendRecv role' ps+ TraceRecvMsg :: AnyMsg role' ps -> TraceSendRecv role' ps++instance (Show (AnyMsg role' ps)) => Show (TraceSendRecv role' ps) where+ show (TraceSendMsg msg) = "Send " ++ show msg+ show (TraceRecvMsg msg) = "Recv " ++ show msg++{- |+Similar to the log function, used to print received or sent messages.+-}+type Tracer role' ps m = TraceSendRecv role' ps -> m ()++{- |+The default trace function. It simply ignores everything.+-}+nullTracer :: (Monad m) => a -> m ()+nullTracer _ = pure ()++{- |+SendMap aggregates the send functions of multiple Channels together.+When sending a message, the send function of the receiver is found from SendMap.+-}+type SendMap role' m bytes = IntMap (bytes -> m ())++{- |++Build Driver through SendMap and MsgCache.+Here we need some help from other functions:++1. `Tracer role' ps n` is similar to the log function, used to print received or sent messages.+2. `Encode role' ps` bytes encoding function, converts Msg into bytes.+3. `forall a. n a -> m a` This is a bit complicated, I will explain it in detail below.++I see Peer as three layers:++1. `Peer` 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.+2. `m` middle layer, describes the business requirements in this layer, and converts the received Msg into specific business actions.+3. `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.+-}+driverSimple+ :: forall role' ps bytes m n+ . ( Monad m+ , Monad n+ , MonadSTM n+ )+ => Tracer role' ps n+ -> Encode role' ps bytes+ -> SendMap role' n bytes+ -> TVar n (MsgCache role' ps)+ -> (forall a. n a -> m a)+ -> Driver role' ps m+driverSimple tracer Encode{encode} sendMap tvar liftFun =+ Driver{sendMsg, recvMsg}+ where+ sendMsg+ :: forall (send :: role') (recv :: role') (from :: ps) (st :: ps) (st1 :: ps)+ . ( SingI recv+ , SingI from+ , SingToInt ps+ , SingToInt role'+ )+ => Sing recv+ -> Msg role' ps from '(send, st) '(recv, st1)+ -> m ()+ sendMsg role msg = liftFun $ do+ case IntMap.lookup (singToInt role) sendMap of+ Nothing -> error "np"+ Just sendFun -> sendFun (encode msg)+ tracer (TraceSendMsg (AnyMsg msg))++ recvMsg+ :: forall (st' :: ps)+ . (SingToInt ps)+ => Sing st'+ -> m (AnyMsg role' ps)+ recvMsg sst' = do+ let singInt = singToInt sst'+ liftFun $ do+ anyMsg <- atomically $ do+ agencyMsg <- readTVar tvar+ case IntMap.lookup singInt agencyMsg of+ Nothing -> retry+ Just v -> do+ writeTVar tvar (IntMap.delete singInt agencyMsg)+ pure v+ tracer (TraceRecvMsg (anyMsg))+ pure anyMsg++{- |+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.+-}+decodeLoop+ :: (Exception failure, MonadSTM n, MonadThrow n)+ => Tracer role' ps n+ -> Maybe bytes+ -> Decode role' ps failure bytes+ -> Channel n bytes+ -> TVar n (MsgCache role' ps)+ -> n ()+decodeLoop tracer mbt d@Decode{decode} channel tvar = do+ result <- runDecoderWithChannel channel mbt decode+ case result of+ Right (AnyMsg msg, mbt') -> do+ let agencyInt = singToInt $ msgFromStSing msg+ atomically $ do+ agencyMsg <- readTVar tvar+ case IntMap.lookup agencyInt agencyMsg of+ Nothing -> writeTVar tvar (IntMap.insert agencyInt (AnyMsg msg) agencyMsg)+ Just _v -> retry+ decodeLoop tracer mbt' d channel tvar+ Left failure -> throwIO failure
+ test/Book.hs view
@@ -0,0 +1,231 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module Book where++import Control.Concurrent.Class.MonadSTM+import Control.Monad+import Control.Monad.Class.MonadFork (MonadFork, forkIO)+import Control.Monad.Class.MonadSay+import Control.Monad.Class.MonadThrow (MonadThrow)+import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)+import qualified Data.IFunctor as I+import qualified Data.IntMap as IntMap+import Data.Kind+import GHC.Exts (dataToTag#)+import GHC.Int (Int (I#))+import TypedProtocol.Codec+import TypedProtocol.Core+import TypedProtocol.Driver++{-++--------------------------------------------------------------------------+ Buyer Seller+ :S0 :S0+ < Title String -> >+ :S1 :S1+ < <- Price Int >+ :S12 s :S12 s++ ---------------------------------------------------------------------+ |:S12 EnoughBudget :S12 s+ | < Afford -> >+ |:S3 :S3+ | < <- Data Int >+ |:End :End+ ---------------------------------------------------------------------++ ---------------------------------------------------------------------+ |:S12 NotEnoughBuget :S12 s+ | < NotBuy -> >+ |:End :End+ ---------------------------------------------------------------------+ -}++data Role = Buyer | Seller+ deriving (Show, Eq, Ord)++data SRole :: Role -> Type where+ SBuyer :: SRole Buyer+ SSeller :: SRole Seller++type instance Sing = SRole++instance SingI Buyer where+ sing = SBuyer++instance SingI Seller where+ sing = SSeller++data BudgetSt+ = EnoughBudget+ | NotEnoughBuget++data BookSt+ = S0+ | S1+ | S12 BudgetSt+ | S3+ | End++data SBookSt :: BookSt -> Type where+ SS0 :: SBookSt S0+ SS1 :: SBookSt S1+ SS12 :: SBookSt (S12 (s :: BudgetSt))+ SS3 :: SBookSt S3+ SEnd :: SBookSt End++type instance Sing = SBookSt++instance SingI S0 where+ sing = SS0++instance SingI S1 where+ sing = SS1++instance SingI (S12 s) where+ sing = SS12++instance SingI S3 where+ sing = SS3++instance SingI End where+ sing = SEnd++type Date = Int++instance SingToInt Role where+ singToInt x = I# (dataToTag# x)++instance SingToInt BookSt where+ singToInt x = I# (dataToTag# x)++instance Protocol Role BookSt where+ type Done Buyer = End+ type Done Seller = 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, S12 s)+ 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)++encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)+encodeMsg = Encode $ \x -> case x of+ Title{} -> AnyMsg x+ Price{} -> AnyMsg x+ Afford{} -> AnyMsg x+ Date{} -> AnyMsg x+ NotBuy{} -> AnyMsg x++decodeMsg+ :: DecodeStep+ (AnyMsg Role BookSt)+ CodecFailure+ (AnyMsg Role BookSt)+decodeMsg =+ DecodePartial $ \case+ Nothing -> DecodeFail (CodecFailure "expected more data")+ Just anyMsg -> DecodeDone anyMsg Nothing++budget :: Int+budget = 100++data CheckPriceResult :: BookSt -> Type where+ Yes :: CheckPriceResult (S12 EnoughBudget)+ No :: CheckPriceResult (S12 NotEnoughBuget)++checkPrice :: (Monad m) => Int -> Peer Role BookSt Buyer m CheckPriceResult (S12 s)+checkPrice i =+ if i <= budget+ then LiftM $ pure (ireturn Yes)+ else LiftM $ pure (ireturn No)++buyerPeer+ :: (Monad m) => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0+buyerPeer = I.do+ yield (Title "haskell book")+ Recv (Price i) <- await+ res <- checkPrice i+ case res of+ Yes -> I.do+ yield Afford+ Recv (Date d) <- await+ returnAt (Just d)+ No -> I.do+ yield NotBuy+ returnAt Nothing++sellerPeer :: (Functor m) => Peer Role BookSt Seller m (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 ()++mvarsAsChannel+ :: (MonadSTM m)+ => TMVar m a+ -> TMVar m a+ -> Channel m a+mvarsAsChannel bufferRead bufferWrite =+ Channel{send, recv}+ where+ send x = atomically (putTMVar bufferWrite x)+ recv = atomically (Just <$> takeTMVar bufferRead)++myTracer :: (MonadSay m) => String -> Tracer Role BookSt m+myTracer st v = say (st <> show v)++instance Show (AnyMsg Role BookSt) where+ show (AnyMsg msg) = case msg of+ Title st -> "Title " <> show st+ Price i -> "Price " <> show i+ Afford -> "Afford"+ Date i -> "Date " <> show i+ NotBuy -> "NotBuy"++runAll :: forall m. (Monad m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()+runAll = do+ buyerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)+ sellerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)+ let buyerChannel = mvarsAsChannel @m buyerTMVar sellerTMVar+ sellerChannel = mvarsAsChannel @m sellerTMVar buyerTMVar+ sendFun bufferWrite x = atomically (putTMVar bufferWrite x)+ sendToRole =+ IntMap.fromList+ [ (singToInt SSeller, sendFun sellerTMVar)+ , (singToInt SBuyer, sendFun buyerTMVar)+ ]+ buyerTvar <- newTVarIO IntMap.empty+ sellerTvar <- newTVarIO IntMap.empty+ let buyerDriver = driverSimple (myTracer "buyer") encodeMsg sendToRole buyerTvar id+ sellerDriver = driverSimple (myTracer "seller") encodeMsg sendToRole sellerTvar id+ -- fork buyer decode thread, seller -> buyer+ forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerChannel buyerTvar+ -- fork seller decode thread, buyer -> seller+ forkIO $ decodeLoop (myTracer "seller") Nothing (Decode decodeMsg) sellerChannel sellerTvar+ -- fork seller Peer thread+ forkIO $ void $ runPeerWithDriver sellerDriver sellerPeer+ -- run buyer Peer+ void $ runPeerWithDriver buyerDriver buyerPeer
+ test/Book1.hs view
@@ -0,0 +1,280 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module Book1 where++import Control.Concurrent.Class.MonadSTM+import Control.Monad+import Control.Monad.Class.MonadFork (MonadFork, forkIO)+import Control.Monad.Class.MonadSay+import Control.Monad.Class.MonadThrow (MonadThrow)+import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)+import qualified Data.IFunctor as I+import qualified Data.IntMap as IntMap+import Data.Kind+import GHC.Exts (dataToTag#)+import GHC.Int (Int (I#))+import TypedProtocol.Codec+import TypedProtocol.Core+import TypedProtocol.Driver++{-++-----------------------------------------------------------------------------------------------+ Buyer Seller Buyer2+ :S0 :S0+ < Title String -> >+ :S1 :S1+ < <- Price Int >+ :S11 :S12 s :S11+ < PriceToBuyer2 Int -> >+ :S110 :S110+ < <- HalfPrice Int >+ :S12 s :End++ ---------------------------------------------------------------------+ |:S12 EnoughBudget :S12 s+ | < Afford -> >+ |:S3 :S3+ | < <- Data Int >+ |:End :End+ ---------------------------------------------------------------------++ ---------------------------------------------------------------------+ |:S12 NotEnoughBuget :S12+ | < NotBuy -> >+ |:End :End+ ---------------------------------------------------------------------+-}++data Role = Buyer | Seller | Buyer2+ deriving (Show, Eq, Ord)++data SRole :: Role -> Type where+ SBuyer :: SRole Buyer+ SBuyer2 :: SRole Buyer2+ SSeller :: SRole Seller++type instance Sing = SRole++instance SingI Buyer where+ sing = SBuyer++instance SingI Buyer2 where+ sing = SBuyer2++instance SingI Seller where+ sing = SSeller++data BudgetSt+ = EnoughBudget+ | NotEnoughBuget++data BookSt+ = S0+ | S1+ | S11+ | S110+ | S12 BudgetSt+ | S3+ | End++data SBookSt :: BookSt -> Type where+ SS0 :: SBookSt S0+ SS1 :: SBookSt S1+ SS11 :: SBookSt S11+ SS110 :: SBookSt S110+ SS12 :: SBookSt (S12 (s :: BudgetSt))+ SS3 :: SBookSt S3+ SEnd :: SBookSt End++type instance Sing = SBookSt++instance SingI S0 where+ sing = SS0++instance SingI S1 where+ sing = SS1++instance SingI S11 where+ sing = SS11++instance SingI S110 where+ sing = SS110++instance SingI (S12 s) where+ sing = SS12++instance SingI S3 where+ sing = SS3++instance SingI End where+ sing = SEnd++type Date = Int++instance SingToInt Role where+ singToInt x = I# (dataToTag# x)++instance SingToInt BookSt where+ singToInt x = I# (dataToTag# x)++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 s)+ 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)++encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)+encodeMsg = Encode $ \x -> case x of+ Title{} -> AnyMsg x+ Price{} -> AnyMsg x+ PriceToB2{} -> AnyMsg x+ HalfPrice{} -> AnyMsg x+ Afford{} -> AnyMsg x+ Date{} -> AnyMsg x+ NotBuy{} -> AnyMsg x++decodeMsg+ :: DecodeStep+ (AnyMsg Role BookSt)+ CodecFailure+ (AnyMsg Role BookSt)+decodeMsg =+ DecodePartial $ \case+ Nothing -> DecodeFail (CodecFailure "expected more data")+ Just anyMsg -> DecodeDone anyMsg Nothing++budget :: Int+budget = 16++data CheckPriceResult :: BookSt -> Type where+ Yes :: CheckPriceResult (S12 EnoughBudget)+ No :: CheckPriceResult (S12 NotEnoughBuget)++checkPrice :: (Monad m) => Int -> Int -> Peer Role BookSt Buyer m CheckPriceResult (S12 s)+checkPrice i h =+ if i <= budget + h+ then LiftM $ pure (ireturn Yes)+ else LiftM $ pure (ireturn No)++buyerPeer+ :: (Monad m) => Peer Role BookSt Buyer m (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++buyer2Peer+ :: (Monad m) => Peer Role BookSt Buyer2 m (At () (Done Buyer2)) S11+buyer2Peer = I.do+ Recv (PriceToB2 i) <- await+ yield (HalfPrice (i `div` 2))++sellerPeer :: (Monad m) => Peer Role BookSt Seller m (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 ()++mvarsAsChannel+ :: (MonadSTM m)+ => TMVar m a+ -> TMVar m a+ -> Channel m a+mvarsAsChannel bufferRead bufferWrite =+ Channel{send, recv}+ where+ send x = atomically (putTMVar bufferWrite x)+ recv = atomically (Just <$> takeTMVar bufferRead)++myTracer :: (MonadSay m) => String -> Tracer Role BookSt m+myTracer st v = say (st <> show v)++instance Show (AnyMsg Role BookSt) where+ show (AnyMsg msg) = case msg of+ Title st -> "Title " <> show st+ Price i -> "Price " <> show i+ PriceToB2 i -> "PriceToB2 " <> show i+ HalfPrice i -> "HalfPrice " <> show i+ Afford -> "Afford"+ Date i -> "Date " <> show i+ NotBuy -> "NotBuy"++runAll :: forall m. (Monad m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()+runAll = do+ buyerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)+ buyer2TMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)+ sellerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)+ let buyerSellerChannel = mvarsAsChannel @m buyerTMVar sellerTMVar+ buyerBuyer2Channel = mvarsAsChannel @m buyerTMVar buyer2TMVar++ sellerBuyerChannel = mvarsAsChannel @m sellerTMVar buyerTMVar++ buyer2BuyerChannel = mvarsAsChannel @m buyer2TMVar buyerTMVar++ sendFun bufferWrite x = atomically (putTMVar bufferWrite x)+ sendToRole =+ IntMap.fromList+ [ (singToInt SSeller, sendFun sellerTMVar)+ , (singToInt SBuyer, sendFun buyerTMVar)+ , (singToInt SBuyer2, sendFun buyer2TMVar)+ ]+ buyerTvar <- newTVarIO IntMap.empty+ buyer2Tvar <- newTVarIO IntMap.empty+ sellerTvar <- newTVarIO IntMap.empty+ let buyerDriver = driverSimple (myTracer "buyer") encodeMsg sendToRole buyerTvar id+ buyer2Driver = driverSimple (myTracer "buyer2") encodeMsg sendToRole buyer2Tvar id+ sellerDriver = driverSimple (myTracer "seller") encodeMsg sendToRole sellerTvar id+ -- fork buyer decode thread, seller -> buyer+ forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerSellerChannel buyerTvar+ -- fork buyer decode thread, buyer2 -> buyer+ forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerBuyer2Channel buyerTvar++ -- fork seller decode thread, buyer -> seller+ forkIO $ decodeLoop (myTracer "seller") Nothing (Decode decodeMsg) sellerBuyerChannel sellerTvar++ -- fork buyer2 decode thread, buyer -> buyer2+ forkIO $ decodeLoop (myTracer "buyer2") Nothing (Decode decodeMsg) buyer2BuyerChannel buyer2Tvar++ -- fork seller Peer thread+ forkIO $ void $ runPeerWithDriver sellerDriver sellerPeer++ -- fork buyer2 Peer thread+ forkIO $ void $ runPeerWithDriver buyer2Driver buyer2Peer+ -- run buyer Peer+ void $ runPeerWithDriver buyerDriver buyerPeer
+ test/Book2.hs view
@@ -0,0 +1,341 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module Book2 where++import Control.Concurrent.Class.MonadSTM+import Control.Monad+import Control.Monad.Class.MonadFork (MonadFork, forkIO)+import Control.Monad.Class.MonadSay+import Control.Monad.Class.MonadThrow (MonadThrow)+import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)+import qualified Data.IFunctor as I+import qualified Data.IntMap as IntMap+import Data.Kind+import GHC.Exts (dataToTag#)+import GHC.Int (Int (I#))+import TypedProtocol.Codec+import TypedProtocol.Core+import TypedProtocol.Driver++{-++-----------------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+-}++data Role = Buyer | Seller | Buyer2+ deriving (Show, Eq, Ord)++data SRole :: Role -> Type where+ SBuyer :: SRole Buyer+ SBuyer2 :: SRole Buyer2+ SSeller :: SRole Seller++type instance Sing = SRole++instance SingI Buyer where+ sing = SBuyer++instance SingI Buyer2 where+ sing = SBuyer2++instance SingI Seller where+ sing = SSeller++data FindBook+ = BookNotFound+ | BookFound++data BudgetSt+ = EnoughBudget+ | NotEnoughBuget++data BookSt+ = S0+ | S1 FindBook+ | S2 FindBook+ | S3 BudgetSt+ | S4+ | S5 BudgetSt+ | S6+ | End++data SBookSt :: BookSt -> Type where+ SS0 :: SBookSt S0+ SS1 :: SBookSt (S1 (s :: FindBook))+ SS2 :: SBookSt (S2 (s :: FindBook))+ SS3 :: SBookSt (S3 (s :: BudgetSt))+ SS4 :: SBookSt S4+ SS5 :: SBookSt (S5 (s :: BudgetSt))+ SS6 :: SBookSt S6+ SEnd :: SBookSt End++type instance Sing = SBookSt++instance SingI S0 where+ sing = SS0++instance SingI (S1 s) where+ sing = SS1++instance SingI (S2 s) where+ sing = SS2++instance SingI (S3 s) where+ sing = SS3++instance SingI S4 where+ sing = SS4++instance SingI (S5 s) where+ sing = SS5++instance SingI S6 where+ sing = SS6++instance SingI End where+ sing = SEnd++type Date = Int++instance SingToInt Role where+ singToInt x = I# (dataToTag# x)++instance SingToInt BookSt where+ singToInt x = I# (dataToTag# x)++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, S2 s) '(Seller, S2 s)+ Price :: Int -> Msg Role BookSt (S2 BookFound) '(Seller, S3 s) '(Buyer, S1 BookFound)+ PriceToB2 :: Int -> Msg Role BookSt (S1 BookFound) '(Buyer, S4) '(Buyer2, S4)+ HalfPrice :: Int -> Msg Role BookSt S4 '(Buyer2, S5 s) '(Buyer, S3 s)+ Afford :: Msg Role BookSt (S3 EnoughBudget) '(Buyer, S6) '(Seller, S6)+ Date :: Date -> Msg Role BookSt S6 '(Seller, End) '(Buyer, S5 EnoughBudget)+ Success :: Int -> Msg Role BookSt (S5 EnoughBudget) '(Buyer, End) '(Buyer2, End)+ NotBuy :: Msg Role BookSt (S3 NotEnoughBuget) '(Buyer, S5 NotEnoughBuget) '(Seller, End)+ Failed :: Msg Role BookSt (S5 NotEnoughBuget) '(Buyer, End) '(Buyer2, End)+ BookNotFoun :: Msg Role BookSt (S2 BookNotFound) '(Seller, End) '(Buyer, S1 BookNotFound)+ SellerNotFoundBook :: Msg Role BookSt (S1 BookNotFound) '(Buyer, End) '(Buyer2, End)++encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)+encodeMsg = Encode $ \x -> case x of+ Title{} -> AnyMsg x+ Price{} -> AnyMsg x+ PriceToB2{} -> AnyMsg x+ HalfPrice{} -> AnyMsg x+ Afford{} -> AnyMsg x+ Date{} -> AnyMsg x+ Success{} -> AnyMsg x+ NotBuy{} -> AnyMsg x+ Failed{} -> AnyMsg x+ BookNotFoun{} -> AnyMsg x+ SellerNotFoundBook{} -> AnyMsg x++decodeMsg+ :: DecodeStep+ (AnyMsg Role BookSt)+ CodecFailure+ (AnyMsg Role BookSt)+decodeMsg =+ DecodePartial $ \case+ Nothing -> DecodeFail (CodecFailure "expected more data")+ Just anyMsg -> DecodeDone anyMsg Nothing++budget :: Int+budget = 16++data CheckPriceResult :: BookSt -> Type where+ Yes :: CheckPriceResult (S3 EnoughBudget)+ No :: CheckPriceResult (S3 NotEnoughBuget)++checkPrice :: (Monad m) => Int -> Int -> Peer Role BookSt Buyer m CheckPriceResult (S3 s)+checkPrice i h =+ if i <= budget + h+ then LiftM $ pure (ireturn Yes)+ else LiftM $ pure (ireturn No)++buyerPeer+ :: (Monad m) => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0+buyerPeer = I.do+ yield (Title "haskell book")+ Recv msg <- await+ case msg of+ BookNotFoun -> I.do+ yield SellerNotFoundBook+ returnAt Nothing+ Price i -> I.do+ yield (PriceToB2 i)+ Recv (HalfPrice hv) <- await+ res <- checkPrice i hv+ case res of+ Yes -> I.do+ yield Afford+ Recv (Date d) <- await+ yield (Success d)+ returnAt (Just d)+ No -> I.do+ yield NotBuy+ yield Failed+ returnAt Nothing++buyer2Peer+ :: (Monad m) => Peer Role BookSt Buyer2 m (At () (Done Buyer2)) (S1 s)+buyer2Peer = I.do+ Recv msg' <- await+ case msg' of+ SellerNotFoundBook -> returnAt ()+ PriceToB2 i -> I.do+ yield (HalfPrice (i `div` 2))+ Recv msg <- await+ case msg of+ Success _ -> returnAt ()+ Failed -> returnAt ()++data FindBookResult :: BookSt -> Type where+ Found :: FindBookResult (S2 BookFound)+ NotFound :: FindBookResult (S2 BookNotFound)++findBook :: (Monad m) => String -> Peer Role BookSt Seller m FindBookResult (S2 s)+findBook st =+ if st /= ""+ then LiftM $ pure (ireturn Found)+ else LiftM $ pure (ireturn NotFound)++sellerPeer :: (Monad m) => Peer Role BookSt Seller m (At () (Done Seller)) S0+sellerPeer = I.do+ Recv (Title name) <- await+ res <- findBook name+ case res of+ Found -> I.do+ yield (Price 30)+ Recv msg <- await+ case msg of+ Afford -> yield (Date 100)+ NotBuy -> returnAt ()+ NotFound -> yield BookNotFoun++mvarsAsChannel+ :: (MonadSTM m)+ => TMVar m a+ -> TMVar m a+ -> Channel m a+mvarsAsChannel bufferRead bufferWrite =+ Channel{send, recv}+ where+ send x = atomically (putTMVar bufferWrite x)+ recv = atomically (Just <$> takeTMVar bufferRead)++myTracer :: (MonadSay m) => String -> Tracer Role BookSt m+myTracer st v = say (st <> show v)++instance Show (AnyMsg Role BookSt) where+ show (AnyMsg msg) = case msg of+ Title st -> "Title " <> show st+ Price i -> "Price " <> show i+ PriceToB2 i -> "PriceToB2 " <> show i+ HalfPrice i -> "HalfPrice " <> show i+ Afford -> "Afford"+ Date i -> "Date " <> show i+ NotBuy -> "NotBuy"+ Success i -> "Success " <> show i+ Failed -> "Failed"+ BookNotFoun -> "BookNotFound"+ SellerNotFoundBook -> "SellerNotFoundBook"++runAll :: forall m. (Monad m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()+runAll = do+ buyerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)+ buyer2TMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)+ sellerTMVar <- newEmptyTMVarIO @m @(AnyMsg Role BookSt)+ let buyerSellerChannel = mvarsAsChannel @m buyerTMVar sellerTMVar+ buyerBuyer2Channel = mvarsAsChannel @m buyerTMVar buyer2TMVar++ sellerBuyerChannel = mvarsAsChannel @m sellerTMVar buyerTMVar++ buyer2BuyerChannel = mvarsAsChannel @m buyer2TMVar buyerTMVar++ sendFun bufferWrite x = atomically (putTMVar bufferWrite x)+ sendToRole =+ IntMap.fromList+ [ (singToInt SSeller, sendFun sellerTMVar)+ , (singToInt SBuyer, sendFun buyerTMVar)+ , (singToInt SBuyer2, sendFun buyer2TMVar)+ ]+ buyerTvar <- newTVarIO IntMap.empty+ buyer2Tvar <- newTVarIO IntMap.empty+ sellerTvar <- newTVarIO IntMap.empty+ let buyerDriver = driverSimple (myTracer "buyer") encodeMsg sendToRole buyerTvar id+ buyer2Driver = driverSimple (myTracer "buyer2") encodeMsg sendToRole buyer2Tvar id+ sellerDriver = driverSimple (myTracer "seller") encodeMsg sendToRole sellerTvar id+ -- fork buyer decode thread, seller -> buyer+ forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerSellerChannel buyerTvar+ -- fork buyer decode thread, buyer2 -> buyer+ forkIO $ decodeLoop (myTracer "buyer") Nothing (Decode decodeMsg) buyerBuyer2Channel buyerTvar++ -- fork seller decode thread, buyer -> seller+ forkIO $ decodeLoop (myTracer "seller") Nothing (Decode decodeMsg) sellerBuyerChannel sellerTvar++ -- fork buyer2 decode thread, buyer -> buyer2+ forkIO $ decodeLoop (myTracer "buyer2") Nothing (Decode decodeMsg) buyer2BuyerChannel buyer2Tvar++ -- fork seller Peer thread+ forkIO $ void $ runPeerWithDriver sellerDriver sellerPeer++ -- fork buyer2 Peer thread+ forkIO $ void $ runPeerWithDriver buyer2Driver buyer2Peer+ -- run buyer Peer+ void $ runPeerWithDriver buyerDriver buyerPeer
+ test/Book3/Main.hs view
@@ -0,0 +1,118 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module Book3.Main where++import Book3.Peer+import Book3.Type+import Control.Carrier.Random.Gen (runRandom)+import Control.Concurrent.Class.MonadSTM+import Control.Effect.Labelled (runLabelledLift, sendM)+import Control.Monad+import Control.Monad.Class.MonadFork (MonadFork, forkIO)+import Control.Monad.Class.MonadSay+import Control.Monad.Class.MonadThrow (MonadThrow)+import qualified Data.IntMap as IntMap+import System.Random (StdGen, split)+import TypedProtocol.Codec+import TypedProtocol.Core+import TypedProtocol.Driver+import Control.Monad.IOSim++mvarsAsChannel+ :: (MonadSTM m)+ => TMVar m a+ -> TMVar m a+ -> Channel m a+mvarsAsChannel bufferRead bufferWrite =+ Channel{send, recv}+ where+ send x = atomically (putTMVar bufferWrite x)+ recv = atomically (Just <$> takeTMVar bufferRead)++myTracer :: (MonadSay m) => String -> Tracer Role BookSt m+myTracer st v = say (st <> show v)++runAll+ :: forall n+ . ( Monad n+ , MonadSTM n+ , MonadSay n+ , MonadThrow n+ , MonadFork n+ )+ => StdGen+ -> n ()+runAll g = do+ buyerTMVar <- newEmptyTMVarIO @n @(AnyMsg Role BookSt)+ buyer2TMVar <- newEmptyTMVarIO @n @(AnyMsg Role BookSt)+ sellerTMVar <- newEmptyTMVarIO @n @(AnyMsg Role BookSt)+ let buyerSellerChannel = mvarsAsChannel @n buyerTMVar sellerTMVar+ buyerBuyer2Channel = mvarsAsChannel @n buyerTMVar buyer2TMVar++ sellerBuyerChannel = mvarsAsChannel @n sellerTMVar buyerTMVar++ buyer2BuyerChannel = mvarsAsChannel @n buyer2TMVar buyerTMVar++ sendFun bufferWrite x = atomically @n (putTMVar bufferWrite x)+ sendToRole =+ IntMap.fromList+ [ (singToInt SSeller, sendFun sellerTMVar)+ , (singToInt SBuyer, sendFun buyerTMVar)+ , (singToInt SBuyer2, sendFun buyer2TMVar)+ ]+ buyerTvar <- newTVarIO IntMap.empty+ buyer2Tvar <- newTVarIO IntMap.empty+ sellerTvar <- newTVarIO IntMap.empty+ let buyerDriver = driverSimple (myTracer "buyer :") encodeMsg sendToRole buyerTvar sendM+ buyer2Driver = driverSimple (myTracer "buyer2 :") encodeMsg sendToRole buyer2Tvar sendM+ sellerDriver = driverSimple (myTracer "seller :") encodeMsg sendToRole sellerTvar sendM+ -- fork buyer decode thread, seller -> buyer+ forkIO $ decodeLoop (myTracer "buyer :") Nothing (Decode decodeMsg) buyerSellerChannel buyerTvar+ -- fork buyer decode thread, buyer2 -> buyer+ forkIO $ decodeLoop (myTracer "buyer :") Nothing (Decode decodeMsg) buyerBuyer2Channel buyerTvar++ -- fork seller decode thread, buyer -> seller+ forkIO $ decodeLoop (myTracer "seller :") Nothing (Decode decodeMsg) sellerBuyerChannel sellerTvar++ -- fork buyer2 decode thread, buyer -> buyer2+ forkIO $ decodeLoop (myTracer "buyer2 :") Nothing (Decode decodeMsg) buyer2BuyerChannel buyer2Tvar++ let (g0, g1) = split g+ (g2, g3) = split g0++ resultTMVar1 <- newEmptyTMVarIO+ resultTMVar2 <- newEmptyTMVarIO++ -- fork seller Peer thread+ forkIO $ do+ runLabelledLift $ runRandom g1 $ runPeerWithDriver sellerDriver sellerPeer+ atomically $ writeTMVar resultTMVar1 ()++ -- fork buyer2 Peer thread+ forkIO $ do+ runLabelledLift $ runRandom g2 $ runPeerWithDriver buyer2Driver buyer2Peer+ atomically $ writeTMVar resultTMVar2 ()++ -- run buyer Peer+ void $ runLabelledLift $ runRandom g3 $ runPeerWithDriver buyerDriver buyerPeer++ -- wait seller, buyer+ atomically $ do+ takeTMVar resultTMVar1+ takeTMVar resultTMVar2++book3Prop :: StdGen -> Either Failure ()+book3Prop v = runSim (runAll v)
+ test/Book3/Peer.hs view
@@ -0,0 +1,159 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}++module Book3.Peer where++import Book3.Type+import Control.Algebra (Has)+import Control.Effect.Random (Random, uniform)+import Data.IFunctor (At (..), ireturn, returnAt)+import qualified Data.IFunctor as I+import Data.Kind+import TypedProtocol.Core++budget :: Int+budget = 16++data CheckPriceResult :: BookSt -> Type where+ Yes :: CheckPriceResult (S3 [Enough, Support, Two, Found])+ No :: CheckPriceResult (S3 [NotEnough, Support, Two, Found])++checkPrice+ :: (Has Random sig m)+ => Int+ -> Int+ -> Peer Role BookSt Buyer m CheckPriceResult (S3 s)+checkPrice _i _h = I.do+ At b <- liftm $ uniform @Bool+ if b+ then LiftM $ pure (ireturn Yes)+ else LiftM $ pure (ireturn No)++data OT :: BookSt -> Type where+ OTOne :: OT (S1 [One, Found])+ OTTwo :: OT (S1 [Two, Found])++choiceOT+ :: (Has Random sig m)+ => Int+ -> Peer Role BookSt Buyer m OT (S1 s)+choiceOT _i = I.do+ At b <- liftm $ uniform @Bool+ if b+ then LiftM $ pure $ ireturn OTOne+ else LiftM $ pure $ ireturn OTTwo++buyerPeer+ :: (Has Random sig m)+ => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0+buyerPeer = I.do+ yield (Title "haskell book")+ await I.>>= \case+ Recv NoBook -> I.do+ yield SellerNoBook+ returnAt Nothing+ Recv (Price i) -> I.do+ choiceOT i I.>>= \case+ OTOne -> I.do+ yield OneAfford+ yield OneAccept+ Recv (OneDate d) <- await+ yield (OneSuccess d)+ returnAt $ Just d+ OTTwo -> f1+ where+ f1+ :: (Has Random sig m)+ => Peer Role BookSt 'Buyer m (At (Maybe Date) (Done Buyer)) ('S1 '[ 'Two, 'Found])+ f1 = I.do+ yield (PriceToBuyer2 300)+ await I.>>= \case+ Recv NotSupport1 -> I.do+ yield TwoNotBuy+ returnAt Nothing+ Recv (SupportVal h) -> I.do+ checkPrice 10 h I.>>= \case+ Yes -> I.do+ yield TwoAccept+ Recv (TwoDate d) <- await+ yield (TwoSuccess d)+ returnAt (Just d)+ No -> I.do+ yield TwoNotBuy1+ yield TwoFailed+ returnAt Nothing++data BuySupp :: BookSt -> Type where+ BNS :: BuySupp (S6 '[NotSupport, Two, Found])+ BS :: BuySupp (S6 '[Support, Two, Found])++choiceB+ :: (Has Random sig m)+ => Int+ -> Peer Role BookSt Buyer2 m BuySupp (S6 s)+choiceB _i = I.do+ At b <- liftm $ uniform @Bool+ if b+ then LiftM $ pure $ ireturn BNS+ else LiftM $ pure $ ireturn BS++buyer2Peer+ :: (Has Random sig m)+ => Peer Role BookSt Buyer2 m (At (Maybe Date) (Done Buyer2)) (S1 s)+buyer2Peer = I.do+ await I.>>= \case+ Recv SellerNoBook -> returnAt Nothing+ Recv OneAfford -> I.do+ Recv (OneSuccess d) <- await+ returnAt (Just d)+ Recv (PriceToBuyer2 i) -> I.do+ choiceB i I.>>= \case+ BNS -> I.do+ yield NotSupport1+ returnAt Nothing+ BS -> I.do+ yield (SupportVal (i `div` 2))+ await I.>>= \case+ Recv (TwoSuccess d) -> returnAt $ Just d+ Recv TwoFailed -> returnAt Nothing++data FindBookResult :: BookSt -> Type where+ NotFound' :: FindBookResult (S2 '[NotFound])+ Found' :: FindBookResult (S2 '[Found])++findBook+ :: (Has Random sig m)+ => String+ -> Peer Role BookSt Seller m FindBookResult (S2 s)+findBook _st = I.do+ At b <- liftm $ uniform @Bool+ if b+ then LiftM $ pure (ireturn Found')+ else LiftM $ pure (ireturn NotFound')++sellerPeer+ :: (Has Random sig m)+ => Peer Role BookSt Seller m (At () (Done Seller)) S0+sellerPeer = I.do+ Recv (Title st) <- await+ findBook st I.>>= \case+ NotFound' -> yield NoBook+ Found' -> I.do+ yield (Price 30)+ await I.>>= \case+ Recv OneAccept -> yield (OneDate 100)+ Recv TwoNotBuy -> returnAt ()+ Recv TwoAccept -> yield (TwoDate 100)+ Recv TwoNotBuy1 -> returnAt ()
+ test/Book3/Type.hs view
@@ -0,0 +1,256 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeFamilies #-}++module Book3.Type where++import Data.IFunctor (Sing, SingI)+import qualified Data.IFunctor as I+import Data.Kind+import GHC.Exts (dataToTag#)+import GHC.Int (Int (I#))+import TypedProtocol.Codec+import TypedProtocol.Core++{-+---------------------------Buyer-------------------------Seller------------------------Buyer2---------------------------+ S0 S0 (S1 s)+ Title | -----> |+ (S2 s) (S2 s) (S1 s)+ ---------------------------------------------------[NotFound]---------------------------------------------------+ (S2 s) (S2 [NotFound]) (S1 s)+ NoBook | <----- |+ (S1 [NotFound]) End (S1 s)+ SellerNoBook | -----> |+ End End End+ Terminal++ ----------------------------------------------------[Found]-----------------------------------------------------+ (S2 s) (S2 [Found]) (S1 s)+ Price | <----- |+ (S1 s) (S3 s) (S1 s)+ ----------------------------------------------[One,Found]-----------------------------------------------+ (S1 [One,Found]) (S3 s) (S1 s)+ OneAfford | -----> |+ (S3 [One,Found]) (S3 s) S4+ OneAccept | -----> |+ S5 S5 S4+ OneDate | <----- |+ S4 End S4+ OneSuccess | -----> |+ End End End+ Terminal++ ----------------------------------------------[Two,Found]-----------------------------------------------+ (S1 [Two,Found]) (S3 s) (S1 s)+ PriceToBuyer2 | -----> |+ (S6 s) (S3 s) (S6 s)+ -------------------------------------[NotSupport,Two,Found]-------------------------------------+ (S6 s) (S3 s) (S6 [NotSupport,Two,Found])+ NotSupport1 | <----- |+ (S3 [NotSupport,Two,Found]) (S3 s) End+ TwoNotBuy | -----> |+ End End End+ Terminal++ --------------------------------------[Support,Two,Found]---------------------------------------+ (S6 s) (S3 s) (S6 [Support,Two,Found])+ SupportVal | <----- |+ (S3 s) (S3 s) (S7 s)+ -------------------------------[Enough,Support,Two,Found]-------------------------------+ (S3 [Enough,Support,Two,Found]) (S3 s) (S7 s)+ TwoAccept | -----> |+ S8 S8 (S7 s)+ TwoDate | <----- |+ (S7 [Enough,Support,Two,Found]) End (S7 s)+ TwoSuccess | -----> |+ End End End+ Terminal++ -----------------------------[NotEnough,Support,Two,Found]------------------------------+ (S3 [NotEnough,Support,Two,Found]) (S3 s) (S7 s)+ TwoNotBuy1 | -----> |+ (S7 [NotEnough,Support,Two,Found]) End (S7 s)+ TwoFailed | -----> |+ End End End+ Terminal++-}++data Role = Buyer | Seller | Buyer2+ deriving (Show, Eq, Ord)++data SRole :: Role -> Type where+ SBuyer :: SRole Buyer+ SBuyer2 :: SRole Buyer2+ SSeller :: SRole Seller++type instance Sing = SRole++instance SingI Buyer where+ sing = SBuyer++instance SingI Buyer2 where+ sing = SBuyer2++instance SingI Seller where+ sing = SSeller++data BookBranchSt+ = NotFound+ | Found+ | One+ | Two+ | Support+ | NotSupport+ | Enough+ | NotEnough+ deriving (Show)++data BookSt+ = S0+ | S1 [BookBranchSt]+ | S2 [BookBranchSt]+ | S3 [BookBranchSt]+ | S4+ | S5+ | S6 [BookBranchSt]+ | S7 [BookBranchSt]+ | S8+ | End++data SBookSt :: BookSt -> Type where+ SS0 :: SBookSt S0+ SS1 :: SBookSt (S1 s)+ SS2 :: SBookSt (S2 s)+ SS3 :: SBookSt (S3 s)+ SS4 :: SBookSt S4+ SS5 :: SBookSt S5+ SS6 :: SBookSt (S6 s)+ SS7 :: SBookSt (S7 s)+ SS8 :: SBookSt S8+ SEnd :: SBookSt End++type instance Sing = SBookSt++instance SingI S0 where+ sing = SS0++instance SingI (S1 s) where+ sing = SS1++instance SingI (S2 s) where+ sing = SS2++instance SingI (S3 s) where+ sing = SS3++instance SingI S4 where+ sing = SS4++instance SingI S5 where+ sing = SS5++instance SingI (S6 s) where+ sing = SS6++instance SingI (S7 s) where+ sing = SS7++instance SingI S8 where+ sing = SS8++instance SingI End where+ sing = SEnd++type Date = Int++instance SingToInt Role where+ singToInt x = I# (dataToTag# x)++instance SingToInt BookSt where+ singToInt x = I# (dataToTag# x)++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, S2 s) '(Seller, S2 s)+ NoBook :: Msg Role BookSt (S2 '[NotFound]) '(Seller, End) '(Buyer, S1 '[NotFound])+ SellerNoBook :: Msg Role BookSt (S1 '[NotFound]) '(Buyer, End) '(Buyer2, End)+ Price :: Int -> Msg Role BookSt (S2 '[Found]) '(Seller, S3 s) '(Buyer, S1 s)+ OneAfford :: Msg Role BookSt (S1 '[One, Found]) '(Buyer, S3 '[One, Found]) '(Buyer2, S4)+ OneAccept :: Msg Role BookSt (S3 '[One, Found]) '(Buyer, S5) '(Seller, S5)+ OneDate :: Date -> Msg Role BookSt S5 '(Seller, End) '(Buyer, S4)+ OneSuccess :: Date -> Msg Role BookSt S4 '(Buyer, End) '(Buyer2, End)+ PriceToBuyer2 :: Int -> Msg Role BookSt (S1 '[Two, Found]) '(Buyer, S6 s) '(Buyer2, S6 s)+ NotSupport1 :: Msg Role BookSt (S6 '[NotSupport, Two, Found]) '(Buyer2, End) '(Buyer, S3 '[NotSupport, Two, Found])+ TwoNotBuy :: Msg Role BookSt (S3 '[NotSupport, Two, Found]) '(Buyer, End) '(Seller, End)+ SupportVal :: Int -> Msg Role BookSt (S6 '[Support, Two, Found]) '(Buyer2, S7 s) '(Buyer, S3 s)+ TwoAccept :: Msg Role BookSt (S3 '[Enough, Support, Two, Found]) '(Buyer, S8) '(Seller, S8)+ TwoDate :: Date -> Msg Role BookSt S8 '(Seller, End) '(Buyer, S7 '[Enough, Support, Two, Found])+ TwoSuccess :: Date -> Msg Role BookSt (S7 '[Enough, Support, Two, Found]) '(Buyer, End) '(Buyer2, End)+ TwoNotBuy1 :: Msg Role BookSt (S3 '[NotEnough, Support, Two, Found]) '(Buyer, S7 '[NotEnough, Support, Two, Found]) '(Seller, End)+ TwoFailed :: Msg Role BookSt (S7 '[NotEnough, Support, Two, Found]) '(Buyer, End) '(Buyer2, End)++encodeMsg :: Encode Role BookSt (AnyMsg Role BookSt)+encodeMsg = Encode $ \x -> case x of+ Title{} -> AnyMsg x+ NoBook{} -> AnyMsg x+ SellerNoBook{} -> AnyMsg x+ Price{} -> AnyMsg x+ OneAfford{} -> AnyMsg x+ OneAccept{} -> AnyMsg x+ OneDate{} -> AnyMsg x+ OneSuccess{} -> AnyMsg x+ PriceToBuyer2{} -> AnyMsg x+ NotSupport1{} -> AnyMsg x+ TwoNotBuy{} -> AnyMsg x+ SupportVal{} -> AnyMsg x+ TwoAccept{} -> AnyMsg x+ TwoDate{} -> AnyMsg x+ TwoSuccess{} -> AnyMsg x+ TwoNotBuy1{} -> AnyMsg x+ TwoFailed{} -> AnyMsg x++decodeMsg+ :: DecodeStep+ (AnyMsg Role BookSt)+ CodecFailure+ (AnyMsg Role BookSt)+decodeMsg =+ DecodePartial $ \case+ Nothing -> DecodeFail (CodecFailure "expected more data")+ Just anyMsg -> DecodeDone anyMsg Nothing++instance Show (AnyMsg Role BookSt) where+ show (AnyMsg msg) = case msg of+ Title st -> "Title " <> show st+ NoBook -> "NoBook"+ SellerNoBook -> "SellerNoBook"+ Price i -> "Price " <> show i+ OneAfford -> "OneAfford"+ OneAccept -> "OneAccept"+ OneDate d -> "OneDate " <> show d+ OneSuccess d -> "OneSuccess" <> show d+ PriceToBuyer2 i -> "PriceToBuyer2 " <> show i+ NotSupport1 -> "NotSupport1"+ TwoNotBuy -> "TwoNotBuy"+ SupportVal v -> "SupportVal " <> show v+ TwoAccept -> "TwoAccept"+ TwoDate d -> "TwoDate " <> show d+ TwoSuccess d -> "TwoSuccess " <> show d+ TwoNotBuy1 -> "TwoNotBuy1"+ TwoFailed -> "TwoFailed"
+ test/Main.hs view
@@ -0,0 +1,15 @@+{-# LANGUAGE TypeApplications #-}+module Main (main) where++import Book3.Main+import Control.Monad+import System.Random+import Control.Exception++main :: IO ()+main = do+ replicateM_ 100 $ do+ g <- newStdGen+ case book3Prop g of+ Left e -> throwIO e+ Right _ -> pure ()
+ test/PingPong.hs view
@@ -0,0 +1,195 @@+{-# LANGUAGE AllowAmbiguousTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE MagicHash #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE NamedFieldPuns #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE QualifiedDo #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeFamilies #-}+{-# OPTIONS_GHC -Wno-unused-do-bind #-}++module PingPong where++import Control.Concurrent.Class.MonadSTM+import Control.Monad+import Control.Monad.Class.MonadFork (MonadFork, forkIO)+import Control.Monad.Class.MonadSay+import Control.Monad.Class.MonadThrow (MonadThrow)+import Data.IFunctor (At (..), Sing, SingI, ireturn, returnAt)+import qualified Data.IFunctor as I+import qualified Data.IntMap as IntMap+import Data.Kind+import GHC.Exts (dataToTag#)+import GHC.Int (Int (I#))+import TypedProtocol.Codec+import TypedProtocol.Core+import TypedProtocol.Driver++{-++--------------------------------------------------------------------------+ Client Server+ :S0 s :S0 s+ -----------------------------------------------------------------------+ | :S0 True :S0 s+ | Ping ->+ | :S1 :S1+ | <- Pong+ | :S0 s :S0 s+ -----------------------------------------------------------------------++ -----------------------------------------------------------------------+ | :S0 False :S0 s+ | Stop ->+ | :End :End+ -----------------------------------------------------------------------+ -}++data Role = Client | Server+ deriving (Show, Eq, Ord)++data SRole :: Role -> Type where+ SClient :: SRole Client+ SServer :: SRole Server++type instance Sing = SRole++instance SingI Client where+ sing = SClient++instance SingI Server where+ sing = SServer++data PingPong+ = S0 Bool+ | S1+ | End++data SPingPong :: PingPong -> Type where+ SS0 :: SPingPong (S0 b)+ SS1 :: SPingPong S1+ SEnd :: SPingPong End++type instance Sing = SPingPong++instance SingI (S0 b) where+ sing = SS0++instance SingI S1 where+ sing = SS1++instance SingI End where+ sing = SEnd++instance SingToInt Role where+ singToInt x = I# (dataToTag# x)++instance SingToInt PingPong where+ singToInt x = I# (dataToTag# x)++instance Protocol Role PingPong where+ type Done Client = End+ type Done Server = End+ data Msg Role PingPong from send recv where+ Ping :: Int -> Msg Role PingPong (S0 True) '(Client, S1) '(Server, S1)+ Pong :: Int -> Msg Role PingPong S1 '(Server, S0 s) '(Client, S0 s)+ Stop :: Msg Role PingPong (S0 False) '(Client, End) '(Server, End)++encodeMsg :: Encode Role PingPong (AnyMsg Role PingPong)+encodeMsg = Encode $ \x -> case x of+ Ping{} -> AnyMsg x+ Pong{} -> AnyMsg x+ Stop{} -> AnyMsg x++decodeMsg+ :: DecodeStep+ (AnyMsg Role PingPong)+ CodecFailure+ (AnyMsg Role PingPong)+decodeMsg =+ DecodePartial $ \case+ Nothing -> DecodeFail (CodecFailure "expected more data")+ Just anyMsg -> DecodeDone anyMsg Nothing++data Choice :: PingPong -> Type where+ ST :: Choice (S0 True)+ SF :: Choice (S0 False)++choice :: (Monad m) => Int -> Peer Role PingPong Client m Choice (S0 s)+choice i =+ if i <= 5+ then LiftM $ pure (ireturn ST)+ else LiftM $ pure (ireturn SF)++clientPeer+ :: (Monad m) => Int -> Peer Role PingPong Client m (At () (Done Client)) (S0 s)+clientPeer i = I.do+ res <- choice i+ case res of+ ST -> I.do+ yield (Ping i)+ Recv (Pong i') <- await+ clientPeer i'+ SF -> yield Stop++serverPeer+ :: (Monad m) => Peer Role PingPong Server m (At () (Done Server)) (S0 s)+serverPeer = I.do+ Recv msg <- await+ case msg of+ Ping i -> I.do+ yield (Pong (i + 1))+ serverPeer+ Stop -> returnAt ()++mvarsAsChannel+ :: (MonadSTM m)+ => TMVar m a+ -> TMVar m a+ -> Channel m a+mvarsAsChannel bufferRead bufferWrite =+ Channel{send, recv}+ where+ send x = atomically (putTMVar bufferWrite x)+ recv = atomically (Just <$> takeTMVar bufferRead)++myTracer :: (MonadSay m) => String -> Tracer Role PingPong m+myTracer st v = say (st <> show v)++instance Show (AnyMsg Role PingPong) where+ show (AnyMsg msg) = case msg of+ Ping i -> "Ping " <> show i+ Pong i -> "Pong " <> show i+ Stop -> "Stop"++runAll :: forall m. (Monad m, MonadSTM m, MonadSay m, MonadFork m, MonadThrow m) => m ()+runAll = do+ clientTMVar <- newEmptyTMVarIO @m @(AnyMsg Role PingPong)+ serverTMVar <- newEmptyTMVarIO @m @(AnyMsg Role PingPong)+ let clientChannel = mvarsAsChannel @m clientTMVar serverTMVar+ serverChannel = mvarsAsChannel @m serverTMVar clientTMVar+ sendFun bufferWrite x = atomically (putTMVar bufferWrite x)+ sendToRole =+ IntMap.fromList+ [ (singToInt SServer, sendFun serverTMVar)+ , (singToInt SClient, sendFun clientTMVar)+ ]+ clientTvar <- newTVarIO IntMap.empty+ serverTvar <- newTVarIO IntMap.empty+ let clientDriver = driverSimple (myTracer "client: ") encodeMsg sendToRole clientTvar id+ serverDriver = driverSimple (myTracer "server: ") encodeMsg sendToRole serverTvar id+ -- fork client decode thread+ forkIO $ decodeLoop (myTracer "client: ") Nothing (Decode decodeMsg) clientChannel clientTvar+ -- fork server decode thread+ forkIO $ decodeLoop (myTracer "server: ") Nothing (Decode decodeMsg) serverChannel serverTvar+ -- fork server Peer thread+ forkIO $ void $ runPeerWithDriver serverDriver serverPeer+ -- run client Peer+ void $ runPeerWithDriver clientDriver (clientPeer 0)
+ typed-session.cabal view
@@ -0,0 +1,129 @@+cabal-version: 3.0+-- The cabal-version field refers to the version of the .cabal specification,+-- and can be different from the cabal-install (the tool) version and the+-- Cabal (the library) version you are using. As such, the Cabal (the library)+-- version used must be equal or greater than the version stated in this field.+-- Starting from the specification version 2.2, the cabal-version field must be+-- the first thing in the cabal file.++-- Initial package description 'typed-session' generated by+-- 'cabal init'. For further documentation, see:+-- http://haskell.org/cabal/users-guide/+--+-- The name of the package.+name: typed-session++-- The package version.+-- See the Haskell package versioning policy (PVP) for standards+-- guiding when and how versions should be incremented.+-- https://pvp.haskell.org+-- PVP summary: +-+------- breaking API changes+-- | | +----- non-breaking API additions+-- | | | +--- code changes with no API change+version: 0.1.0.0++-- A short (one-line) description of the package.+synopsis: typed session framework++-- A longer description of the package.+description:+ Typed session are used to ensure desirable properties in concurrent and distributed systems,+ i.e. absence of communication errors or deadlocks, and protocol conformance.++-- The license under which the package is released.+license: MIT++-- The file containing the license text.+license-file: LICENSE++-- The package author(s).+author: sdzx-1++-- An email address to which users can send suggestions, bug reports, and patches.+maintainer: shangdizhixia1993@163.com++category: Control, Network+-- A copyright notice.+-- copyright:+build-type: Simple++-- Extra doc files to be distributed with the package, such as a CHANGELOG or a README.+extra-doc-files: CHANGELOG.md++-- Extra source files to be distributed with the package, such as examples, or a tutorial module.+-- extra-source-files:+extra-doc-files: data/*.png++common warnings+ ghc-options: -Wall++library+ -- Import common warning flags.+ import: warnings++ -- Modules exported by the library.+ exposed-modules: Data.IFunctor+ , TypedProtocol.Core+ , TypedProtocol.Codec+ , TypedProtocol.Driver++ -- Modules included in this library but not exported.+ -- other-modules:++ -- LANGUAGE extensions used by modules in this package.+ -- other-extensions:++ -- Other library packages from which modules are imported.+ build-depends: base >= 4.20.0 && < 4.21+ , containers >= 0.7 && < 0.8+ , io-classes >= 1.5.0 && < 1.6++ -- Directories containing source files.+ hs-source-dirs: src++ -- Base language which the package is written in.+ default-language: Haskell2010++test-suite typed-session-test+ -- Import common warning flags.+ import: warnings++ -- Base language which the package is written in.+ default-language: Haskell2010++ -- Modules included in this executable, other than Main.+ other-modules: Book+ , Book1+ , Book2+ , Book3.Type+ , Book3.Peer+ , Book3.Main+ , PingPong++ -- LANGUAGE extensions used by modules in this package.+ -- other-extensions:++ -- The interface type and version of the test suite.+ type: exitcode-stdio-1.0++ -- Directories containing source files.+ hs-source-dirs: test++ -- The entrypoint to the test suite.+ main-is: Main.hs++ -- Test dependencies.+ build-depends:+ base >=4.20.0.0,+ typed-session,+ containers,+ io-classes,+ io-sim,+ random,+ fused-effects,+ fused-effects-random+ ghc-options: -Werror=inaccessible-code -threaded++source-repository head+ type: git+ location: https://github.com/sdzx-1/typed-session