Skip to content

Explicit "unsafe" in session type language #80

@plaidfinch

Description

@plaidfinch

Currently, if one needs to escape the session typing regimen temporarily, there is no way to do so while retaining the drop guards which are necessary to continue in over/split/call. Additionally, there is no marker in the type system to point at locations in a protocol where extra scrutiny is required due to departure from the listed session type.

Both of these issues can be allayed by the introduction of:

  • a new session type constructor, Unsafe<P> (only parameter is continuation, since its innards are opaque),
  • its corresponding Session! macro keyword unsafe; (no block, since its innards are opaque), and
  • a new method on Chan<S, Tx, Rx>:
async fn unsafe_with<F, Fut>(
    self, F
) -> (
    Fut::Output,
    Result<Chan<P, Tx, Rx>, IncompleteSession<Tx, Rx>>
)
where
    S: Session<Action = Unsafe<P>>
    F: FnOnce(DropGuard<Tx>, DropGuard<Rx>) -> Fut,
    Fut: Future
{
    // Call function on the drop guards for the transport ends, recover the transport ends or return an error.
}

In the above, DropGuard<T> is similar to the existing pattern in Dialectic of pairing a T with an Arc<Mutex<Result<T, IncompleteHalf<T>>>> and a Drop implementation that places T in the mutex. In the case of DropGuard, we don't need to worry about the case of an unfinished session, since Unsafe doesn't specify what session completion means. Thus, DropGuard should contain merely an Arc<Mutex<Option<T>>>. We can then implement Deref and DerefMut for DropGuard, allowing it to be used however the underlying Tx/Rx can be—including as the transmitter/receiver for a new Chan. This last ability means that Unsafe can crucially be used to nest protocols with different ways of using the underlying transport: for instance, to use different encodings/framings for messages in different parts of a protocol, or to embed a multiplexed subprotocol in a larger protocol, per the multiplexing backend described in #79.

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions