Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
plaidfinch opened this issue Feb 17, 2021 · 0 comments

Comments

@plaidfinch
Copy link
Contributor

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.

plaidfinch added a commit that referenced this issue Feb 18, 2021
Fixes #32. This also eliminates unnecessary bounds left over from
previous iterations of the type system.
sdleffler pushed a commit that referenced this issue Feb 18, 2021
Fixes #32. This also eliminates unnecessary bounds left over from
previous iterations of the type system.
sdleffler pushed a commit that referenced this issue Feb 22, 2021
Fixes #32. This also eliminates unnecessary bounds left over from
previous iterations of the type system.
@plaidfinch plaidfinch reopened this Feb 23, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant