Experiment with a custom `Sing` type family and `SingI` instances.

[coot]

We can have something like

class Protocol ps where

  -- | The messages for this protocol. It is expected to be a GADT that is
  -- indexed by the @from@ and @to@ protocol states. That is the protocol state
  -- the message transitions from, and the protocol state it transitions into.
  -- These are the edges of the protocol state transition system.
  --
  data Message ps (st :: ps) (st' :: ps)

  -- | Associate an 'Agency' for each state.
  --
  type StateAgency (st :: ps) :: Agency

  -- | A protocol state token, i.e. a term level representation of type level
  -- state (also known as a singleton).
  --
  type StateToken :: ps -> Type

-- | An association from type level states to term level 'StateToken's.
--
class StateTokenI (st :: ps) where
  stateToken :: StateToken st

It would be nice to be able to declare something like:

-- using `QuantifiedConstraints`
class (forall (st :: ps). StateTokenI st) => Protocol ps where ...

But the problem is that there's no nice way to provide an evidence for the QuantifiedConstraint. StateTokenI instance must be defined per state, not in bulk, unless we do something ugly like:

data PingPong = Idle | Busy | Done
  deriving Typeable

data SingPingPong (st :: PingPong) where
  SingIdle :: SingPingPong Idle
  SingBusy :: SingPingPong Busy
  SingDone :: SingPingPong Done

instance Typeable st => StateTokenI (st :: PingPong) where
  stateToken =     case eqT @st @StIdle of
    { Just Refl -> SingIdle
    ; Nothing   -> case eqT @st @StBusy of
    { Just Refl -> SingBusy
    ; Nothing   -> case eqT @st @StDone of
    { Just Refl -> SingDone
    ; Nothing   -> error "impossible"
    }}}

[coot]

Another drawback of using custom StateToken is that for ChainSync we will still need to use singletons.

data SingNextKind (k :: StNextKind) where
  SingCanAwait  :: SingNextKind StCanAwait
  SingMustReply :: SingNextKind StMustReply

-- we cannot use `StateTokenI` as `SingNextKind` is defined outside of the scope of `Protocol` -- type class.
type instance Sing = SingNextKind
instance SingI StCanAwait  where sing = SingCanAwait
instance SingI StMustReply where sing = SingMustReply

instance Protocol (ChainSync header point tip) where
  data Message ...
  type StateAgency ...
  data StateToken (k :: ChainSync header point tip) where
    SingIdle      :: StateToken StIdle
    SingNext      :: SingNextKind k
                  -> StateToken (StNext k)
    SingIntersect :: StateToken StIntersect
    SingDone      :: StateToken StDone

instance StateTokenI StIdle      where stateToken = SingIdle
instance SingI k =>
         StateTokenI (StNext k)  where stateToken = SingNext sing
instance StateTokenI StIntersect where stateToken = SingIntersect
instance StateTokenI StDone      where stateToken = SingDone

Furthermore we cannot just use something like withSingI, which implementation. is rather tricky. withSingI is actually a useful tool, here is a showcase example in ChainSync's codec.

I think it's better to use SingI from singletons, but it means we will also need to use Sing. We still could include the StateToken data family as part of the Protocol class but one will need to provide Sing and SingI instances for it outside of the Protocol class.

[coot]

Although I don't see how to define Sing instance, obviously this will overlap with everything:

type instance Sing = StateToken

in some cases this will probably work:

type instance Sing = StateToken @PingPong

but this will not:

type instance Sing = StateToken @(ReqResp req resp) -- req and resp are not defined.

So we're left with the singletons defined out of the scope of Protocol type class.

[coot]

This leads me to the following idea:

class Protocol ps where
  data Message ps (st :: ps) (st' :: ps)
  type StateAgency (st :: ps) :: Agency

  -- | A 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

• Protocol type class requires all data types (Message and StateToken) and the type StateAgency type family
• It does not require Sing and SingI instances as constraints, although they must be provided.
• We can use withSingI and other singletons goodies.