boltlabs-inc / dialectic Goto Github PK
View Code? Open in Web Editor NEWTransport-polymorphic, asynchronous session types for Rust
Home Page: https://docs.rs/dialectic
License: MIT License
Transport-polymorphic, asynchronous session types for Rust
Home Page: https://docs.rs/dialectic
License: MIT License
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.
In so doing, double-check that the proc-macro version of offer! is actually faster than the old version.
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:
Choose
and Offer
types to Choice<N>
and NotChoice<T>
.Session!
macro, which has the necessaryMatch
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.
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:
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)
.offer!
macro will take normal integer literals in its arms, not underscore-prefixed ones.choose
and offer
constructs in the Session!
macro will also take normal integer literals in their arms, not underscore-prefixed ones.Continue
will become a const generic argument rather than a unary number.Choice
will become a const generic argument rather than a unary number.dialectic::unary::types
and dialectic::unary::constants
will entirely be removed.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.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.From how I see it, this breaks down into several phases, in this order:
min_const_generics
lands on stable.Session!
and offer!
to use non-underscore-prefixed numerals, and alter their documentation and associated tests to match (including tutorial).ToUnary
trait and the procedural macro to generate all its instances. Document and test.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.)Choice
to use a const generic parameter.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.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:
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.
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).
This should be a request coming from the local client. The function should take the secret information passed from the client, store it, and return either a success or an error indicator.
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)
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:
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.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.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.The documentation should make use of the Session!
macro, once it is introduced to the library.
Some outlying questions:
Examples should definitely be all converted to Session!
invocations.
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.
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.
We might be able to improve how type errors are presented to the user. There are a couple avenues forward:
Session!
invocationsThese two could be paired together!
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:
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.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:
(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.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
.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.
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 Chan
s are known to be statically valid for the whole session, and can't get stuck.
Issues/complications:
Split
, where it must be disallowed to send
/choose
from the receive-only end, and recv
/offer
from the send-only end.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.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.
These could be auto-generated by readme.py
, from the existing documentation for those crates.
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.
T
; it alsoCopy
bounds, because RustAnd a couple properties of the Dialectic backend.
TransmitCase
for Transmit
wherever T: Match
, then Transmit
must<T as Case<N>>::Case
as a T
without knowing the difference betweenT::Case
and T
. Which is impossible; there is data lost in the conversion to T::Case
whichTypeId
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.
Currently, the Action
for methods on Chan
s 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:
Downsides:
impl
blocksRight 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.
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.
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.
This is a tracking issue for the macro-compiler-dev branch (PR #36).
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:
?
and !
operators, as customary with session type notation, indicate Recv
and Send
respectively. (Should we pick something else given the meaning of ?
in Rust?)loop
s 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 looploop
heads can optionally be named, just like in Rust, and you can break out of a named loop, rather than using an indexOffer
is denoted with |
and has lowest precedence of any operatorChoose
is denoted with +
and has higher precedence than |
but less than anything elseSplit
is denoted with &
and has higher precedence than |
, +
, and sequential composition, but less than the unary primitive operatorsloop
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?
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!
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.
It should be possible to entirely decouple the serde backend from serde itself, making it a tokio-codec backend parametrized by a serializer/deserializer pair, which may or may not be based on serde.
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:
Unsafe<P>
(only parameter is continuation, since its innards are opaque),Session!
macro keyword unsafe;
(no block, since its innards are opaque), andChan<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.
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 Loop
s, but in general an auxiliary function to increment de Bruijn indices in the substituted terms is necessary to make Continue
s point to the correct place.
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.
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:
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.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.
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.
This means we can improve error message quality and locality, as well as prevent documentation from exposing macro internals.
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.
Prior to 0.4 release, we need to be back on the stable channel and ensure that everything builds.
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 => ...,
})?;
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 Block
s 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.
This way we don't need to provide any privileged implementation of the traits from the backend module. This would implicitly supersede #51.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.