Macro dialectic::Session

Session!() { /* proc-macro */ }

The Session! macro compiles a small domain-specific language for describing session types into the types themselves. It should be invoked in type position.

The Session! macro language looks a lot like Rust code: sequential instructions are separated by semicolons, blocks are delimited with curly braces, etc.

The language defines several keywords, each of which corresponding to the session type of the same name (except for break, which is translated by the macro into other constructs):

• send and recv
• offer and choose
• loop, break, and continue
• call
• split

Additionally, arbitrary session types can be used inline by name, so specifications can be composed.

Examples

In these examples, each example of a session type defined using Session! is paired with its equivalent session type written out using the session type constructors in types.

You can find further examples of the use of Session! and its meaning throughout this reference documentation, the tutorial, and in the Dialectic crate’s examples.

In the below examples, all code blocks import:

use static_assertions::assert_type_eq_all as type_eq;
use dialectic::prelude::*;

// Normally you don't need to import these, because they are only useful
// when writing session types directly, not when using the `Session!` macro:
use dialectic::types::*;

The send and recv keywords

These keywords take the type to be sent or received as an argument, with no parentheses. See also: the Send type and send method, and the Recv type and recv method.

type_eq!(
    Session! { send bool },
    Send<bool, Done>,
);

type_eq!(
    Session! { recv bool },
    Recv<bool, Done>,
);

The offer and choose keywords

Using offer and choose matches the syntax of the offer! macro, with each numerically-labeled branch listed in order, corresponding to the session type to be used in the case of each potential choice.

See also: the Choose type and the choose method, and the Offer type and the offer! macro.

type_eq!(
    Session! { offer { 0 => {}, 1 => {} } },
    Offer<(Done, Done)>
);

type_eq!(
    Session! { choose { 0 => {}, 1 => {} } },
    Choose<(Done, Done)>
);

The loop, break, and continue keywords

The syntax of loop, break and continue are identical to in Rust syntax, including optional named labels.

Just like Rust’s loop keyword, but unlike Dialectic’s Loop type, when control flow reaches the end of a loop in a Session!, it automatically returns to the head of the loop. To exit a loop, you must use break.

type_eq!(
    Session! { loop { break } },
    Loop<Done>
);

type_eq!(
    Session! { loop { send (); } },
    Session! { loop { send (); continue; } },
    Loop<Send<(), Continue<0>>>,
);

type_eq!(
    Session! {
        'outer: loop {
            loop {
                break 'outer;
            }
        }
    },
    Loop<Loop<Done>>
);

type_eq!(
    Session! {
        'outer: loop {
            send ();
            loop {
                continue 'outer;
            }
        }
    },
    Loop<Send<(), Loop<Continue<1>>>>
);

The call keyword

The call keyword either precedes a named session type, or a block. It corresponds to the Call session type and the call method.

type P = Session! { send i64 };
type Q = Session! { call P };

type_eq!(Q, Call<Send<i64, Done>, Done>);

type R = Session! {
    loop {
        choose {
            0 => {
                send i64;
                call { continue };
                recv i64;
            },
            1 => break,
        }
    }
};

type_eq!(R, Loop<Choose<(Send<i64, Call<Continue<0>, Recv<i64, Continue<0>>>>, Done)>>);

The split keyword

The split keyword precedes a block with two clauses, indicating two concurrent sessions to be run, one (marked by ->) which can only transmit information, and the other (marked by <-) which can only receive information. It corresponds to the Split session type and the split method.

type P = Session! {
    split {
        -> send i64,
        <- recv bool,
    };
    send String;
};

type_eq!(P, Split<Send<i64, Done>, Recv<bool, Done>, Send<String, Done>>);

External session types

Arbitrary session types defined outside the macro invocation can be spliced in as an individual statement, or even used as generic parameters.

type Parity = Session! { send i64; recv bool };
type Twice<T> = Session! { T; T };
type Protocol = Session! {
    loop {
        choose {
            0 => Twice<Parity>,
            1 => break,
        }
    }
};

type_eq!(
    Protocol,
    Loop<Choose<(Send<i64, Recv<bool, Send<i64, Recv<bool, Continue<0>>>>>, Done)>>,
);