{-# LANGUAGE GADTs #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE EmptyCase #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE FlexibleInstances #-} module Network.TypedProtocol.PingPong.Type where import Network.TypedProtocol.Core -- | The ping\/pong protocol and the states in its protocol state machine. -- -- This protocol serves as a simple example of the typed protocols framework -- to help understand the framework and as a template for writing other -- protocols. -- -- For a slightly more realistic example, see the request\/response protocol -- "Network.TypedProtocol.ResResp.Type". -- -- This declares the protocol itself. It is used both as a type level tag for -- the protocol and as the kind of the types of the states in the protocol -- state machine. That is @PingPong@ is a kind, and @StIdle@ is a type of -- that kind. -- -- If the protocol needs any type parameters (e.g. for thing that end up in -- the messages) then those type parameters go here. See the request\/response -- protocol for an example. It is parametrised over the types of the request -- and response. -- data PingPong where StIdle :: PingPong StBusy :: PingPong StDone :: PingPong instance Protocol PingPong where -- | The actual messages in our protocol. -- -- These involve transitions between different states within the 'PingPong' -- states. A ping request goes from idle to busy, and a pong response go from -- busy to idle. -- -- This example is so simple that we have all the messages directly as -- constructors within this type. In more complex cases it may be better to -- factor all (or related) requests and all responses within one case (in -- which case the state transitions may depend on the particular message via -- the usual GADT tricks). -- data Message PingPong from to where MsgPing :: Message PingPong StIdle StBusy MsgPong :: Message PingPong StBusy StIdle MsgDone :: Message PingPong StIdle StDone -- | We have to explain to the framework what our states mean, in terms of -- who is expected to send and receive in the different states. -- -- Idle states are where it is for the client to send a message. -- data ClientHasAgency st where TokIdle :: ClientHasAgency StIdle -- | Busy states are where the server is expected to send a reply (a pong). -- data ServerHasAgency st where TokBusy :: ServerHasAgency StBusy -- | In the done state neither client nor server can send messages. -- data NobodyHasAgency st where TokDone :: NobodyHasAgency StDone exclusionLemma_ClientAndServerHaveAgency :: ClientHasAgency st -> ServerHasAgency st -> Void exclusionLemma_ClientAndServerHaveAgency ClientHasAgency st TokIdle ServerHasAgency st tok = case ServerHasAgency st tok of {} exclusionLemma_NobodyAndClientHaveAgency :: NobodyHasAgency st -> ClientHasAgency st -> Void exclusionLemma_NobodyAndClientHaveAgency NobodyHasAgency st TokDone ClientHasAgency st tok = case ClientHasAgency st tok of {} exclusionLemma_NobodyAndServerHaveAgency :: NobodyHasAgency st -> ServerHasAgency st -> Void exclusionLemma_NobodyAndServerHaveAgency NobodyHasAgency st TokDone ServerHasAgency st tok = case ServerHasAgency st tok of {} deriving instance Show (Message PingPong from to) instance Show (ClientHasAgency (st :: PingPong)) where show :: ClientHasAgency st -> String show ClientHasAgency st TokIdle = String "TokIdle" instance Show (ServerHasAgency (st :: PingPong)) where show :: ServerHasAgency st -> String show ServerHasAgency st TokBusy = String "TokBusy"