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

input-output-hk · Jul 25, 2024 · 15dbb3c · 15dbb3c
1 parent 3bba149
commit 15dbb3c
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 0 deletions.
diff --git a/typed-protocols-examples/src/Network/TypedProtocol/PingPong/Type.hs b/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)
diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp/Type.hs b/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)

diff --git a/typed-protocols-examples/src/Network/TypedProtocol/ReqResp2/Type.hs b/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)

diff --git a/typed-protocols-examples/src/Network/TypedProtocol/Trans/Wedge.hs b/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

diff --git a/typed-protocols/src/Network/TypedProtocol/Core.hs b/typed-protocols/src/Network/TypedProtocol/Core.hs
@@ -49,6 +49,8 @@ module Network.TypedProtocol.Core
   , IsActiveState (..)
   , ActiveState
   , notActiveState
+    -- * Utils
+  , stateToken
   ) where
 
 import           Data.Kind (Constraint, Type)
@@ -404,6 +406,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