diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,6 @@ # Revision history for typed-session +## 0.1.1.0 +* add protocol TH + ## 0.1.0.0-- 2024-8-6 diff --git a/src/TypedProtocol/Codec.hs b/src/TypedProtocol/Codec.hs deleted file mode 100644 --- a/src/TypedProtocol/Codec.hs +++ /dev/null @@ -1,72 +0,0 @@ --- 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 deleted file mode 100644 --- a/src/TypedProtocol/Core.hs +++ /dev/null @@ -1,254 +0,0 @@ -{-# 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 deleted file mode 100644 --- a/src/TypedProtocol/Driver.hs +++ /dev/null @@ -1,216 +0,0 @@ --- 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/src/TypedSession/Codec.hs b/src/TypedSession/Codec.hs new file mode 100644 --- /dev/null +++ b/src/TypedSession/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 TypedSession.Codec where + +import Control.Exception (Exception) +import TypedSession.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/TypedSession/Core.hs b/src/TypedSession/Core.hs new file mode 100644 --- /dev/null +++ b/src/TypedSession/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 TypedSession.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/TypedSession/Driver.hs b/src/TypedSession/Driver.hs new file mode 100644 --- /dev/null +++ b/src/TypedSession/Driver.hs @@ -0,0 +1,217 @@ +-- 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 TypedSession.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 TypedSession.Codec +import TypedSession.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/src/TypedSession/TH.hs b/src/TypedSession/TH.hs new file mode 100644 --- /dev/null +++ b/src/TypedSession/TH.hs @@ -0,0 +1,293 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE NamedFieldPuns #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# OPTIONS_GHC -Wno-unused-imports #-} +{-# OPTIONS_GHC -split-sections #-} + +module TypedSession.TH where + +import Control.Monad (forM) +import Data.Either (fromRight) +import Data.Kind +import qualified Data.Set as Set +import Language.Haskell.TH hiding (Type) +import qualified Language.Haskell.TH as TH +import Language.Haskell.TH.Quote +import TypedSession.State.GenDoc +import TypedSession.State.Parser (runProtocolParser) +import TypedSession.State.Piple (PipleResult (..), piple) +import TypedSession.State.Render +import TypedSession.State.Type (BranchSt (..), Creat, MsgOrLabel (..), MsgT1, Protocol (..), ProtocolError, T (..)) + +roleDecs :: Name -> Q [Dec] +roleDecs name = do + res <- reify name + case res of + TyConI (DataD [] dName [] Nothing cons _) -> do + a <- newName "a" + x <- newName "x" + pure $ + [ DataD + [] + (addS dName) + [KindedTV a BndrReq (ConT dName)] + Nothing + [GadtC [addS n] [] (AppT (ConT (addS dName)) (PromotedT n)) | NormalC n [] <- cons] + [] + , TySynInstD (TySynEqn Nothing (ConT (mkName "Data.IFunctor.Sing")) (ConT (addS dName))) + ] + ++ [ InstanceD + Nothing + [] + (AppT (ConT $ mkName "Data.IFunctor.SingI") (PromotedT n)) + [FunD (mkName "sing") [Clause [] (NormalB (ConE (addS n))) []]] + | NormalC n [] <- cons + ] + ++ [ InstanceD + Nothing + [] + (AppT (ConT (mkName "TypedSession.Core.SingToInt")) (ConT name)) + [ FunD + (mkName "singToInt") + [Clause [VarP x] (NormalB (AppE (ConE (mkName "I#")) (AppE (VarE $ mkName "dataToTag#") (VarE x)))) []] + ] + ] + _ -> error "np" + +addS :: Name -> Name +addS name = + let n = (nameBase name) + in mkName ("S" <> n) + +protDecsAndMsgDecs :: forall r bst. (Show r, Show bst) => String -> Name -> Name -> PipleResult r bst -> Q [Dec] +protDecsAndMsgDecs protN roleName bstName PipleResult{msgT1, dnySet, stBound = (fromVal, toVal)} = do + sVar <- newName "s" + let protName = mkName protN + protSName = mkName ("S" <> protN) + genConstr i = + if i == -1 + then NormalC (mkName "End") [] + else + if i `Set.member` dnySet + then + NormalC + (mkName $ "S" <> show i) + [(Bang NoSourceUnpackedness NoSourceStrictness, ConT bstName)] + else NormalC (mkName $ "S" <> show i) [] + genSConstr i = + if i == -1 + then + GadtC [mkName "SEnd"] [] (AppT (ConT protSName) (PromotedT (mkName "End"))) + else + if i `Set.member` dnySet + then + ForallC + [KindedTV sVar SpecifiedSpec (ConT bstName)] + [] + ( GadtC + [mkName $ "SS" <> show i] + [] + (AppT (ConT protSName) (AppT (PromotedT $ mkName $ "S" <> show i) (VarT sVar))) + ) + else + GadtC [mkName $ "SS" <> show i] [] (AppT (ConT protSName) (PromotedT $ mkName $ "S" <> show i)) + + isTAny :: T bst -> Bool + isTAny = \case + TAny _ -> True + _ -> False + + mkInstanceMsg :: Name -> Protocol (MsgT1 r bst) r bst -> Q [Con] + mkInstanceMsg s = \case + Msg ((a, b, c), (from, to), _) constr args _ _ :> prots -> do + let tAnyToType :: T bst -> TH.Type + tAnyToType = \case + TNum i -> PromotedT (mkName $ "S" <> show i) + BstList i bst -> AppT (PromotedT (mkName $ "S" <> show i)) (PromotedT (mkName (show bst))) + TAny i -> AppT (PromotedT (mkName $ "S" <> show i)) (VarT s) + TEnd -> PromotedT $ mkName "End" + + let mkTName = + ( AppT + ( AppT + ( AppT + ( AppT + ( AppT + (ConT $ mkName "Msg") + (ConT roleName) + ) + (ConT protName) + ) + (tAnyToType a) + ) + (AppT (AppT (PromotedTupleT 2) (PromotedT (mkName (show from)))) (tAnyToType b)) + ) + (AppT (AppT (PromotedTupleT 2) (PromotedT (mkName (show to)))) (tAnyToType c)) + ) + let val = + let gadtc = + GadtC + [mkName constr] + [ ( Bang NoSourceUnpackedness NoSourceStrictness + , case words ag of + [] -> error "np" + (x : xs) -> foldl' AppT (ConT (mkName x)) (map (ConT . mkName) xs) + ) + | ag <- args + ] + mkTName + in if any isTAny [a, b, c] + then + ForallC + [KindedTV s SpecifiedSpec (ConT bstName)] + [] + gadtc + else gadtc + res <- mkInstanceMsg s prots + pure (val : res) + Label _ _ :> prots -> mkInstanceMsg s prots + Branch _ _ ls -> do + ls' <- forM ls $ \(BranchSt _ _ prot) -> mkInstanceMsg s prot + pure $ concat ls' + _ -> pure [] + + a <- newName "a" + s1 <- newName "s1" + x <- newName "x" + + -- make instance Done + res <- reify roleName + instDoneDesc <- case res of + TyConI (DataD [] _ [] Nothing cons _) -> do + pure + [ TySynInstD + ( TySynEqn + Nothing + (AppT (ConT (mkName "Done")) (PromotedT n)) + (PromotedT (mkName "End")) + ) + | NormalC n [] <- cons + ] + _ -> error "np" + + -- make instance msg + ss <- newName "s" + instMsgDesc <- mkInstanceMsg ss (msgT1) + + fromVar <- newName "from" + sendVar <- newName "send" + recvVar <- newName "recv" + pure $ + [ DataD [] protName [] Nothing [genConstr i | i <- [fromVal .. toVal]] [] + ] + ++ [DataD [] protSName [KindedTV a BndrReq (ConT protName)] Nothing [genSConstr i | i <- [fromVal .. toVal]] []] + ++ [TySynInstD (TySynEqn Nothing (ConT (mkName "Data.IFunctor.Sing")) (ConT protSName))] + ++ [ InstanceD + Nothing + [] + ( AppT + (ConT $ mkName "Data.IFunctor.SingI") + ( if i == -1 + then PromotedT (mkName "End") + else + if i `Set.member` dnySet + then SigT (AppT (PromotedT (mkName ("S" <> show i))) (VarT s1)) (ConT protName) + else PromotedT (mkName ("S" <> show i)) + ) + ) + [ FunD + (mkName "sing") + [Clause [] (NormalB (ConE (mkName $ "S" <> (if i == -1 then "End" else ("S" <> show i))))) []] + ] + | i <- [fromVal .. toVal] + ] + ++ [ InstanceD + Nothing + [] + (AppT (ConT (mkName "TypedSession.Core.SingToInt")) (ConT protName)) + [ FunD + (mkName "singToInt") + [Clause [VarP x] (NormalB (AppE (ConE (mkName "I#")) (AppE (VarE $ mkName "dataToTag#") (VarE x)))) []] + ] + ] + ++ [ InstanceD + Nothing + [] + ( AppT + (AppT (ConT (mkName "TypedSession.Core.Protocol")) (ConT roleName)) + (ConT protName) + ) + ( instDoneDesc + ++ let ct1 = (AppT (AppT (TupleT 2) (ConT roleName)) (ConT protName)) + in [ DataInstD + [] + ( Just + [ KindedTV fromVar () (ConT protName) + , KindedTV sendVar () ct1 + , KindedTV recvVar () ct1 + ] + ) + ( AppT + ( AppT + ( AppT + ( AppT + ( AppT + (ConT $ mkName "Msg") + (ConT roleName) + ) + (ConT protName) + ) + (SigT (VarT fromVar) (ConT protName)) + ) + (SigT (VarT sendVar) ct1) + ) + (SigT (VarT recvVar) ct1) + ) + Nothing + instMsgDesc + [] + ] + ) + ] + +protocol + :: forall r bst + . ( Enum r + , Bounded r + , Show r + , Enum bst + , Bounded bst + , Show bst + , Ord r + ) + => String -> Name -> Name -> QuasiQuoter +protocol protN roleName bstName = + QuasiQuoter + { quoteExp = const $ fail "No protocol parse for exp" + , quotePat = const $ fail "No protocol parse for pat" + , quoteType = const $ fail "No protocol parser for type" + , quoteDec = parseOrThrow + } + where + parseOrThrow :: String -> Q [Dec] + parseOrThrow st = case runProtocolParser @r @bst st of + Left e -> fail (show e) + Right protCreat -> case piple protCreat of + Left e -> fail (show e) + Right pipResult -> do + let graphStr = genGraph @r @bst defaultStrFilEnv pipResult + runIO $ do + writeFile (protN <> ".prot") graphStr + putStrLn graphStr + d1 <- roleDecs roleName + d2 <- protDecsAndMsgDecs protN roleName bstName pipResult + pure (d1 ++ d2) diff --git a/test/Book.hs b/test/Book.hs --- a/test/Book.hs +++ b/test/Book.hs @@ -28,9 +28,9 @@ import Data.Kind import GHC.Exts (dataToTag#) import GHC.Int (Int (I#)) -import TypedProtocol.Codec -import TypedProtocol.Core -import TypedProtocol.Driver +import TypedSession.Codec +import TypedSession.Core +import TypedSession.Driver {- diff --git a/test/Book1.hs b/test/Book1.hs --- a/test/Book1.hs +++ b/test/Book1.hs @@ -28,9 +28,9 @@ import Data.Kind import GHC.Exts (dataToTag#) import GHC.Int (Int (I#)) -import TypedProtocol.Codec -import TypedProtocol.Core -import TypedProtocol.Driver +import TypedSession.Codec +import TypedSession.Core +import TypedSession.Driver {- diff --git a/test/Book2.hs b/test/Book2.hs --- a/test/Book2.hs +++ b/test/Book2.hs @@ -28,9 +28,9 @@ import Data.Kind import GHC.Exts (dataToTag#) import GHC.Int (Int (I#)) -import TypedProtocol.Codec -import TypedProtocol.Core -import TypedProtocol.Driver +import TypedSession.Codec +import TypedSession.Core +import TypedSession.Driver {- diff --git a/test/Book3/Main.hs b/test/Book3/Main.hs --- a/test/Book3/Main.hs +++ b/test/Book3/Main.hs @@ -16,6 +16,7 @@ module Book3.Main where import Book3.Peer +import Book3.Protocol import Book3.Type import Control.Carrier.Random.Gen (runRandom) import Control.Concurrent.Class.MonadSTM @@ -24,12 +25,12 @@ import Control.Monad.Class.MonadFork (MonadFork, forkIO) import Control.Monad.Class.MonadSay import Control.Monad.Class.MonadThrow (MonadThrow) +import Control.Monad.IOSim import qualified Data.IntMap as IntMap import System.Random (StdGen, split) -import TypedProtocol.Codec -import TypedProtocol.Core -import TypedProtocol.Driver -import Control.Monad.IOSim +import TypedSession.Codec +import TypedSession.Core +import TypedSession.Driver mvarsAsChannel :: (MonadSTM m) @@ -42,7 +43,7 @@ send x = atomically (putTMVar bufferWrite x) recv = atomically (Just <$> takeTMVar bufferRead) -myTracer :: (MonadSay m) => String -> Tracer Role BookSt m +myTracer :: (MonadSay m) => String -> Tracer BookRole Book m myTracer st v = say (st <> show v) runAll @@ -56,9 +57,9 @@ => StdGen -> n () runAll g = do - buyerTMVar <- newEmptyTMVarIO @n @(AnyMsg Role BookSt) - buyer2TMVar <- newEmptyTMVarIO @n @(AnyMsg Role BookSt) - sellerTMVar <- newEmptyTMVarIO @n @(AnyMsg Role BookSt) + buyerTMVar <- newEmptyTMVarIO @n @(AnyMsg BookRole Book) + buyer2TMVar <- newEmptyTMVarIO @n @(AnyMsg BookRole Book) + sellerTMVar <- newEmptyTMVarIO @n @(AnyMsg BookRole Book) let buyerSellerChannel = mvarsAsChannel @n buyerTMVar sellerTMVar buyerBuyer2Channel = mvarsAsChannel @n buyerTMVar buyer2TMVar diff --git a/test/Book3/Peer.hs b/test/Book3/Peer.hs --- a/test/Book3/Peer.hs +++ b/test/Book3/Peer.hs @@ -15,40 +15,43 @@ module Book3.Peer where +import Book3.Protocol 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 +import TypedSession.Core budget :: Int budget = 16 -data CheckPriceResult :: BookSt -> Type where - Yes :: CheckPriceResult (S3 [Enough, Support, Two, Found]) - No :: CheckPriceResult (S3 [NotEnough, Support, Two, Found]) +type Date = Int +data CheckPriceResult :: Book -> Type where + Yes :: CheckPriceResult (S5 Enough) + No :: CheckPriceResult (S5 NotEnough) + checkPrice :: (Has Random sig m) => Int -> Int - -> Peer Role BookSt Buyer m CheckPriceResult (S3 s) + -> Peer BookRole Book Buyer m CheckPriceResult S8 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]) +data OT :: Book -> Type where + OTOne :: OT (S5 One) + OTTwo :: OT (S1 Two) choiceOT :: (Has Random sig m) => Int - -> Peer Role BookSt Buyer m OT (S1 s) + -> Peer BookRole Book Buyer m OT S4 choiceOT _i = I.do At b <- liftm $ uniform @Bool if b @@ -57,7 +60,7 @@ buyerPeer :: (Has Random sig m) - => Peer Role BookSt Buyer m (At (Maybe Date) (Done Buyer)) S0 + => Peer BookRole Book Buyer m (At (Maybe Date) (Done Buyer)) S0 buyerPeer = I.do yield (Title "haskell book") await I.>>= \case @@ -67,7 +70,6 @@ Recv (Price i) -> I.do choiceOT i I.>>= \case OTOne -> I.do - yield OneAfford yield OneAccept Recv (OneDate d) <- await yield (OneSuccess d) @@ -76,7 +78,7 @@ where f1 :: (Has Random sig m) - => Peer Role BookSt 'Buyer m (At (Maybe Date) (Done Buyer)) ('S1 '[ 'Two, 'Found]) + => Peer BookRole Book 'Buyer m (At (Maybe Date) (Done Buyer)) ('S1 'Two) f1 = I.do yield (PriceToBuyer2 300) await I.>>= \case @@ -95,14 +97,14 @@ yield TwoFailed returnAt Nothing -data BuySupp :: BookSt -> Type where - BNS :: BuySupp (S6 '[NotSupport, Two, Found]) - BS :: BuySupp (S6 '[Support, Two, Found]) +data BuySupp :: Book -> Type where + BNS :: BuySupp (S6 NotSupport) + BS :: BuySupp (S6 Support) choiceB :: (Has Random sig m) => Int - -> Peer Role BookSt Buyer2 m BuySupp (S6 s) + -> Peer BookRole Book Buyer2 m BuySupp S7 choiceB _i = I.do At b <- liftm $ uniform @Bool if b @@ -111,13 +113,11 @@ buyer2Peer :: (Has Random sig m) - => Peer Role BookSt Buyer2 m (At (Maybe Date) (Done Buyer2)) (S1 s) + => Peer BookRole Book 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 (OneSuccess d) -> returnAt (Just d) Recv (PriceToBuyer2 i) -> I.do choiceB i I.>>= \case BNS -> I.do @@ -129,14 +129,14 @@ Recv (TwoSuccess d) -> returnAt $ Just d Recv TwoFailed -> returnAt Nothing -data FindBookResult :: BookSt -> Type where - NotFound' :: FindBookResult (S2 '[NotFound]) - Found' :: FindBookResult (S2 '[Found]) +data FindBookResult :: Book -> Type where + NotFound' :: FindBookResult (S2 NotFound) + Found' :: FindBookResult (S2 Found) findBook :: (Has Random sig m) => String - -> Peer Role BookSt Seller m FindBookResult (S2 s) + -> Peer BookRole Book Seller m FindBookResult S3 findBook _st = I.do At b <- liftm $ uniform @Bool if b @@ -145,7 +145,7 @@ sellerPeer :: (Has Random sig m) - => Peer Role BookSt Seller m (At () (Done Seller)) S0 + => Peer BookRole Book Seller m (At () (Done Seller)) S0 sellerPeer = I.do Recv (Title st) <- await findBook st I.>>= \case diff --git a/test/Book3/Protocol.hs b/test/Book3/Protocol.hs new file mode 100644 --- /dev/null +++ b/test/Book3/Protocol.hs @@ -0,0 +1,143 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MagicHash #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuasiQuotes #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# OPTIONS_GHC -Wno-orphans #-} + +module Book3.Protocol where + +import Book3.Type + +import Data.IFunctor (Sing, SingI (sing)) +import GHC.Exts (Int (..), dataToTag#) +import TypedSession.Codec +import TypedSession.Core + +[bookProtocol| + Label 0 + Msg "Title" ["String"] Buyer Seller + Branch Seller { + BranchSt NotFound + Msg "NoBook" [] Seller Buyer + Msg "SellerNoBook" [] Buyer Buyer2 + Terminal + BranchSt Found + Msg "Price" ["Int"] Seller Buyer + Branch Buyer { + BranchSt One + Msg "OneAccept" [] Buyer Seller + Msg "OneDate" ["Int"] Seller Buyer + Msg "OneSuccess" ["Int"] Buyer Buyer2 + Terminal + BranchSt Two + Msg "PriceToBuyer2" ["Int"] Buyer Buyer2 + Branch Buyer2 { + BranchSt NotSupport + Msg "NotSupport1" [] Buyer2 Buyer + Msg "TwoNotBuy" [] Buyer Seller + Terminal + BranchSt Support + Msg "SupportVal" ["Int"] Buyer2 Buyer + Branch Buyer { + BranchSt Enough + Msg "TwoAccept" [] Buyer Seller + Msg "TwoDate" ["Int"] Seller Buyer + Msg "TwoSuccess" ["Int"] Buyer Buyer2 + Terminal + BranchSt NotEnough + Msg "TwoNotBuy1" [] Buyer Seller + Msg "TwoFailed" [] Buyer Buyer2 + Terminal + } + } + } + } + +|] + +{- +-----------------------------------------------Buyer-------------------------Seller------------------------Buyer2 +LABEL 0 S0 S0 S1 s + Title S0-> ->S0 S1 s + [Branch Seller] S2 s S3 S1 s + NoBook S2 s<- <-{S2 NotFound} S1 s + SellerNoBook S1 NotFound-> End ->S1 s + Terminal End End End + Price S2 s<- <-{S2 Found} S1 s + [Branch Buyer] S4 S5 s S1 s + OneAccept {S5 One}-> ->S5 s S1 s + OneDate S10<- <-S10 S1 s + OneSuccess S1 One-> End ->S1 s + Terminal End End End + PriceToBuyer2 {S1 Two}-> S5 s ->S1 s + [Branch Buyer2] S6 s S5 s S7 + NotSupport1 S6 s<- S5 s <-{S6 NotSupport} + TwoNotBuy S5 NotSupport-> ->S5 s End + Terminal End End End + SupportVal S6 s<- S5 s <-{S6 Support} + [Branch Buyer] S8 S5 s S9 s + TwoAccept {S5 Enough}-> ->S5 s S9 s + TwoDate S11<- <-S11 S9 s + TwoSuccess S9 Enough-> End ->S9 s + Terminal End End End + TwoNotBuy1 {S5 NotEnough}-> ->S5 s S9 s + TwoFailed S9 NotEnough-> End ->S9 s + Terminal End End End + +-} + +encodeMsg :: Encode BookRole Book (AnyMsg BookRole Book) +encodeMsg = Encode $ \x -> case x of + Title{} -> AnyMsg x + NoBook{} -> AnyMsg x + SellerNoBook{} -> AnyMsg x + Price{} -> 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 BookRole Book) + CodecFailure + (AnyMsg BookRole Book) +decodeMsg = + DecodePartial $ \case + Nothing -> DecodeFail (CodecFailure "expected more data") + Just anyMsg -> DecodeDone anyMsg Nothing + +instance Show (AnyMsg BookRole Book) where + show (AnyMsg msg) = case msg of + Title st -> "Title " <> show st + NoBook -> "NoBook" + SellerNoBook -> "SellerNoBook" + Price i -> "Price " <> show i + 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/Book3/Type.hs b/test/Book3/Type.hs --- a/test/Book3/Type.hs +++ b/test/Book3/Type.hs @@ -10,101 +10,17 @@ {-# LANGUAGE QualifiedDo #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeApplications #-} {-# 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 +import Language.Haskell.TH.Quote (QuasiQuoter) +import TypedSession.TH (protocol) -instance SingI Seller where - sing = SSeller +data BookRole = Buyer | Seller | Buyer2 + deriving (Show, Eq, Ord, Enum, Bounded) data BookBranchSt = NotFound @@ -115,142 +31,13 @@ | 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 + deriving (Show, Eq, Ord, Enum, Bounded) -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" +bookProtocol :: QuasiQuoter +bookProtocol = + protocol + @BookRole + @BookBranchSt + "Book" + ''BookRole + ''BookBranchSt diff --git a/test/PingPong.hs b/test/PingPong.hs --- a/test/PingPong.hs +++ b/test/PingPong.hs @@ -28,9 +28,9 @@ import Data.Kind import GHC.Exts (dataToTag#) import GHC.Int (Int (I#)) -import TypedProtocol.Codec -import TypedProtocol.Core -import TypedProtocol.Driver +import TypedSession.Codec +import TypedSession.Core +import TypedSession.Driver {- diff --git a/typed-session.cabal b/typed-session.cabal --- a/typed-session.cabal +++ b/typed-session.cabal @@ -20,7 +20,7 @@ -- PVP summary: +-+------- breaking API changes -- | | +----- non-breaking API additions -- | | | +--- code changes with no API change -version: 0.1.0.0 +version: 0.1.1.0 -- A short (one-line) description of the package. synopsis: typed session framework @@ -63,9 +63,10 @@ -- Modules exported by the library. exposed-modules: Data.IFunctor - , TypedProtocol.Core - , TypedProtocol.Codec - , TypedProtocol.Driver + , TypedSession.Core + , TypedSession.Codec + , TypedSession.Driver + , TypedSession.TH -- Modules included in this library but not exported. -- other-modules: @@ -77,6 +78,8 @@ build-depends: base >= 4.20.0 && < 4.21 , containers >= 0.7 && < 0.8 , io-classes >= 1.5.0 && < 1.6 + , template-haskell + , typed-session-state-algorithm -- Directories containing source files. hs-source-dirs: src @@ -96,6 +99,7 @@ , Book1 , Book2 , Book3.Type + , Book3.Protocol , Book3.Peer , Book3.Main , PingPong @@ -121,7 +125,8 @@ io-sim, random, fused-effects, - fused-effects-random + fused-effects-random, + template-haskell ghc-options: -Werror=inaccessible-code -threaded source-repository head