improve modality comments

Author: riaqn

typing/mode.ml

@@ -2597,6 +2597,62 @@ module Modality = struct
     | Atom (ax, Meet_with c) ->
       Format.fprintf ppf "meet_with(%a)" (C.print (Value.proj_obj ax)) c
 
+  (* Inferred modalities
+
+      Similar to constant modalities, an inferred modality maps the mode of a
+      record/structure to the mode of a value therein. An inferred modality [f]
+      is inferred from the structure/record mode [mm] and the value mode [m]. It
+      will only be applied on some [x >= mm]: That is, it will only be applied
+      on the original module.
+
+      It should satisfy the following conditions:
+
+      Zapping: [f] should be of the form [join_c] for monadic axes, or [meet_c]
+      for comonadic axes.
+
+      Soundness: You should not get a value from a record/structure at a mode
+      strictly stronger than how it was put in. That is, for any [x >= mm], [f x
+      >= m].
+
+      Completeness: Ideally we also want [f mm <= m].
+
+      Monadic axes
+
+      Soundness condition says [join_c x >= m] for any [x >= mm]. Equivalently,
+      [join_c mm >= m]. By adjunction, [c >= subtract_mm m]. We take the lower
+      bound [c := subtract_mm m]. Note that this is equivalent to taking [c := m
+      >= subtract_mm m]. Proof:
+
+      - [join_m x >= join_(subtract_mm m) x] is trivial since [m >= subtract_mm
+        m].
+      - [join_m x <= join_(subtract_mm m) x], or equivalently [m <=
+      join_(subtract_mm m) x], or equivalently [subtract_x m <= subtract_mm m],
+      which is trivial since [x >= mm].
+
+      Taking [c := subtract_mm m] is better for zapping since it's lower and
+      thus closer to identity modality. Taking [c := m] is easier for [apply]
+      and [sub].
+
+      Comonadic axes
+
+      Soundness condition says [meet_c x >= m] for any [x >= mm]. Equivalently,
+      [meet_c mm >= m]. By def. of [meet], we have both [c >= m] and [mm >= m].
+      The latter is guaranteed by the user of [infer]. We guarantee the former
+      by taking [c := imply_mm m >= m]. One might worry that this is too relaxed
+      and will be "less complete" than taking [c := m]; however, note that
+      [imply_mm m <= imply_mm m] and thus by adjunction [meet_(imply_mm m) mm <=
+      m], which means the chosen [c] is complete.
+
+      Taking [c := m] is easier for [apply] and [sub]. Taking [c := imply_mm m]
+      is better for zapping since it's higher and thus closer to identity
+      modality. However, note that we DON'T have [meet_m x = meet_(imply_mm m)
+      x], which means [apply/sub] and [zap] might behave in a confusing (albeit
+      sound) manner.
+
+      CR zqian: once we support binary mode solver, we will stick to
+      [c := imply_mm m].
+  *)
+
   module Monadic = struct
     module Mode = Value.Monadic
 
@@ -2655,20 +2711,9 @@ module Modality = struct
         | Join_const c -> Format.fprintf ppf "join_const(%a)" Mode.Const.print c
     end
 
-    (* Similar to constant modalities, an inferred modality maps the mode of a
-       record/structure to the mode of a value therein. An inferred modality [f] is
-       inferred from the structure/record mode [mm] and the value mode [m].
-
-       Soundness: You should not get a value from a record/structure at a mode strictly
-       stronger than how it was put in. That is, [f mm >= m].
-
-       Completeness: You should be able to get a value from a record/structure at a mode
-       not strictly weaker than how it was put in. That is, [f mm <= m]. *)
-
     type t =
       | Const of Const.t
-      | Diff of Mode.lr * Mode.lr
-          (** inferred modality. See [apply] for its behavior. *)
+      | Diff of Mode.lr * Mode.lr  (** See "Inferred modalities" comments *)
       | Undefined
 
     let sub_log left right ~log : (unit, error) Result.t =
@@ -2817,17 +2862,19 @@ module Modality = struct
     type t =
       | Const of Const.t
       | Undefined
-      | Exactly of Mode.lr * Mode.lr
-          (** inferred modality. See [apply] for its behavior. *)
+      | Exactly of Mode.lr * Mode.lr  (** See "Inferred modalities" comments *)
 
     let sub_log left right ~log : (unit, error) Result.t =
       match left, right with
       | Const c0, Const c1 -> Const.sub c0 c1
       | Exactly (_mm, m), Const (Meet_const c) -> (
-        (* Check for all x >= mm, m <= meet x c. Equivalent to check [m <= meet
-           mm c]. By definition of meet, equivalent to check [m <= mm] and [m <=
-           c]. The former is the precondition of [Exactly]. So we only check the
-           latter. *)
+        (* Check for all [x >= mm], [meet_(imply_mm m) x <= meet_c x], or
+           equivalently [meet_(imply_mm m) x <= c], or equivalently [meet_(imply_mm
+           m) max <= c], or equivalently [imply_mm m <= c]. We can't check this
+           without binary mode solver.
+
+           So instead we check [meet_m x <= meet_c x] (See "Inferred modalities"
+           comments), which amounts to [m <= c]. *)
         match Mode.submode_log m (Mode.of_const c) ~log with
         | Ok () -> Ok ()
         | Error (Error (ax, { left; _ })) ->
@@ -2856,7 +2903,12 @@ module Modality = struct
       | Const c -> Const.apply c x |> Mode.disallow_right
       | Undefined ->
         Misc.fatal_error "modality Undefined should not be applied."
-      | Exactly (_mm, m) -> Mode.disallow_right m
+      | Exactly (_mm, m) ->
+        (* Ideally want to return [meet_(imply_mm m) x], which we can't do
+           without binary mode solver, so instead we return [meet_m x] (See
+           "Inferred modalities" comments), which because of [x >= mm >= m] is
+           equal to [m]. *)
+        Mode.disallow_right m
 
     let print ppf = function
       | Const c -> Const.print ppf c

typing/mode_intf.mli

@@ -630,7 +630,12 @@ module type S = sig
       (** The undefined modality. *)
       val undefined : t
 
-      (** Apply a modality on a left mode. *)
+      (* CR zqian: note that currently, [apply] and [sub] and [zap] are NOT
+      coherent for comonadic axes. That is, we do NOT have
+      [apply t m = Const.apply (zap t) m]. This is probably fine. *)
+
+      (** Apply a modality on a left mode. The calller should ensure that [apply
+      t m] is only called for [m >= md_mode] for inferred modalities. *)
       val apply : t -> (allowed * 'r) Value.t -> Value.l
 
       (** [sub t0 t1] checks that [t0 <= t1].