Monadic local state transitions

[coot]

Currently we expose Await of this shape:

  Await
    :: forall ps pr (st :: ps) f m a.
       ( StateTokenI st
       , ActiveState st
       )
    => TheyHaveAgencyProof pr st
    -- ^ agency singleton
    -> (forall (st' :: ps).
           f st
        -- ^ associated local state to the source protocol state 'st'
        -> Message ps st st'
        -> ( Peer ps pr st' f m a
           , f st'
           )
         -- ^ continuation and associated local state to the target protocol
         -- state `st'`
       )
    -- ^ continuation
    -> Peer ps pr st f m a

It only allows for pure transitions of local state, e.g. f st -> f st'. We argue that this isn't actually a major limiting factor. The transition f st -> f st' has access to Message ps st st' which might contain information we want to contain in the local state (as we do in the ReqResp example). The local state hasn't been designed to store another type of information (e.g. IO state), which can be preserved by other means, although it won't be available in the codecs.