Proc-macro DSL for protocol/session type specifications

[sdleffler]

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.

[plaidfinch]

This supercedes #4.