typed-protocols: added StateToken type family to Protocol type class

Author: coot

typed-protocols-examples/src/Network/TypedProtocol/PingPong/Type.hs

@@ -76,5 +76,7 @@ instance Protocol PingPong where
   type StateAgency StBusy = ServerAgency
   type StateAgency StDone = NobodyAgency
 
+  type StateToken = SPingPong
+
 
 deriving instance Show (Message PingPong from to)

typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Type.hs

@@ -46,6 +46,8 @@ instance Protocol (ReqResp req resp) where
   type StateAgency StBusy = ServerAgency
   type StateAgency StDone = NobodyAgency
 
+  type StateToken = SReqResp
+
 
 deriving instance (Show req, Show resp)
                => Show (Message (ReqResp req resp) from to)

typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Type.hs

@@ -55,6 +55,8 @@ instance Protocol (ReqResp2 req resp) where
   type StateAgency StBusy' = ServerAgency
   type StateAgency StDone  = NobodyAgency
 
+  type StateToken = SReqResp2
+
 
 deriving instance (Show req, Show resp)
                => Show (Message (ReqResp2 req resp) from to)

typed-protocols-examples/src/Network/TypedProtocol/Trans/Wedge.hs

@@ -105,6 +105,8 @@ instance Protocol (Wedge ps (stIdle :: ps) ps' (stIdle' :: ps')) where
     type StateAgency (StFst st) = StateAgency st
     type StateAgency (StSnd st) = StateAgency st
 
+    type StateToken = SingWedge
+
 
 type PingPong2 = Wedge PingPong.PingPong PingPong.StIdle
                        PingPong.PingPong PingPong.StIdle

typed-protocols/src/Network/TypedProtocol/Core.hs

@@ -47,6 +47,8 @@ module Network.TypedProtocol.Core
   , IsActiveState (..)
   , ActiveState
   , notActiveState
+    -- * Utils
+  , stateToken
   ) where
 
 import           Data.Kind (Constraint, Type)
@@ -402,6 +404,16 @@ class Protocol ps where
   --
   type StateAgency (st :: ps) :: Agency
 
+  -- | A type alias for protocol state token, e.g. term level representation of
+  -- type level state (also known as singleton).
+  --
+  type StateToken :: ps -> Type
+
+-- | An alias for 'sing'.
+--
+stateToken :: (SingI st, Sing st ~ StateToken st) => StateToken st
+stateToken = sing
+
 type ActiveAgency' :: ps -> Agency -> Type
 data ActiveAgency' st agency where
   ClientHasAgency :: StateAgency st ~ ClientAgency