Various fixes on unboxed and kinds (#4024)

* Various fixes on unboxed and kinds

* Update jane/doc/extensions/_02-unboxed-types/intro.md

Co-authored-by: Richard Eisenberg <[email protected]>

* Update jane/doc/extensions/_02-unboxed-types/or-null.md

Co-authored-by: Richard Eisenberg <[email protected]>

* Update jane/doc/extensions/_05-kinds/intro.md

Co-authored-by: Richard Eisenberg <[email protected]>

* possible rewrite

* new or_null intro

* typo

---------

Co-authored-by: Richard Eisenberg <[email protected]>

Author: cuihtlauac

jane/doc/extensions/_02-unboxed-types/intro.md

@@ -118,8 +118,7 @@ design decisions and contains additional examples.
 ## Layouts in module inclusion
 
 Layouts are part of kinds, and therefore work just like kinds for the purposes
-of module inclusion. See the [kinds
-documentation][../kinds.md#inclusion-and-variance] for more.
+of module inclusion. See the [kinds documentation](../../kinds/intro#inclusion-and-variance) for more.
 
 # Unboxed numbers
 
@@ -140,8 +139,7 @@ the other unboxed types) that has layout
 float# ... end`.
 
 Each numeric type has its own library for working with it: `float_u`,
-`int32_u`, `int64_u`, and `nativeint_u`. (Outside of Jane Street, these will be
-modules in the `janestreet_shims` library.)
+`int32_u`, `int64_u`, and `nativeint_u` (all in the `janestreet_shims` library).
 
 * Unboxed constants are written with a prepended `#`.
   There is no literal syntax for unboxed vectors: use the `Ocaml_simd_sse` library instead.

jane/doc/extensions/_02-unboxed-types/or-null.md

@@ -21,10 +21,10 @@ works.
 
 ## The `value_or_null` layout
 
-The key observation powering `or_null` is that ordinary OCaml values are
-never equal to the word 0. A pointer will always be non-null (and thus different
-from 0), and a tagged integer always has its bottom bit set. Because 0 can
-never be a valid pointer, we can safely update the garbage collector not to
+The key observation powering `or_null` is that no ordinary OCaml value equals the
+word 0. A valid pointer will always be non-null, and an immediate (represented
+as a tagged integer) will always have its bottom bit set. Thus, all are
+different from 0. Therefore, we can safely update the garbage collector not to
 traverse null pointers.
 
 We thus want `t or_null` to be just like `t`, except now with a meaning
@@ -89,7 +89,7 @@ annotation burden on programmers.
 
 ## Arrays
 
-The flat-float-array optimization demands that all types in OCaml are *separable*:
+The float array optimization demands that all types in OCaml are *separable*:
 either all elements of that type are float values, or none of them are. But
 `float or_null` is not separable: as possible values, it has all floating-point
 numbers, plus the null pointer. Therefore, `float or_null array`s must be forbidden.

jane/doc/extensions/_05-kinds/intro.md

@@ -20,8 +20,12 @@ several different dimensions. For example, kinds can be used to identify which
 types have values that are passed in floating point registers, or are safely
 ignored by the garbage collector.
 
-The kind of a type has four components: the _layout_, the _modal bounds_, the
-_with-bounds_, and the _non-modal bounds_. The layout describes the shape of the
+The kind of a type has four components:
+* the _layout_,
+* the _modal bounds_,
+* the _with-bounds_,
+* and the _non-modal bounds_.
+The layout describes the shape of the
 data at runtime, and is used to support unboxed types. The modal bounds describe
 how different types interact with our mode system. In particular, some types
 don't have interesting interactions with some modes, so values of these types
@@ -80,7 +84,7 @@ addition, `int`s are not `float`s and they do not need to be garbage-collected
 
 # The meaning of kinds
 
-In additional to `value`, OxCaml supports layouts like `float64` (unboxed
+In addition to `value`, OxCaml supports layouts like `float64` (unboxed
 floating point numbers that are passed in SIMD registers), `bits64`
 and `bits32` (for types represented by unboxed/untagged integers) and product
 layouts like `float64 & bits32` (an unboxed pair that is passed in two
@@ -94,7 +98,7 @@ meaning of the mode and details of the implementation of related features in the
 OxCaml runtime. See the documentation for each mode to understand which types
 cross on its axis.
 
-Formally, these are called modal _bounds_ because the represent upper or lower
+Formally, these are called modal _bounds_ because they represent upper or lower
 bounds on the appropriate modal axes. For _future_ modal axes (like portability
 and linearity), the kind records an upper bound on the mode of values of this
 type. For example, `int` is `mod portable` because if you have an `int` that is
@@ -104,11 +108,11 @@ _expectations_.  For example, `int` is `mod contended` because in a place where
 an `uncontended` value is expected, it's still safe to use a `contended` int.
 
 Why do past and future modal axes get different treatment in kinds? This is
-covered in the "Advanced Topics" section below, but isn't essential to
+covered in the [Advanced Topics](#advanced-topics) section below, but isn't essential to
 understand for day-to-day use of the system.
 
-The non-modal bounds encode several different properties; see the section
-"Non-modal bounds" below. They are called bounds because each non-modal axis
+The non-modal bounds encode several different properties; see the
+[Non-modal bounds](../non-modal) document. They are called bounds because each non-modal axis
 still supports a sub-kinding relationship, where a type of a more specific kind
 can be used in place of a variable of a less specific kind.
 
@@ -130,16 +134,16 @@ contended`, or `value mod portable` and `value mod aliased`.
 Adding bounds to a kind always makes the kind more specific, or lower. That is,
 for any kind `k`, `k mod <bounds> <= k`.
 
-Along the future modal axes, a lower mode leads to a lower kind. So `value mod
-stateless <= value mod observing`, and bounding by the maximum mode has no
-effect. However, along the past modal axes, a _higher_ mode leads to a lower
-kind. So `value mod contended <= value mod sharing` and bounding by the minimum
-mode has no effect. We can think of the past axes as flipped, when used in a
-kind. This is because `value mod contended` is more restrictive than `value mod
-sharing` (the former contains types that do not care at all about the value of
-the contention axis, while the latter contains types that still care about the
-distinction between `contended` and `sharing`/`uncontended`), and so we must
-flip these past axes (somewhat unfortunately).
+Along the future modal axes, a _lower_ mode leads to a lower kind. So `stateless
+< observing` leads to `value mod stateless <= value mod observing`, and bounding
+by the maximum mode has no effect. However, along the past modal axes, a
+_higher_ mode leads to a lower kind. So `shared < contended` leads to `value mod
+contended <= value mod shared` and it's bounding by the minimum mode that has no
+effect. Thus (beware), past modal axes are flipped, when used in a kind. For
+instance, `value mod contended` is _more restrictive_ than `value mod shared`.
+The former only contains types that do not care about the value of the
+contention axis, while the latter also contains types that care about the
+distinction between `contended` and `shared`/`uncontended`.
 
 If you want to get nerdy about it, each individual piece of a kind (the layout
 and each possible axis of bounds) is a join semilattice, and the order we're
@@ -210,7 +214,7 @@ by types with any kind (e.g., `Sexpable`).
 # With-bounds
 
 Sometimes the kind of a type constructor depends on the kinds of the types that
-instantiate its parameters.  For example, the type `'a list` can mode cross on
+are passed as arguments.  For example, the type `'a list` can mode cross on
 the portability axis if `'a` does.
 
 We could have a `list` whose kind is restricted to work on types that more cross