Tests fail when using semantic Eq for Term

[konstin]

Currently, Term uses a derived PartialEq/Eq in which negative and positive terms are never equal. Replacing it by the implementation below that uses the complement for a proper equals, tests start failing (confusing_with_lots_of_holes, prop_errors_the_same_with_only_report_dependencies, prop_limited_independence_of_irrelevant_alternatives, prop_removing_a_dep_cant_break). I'm trying to understand why that is, is pugrub relying on a non-mathematical implementation of equals in Term, and if so, why and what are the properties that need to be preserved when performing binary operations on two Terms?

///  A positive or negative expression regarding a set of versions.
#[derive(Debug, Clone)]
pub enum Term<VS: VersionSet> {
    /// For example, "1.0.0 <= v < 2.0.0" is a positive expression
    /// that is evaluated true if a version is selected
    /// and comprised between version 1.0.0 and version 2.0.0.
    Positive(VS),
    /// The term "not v < 3.0.0" is a negative expression
    /// that is evaluated true if a version is selected >= 3.0.0
    /// or if no version is selected at all.
    Negative(VS),
}

impl<VS: VersionSet> PartialEq for Term<VS> {
    fn eq(&self, other: &Self) -> bool {
        match (self, other) {
            (Self::Positive(r1), Self::Positive(r2)) => r1 == r2,
            (Self::Positive(r1), Self::Negative(r2)) => r1 == &r2.complement(),
            (Self::Negative(r1), Self::Positive(r2)) => &r1.complement() == r2,
            (Self::Negative(r1), Self::Negative(r2)) => r1 == r2,
        }
    }
}

impl<VS: VersionSet> Eq for Term<VS> {}

[Eh2406]

This took me a few attempts to get my head around when I was first optimizing the code base. I think I had a branch where I entirely removed Term and used VS directly - removing tests to make things work - until the prop tests pointed out that I was getting the wrong answer.

If a version is selected then Positive(r) <=> Negative(r.complement()), but they have different semantics when no version is selected. A Positive term in the partial solution requires a version to be selected. But a Negative term allows for a solution that does not have that package selected.

For example the incompatibility for not root is Negative(singleton(version)). Interpreted as "there shall be no solution (this negation from the definition of incompatibility) where root is different from version or where root is unselected". Whereas the incompatibility for no versions is the very similar Positive(set). Interpreted as "there shall be no solution where p is in set but if p is unselected that's fine". The proposed definition of equality means that the incompatibilities for "we require package p @ v" and "v is the only version of p" are equivalent. This builds up to bugs because "v is the only version of p" implies "we require package p @ v" implies "we need to select versions that match the dependencies of p @ v".

Here's a totally different way to think about it. A VS has the basic operation contains, which takes a V and returns a bool. A VS is a Set<V>, a set whose members are Vs. It takes a version and decides whether it's happy with that version. If Term had a contains operation, it would take an Option<V> and return a bool. A Term is a Set<Option<V>>, a set whose members are Option<V>s. It takes a (version|None) and decides whether it's happy with it. Because Term handles one more potential input than its underlying VS, Term needs to maintain one bit of additional data. The current implementation stores that bit in the Enum discriminate.

I have thought about adding contains to Term, or implementing VersionSet on Term, to hang this documentation on and make it clear to the next contributor what the differences. But I have not found a use for that method that is important enough for the next zealous contributor not to remove/ignore while simplifying things. I am open to additional code or a different representation if it makes these important distinctions easier to remember.

[konstin]

The question for me is, how should this behave through T1 <op> T2? E.g. for intersection and union we have on dev:

Intersection:

Positive, Positive -> Positive
Positive, Negative -> Positive
Negative, Positive -> Positive
Negative, Negative -> Negative

Union (First equals by dev definition):

Union(Positive, Positive) = Not (Intersection(Not Positive, Not Positive)) -> Not (Negative) -> Positive
Union(Positive, Negative) = Not (Intersection(Not Positive, Not Negative)) -> Not (Positive) -> Negative
Union(Negative, Positive) = Not (Intersection(Not Negative, Not Positive)) -> Not (Positive) -> Negative
Union(Negative, Negative) = Not (Intersection(Not Negative, Not Negative)) -> Not (Positive) -> Negative

But even when upholding that and using the derived equals definition, i'm getting failing tests.

[Eh2406]

By careful use of re-factor>in-line and repeatedly running tests, this seems to work:

    pub(crate) fn union(&self, other: &Self) -> Self {
        use self::Term::*;
        match (self, other) {
            (Positive(r1), Positive(r2)) => Positive(r1.union(r2)),
            (Positive(r1), Negative(r2)) => Negative(r1.complement().intersection(r2)),
            (Negative(r1), Positive(r2)) => Negative(r1.intersection(&r2.complement())),
            (Negative(r1), Negative(r2)) => Negative(r1.intersection(r2)),
        }
    }

This makes some amount of intuitive sense. The definition of union is that if an input is contained in either one, that must be contained in the union. And if either term is Negative then None is an included version and so must be included in the union.

[konstin]

I figured out why the tests still failed, is_disjoint has to return false for negative ∩ negative since it can never be a positive empty term.

Should we document the expectations on intersection and union?

[Eh2406]

I'm always up for more documentation or tests!

[konstin]

What i haven't fully understood yet, where a new positive or negative terms "minted", and how do the rules for intersections follow from this?

[Eh2406]

What i haven't fully understood yet, where a new positive or negative terms "minted"

They are constructed in the creation of incompatibilities. For example both kinds are used in the normal construction of a dependency incompatibility https://github.com/pubgrub-rs/pubgrub/blob/dev/src/internal/incompatibility.rs#L117

and how do the rules for intersections follow from this?

The definition of intersection is that an input is only contained in the intersection if it is contained in both. And if either term is Negative then None is an excluded version and so must be excluded in the intersection.