Negated types

[ssalbdivad]

This would allow some or all types to be negated (likely using a new ! operator). The challenge here would be integrating these checks with the type system so that intersections can still be reduced to the fullest extent possible.

If this turns out to not be feasible, we could implement it shallowly using a similar approach to narrows where we'd only check equality to determine assignability, or could potentially restrict the set of types that could be negated to literals.

More investigation required.

A couple additional notes after spending a minute thinking about this:

My intuition is that there'd be a "negated" node that could be attached to each branch node. You'd maintain it opposite the normal node- intersections would be attached as unions. It's kind of mind bending that it could essentially continue to invert but maybe the recursion would work everything out and it would be doable. All the second level negations would be intersected back up to the base type? But what if they're in branches of a union? That seems like a problem.

A couple notes based on a followup conversation:

ssalbdivad: Say you have !T. You intersect this with !U. The result could either be represented as !T & !U or !(T | U). In this case, a negated type would be a constraint like any other attached to an intersection

ssalbdivad: So in this scenario, say that T actually already had attached to it another negated type, !A.

ssalbdivad: To reduce the negation of T, you would have to intersect A (now unnegated) with the intersection !T & !U is being attached to

ssalbdivad: Is it possible this will never actually require you to use a union directly in your representation? I still have to think that through, maybe it's possible to distribute it so each negation is only ever an intersection. That would solve the problem

ssalbdivad: Maybe the key is just using !T & !U instead of !(T | U) like I was thinking initially

ssalbdivad: Yeah that makes sense because negation can always be distributed over a union

ssalbdivad: So that would never be the reduced representation anyways

ssalbdivad: You just have to make sure when you define the intersection, you define it in such a way that behaves like reducing a union

TypeHoles: Sounds about right.

ssalbdivad: So if we have the first representation

ssalbdivad: Could every second-level negated type could be directly intersected with the base intersection and pruned from the negations? So you'd only ever have one level of negation?

ssalbdivad: I think so. I think my problem is when I thought "oh yeah, intersecting negations would act like a union" I thought it had to be represented that way but it just has to be reduced that way

ssalbdivad: Oh wait no this was wrong 😞 The behavior has to act like a union because !T could be satisfied by any constraint of T not being satisfied, not just the negated ones. Intersecting !A from T back up to the base intersection as A doesn't work

ssalbdivad: This object foo thing is kind of weird with objects being the only types that can have arbitrary props so we'll change it to {a: 0, b: 1} ssalbdivad: You could negate it as !{a: 0} | !{b: 1} ssalbdivad: So if you intersected that with e.g. {b: 1} you could reduce the negated portion to !{ a: 0 } ssalbdivad: If the last negated branch is ever pruned the type is unsatisfiable