Clarify and expand modes syntax docs #3943
Conversation
| A mode expression actually contains a specification for each modal axis, whether | ||
| you have written a choice for that axis or not. For axes that are omitted, the | ||
| so-called *legacy* modes are used instead. The legacy modes are as follows: | ||
|
|
||
| ```ocaml | ||
| global aliased many nonportable uncontended unyielding stateful read_write | ||
| ``` |
There was a problem hiding this comment.
This is only true for modes on arrow types. But I think maybe better to move this to another document about semantics.
There was a problem hiding this comment.
Really? There are contexts where these aren't the legacy modes?
Not sure whether this is syntax or semantics. I've always thought of the legacy modes as just syntax ("when you don't specify an axis in a mode expression, you get this one"), but I suppose it also plays into what's accepted in modules, etc.
There was a problem hiding this comment.
Yeah when you write (exp : _ @ local) you are only specifying the locality; the rest are not constrained.
| Modalities are used to describe the relationship between a container and an | ||
| element in that container; for example, if you have a record field `x` with | ||
| a `portable` modality, then `r.x` is `portable` even if `r` is `nonportable`. | ||
| We say that the `portable` modality applied to the `nonportable` record mode | ||
| produces the `portable` mode of the field. | ||
|
|
||
| Modalities work differently on future axes vs. past axes. On a future axis, the | ||
| modality imposes an upper bound on the mode (thus always lowering that | ||
| mode). Thus applying the `portable` modality to a `nonportable` records yields a | ||
| `portable` field, because `portable < nonportable`. On a past axis, the modality | ||
| imposes a lower bound (thus always raising that mode). Accordingly, a | ||
| `contended` modality applied to an `uncontended` record yields a `contended` | ||
| field, because `uncontended < contended`. | ||
|
|
||
| Any axis left out of a modality expression is assumed to be the identity | ||
| modality. (When a modality is the identity, then the mode of a field is the same | ||
| as the mode of the record.) For future axes, this would be the top mode; for | ||
| past axes, this would be the bottom mode. These are the identity modalities: | ||
|
|
||
| ```ocaml | ||
| local unique once nonportable uncontended unyielding stateless immutable | ||
| ``` | ||
|
|
||
| Note that a legacy mode might or might not be the same as the identity modality. |
There was a problem hiding this comment.
While the added text is very informative, it probably belongs to another page dedicated to the semantics of modes and modalities. This document was intended as a quick lookup for where and how mode/modalities can show up in syntax.
There was a problem hiding this comment.
Yes, quite right, thanks. I've added a CR to move it once we have a place to move it to.
I was reading through this on my way to somewhere else and made some edits.
Review: @riaqn, who I have also requested to add an entry that I don't feel qualified to do myself.