diff --git a/jane/doc/extensions/_04-modes/syntax.md b/jane/doc/extensions/_04-modes/syntax.md index f43cda7eb22..c096cb31ab4 100644 --- a/jane/doc/extensions/_04-modes/syntax.md +++ b/jane/doc/extensions/_04-modes/syntax.md @@ -4,14 +4,26 @@ collectionName: Modes title: Syntax --- -# Modes and modalities -Currently a mode expression is simply a space-delimited list of modes. +# Modes + +A mode expression is simply a space-delimited list of modes. ``` -mode := local | global | unique | shared | many | once | portable | nonportable - | contended | noncontended | .. +mode ::= locality | uniqueness | linearity | portability | contention + | yield | statefulness | visibility + +(* these are the modal axes: *) +locality ::= `global` | `local` +uniqueness ::= `unique` | `aliased` +linearity ::= `many` | `once` +portability ::= `portable` | `nonportable` +contention ::= `uncontended` | `shared` | `contended` +yield ::= `unyielding` | `yielding` +statefulness ::= `stateless` | `observing` | `stateful` +visibility ::= `read_write` | `read` | `immutable` -modes := separated_nonempty_list(SPACE, mode) +modes ::= mode + | mode modes ``` For example: @@ -24,19 +36,19 @@ Modes are in a dedicated namespace separated from variable names or type names, which means you can continue to use `local` or `unique` as variable or type names. -Currently a modality expression is simply a space-delimited list of modalities. +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 ``` -modality := local | global | .. -modalities := separated_nonempty_list(SPACE, modality) -``` -Similarly, modalities are in a dedicated namespace. -# Where can they appear +It is an error to specify more than one mode along the same axis in one mode +expression. To write a mode expression in program, it has to be prefixed by an `@` symbol. -Similarly, a modality expression has to be prefixed by an `@@` symbol. They can -appear in several places in a program as described below. +It can appear in several places in a program as described below. ## Arrow types ```ocaml @@ -57,10 +69,12 @@ following example, `modes` annotates `b -> c`. a -> (b -> c) @ modes ``` -## Function parameter -The rule of thumb is: wherever a type constraint `x : ty` is allowed, a similar -mode constraint `x @ modes` or type-and-mode constraint `x : ty @ modes` will be -allowed. +## Function parameters + +The rule of thumb is: wherever a type constraint `x : ty` is allowed in a +function parameter, a similar mode constraint `x @ modes` or type-and-mode constraint `x : +ty @ modes` is allowed. + ```ocaml let foo ?(x : int @ modes = default) = .. let foo ?x:((a, b) : int @ modes = default) @@ -68,6 +82,7 @@ let foo ~(x : int @ modes) = .. let foo ~x:((a, b) : int @ modes) = .. let foo ((a, b) : int @ modes) = .. ``` + Patterns that are not directly function parameters can’t have modes. For example, the following is not allowed, because `x @ local` is not a function parameter (but the first component of one). @@ -100,40 +115,120 @@ You can also specify the mode of the function body: ```ocaml let foo x y @ modes = .. let foo x y : ty @ modes = .. -fun foo x y @ modes -> .. +fun x y @ modes -> .. ``` -We don't support `fun foo x y : ty @ modes -> 42` due to a limitation in the +We don't support `fun x y : ty @ modes -> 42` due to a limitation in the parser. ## Expressions ```ocaml -(expression : ty @ local) +(expression : ty @ modes) ``` We don't support `(expression @ modes)` because `@` is already parsed as a binary operator. +However, you can write `(expression : _ @ modes)` if you do not want to constrain the type. + +## Modules +Support for modules with modes is being worked on and not ready for wide adoption. +More documentation will come +as it becomes ready. + +# Modalities + +Similar to modes, a modality expression is simply a space-delimited list of +modalities. As of this writing, every modality is also the name of a mode, +though it is conceivable we will have modalities other than modes in the future. + +``` +modalities ::= modes +``` + + + +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. + +It is an error to specify more than one modality along the same axis in one modality +expression. + +All modality expressions are prefixed by an `@@` symbol, +in one of several places in the syntax, as described below. ## Record fields -Record fields can have modalities, for example: +Record fields can have modalities: ```ocaml type r = {x : string @@ modalities} type r = {x : string @ modes -> string @ modes @@ modalities} ``` +## Constructor fields +Constructor fields can have modalities: +```ocaml +type v = + | K1 of string @@ modalities + | K2 of string @@ modalities * int array + | K3 of string @@ modalities * int array @@ modalities + | K4 of (int -> int) @@ modalities (* parentheses around functions are required even without modalities *) + | K5 : string @@ modalities -> v + | K6 : string @@ modalities * int array @@ modalities -> v + | K7 of { x : string @@ modalities; y : string @@ modalities } + | K8 : { x : string @@ modalities; y : string @@ modalities } -> v +``` + ## Signature items -Signature items such as values can have modalities; for example: +A `val` signature item can have modalities: ```ocaml val foo : string @@ modalities val bar : string @ modes -> string @ modes @@ modalities ``` -A signature can have default modalities that each item can override; for example: +Similarly, so can an `external` signature item: +```ocaml +external id : 'a -> 'a @@ modalities = "%identity" +``` + +A signature can have default modalities that each item can override: ```ocaml sig @@ portable val foo : string (* have portable modality *) val bar : string -> string @@ nonportable (* not have portable modality *) end ``` +These default modalities must be the first item in the signature. + +An .mli file is like a signature, but we do not write the `sig` and the +`end`. Accordingly, you may put `@@ modalities` as the first item in an .mli +file. + +## Kinds +Modality expressions can appear in [kinds](../kinds/intro), documented with the +kind syntax. ## Modules -Support for modules with modes is being worked on and not ready for company-wide adoption. -For the few use sites, the syntax should be self-explanatory. More documentation will come +Support for modules with modes is being worked on and not ready for wide adoption. +More documentation will come as it becomes ready. +