Description
Description
The complement ~T of a type is disjoint from the type T itself. In fact, it is disjoint from all subtypes of S <: T.
It is rather straightforward to implement this. The problem I am facing is that this leads to new property test failures, because it breaks the symmetry of the is-disjoint-from relation when done naively.
The reason for that are pairs like T & Any and ~T. In one direction, if we check if T & Any is disjoint from ~T, we start by checking if any positive element of the intersection T & Any is disjoint from ~T. And since T is disjoint from ~T according to this new check, we return true, as we should.
But when we check if ~T is disjoint from T & Any, we have no positive elements in the left-hand side intersection. The only remaining check is therefore the new check which tries if T & Any is a subtype of T. This is not the case, because T & Any is not fully-static. But if feels like this "is-subtype-of" relation in the check could be replaced by a subtyping-relation on gradual types that would check if all materializations of S are subtypes of all materializations of T (which is different from the consistent-subtype relation on gradual types).
For context, this came up when trying to write the following test that intends to demonstrate that AlwaysTruthy/AlwaysFalys are disjoint from AmbiguousTruthiness
type Truthy = Not[AlwaysFalsy]
type Falsy = Not[AlwaysTruthy]
type AmbiguousTruthiness = Intersection[Truthy, Falsy]
static_assert(is_disjoint_from(AlwaysTruthy, AmbiguousTruthiness))
static_assert(is_disjoint_from(AlwaysFalsy, AmbiguousTruthiness))