links-lang / links

Links: Linking Theory to Practice for the Web
http://www.links-lang.org
Other
333 stars 43 forks source link

Generative labels #1169

Open dhil opened 1 year ago

dhil commented 1 year ago

This PR is a rebase of #1148 on top of the latest changes to master -- in particular those made to effect handlers.

This PR also generalises the previous work the following ways:

This PR also fixes a regression for session exceptions introduced by one of the previous patches, which made a change to the operation syntax at the type level. However, this change was never propagated properly, as a result session exceptions continued to use the reinterpretation of the function arrow.

dhil commented 1 year ago

The feature, as implemented by this patch, does not interact well with some of Links' other features, e.g. modules. However that shouldn't be a blocker. Another thing, after doing some thinking os that I would like to repurpose new for label generation, then we can avoid introducing fresh as a keyword.

dhil commented 1 year ago

It is worth remarking that this patch further widens the gap between type-inferable expressions and type-ascribable expressions. For instance,

links> fun () { fresh `Foo; do `Foo }
fun : () {`Foo:() => a|_}-> a

The programmer can never manually ascribe the effect-type to the above function, because the label \Foo` is not in scope at the point where the type signature would be written down, e.g.

links> fun () { fresh `Foo; do `Foo } : () {`Foo: () => a |_}-> a;
***: Fatal error : The local label `Foo is not bound

A similar problem also exists in SML with local datatype definitions, e.g.

- fn () => let datatype t = Unit in Unit end;;
val it = fn : unit -> ?.t
slindley commented 1 year ago

The new function creates a new access point. We cannot also use it for creating a fresh effect.

dhil commented 1 year ago

The new function creates a new access point. We cannot also use it for creating a fresh effect.

Of course we can. The question is whether we should.

slindley commented 1 year ago

The new function creates a new access point. We cannot also use it for creating a fresh effect.

Of course we can. The question is whether we should.

Well... it's true that we could in theory (with a bit of care to disambiguate syntax) choose to overload new as a keyword for one thing and a built-in function for another, and indeed we do just that for receive (a keyword for a blocking receive from the current mailbox versus a function for receiving a message through a session endpoint).

Here's the relevant parser code for supporting receive as a function:

/* HACK: allows us to support both mailbox receive syntax
and receive for session types. */
| RECEIVE                                                      { with_pos $loc (Var "receive") }

This is indeed a hack... and arguably bad language design. But I could imagine a more systematic way of allowing certain suitably contextually-distinguished keywords (e.g. those that must appear before an open brace character such as spawn) to be reused as function names.