Resolving spec inconsistency caused by join allowing value annihilation

pathmap-book/src/1.01.01_trie_and_value_lattice.md

@@ -0,0 +1,49 @@
+# Trie and Value Lattices
+
+Algebraic operations in [PathMap] combine rules at two levels. At the outer level, lattices over tries and subtries describe relationships between trie structures. At the inner level, where values occupy corresponding locations in the tries, value-specific lattice rules describe how those values interact.
+
+This behavior is usually intuitive, but there are edge cases to understand, concerning empty subtries, absent values, and present values that represent a bottom element.
+
+## Structural Relations Between Tries
+
+Tries are ordered by structural containment. One trie is below another when all of its structure occurs in the other. Join is the least upper bound, meet is the greatest lower bound, and the empty trie is the bottom element.
+
+A whole [`PathMap`] is one trie in this ordering. The same relationships apply to every subtrie, including a subtrie exposed through a zipper.
+
+Trie structure is independent of stored values. A path may exist without a value. A dangling path may exist without a value or child. Both still participate in structural operations.
+
+## Value Interactions at Collisions
+
+Value lattice rules define how values relate and how an operation combines them. The trie applies these rules when multiple operands contain values at the same location.
+
+Different value policies may define a different ordering over the same value type. A join policy may define a join-semilattice, while a meet policy may define a meet-semilattice. They form one lattice only when they describe the same order and satisfy the compatibility laws. The API does not assume this.
+
+Value orderings need not resemble trie containment. For example, permission sets might use union for join and intersection for meet.   If two tries store permission sets at `users:ada`, joining the tries also joins those values according to the value policy.  But If only one trie stores a value at `users:lin`, that value will be included in the resulting trie without invoking the value policy's function.
+
+## Absence Is Not a Bottom Value
+
+An absent value is different from a present bottom value. When a value is not present at a path, algebraic operations on the outer lattice will often bypass the value policy entirely. A stored bottom value, however, will cause the policy to be invoked when appropriate.  This is true even when if the bottom value has an application-level meaning is equivalent to "empty."
+
+For example, joining two locations without values leaves no stored value and does not invoke the policy. But joining two stored `Option::None` values invokes the polcity and produces a new `Option::None` value. A join of present operands must produce an upper bound, so it cannot turn present values into structural absence.
+
+## Composition Rules for the Trie Level and Value Level
+
+A generic trie operation can be conceptualized as two steps:
+
+1. Apply the structural operation to determine which paths and subtries belong in the result.
+2. Apply the value operation where values coincide.
+
+The implementation interleaves these steps for efficiency. Structural guarantees allow it to reuse or skip entire subtries. It invokes value rules only where values interact.
+
+
+GOAT:
+* TrieLattice policies and ValueLattice policies are separate objects
+* The trie policy decides when and how the value policy is called, and even whether it's called
+* Therefore it makes sense to make the ValuePolicy a generic argument to the object that implements the TriePolicy
+* Of course we can have shortcuts so the caller doesn't need to say `alg_op::<TrieJoin<V, ValJoin<V>>>()`
+
+* The open question is how we slice the implementation.  If we make the impl generic enough, we will limit flexibility by trying to express limitations like direction constraints (up, down, unconstrained) in the types.  But also the mind-melting logic that is generic meet will certainly need some implementation-provided scaffolding.  And therefore how much of that scaffolding will need to know about the nature of the policies to be optimal??
+*  I don't think I'm going to be confident in the answer to that until I actually do the implementation for real.
+
+
+{{#include api_links.md}}

pathmap-book/src/1.01.02_algebraic_traits.md

@@ -0,0 +1,106 @@
+# [`Lattice`] and [`DistributiveLattice`] Traits
+
+The previous section introduced structural lattice operations on tries and the operation-specific rules applied to values. This section describes the current traits and result types, followed by the planned policy model for value-level operations.
+
+The [`Lattice`] trait and related traits in the [`ring`] module are used to define [`join`] and [`meet`] behaviors on values within a [`PathMap`]. So two values at the same path may interact with each other as part of these operations.
+
+WARNING: This mechanism is planned for rework, to allow a "policy" to be provided instead of forcing a [`Lattice`] implementation to be associated to the value type. Therefore the current API entry points will not be explained further.
+
+## Planned Policy Model (for value operations)
+
+The planned API separates algebraic operations along two axes, creating 6 possible policy types. The type describes the guarantees that the implementation may rely upon; a policy remains responsible for defining the operation's particular value semantics.
+
+### Axes to Classify Operations
+
+The first axis describes the roles of the operands:
+
+- **Symmetric:** Operand positions are interchangeable. These operations support equivalent two-operand and multi-operand forms; their policy contract includes the associativity needed to fold multiple operands, in addition to permutation symmetry. Join and meet are symmetric.
+- **Positional:** Each operand has a distinct role, and exchanging operands may change the result. A general multi-operand fold is therefore not implied. Subtract is positional.
+
+The second axis describes how the result may move through the ordering defined by the policy:
+
+- **Upward:** The result is greater than or equal to the relevant input operands. An operation invoked with present operands cannot remove the value. Join is upward.
+- **Downward:** The result is less than or equal to the relevant input operands and may remove the value. Meet and subtract are downward.
+- **Unconstrained:** The result may move either upward or downward. The trie cannot apply optimizations that depend upon a known direction of movement.
+
+For a symmetric operation, "relevant input operands" means every operand. For a positional operation, the ordering guarantee is relative to the primary (left or `self`) operand unless the policy documents a stronger guarantee. For example, subtraction is downward from its left operand, but its result need not be below its right operand.
+
+### Table of Ops
+
+| Movement | Symmetric | Positional |
+| --- | --- | --- |
+| Upward | Join | future policy-defined op |
+| Downward | Meet | Subtract, ^restrict |
+| Unconstrained | future policy-defined op | future policy-defined op |
+
+These guarantees also constrain valid operation results. An upward value-level operation cannot report that no value remains. A symmetric operation may identify any equivalent operand, including multiple operands in an n-ary operation. A positional operation preserves operand roles, so any identity information must identify an operand that the policy permits the caller to reuse.  In practice this probably means only the first operand.
+
+GOAT: ^restrict doesn't make much sense as a value policy.
+
+## Algebraic Operation Results
+
+[`AlgebraicResult`] reports whether the operation produced no element ([`None`][`AlgebraicResult::None`]), a result equal to one or more operands ([`Identity`][`AlgebraicResult::Identity`]), or an element that must be returned ([`Element`][`AlgebraicResult::Element`]). Joining supplied elements always produces an element, even when that element is the bottom under the applicable value ordering. At the structural level, however, joining two absent operands produces no element; the value-level join operation is not called.
+
+For subtraction and restriction, only the left operand can be an identity. These operations are positional, so equality with the right operand in a degenerate case does not make the right operand interchangeable with the left.
+
+[`AlgebraicStatus`] expresses the corresponding outcome for an operation performed in place. [`Identity`][`AlgebraicStatus::Identity`] means the left operand was unchanged, [`Element`][`AlgebraicStatus::Element`] means it now contains the result without making the stronger unchanged claim, and [`None`][`AlgebraicStatus::None`] means that no result remains. Some facts can overlap: if the left operand was already empty and remains empty, both [`Identity`][`AlgebraicStatus::Identity`] and [`None`][`AlgebraicStatus::None`] describe part of what happened.
+
+## Result Cases (for binary ops)
+
+Let `A` be the left (`self`) operand, `B` the right (`other`) operand, and `R` the result. The tables use set notation for the lattice order: `A ⊆ B` means that all information represented by `A` is also represented by `B`, and `∅` denotes the empty or bottom element. For the structural part of a `PathMap`, this can be read as ordinary inclusion between sets of paths.
+
+### Union (aka join), `A ∪ B`
+
+| Case | Result | [`AlgebraicResult`] |
+| --- | --- | --- |
+| `B ⊂ A` | `R = A` | [`Identity(SELF_IDENT)`][`AlgebraicResult::Identity`] |
+| `A ⊂ B` | `R = B` | [`Identity(COUNTER_IDENT)`][`AlgebraicResult::Identity`] |
+| `A = B ≠ ∅` | `R = A = B`; the result equals both operands | [`Identity(SELF_IDENT \| COUNTER_IDENT)`][`AlgebraicResult::Identity`] |
+| `A ⊈ B` and `B ⊈ A` | `R` is a new, nonempty result containing information from both operands | [`Element`][`AlgebraicResult::Element`] |
+| `A = B = ∅` | `R = ∅` | [`None`][`AlgebraicResult::None`] |
+
+### Intersect (aka meet), `A ∩ B`
+
+| Case | Result | [`AlgebraicResult`] |
+| --- | --- | --- |
+| `A ⊂ B` and `A ≠ ∅` | `R = A`; the result is the smaller operand | [`Identity(SELF_IDENT)`][`AlgebraicResult::Identity`] |
+| `B ⊂ A` and `B ≠ ∅` | `R = B`; the result is the smaller operand | [`Identity(COUNTER_IDENT)`][`AlgebraicResult::Identity`] |
+| `A = B ≠ ∅` | `R = A = B`; the result equals both operands | [`Identity(SELF_IDENT \| COUNTER_IDENT)`][`AlgebraicResult::Identity`] |
+| `A ∩ B ≠ ∅`, `A ⊈ B`, and `B ⊈ A` | `R` is a new, nonempty result containing information common to both operands | [`Element`][`AlgebraicResult::Element`] |
+| `A ≠ ∅`, `B ≠ ∅`, and `A ∩ B = ∅` | `R = ∅` | [`None`][`AlgebraicResult::None`] |
+| `A = ∅` or `B = ∅` | `R = ∅` | [`None`][`AlgebraicResult::None`] |
+
+### Subtract, `A ∖ B`
+
+| Case | Result | [`AlgebraicResult`] |
+| --- | --- | --- |
+| `A ≠ ∅` and `A ∩ B = ∅` | `R = A` | [`Identity(SELF_IDENT)`][`AlgebraicResult::Identity`] |
+| `A ∩ B ≠ ∅` and `A ⊈ B` | `R` is a new, nonempty result containing the information in `A` that is not in `B` | [`Element`][`AlgebraicResult::Element`] |
+| `A = B` | `R = ∅`; an operand subtracts completely from itself | [`None`][`AlgebraicResult::None`] |
+| `A ⊆ B` | `R = ∅`; this is the general case of `A = B` | [`None`][`AlgebraicResult::None`] |
+| `A = ∅` | `R = ∅` | [`None`][`AlgebraicResult::None`] |
+
+For these operations, values at coincident paths are combined according to their own trait implementations, so their behavior may add another reason for a whole-map result to differ from either operand.
+
+### Restrict
+
+Restriction is currently a separate operation, but is conceptually a policy layered on meet. It keeps a path from `A` exactly when that path has a prefix carrying a value in `B`:
+
+`R = { a ∈ A | some b ∈ B is a prefix of a }`
+
+The phrase “prefix-covers `B`” below means that every path in `B` is a prefix of at least one path in `R`. This is a prefix relationship, not ordinary set containment. The rows describing a nonempty result can overlap; the refinements state whether restriction also dropped anything from `A`.
+
+| Case | Result | [`AlgebraicResult`] |
+| --- | --- | --- |
+| `A ≠ ∅` and every path in `A` is prefixed by a valued path in `B` | `R = A`; no path from `A` was dropped | [`Identity(SELF_IDENT)`][`AlgebraicResult::Identity`] |
+| `R = B ≠ ∅` and `A = B` | The result equals both operands; no path from `A` was dropped | [`Identity(SELF_IDENT)`][`AlgebraicResult::Identity`] |
+| `R = B ≠ ∅` and `A ≠ B` | The result equals `B`; the paths in `A ∖ B` were dropped | [`Element`][`AlgebraicResult::Element`] |
+| `R` prefix-covers `B`, `R ≠ B`, and `R = A` | `R` is a prefix-superset of `B`; no path from `A` was dropped | [`Identity(SELF_IDENT)`][`AlgebraicResult::Identity`] |
+| `R` prefix-covers `B`, `R ≠ B`, and `R ≠ A` | `R` is a prefix-superset of `B`; the paths in `A ∖ R` were dropped | [`Element`][`AlgebraicResult::Element`] |
+| Some, but not all, paths in `A` are prefixed by paths in `B`, and some paths in `B` serve as no prefix | `R` is a bespoke nonempty result; the unprefixed paths in `A` were dropped | [`Element`][`AlgebraicResult::Element`] |
+| `A = ∅` and `B = ∅` | `R = ∅`; both operands were empty | [`None`][`AlgebraicResult::None`] |
+| `A = ∅` and `B ≠ ∅` | `R = ∅`; only the left operand was empty | [`None`][`AlgebraicResult::None`] |
+| `A ≠ ∅` and `B = ∅` | `R = ∅`; only the right operand was empty, so every path in `A` was dropped | [`None`][`AlgebraicResult::None`] |
+| `A ≠ ∅` and `B ≠ ∅`, but no path in `A` is prefixed by a path in `B` | `R = ∅`; both operands were nonempty, but every path in `A` was dropped | [`None`][`AlgebraicResult::None`] |
+
+{{#include api_links.md}}

pathmap-book/src/SUMMARY.md

@@ -5,7 +5,8 @@
 - [PathMap Intro](./1.00.00_intro.md)
     - [Basic Structure](./1.00.01_basics.md)
 - [Algebraic Operations](./1.01.00_algebraic_ops.md)
-    - [Traits and Values](./1.01.01_algebraic_traits.md)
+    - [Trie and Value Lattices](./1.01.01_trie_and_value_lattice.md)
+    - [Traits and Values](./1.01.02_algebraic_traits.md)
 - [Zippers](./1.02.00_zippers.md)
     - [Base Trait](./1.02.01_zipper_trait.md)
     - [Value Access](./1.02.02_zipper_values.md)

pathmap-book/src/api_links.md

@@ -99,6 +99,17 @@
 [`join_into_take`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#tymethod.join_into_take
 [`join_into`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#tymethod.join_into
 [`join_k_path_into`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#tymethod.join_k_path_into
+[`ring`]: https://docs.rs/pathmap/latest/pathmap/ring/index.html
+[`Lattice`]: https://docs.rs/pathmap/latest/pathmap/ring/trait.Lattice.html
+[`DistributiveLattice`]: https://docs.rs/pathmap/latest/pathmap/ring/trait.DistributiveLattice.html
+[`AlgebraicResult`]: https://docs.rs/pathmap/latest/pathmap/ring/enum.AlgebraicResult.html
+[`AlgebraicResult::None`]: https://docs.rs/pathmap/latest/pathmap/ring/enum.AlgebraicResult.html#variant.None
+[`AlgebraicResult::Identity`]: https://docs.rs/pathmap/latest/pathmap/ring/enum.AlgebraicResult.html#variant.Identity
+[`AlgebraicResult::Element`]: https://docs.rs/pathmap/latest/pathmap/ring/enum.AlgebraicResult.html#variant.Element
+[`AlgebraicStatus`]: https://docs.rs/pathmap/latest/pathmap/ring/enum.AlgebraicStatus.html
+[`AlgebraicStatus::None`]: https://docs.rs/pathmap/latest/pathmap/ring/enum.AlgebraicStatus.html#variant.None
+[`AlgebraicStatus::Identity`]: https://docs.rs/pathmap/latest/pathmap/ring/enum.AlgebraicStatus.html#variant.Identity
+[`AlgebraicStatus::Element`]: https://docs.rs/pathmap/latest/pathmap/ring/enum.AlgebraicStatus.html#variant.Element
 [`join_map`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#tymethod.join_map
 [`make_map`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperSubtries.html#tymethod.make_map
 [`meet_2`]: https://docs.rs/pathmap/latest/pathmap/zipper/trait.ZipperWriting.html#tymethod.meet_2

src/dense_byte_node.rs

@@ -1857,7 +1857,11 @@ impl<V: Clone + Send + Sync + Lattice, A: Allocator, Cf: CoFree<V=V, A=A>, Other
         };
         let val_status = match self.val_mut() {
             Some(self_val) => match other_val {
-                Some(other_val) => self_val.join_into(other_val),
+                Some(other_val) => {
+                    let status = self_val.join_into(other_val);
+                    debug_assert!(!status.is_none(), "Lattice::join_into returned None for a join");
+                    status
+                },
                 None => AlgebraicStatus::Identity,
             },
             None => match other_val {