diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,3 @@ +# Revision history for typed-session + +## 0.1.0.0-- 2024-8-6 diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/data/fm.png b/data/fm.png new file mode 100644 Binary files /dev/null and b/data/fm.png differ diff --git a/src/Data/IFunctor.hs b/src/Data/IFunctor.hs new file mode 100644 --- /dev/null +++ b/src/Data/IFunctor.hs @@ -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 diff --git a/src/TypedProtocol/Codec.hs b/src/TypedProtocol/Codec.hs new file mode 100644 --- /dev/null +++ b/src/TypedProtocol/Codec.hs @@ -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 diff --git a/src/TypedProtocol/Core.hs b/src/TypedProtocol/Core.hs new file mode 100644 --- /dev/null +++ b/src/TypedProtocol/Core.hs @@ -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) diff --git a/src/TypedProtocol/Driver.hs b/src/TypedProtocol/Driver.hs new file mode 100644 --- /dev/null +++ b/src/TypedProtocol/Driver.hs @@ -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: +![fm](data/fm.png) + +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 diff --git a/test/Book.hs b/test/Book.hs new file mode 100644 --- /dev/null +++ b/test/Book.hs @@ -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 diff --git a/test/Book1.hs b/test/Book1.hs new file mode 100644 --- /dev/null +++ b/test/Book1.hs @@ -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 diff --git a/test/Book2.hs b/test/Book2.hs new file mode 100644 --- /dev/null +++ b/test/Book2.hs @@ -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 diff --git a/test/Book3/Main.hs b/test/Book3/Main.hs new file mode 100644 --- /dev/null +++ b/test/Book3/Main.hs @@ -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) diff --git a/test/Book3/Peer.hs b/test/Book3/Peer.hs new file mode 100644 --- /dev/null +++ b/test/Book3/Peer.hs @@ -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 () diff --git a/test/Book3/Type.hs b/test/Book3/Type.hs new file mode 100644 --- /dev/null +++ b/test/Book3/Type.hs @@ -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" diff --git a/test/Main.hs b/test/Main.hs new file mode 100644 --- /dev/null +++ b/test/Main.hs @@ -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 () diff --git a/test/PingPong.hs b/test/PingPong.hs new file mode 100644 --- /dev/null +++ b/test/PingPong.hs @@ -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) diff --git a/typed-session.cabal b/typed-session.cabal new file mode 100644 --- /dev/null +++ b/typed-session.cabal @@ -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