arktype
arktype copied to clipboard
Negated types
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 ofT
not being satisfied, not just the negated ones. Intersecting!A
from T back up to the base intersection asA
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