links-lang / links

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

Modernise and properly test CP syntactic sugar #652

Open SimonJF opened 5 years ago

SimonJF commented 5 years ago

The CP syntactic sugar allows process calculus-like syntactic sugar for writing session-typed applications. (Note: for those who are familiar with the CP/GV literature, CP here is a misnomer: the syntax in Links does not require the syntactic restrictions of CP; it's more like a standard process calculus notation).

@slindley has made a case that it greatly reduces syntactic noise and should stay. I would shed no tears if it were to disappear, but regardless, if it is to stay then it needs to be done properly.

Currently though, CP is broken on the client, and its implementation is brittle. Part of this is because the CP implementation relies on a translation to lesser-used logically-inspired primitives.

If CP is to stay, we need to modernise and properly test the implementation.

slindley commented 5 years ago

The case for the syntactic sugar is made in Section 1.5.1 of Lightweight Functional Session Types.

http://homepages.inf.ed.ac.uk/slindley/papers/fst.pdf

Crudely put, the calculator server example with sugar fits on 2 lines and without sugar fits on 5 lines.

Some of the more esoteric features drawn from CP are quite unnecessary, though (really this is just a syntactic sugar to avoid unnecessary rebinding, and isn't about implementing CP itself).

I'm not quite sure what "broken on the client means", given that this is supposed to be syntactic sugar that gets elaborated away in the frontend.