portable lazy allows nonportable thunk (#3436)

* portable lazy allows nonportable thunk

* add documentation

* improve documentation

* add examples

* improve comments in test

* say "not stronger"

jane/doc/extensions/modes/reference.md

@@ -0,0 +1,42 @@
+The goal of this document is to be a reasonably complete reference to the mode system in
+OCaml.
+
+<!-- CR zqian: For a gentler introduction, see [the introduction](intro.md). -->
+
+The mode system in the compiler tracks various properties of values, so that certain
+performance-enhancing operations can be performed safely. For example:
+- Locality tracks escaping. See [the local allocations reference](../local/reference.md)
+- Uniqueness and linearity tracks aliasing. See [the uniqueness reference](../uniqueness/reference.md)
+- Portability and contention tracks inter-thread sharing.
+    <!-- CR zqian: reference for portability and contention -->
+
+# Lazy
+`lazy e` contains a thunk that evaluates `e`, as well as a mutable cell to store the
+result of `e`. Upon construction, the mode of `lazy e` cannot be stronger than `e`. For
+example, if `e` is `nonportable`, then `lazy e` cannot be `portable`. Upon destruction
+(forcing a lazy value), the result cannot be stronger than the mode of lazy value. For
+example, forcing a `nonportable` lazy value cannot give a `portable` result. Additionally,
+forcing a lazy value involves accessing the mutable cell and thus requires the lazy value
+to be `uncontended`.
+
+Currently, the above rules don't apply to the locality axis, because both the result and
+the lazy value are heap-allocated, so they are always `global`.
+
+Additionally, upon construction, the comonadic fragment of `lazy e` cannot be stronger
+than the thunk. The thunk is checked as `fun () -> e`, potentially closing over variables,
+which weakens its comonadic fragment. This rule doesn't apply to several axes:
+- The thunk is always heap-allocated so always `global`.
+- Since the thunk is only evaluated if the lazy value is `uncontended`, one can construct
+a lazy value at `portable` even if the thunk is `nonportable` (e.g., closing over
+`uncontended` or `nonportable` values). For example, the following is allowed:
+```ocaml
+let r = ref 0 in
+let l @ portable = lazy (r := 42) in
+```
+- Since the thunk runs at most once even if the lazy value is forced multiple times, one
+can construct the lazy value at `many` even if the thunk is `once` (e.g., closing over
+`unique` or `once` values). For example, the following is allowed:
+```ocaml
+let r = { x = 0 } in
+let l @ many = lazy (overwrite_ r with { x = 42 })
+```

testsuite/tests/typing-modes/lazy.ml

@@ -43,8 +43,7 @@ let foo (x @ local) =
 val foo : local_ 'a lazy_t -> 'a = <fun>
 |}]
 
-(* one can construct portable lazy, if both the thunk and the result are
-   portable *)
+(* one can construct [portable] lazy only if the result is [portable] *)
 let foo () =
     let l = lazy (let x @ nonportable = fun x -> x in x) in
     use_portable l
@@ -55,32 +54,21 @@ Line 3, characters 17-18:
 Error: This value is "nonportable" but expected to be "portable".
 |}]
 
+(* thunk is evaluated only when [uncontended] lazy is forced, so the thunk can be
+    [nonportable] even if the lazy is [portable]. *)
 let foo (x @ nonportable) =
     let l = lazy (let _ = x in ()) in
     use_portable l
 [%%expect{|
-Line 3, characters 17-18:
-3 |     use_portable l
-                     ^
-Error: This value is "nonportable" but expected to be "portable".
-|}]
-
-let foo (x @ portable) =
-    let l = lazy (let _ = x in let y = fun () -> () in y) in
-    use_portable l
-[%%expect{|
-val foo : 'a @ portable -> unit = <fun>
+val foo : 'a -> unit = <fun>
 |}]
 
-(* inside a portable lazy, things are available as contended *)
+(* For the same reason, [portable] lazy can close over things at [uncontended]. *)
 let foo (x @ uncontended) =
-    let l @ portable = lazy ( let x' @ uncontended = x in ()) in
+    let l @ portable = lazy ( let _x @ uncontended = x in ()) in
     use_portable l
 [%%expect{|
-Line 2, characters 53-54:
-2 |     let l @ portable = lazy ( let x' @ uncontended = x in ()) in
-                                                         ^
-Error: This value is "contended" but expected to be "uncontended".
+val foo : 'a -> unit = <fun>
 |}]
 
 (* Portable lazy gives portable result *)
@@ -91,6 +79,7 @@ let foo (x @ portable) =
 val foo : 'a lazy_t @ portable -> unit = <fun>
 |}]
 
+(* Nonportable lazy gives nonportable result *)
 let foo (x @ nonportable) =
     match x with
     | lazy r -> use_portable x

typing/typecore.ml

@@ -551,6 +551,9 @@ let mode_lazy expected_mode =
     (* The thunk is evaluated only once, so we only require it to be [once],
        even if the [lazy] is [many]. *)
     |> Value.join_with (Comonadic Linearity) Linearity.Const.Once
+    (* The thunk is evaluated only when the [lazy] is [uncontended], so we only require it
+       to be [nonportable], even if the [lazy] is [portable]. *)
+    |> Value.join_with (Comonadic Portability) Portability.Const.Nonportable
   in
   {expected_mode with locality_context = Some Lazy }, closure_mode