-
Notifications
You must be signed in to change notification settings - Fork 6
Typed Protocols vs Categories
Typed Protocols allow to encode protocol state machines using simple (caugh, caugh) api: the Peer
type. Peer
has some disadvantages though.
One that comes up from time to time is that Peer
, by being a recursive data structure, is not compositional as categorical arrows are. So could there be a more composable API of typed-protocols
build around categories? The advantage of something like the Category
type class, is the .
operator which allows to combine two simpler arrows into one. This gives a chance for a maintainer of a protocol to split a protocol into smaller chunks, or even build composable components from which different applications can be derived.
First of all, to describe a protocol one needs to types of arrows, one which can be interpreted as sending a message and another as receiving one:
data ProtocolArrow ps pr st st' where
Send :: forall ps pr (st :: ps) (st' :: ps).
( SingI st
, SingI st'
, ActiveState st
)
=> WeHaveAgencyProof pr st
-> Message ps st st'
-> ProtocolArrow ps pr st st'
-- as with `Peer` we use existential variables, so the remote peer decides
-- the next state. `Recv` is recursive.
Recv :: forall ps pr (st :: ps) (st'' :: ps).
( SingI st
, ActiveState st
)
=> TheyHaveAgencyProof pr st
-> (forall (st' :: ps). Message ps st st' -> ProtocolArrow ps pr st' st'')
-> ProtocolArrow ps pr st st''
Compose :: ProtocolArrow ps pr st st'
-> ProtocolArrow ps pr st' st''
-> ProtocolArrow ps pr st st''
compose :: ProtocolArrow ps pr st st'
-> ProtocolArrow ps pr st' st''
-> ProtocolArrow ps pr st st''
compose = Compose
Now we can see that it's not really possible to construct a Peer
which:
arrowToPeer :: ProtocolArrow ps pr st st'
-> Peer ps pr NonPipelined Empty st m stm a
arrowToPeer (Send proof msg) = Yield proof msg undefined
-- this is not possible just
-- because of limitation of
-- `ProtocolArrow` which could
-- be improved
arrowToPeer (Recv proof k) = Await proof (\msg -> arrowToPeer (k msg))
arrowToPeer (Compose f g) = undefined
-- this is fundamentally not possible
-- `arrowToPeer f` cannot be composed with
-- `arrowToPeer g`!
But that's ok, it doesn't mean the ProtocolArrow
api cannot be developed further. It's also not possible to write:
peerToArrow :: Peer ps pr NonPipelined Empty st m stm a
-> SomeProtocolArrow ps pr st
peerToArrow (Yield proof msg k) =
case peerToArrow k of
SomeProtocolArrow k' ->
SomeProtocolArrow (Compose (Send proof msg) k')
peerToArrow (Await proof k) =
SomeProtocolArrow $ Recv proof $ \msg ->
case peerToArrow (k msg) of
SomeProtocolArrow k' -> undefined -- k'
-- • Couldn't match type ‘st'0’ with ‘st'1’
-- Expected: ProtocolArrow ps pr st' st'0
-- Actual: ProtocolArrow ps1 pr st' st'1
-- because type variable ‘st'1’ would escape its scope
-- This (rigid, skolem) type variable is bound by
-- a pattern with constructor:
-- SomeProtocolArrow :: forall {ps1} ps2 (pr :: PeerRole) (st :: ps1)
-- (st' :: ps1).
-- ProtocolArrow ps2 pr st st' -> SomeProtocolArrow ps2 pr st,
-- in a case alternative
-- at src/Network/TypedProtocol/Composition.hs:72:9-28
And still it doesn't mean that the ProtocolArrow
cannot be developed into feature full solution. But both quite convincingly demonstrate that the standard notion of composition is not compatible with a Peer
.
The code comes from the coot/idea-protocolarrows branch.