Protocol Parameters Proposals
I am still not happy with the any of the current proposals for protocol parameters. This issue is supposed to serve as a place to gather all proposals and evaluate them.
I use interpC
as a shorthand for bool -> loc -> state -> val -> vPred
in some places.
Proposal 1.: Add a new parameter to the type of protocol interpretations
The current type of protocol interpretations is bool -> loc -> state -> val -> vPred
. The original type – before I removed protocol parameters – was InfoT -> bool -> loc -> state -> val -> vPred
. This design lends itself well to the following syntax for protocol assertions: [PP l : s | τ @ (x1, x2)]
, where (x1,x2)
are a pair of values of countable types which are implicitly encoded to InfoT
by the notation.
Equality on Parameters
The lemmas for combining protocol assertions would yield an equality on the encoding of (x1, x2)
. Some plumbing with typeclasses or canonical structures could probably recover equalities on the values of x1
and x2
automagically.
Interaction with Recursive Protocols
In the only example we have for recursive protocols with parameters, the Michael-Scott queue, the coq parameter γ
is also a protocol parameter (in the sense that we want to make use of the equality on γ
). However, γ
is also needed during the construction of the fixpoint and should be of type ghost name – not an arbitrary InfoT
as that would lead to annoying boilerplate to deal with non-decodable values. I see no workaround to avoid boilerplate here. Thus, while not impossible, this proposal is inconvenient when dealing with recursive protocols.
Proposal 2.: Make protocol interpretations announce their parameters
This proposal would change the type of protocol interpretations to interpC × InfoT
. The second component signifies parameters given to the interpretation. The benefit of this proposal is that the syntax of protocol assertions would be unchanged: an interpretation comes with its own parameters.
Equality on Parameters
Just as before, the lemmas yield equalities on encodings. However, we know that the encodings are of a specific form dictated by the interpretation itself. This should simplify the automatic recovery of equalities on the actual types.
Interaction with Recursive Protocols
This proposal interacts very nicely with recursive protocols. The MS queue example would simply announce encode γ
as its parameter.
Drawbacks
This changes the type of protocol interpretations in a way that might be hard to motivate without giving the technical details outlined above.