Munksgaard / session-types

MIT License
555 stars 21 forks source link

Add a proto!() macro #44

Open laumann opened 6 years ago

laumann commented 6 years ago

Suggestion is to add a macro for writing the session types down.

Something like:

proto!{Atm, Client,
    ?<Id>,
    +[
        act: &[
            ?<u64>, !<u64>, act;
            ?<u64>, +[act; act];
            !<u64>;
            eps
        ];
        eps
    ]
}

where

The output of proto!() is then two type aliases:

type Atm = ...;
type Client = <Atm as HasDual>::Dual;

This should replace the current constructs like this:

type Atm = Recv<Id, Choose<Rec<AtmInner>, Eps>>;

type AtmInner = Offer<AtmDeposit, Offer<AtmWithdraw, Offer<AtmBalance, Eps>>>;

type AtmDeposit = Recv<u64, Send<u64, Var<Z>>>;
type AtmWithdraw = Recv<u64, Choose<Var<Z>, Var<Z>>>;
type AtmBalance = Send<u64, Var<Z>>;

type Client = <Atm as HasDual>::Dual;
laumann commented 6 years ago

Maybe more readable if labels were supported:

proto!{Atm, Client,
    ?<Id>,
    +[
        act. &[
            deposit: ?<u64>, !<u64>, act;
            withdraw: ?<u64>, +[ok: act; err: act];
            balance: !<u64>;
            exit: eps
        ];
        eps
    ]
}

Recursion labels could then be followed by . and branch labels be followed by : to separate the two.