Giter Club home page Giter Club logo

dialectic's Introduction

Dialectic

Rust license: MIT crates.io docs.rs documentation

dialectic (noun): The process of arriving at the truth by stating a thesis, developing a contradictory antithesis, and combining them into a coherent synthesis.

dialectic (crate): Transport-polymorphic session types for asynchronous Rust.

When two concurrent processes communicate, it's good to give their messages types, which ensure every message is of an expected form.

  • Conventional types merely describe what is valid to communicate.
  • Session types describe when it is valid to communicate, and in what manner.

This crate provides a generic wrapper around almost any type of asynchronous channel that adds compile-time guarantees that a specified session protocol will not be violated by any code using the channel. Such a wrapped channel:

  • has almost no runtime cost in time or memory;
  • is built on async/.await to allow integration with Rust's powerful async ecosystem;
  • gracefully handles runtime protocol violations, introducing no panics;
  • allows for full duplex concurrent communication, if specified in its type, while preserving all the same session-type safety guarantees; and
  • can even implement context free sessions, a more general form of session type than supported by most other session typing libraries.

Together, these make Dialectic ideal for writing networked services that need to ensure high levels of availability and complex protocol correctness properties in the real world, where protocols might be violated and connections might be dropped.

Dialectic supports a number of async runtimes and backends out-of-the-box, if you don't want to or don't need to write your own:

These crates also serve as good references for writing your own backends.

What now?

dialectic's People

Contributors

marsella avatar plaidfinch avatar sdleffler avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

dialectic's Issues

Try lifting `Session<Action = _>` bounds into `impl` for better errors

Currently, the Action for methods on Chans is restricted in the where-clause of the methods themselves. This means that errors involving session type mismatches restate the full session type of the expected session in a way that can be hard to parse. It's possible that moving this bound upward to the enclosing impl block for each method would cause these errors to be easier to read. This change will require each method to be enclosed in its own impl block.

Upsides:

  • better error messages?

Downsides:

  • documentation will become more verbose, because there will be more separate impl blocks
  • potentially it won't actually improve error messages?

Proc-macro DSL for protocol/session type specifications

