The structs in this module enumerate the shapes of all expressible sessions.
💡 Generally speaking, users of Dialectic (that’s you!) don’t need to write these types
directly; it’s more readable to instead use the Session! macro to
specify a session type.
The traits in this module are used to implement the session type system rules, and generally do
not need to be referred to directly from code that uses this library. All of them are sealed, so
that they can only ever apply to the session types defined in this crate. If you want to state
the bound that a type is a session type, use the Session trait rather
than any of these bounds individually.
| Call | Call the session P as a subroutine using call, then do the session Q.
|
| Choose | Actively choose between any of the protocols in the tuple
Choices.
|
| Continue | Repeat a Loop. The type-level index points to the loop to be repeated, counted from the
innermost starting at 0.
|
| Done | A finished session. The only thing to do with a Chan when it is Done is to
drop it or, preferably, close it.
|
| Loop | Label a loop point, which can be reiterated with Continue.
|
| Offer | Passively offer! a choice between any of the protocols in the tuple Choices.
|
| Recv | Receive a message of type T using recv, then continue with
protocol P.
|
| Send | Send a message of type T using send, then continue with
protocol P.
|
| Split | Split the connection into send-only and receive-only halves using split.
|
| Actionable | Each session type has a canonical Actionable::NextAction, the session type which corresponds
to the next thing to do on the channel. For most types, this is the same as Self, but for
control constructs like Loop, this corresponds to the inside of the Loop.
|
| EachHasDual | In the Choose and Offer session types, we provide the ability to choose/offer a list of
protocols. The sealed EachHasDual trait ensures that every protocol in a type level list of
protocols HasDual.
|
| EachLift | Analogously to EachSubst, this trait allows iteration/mapping of the Then transform
over a type level list.
|
| EachScoped | In the Choose and Offer session types, we provide the ability to choose/offer a list of
protocols. The sealed EachScoped trait ensures that every protocol in a type level list of
protocols is Scoped.
|
| EachSubst | In the Choose and Offer session types, we provide the ability to choose/offer a list of
protocols. The sealed EachSubst trait ensures that every protocol in a type level list of
protocols can Subst.
|
| EachThen | Analogously to EachSubst, this trait allows iteration/mapping of the Then transform
over a type level list.
|
| HasDual | Each session type has a HasDual::DualSession, the type of the corresponding client on the
other side of the channel. The sealed trait HasDual enumerates these types, and provides the
dual of each.
|
| Lift | For every “open” Continue (i.e. with an index larger than the number of Loops that
contain it), increment its index by N.
|
| Scoped | A session type is Scoped if none of its Continues refer to outside of the
Loops which they are within.
|
| Select | Select by index from a type level list.
|
| Subst | Substitute P for every Continue referring to the outermost scope in the given session
type.
|
| Then | Substitute P for every Done in Self, thus concatenating the session P to Self.
|