Just making a few notes out of our (my and @kwf's) discussion on syntax for a proc macro language to specify Dialectic protocol types. Here's a sample taken from our discussion, a translation of the session types from the tally.rs example:

session!(
    priv type ClientTally =
        loop {
            choose {
                _0 => send(i64),
                _1 => {
                    recv(i64);
                    break;
                },
            }
        };

    type Client =
        loop {
            choose {
                _0 => break,
                _1 => {
                    send(Operation);
                    call(ClientTally);
                },
            }
        };
);

A couple critical things we noticed:

  • Without full knowledge of any other session types, we can't make intelligent substitutions of those types into the definitions of some given other session type (e.g. substituting ClientTally into Client), and the only other way to reference an external session type is to use the Call type. To solve this, we think it would be a good idea to allow multiple definitions of session types within a single proc-macro (session!) call, which allows splitting session types into multiple "subroutines" without having to use the Call type, as with full knowledge of their definitions they can be directly spliced into the points where they are referenced.
  • The difference in looping semantics between the proposed macro DSL and current type implementation means that nontrivial (but not extremely difficult) analysis needs to be done to "compile" the macro DSL's continue-by-default semantics to the type-level implementation's break-by-default semantics.
  • The Split type, while practically useful, adds nothing in terms of semantics, so an initial implementation of the DSL can ignore it (and a solid implementation as we discussed should make it easy to add.)

With that out of the way, here's a rough overview of the syntax as we discussed it:

  • Types are to be defined as (priv | pub)? type = <statement>;, where priv indicates a type which should not be compiled to a Rust type definition, whether public to other modules or not. priv types are intended to be directly substituted into other, non-priv session types defined in the same session! macro call.
  • Statements (or should we call them expressions?) look a lot like a subset of Rust value expressions, with a few extra syntactic constructs. In short, loop, continue, and break act roughly as you would expect in Rust. choose and offer use match-like syntax, look identical to each other, and operate much like the offer! macro. Finally recv, send, and call are used w/ a function-like syntax to represent instances of the Send, Recv, and Call types. In addition, while call can be used to generate a Call type referring to an "externally" or "internally" defined "subroutine" session type, an internally defined session type (such as ClientTally in the example above, which is "internally" defined with respect to the Client session type) can be directly substituted in place of a "block", similarly to break in the choose statement (expression?) inside Client.
  • Compilation will be a two-stage process, parsing the DSL into an AST, lowering that AST into an intermediate representation which maps directly to the break-by-default semantics of the type-level representation while performing substitutions of internal references to other session types, and then lowering that IR into Rust code to be quasiquoted into the calling program. During this compilation process we can emit errors for things like attempts to directly substitute in definitions of session types which are external to the current session! invocation, etc.

With that in mind, parsing will likely be done carefully w/ syn, and since ASTs will be very small (less than 1k nodes generally) it doesn't make much sense to prematurely optimize allocation. We'll start with a fairly naive Box-everywhere representation and move on from there.

Improve type error presentation

We might be able to improve how type errors are presented to the user. There are a couple avenues forward:

  • Pretty-formatter for dialectic types that reverse-compiles them back to Session! invocations
  • Work with Rust upstream to use some manner of custom type error

These two could be paired together!

Control flow analysis pass for macro compiler

Session! macro invocations that contain "dead code"—that is, surface syntax which would be compiled to nothing, can be written and parsed, but we should not allow them, to avoid confusion. For instance, consider the type:

type NeverSends0 = Session! {
    loop {
        recv ();
        continue;
        send ();
};

The macro compiler must translate this to the session type Loop<Recv<(), Continue>>, but this is confusing to the end user because while they wrote send (), it never occurs in the type. Such dead code should be marked by the macro. Unfortunately, we can't generate a warning (as Rust does in value-level dead code), so instead we should generate an error.

Naively, we might imagine we could avoid such situations by scanning all Blocks in the IR AST to see whether they contain continue or break statements that are not at their end, but this is not sufficient. Consider the following:

type NeverSends1 = Session! {
    loop {
        recv ();
        offer {
            _0 => continue,
            _1 => break,
        };
        send ();
};

This would compile to Loop<Recv<(), Offer<(Continue, Done)>>>. The naive analysis above would not identify this case because neither continue nor break occur in the middle of a block in this macro invocation. What is needed is true control flow analysis.

The analysis must run before the elimination of Break nodes, because that pass itself slices out sections of dead code and makes them unreachable. Additionally, if any errors are discovered in this pass, we should not proceed to eliminate Break nodes, as this would remove the very error nodes inserted by this pass! We need to produce to the user both the errors generated during this pass and all others currently embedded in the AST.

A related control flow analysis which could be bundled in this pass: session types are only impl Session if all their loops are productive: that is, there is at least one real action (something other than Loop) between the loop head and the Continue that points to it. If this is not the case, a rather obscure constraint solver overflow error occurs. We could detect this error during this pass, and report it, improving diagnostics for users.

Ensure channel_id is actually unique

Currently, merchant_channels.channel_id is not guaranteed to be unique in the very unlikely case there is a hash collision. It would be very easy to address this:

during establishing the last step before generating channel id is making merchant randomness
the merchant could check if the resultant id would be a duplicate and regenerate the randomness if so
loop until its unique
then send the randomness

Also, add the unique constraint to the db index.

Benchmark offer/choose

In so doing, double-check that the proc-macro version of offer! is actually faster than the old version.

Implement type-level substitution of an arbitrary (open) session type for `Done`

In order to support the development of the session! macro to fulfill #30, we need to implement a more general form of type-level substitution, namely substituting an arbitrary session type for Done to "extend" a session. This is needed because the ; operator in the macro language does not necessarily have the information to expand out a type synonym within the context of the macro invocation, since the type could be defined elsewhere, yet it needs to substitute the continuation (everything after the ;) for every Done in the preceding type.

This must be implemented for even open session types like Continue. For instance, imagine the following:

type P = session!(send i64);
type Q = session!(recv bool);
type S = session!(loop { P; Q });

In this example, we would want to compile to:

type P = Send<i64, Done>;
type Q = Recv<bool, Done>;
type S = Loop<Send<i64, Recv<bool, Continue>>>;

This requires us to substitute Continue for Done in Q (due to the fact that our macro language implicitly loops if not break-ed), and then Q for Done in P.

Note that the de Bruijn index associated with the Continue is not incremented as it is substituted, because the types of P and Q don't contain Loops, but in general an auxiliary function to increment de Bruijn indices in the substituted terms is necessary to make Continues point to the correct place.

Make serialization non-dependent on serde

Currently, dialectic-tokio-serde requires precisely a Serialize + DeserializeOwned bound. This can be made more generic, to enable, for instance, custom serialization approaches or whitelists of allowed types.

At present, the Serializer and Deserializer traits are:

pub trait Serializer {
    type Error;
    type Output;
    fn serialize<T: ?Sized + Serialize>(&mut self, item: &T) -> Result<Self::Output, Self::Error>;
}

pub trait Deserializer<Input> {
    type Error;
    fn deserialize<T: for<'a> Deserialize<'a>>(&mut self, src: &Input) -> Result<T, Self::Error>;
}

This could be changed to:

pub trait Serializer {
    type Error;
    type Output;
}

pub trait SerializerFor<T>: Serializer {
    fn serialize(&mut self, item: &T) -> Result<Self::Output, Self::Error>;
}

pub trait Deserializer<Input> {
    type Error;
}

pub trait DeserializerFor<Input, T>: Deserializer<Input> {
    fn deserialize(&mut self, src: &Input) -> Result<T, Self::Error>;
}

This would separate the crate entirely from a dependency on Serde, allowing downstream crates to depend on it if necessary, but also to use their own serialization strategies while still sharing the framing/encoding logic in this crate. Additionally, it allows for the creation of wrapper Serializer/Deserializer structs which wrap an existing such Serializer/Deserializer but restrict its instance further, for instance to enforce a whitelist of permitted types.

Procedural macro for simplifying session type definitions

It would be a fantastic thing to have a procedural macro that compiles a DSL using Rust value-level syntax (sort of) into a session type. Something like:

type Protocol = session!(
    i64!
    'outer: loop {
        String!
        loop {
            bool?
            { break 'outer
            | break
            | i8? + continue
            }
        }
        u8!
    }
    Vec<bool>! & String?
    i128!
);

should compile to the session type:

type Protocol =
    Send<i64,
        Loop<
            Send<String,
                Loop<
                    Recv<bool,
                        Offer<(
                            Split<
                                Send<Vec<bool>,
                                    Send<i128,
                                        End
                                    >
                                >,
                                Recv<String,
                                    Send<i128,
                                        End
                                    >
                            >,
                            Send<u8, Recur<S<Z>>>,
                            Choose<(
                                Recv<i8,
                                    Recur<Z>
                                >,
                                Recur<Z>,
                            )>
                        )>
                    >
                >
            >
        >
    >;

Notable things going on here:

  • The ? and ! operators, as customary with session type notation, indicate Recv and Send respectively. (Should we pick something else given the meaning of ? in Rust?)
  • loops automatically Recur unless a break is encountered, just like in Rust (as opposed to in the current type syntax which requires manual noting of all recur points)
  • continue can be used to explicitly recur to the head of a loop
  • loop heads can optionally be named, just like in Rust, and you can break out of a named loop, rather than using an index
  • Offer is denoted with | and has lowest precedence of any operator
  • Choose is denoted with + and has higher precedence than | but less than anything else
  • Split is denoted with & and has higher precedence than |, +, and sequential composition, but less than the unary primitive operators
  • Anything after a loop is substituted in for break

For modularity, there needs to be the ability to use session types defined outside the block. Proposal for syntax:

type Swap<T, U> = session!(
    T! & U?
);

type SwapMany<T, U> = session!(
   loop {
      Swap<T, U> | break
   }
);

This would translate to:

type Swap<T, U> =
    Split<Send<T, End>, Recv<U, End>>;

type SwapMany = Loop<Offer<(Then<Swap<T, U>, Recur<Z>>, End)>>;

...where Then needs to be a new type-level function substituting its second argument for End in the input.

We also need to decide how to handle session types that are parameterized by other session types. For instance, I think the following should be valid:

type StreamThen<T, P> = session!(
    loop {
        T! + break
    }
    P
);

type OfferStreams<T> = session!(
    loop {
        StreamThen<T, continue | break>
    }
);

...which should translate to:

type StreamThen<T, P> =
    Loop<Choose<(Send<T, Recur>, P)>>;

type OfferStreams<T> =
    Loop<StreamThen<T, Offer<(Recur<_1>, End)>>>;

But this is tricky! Naively substituting Recur instead of Recur<_1> would have meant that the wrong loop was entered! How do we solve this?

  • We could ban non-closed session types as parameters... how to enforce?
  • Potentially by changing the environment parameter to a stack of environments and adding Push/Pop instructions (that would only ever get emitted by this macro)? This would mean:
    type OfferStreams<T> =
        Loop<Push<StreamThen<T, Pop<Offer<(Recur<Z>, End)>>>>;

There's a lot going on to translate this natural syntax to the corresponding type!

Refactor backend traits to decrease where-clause bloat in generic situations

Currently, when writing code generic over backend transports Tx and Rx, we have to state a variety of bounds about these. Absent stable specialization or an equivalent of Haskell's constraint kinds (trait-associated-traits?), we can't compute these bounds in the where-clause itself, which means the developer is left to write them, mechanistic though they may be. To ease this burden, a proposal:

  • Create two new traits, TransmitChoices and ReceiveChoices, whose supertrait bounds require that Self: Transmit<Choice<N>, Val> or Self: Receive<Choice<N>> for N from 0 through 255. These can be used in place of manually noting that a transport supports each arity in a given session type, e.g. Tx: TransmitChoices or Rx: ReceiveChoices. The definition and implementation of these extension traits probably should be done with a teensy proc macro.
  • Create two new traits Transmitter and Receiver, each with an associated Error type, as supertraits of Transmit<T, Convention> and Receive<T>, removing the associated Error type from those subtraits. This uniformization of errors across all sent/received types means that larger session types will not incur larger sets of Into<E> constraints when the ? operator is used on their results. Instead, a single Tx::Error: Into<E> or Rx::Error: Into<E> constraint may be used, for whatever error type E is the top-level error.
  • Optionally, create an fn-item-level attribute macro that slaps these constraints as well as Transmit<T> / Receive<T> constraints for specified lists of types into the where-clause of the given function item, as a more succinct syntax for specifying these bounds.

Enumerative and random testing for macro compiler

In support of #36, we want enumerative testing to test both the parser and the code generation of the macro compiler. Two different testing regimens are suggested:

  • Test in the dialectic-compiler crate that (1) parse ; print is idempotent and (2) print ; parse is identity. This can be accomplished with random testing, which will cover more cases more efficiently than enumeration testing.
  • Test in the dialectic crate that valid invocations of the Session! macro result in valid session types satisfying the Session trait. This can be done using build.rs to enumerate such invocations at compile time.

Tentatively, if we build a decompiler (which would also be useful for parsing error messages), we could test that (1) compile ; decompile is idempotent and (2) decompile ; compile is identity, also in the dialectic-compiler crate, also using random testing. However, this requires building a decompiler, which we may wish to postpone.

[transmit-case] Ergonomics for `Choice<N>` bounds

Just dumping some thoughts from DMs into a more permanent location.

Currently the issue is that Choice<N> is treated specially when it cannot be, as it is quantified
and the vast majority of types which will be sent via TransmitCase will not be. At current, the
TransmitCase impl for Choice<N> is for all types Choice<LENGTH> for all const LENGTH: usize,
given a TransmitChoice impl. If we keep TransmitCase, add a NotChoice<T> type used for
transmitting non-Choice<N> types, and then add an impl for TransmitCase<NotChoice<T>>
where T: Match + Transmittable, Self: Transmit<T> and then seal TransmitCase, we can provide two
functions for choose which work for Choice<N> and NotChoice<T>. In this case it becomes very
clear how Choice and non-Choice case choosing is so different; they are of different kinds,
specifically one is a parameter of the const usize kind and the other is a type.

However, unless we extend this sealed type distinction to the type-level session language, we are
now forced to have two different variations of the offer! macro. So I propose the following:

  • Restrict types allowed in Choose and Offer types to Choice<N> and NotChoice<T>.
  • Generate the appropriate output type from the Session! macro, which has the necessary
    information to deal with this.
  • Implement Match for NotChoice<T> transparently delegating to the wrapped value.

Given this, the same offer! will happily work for both cases. And we would likely also be able to
have a single implementation of choose that works for both cases as well.

Support batching backends

More efficient backends may wish to batch messages transparently. This can be enabled by adding a flush async method to Transmitter with a default implementation of doing nothing. Invoking recv-requiring methods on Chan will implicitly call flush first (or concurrently?) to ensure communication dependency ordering is preserved. It's also necessary to call flush implicitly before split, since the concurrent receiving half might be waiting for a response to something already sent. A new method on Chan should be added which manually invokes flush, too. Finally, close should be made an async function, and it should call flush prior to dropping the channel, but only if there are no other references to the Arc awaiting the Tx—i.e., the transmitter should be automatically flushed on close only when the session is not going to be resumed by an outer context.

For non-batching backends, no code changes are necessary. Uses of close will need to be changed to be async.

The primary use case for this would be in the serde backend, which could now support a BufferedSender/BufferedReceiver pair, parametrized by all the parameters of the underlying transport for the non-buffering variety, as well as a maximum buffer size (which, if exceeded, triggers an automatic flush).

Tracking issue for macro compiler

This is a tracking issue for the macro-compiler-dev branch (PR #36).

  • Allow the user to omit commas for some statements of split/choose/offer constructs (#45)
  • Enumerative testing of the full macro compiler (nice to have but not necessary) (#40)
  • Random testing of the parser (#40)
  • Analyze control flow to report unreachable code and unproductive loops which would produce odd type errors (#41)
  • Write missing internal documentation for large and complex functions, especially transformations of the CFG
  • Write README documenting the whole compiler, including CFG passes and what they do/how they work and what invariants are upheld

Remove needless feature flags

I'm pretty don't need to replicate the underlying features of the serde backend modules, because they can be toggled by downstream users without our exposing them.

Explicit "unsafe" in session type language

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.

Multiplexing backend adapter

It may be desirable to convert a 1:1 "physical" connection on some backend into a set of N:N "logical" connections, each of which behaves as its own separate channel.

Proposal: two complementary wrappers around a pair of Tx/Rx that provides methods analogous to TCP. One wrapper, Acceptor, provides an accept method that awaits new connections; the other, Connector, provides a connect method that creates a new connection by generating a unique (at least, non-temporally-overlapping-on-this-connection) id and sends it. Ids could be generated by a Slab<()> or by the memory address of some pinned value that lasts the lifetime of the logical connection.

Use of the transmitter and receiver must be synchronized using one async mutex each, to ensure messages are fully sent.

Benchmark dialectic with null backend

In the benchmarks, also try benchmarking with a backend that just eats inputs and invents outputs, to measure merely the overhead of dialectic with almost nothing else happening.

Validity checking for sessions

Consider the following:

type S = Send<bool, Recv<bool, Done>>;
let Chan<S, (), ()> = S::wrap((), ());

This code currently typechecks in Dialectic, even though the unit type () has no implementation of Transmit or Receive, making it such that enacting the session on this channel is impossible. It is only when we try to invoke the send or recv methods on the Chan that the error about Transmit or Receive would be thrown. Although in this case, it's clear that () is a silly channel type, we could imagine other scenarios with complex session types and/or channel backends with complex invariants about what can be sent (i.e. serialization constraints), which would make it non-trivial to tell at a glance whether a given session is possible to fulfill on a given backend.

Proposal:

pub trait ValidFor<Tx, Rx>: Session {}

We could then require this bound on Chan, so that all Chans are known to be statically valid for the whole session, and can't get stuck.

Issues/complications:

  • The calling-convention polymorphism means there is more than one way to send a value, and it's not possible to know even from the combination of the backend and the session type which calling convention will be used. Only one of them might be valid, or multiple, or none. How can we handle this?
  • We will need to correctly handle Split, where it must be disallowed to send/choose from the receive-only end, and recv/offer from the send-only end.
  • Lack of constraint kinds means we can't prove that ValidFor<Tx, Rx> implies any particular other constraint. In particular, in contexts polymorphic over Tx and Rx, we'll have to always add ValidFor<Tx, Rx>... and then go on to list precisely the constraints that this entails on Tx and Rx, despite ValidFor implying them already.

`offer!` macro does not catch too-small arity

This compiles, but it shouldn't:

use dialectic::prelude::*;

type S = Session! {
    offer {
        0 => {}
    }
};

#[Transmitter(Tx)]
#[Receiver(Rx)]
async fn run<Tx, Rx, E>(chan: Chan<S, Tx, Rx>) -> Result<(), E>
where
    E: From<Tx::Error> + From<Rx::Error>,
{
    offer!(in chan {
        // no branches!!!
    })?
}

The current offer! macro (not on the carrier-type branch) does not catch this error, and indeed can't catch this error in the macro itself. This bug increases the urgency with which I would like to merge the carrier-type branch, because the offer! macro which integrates Vesta should catch this bug.

Backend wrapper restricted by an explicit allow-list

A backend wrapper could be created that is parameterized by an allow-list which statically prevents things from being sent/received that shouldn't be.

First, this setup would let you define a new marker type and enumerate a specific set of types which are allowed on the "allow list" denoted by that type.

/// A marker type standing in for allowing every type to be serialized/deserialized.
pub struct AllowAll;

/// A marker trait that indicates whether or not the type `T` belongs to the allow-list `Self`.
pub trait Allow<T> {}

/// The `AllowAll` marker type allows all types.
impl<T> Allow<T> for AllowAll {}

You would use it like so:

pub struct OnlyByteAndBool;

impl Allow<u8> for OnlyByteAndBool {}
impl Allow<bool> for OnlyByteAndBool {}

Because of trait coherence rules, nobody outside the crate in which OnlyByteAndBool can add another impl for OnlyByteAndBool: Allow<T> for some new T.

Then, this abstraction can be used to implement a general restriction mechanism for backends:

#[repr(transparent)]
struct Restricted<T, List = AllowAll>{
    inner: T,
    list: PhantomData<fn() -> List>,
}

Then, we would implement all the backend traits, forwarding their implementations, for Restricted, except adding the clause where List: Allow<T> to each impl.

Edited from the comment posted by @kwf in #107 (comment)

Alter documentation to introduce and use the Session! macro

The documentation should make use of the Session! macro, once it is introduced to the library.

Some outlying questions:

  • To what degree should "raw" session types occur in the reference documentation? Should they be shown in usage examples?
  • To what degree should "raw" session types occur in the tutorial? Just when first introducing a construct? Everywhere, in parallel, as a reminder? A mixture?

Examples should definitely be all converted to Session! invocations.

Allow sending types "as" other types

Currently, if we try to send say, an &str where the specification expects a String, we have to allocate a String in order to send it instead. This is somewhat un-ergonomic and forces the user to ignore certain Rust idioms if they need this use case with some kind of efficiency, because one can no longer pass around an &str instead of an &String for example.

Transition to using min_const_generics for user-facing type-level numbers

The min_const_generics feature of Rust stabilizes on March 25 some unknown date. This feature enables us to do away with the constants defined in dialectic::unary::constants and dialectic::unary::types, and instead use const generics to specify numbers in the user interface. Because const generics in the minimal formulation currently present do not do symbolic computation (i.e. compute on unknown constants), we still need to internally convert to unary numbers, but we can hide this from the user.

This change involves:

  • The signature of Chan::choose will now take a turbofish-specified const generic argument rather than a value-level ZST representing a unary number, leading to syntax like chan.choose::<1>() over the previous chan.choose(_1).
  • The surface syntax of the offer! macro will take normal integer literals in its arms, not underscore-prefixed ones.
  • The surface syntax of the choose and offer constructs in the Session! macro will also take normal integer literals in their arms, not underscore-prefixed ones.
  • The de Bruijn index type argument of Continue will become a const generic argument rather than a unary number.
  • The upper bound type argument of Choice will become a const generic argument rather than a unary number.
  • The modules dialectic::unary::types and dialectic::unary::constants will entirely be removed.
  • A new sealed trait, ToUnary, will be introduced, which has a single associated type with a Unary bound. Each constant from 0 to 128 will be given an implementation of this trait (we can do more, but that's all we need for now), auto-generated by a new procedural macro exposed by the dialectic-macro crate.
  • The various bounds requiring arguments which have changed per above from unary numbers to const generics will be updated from Unary to ToUnary, and various types referring to those unary numbers will need to be updated to use the converted unary number rather than the type parameter directly.
  • Documentation and tests, including the tutorial, item documentation, quick reference, and examples, will need to be updated to reflect the new interface.

From how I see it, this breaks down into several phases, in this order:

  1. Switch our development process temporarily to using the beta compiler, including updating our CI infrastructure to use the beta channel. This will be reverted once min_const_generics lands on stable.
  2. Change the surface syntax of Session! and offer! to use non-underscore-prefixed numerals, and alter their documentation and associated tests to match (including tutorial).
  3. Define the ToUnary trait and the procedural macro to generate all its instances. Document and test.
  4. Change the generic parameter of Continue to use a const generic argument, altering all necessary traits in the types module to depend on ToUnary for indexing when doing substitution, scope-checking, etc. Also alter the Session! macro to generate numerals rather than unary numbers as the argument to Continue in the ToTokens implementation of Target. Update documentation and tests to reflect this change. (This change should not require modifying the examples, since they should transparently continue to work.)
  5. Change the generic parameter of Choice to use a const generic parameter.
  6. Change the generic parameter of Chan::choose to take a const generic argument, removing its value level argument. Alter its documentation (both for the item and in the tutorial and quick reference) and update its tests, including in examples.
  7. Remove the unary::types and unary::constants modules, and ensure that no documentation, tests, or code continue to refer to them (double-check the tutorial).

Ordering constraints:

  • 0 must happen before all others.
  • 1 and 2 can happen simultaneously.
  • 3, 4, and 5 can happen simultaneously.
  • 6 must happen after all others.

I propose that we create a new development branch for this change, and make each change as a separate pull request against that development branch.

[transmit-case] Issues with `TransmitCase` by ref

Just dumping out some thoughts from DMs.

So, let's first lay out some known properties of Rust and the Rust type system/memory model.

  1. A reference is not just a transparent wrapper over an immutable view into some T; it also
    encodes a "place", also called a "region" or lifetime.
  2. Reconstructing an enum from a discriminant involves taking two pieces of data which have
    different regions/come from different places and producing a piece of data which lives in one
    place, which we can then encode a reference to.
  3. There is no way to safely do the latter for any type without Copy bounds, because Rust
    explicitly does not allow you to move out of an immutable or mutable reference, as per the
    borrowing rules.

And a couple properties of the Dialectic backend.

  1. In order for a backend to send something by reference, that thing must all live in the same place
    (it must be behind a single immutable reference.)
  2. A backend cannot be expected to send an enum case detached from its discriminant. If we are to
    allow a blanket impl of TransmitCase for Transmit wherever T: Match, then Transmit must
    be able to send a <T as Case<N>>::Case as a T without knowing the difference between
    T::Case and T.
    Which is impossible; there is data lost in the conversion to T::Case which
    cannot be recovered, beginning with the type itself (in the case of the mpsc backend the TypeId
    is lost) and ending with a possible enum discriminant (which cannot be inferred for an enum that
    has more than one variant with the same case type.)

To sum up: the first issue we have is that it is absolutely not possible to send some T::Case as
T. We must send the T. The second issue we have is that it is absolutely not possible to go
from some &T::Case to some &T; besides the type, there is the additional region information to
be lost, which is important to the Rust compiler even if it is unimportant to us. We cannot expect
it to be unimportant to types we are sending.

So, in conclusion: it is impossible to send an &T::Case without first constructing a T from the
&T::Case. Therefore, it does not make sense to allow any sort of transparent sending of
&T::Case. In any event that it will be cheap or expensive, that cost in the backend cannot be
less than any cloning cost in user code; it could even be more expensive, as the backend code will
have to make assumptions about how to construct a T from an &T::Case. Even in the case where we
risk unsafety, we have to construct a T, unsafely, in order to be sent.
As such, the best solution is to only allow TransmitCase by value.

Self-documenting `offer!()` and `choose!()`

Could we do something like:

offer!(in chan {
    End => break chan.close(),
    Push => {
        // push a value
    }
})?;

End and Push would reduce to enums:

enum Choice {
    End,
    Push
}

offer!(in chan {
    Choice::End => ...,
    Choice::Push => ...,
})?;

Add small "real-world" protocol specification/example to the tutorial

Currently, the tutorial docs are very compartmentalized into sections for each operation/"instruction" type. It would be really nice to have a simple real-world protocol in the tutorial, at least as a specification using the Session! macro if not a fully working implementation. A couple candidates for potential protocols to use:

A full implementation would require a custom backend as well since these would have their own serialization mechanisms which would need to be built to their specifications.

Transition to poll_fn style backend traits

Currently, the extra allocation and virtual call necessary for the boxed future returned by the backend traits leaves us about 50% slower on the microbenchmark against plain Tokio MPSC channels. Until just now, I thought this wasn't soluble without either proper async trait method support or GATs in Rust. However, this ignores the other remaining option: relinquish the design requirement that Transmit/Receive implementations be possible to write using async/await syntax.

If instead the traits are defined in terms of poll functions, similarly to how Sink and Stream are, we can define our own internal explicit futures that wrap an &mut Tx or &mut Rx and use these poll functions to provide the same interface. We could even provide extension traits TransmitExt/ReceiveExt to allow transmitters/receivers to be directly manipulated in async blocks. And all of this doesn't require any boxed future manipulations, which means it should compile away to essentially the same result as invoking the underlying transport directly.

Use build.rs to generate Tuple, List, HasLength, and unary type/const synonyms

Right now these pieces of boilerplate were generated once using a bespoke python script, but it would be better for them to be generated by build.rs to ensure they are more maintainable. This should have no externally visible consequences whatsoever, it's merely an internal refactor of relatively low priority.

Optional comma omission in Session! macro's choose/offer/split statements

In Rust, it's permissible to write match expr { pat1 => { stmts } pat2 => expr }, that is to say, to omit a trailing comma in a match statement (and several other syntactic constructs) when the expression is a block. Currently the Session! macro does not allow this, but if we want to be at parity with Rust's lexical flexibility, we might endeavor to allow it.

Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. 📊📈🎉

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google ❤️ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.