[red-knot] Move intersection type tests to Markdown #15396
Conversation
sharkdp
requested review from
carljm,
MichaReiser and
AlexWaygood
as code owners
This comment was marked as off-topic.
This comment was marked as off-topic.
Moves most of our existing intersection-types tests to a dedicated
Markdown test suite, extends the test coverage, unifies the notation
for these tests, groups tests into a proper structure, and adds some
explanations for various simplification strategies.
This changeset also:
- Adds a new simplification where `~Never` is removed from
intersections.
- Adds a new simplification where adding `~object` simplifies the
whole intersection to `Never`
- Avoids unnecessary assignment-checks between inferred and declared
type. This was added to this changeset to avoid many false positive
errors in this test suite.
sharkdp
force-pushed
the
david/intersection-type-tests
branch
from
7e8a1eb to
94447af
Compare
crates/red_knot_python_semantic/resources/mdtest/intersection_types.md
Outdated
Show resolved
Hide resolved
crates/red_knot_python_semantic/resources/mdtest/intersection_types.md
Outdated
Show resolved
Hide resolved
crates/red_knot_python_semantic/resources/mdtest/intersection_types.md
Outdated
Show resolved
Hide resolved
crates/red_knot_python_semantic/resources/mdtest/intersection_types.md
Outdated
Show resolved
Hide resolved
| `Never` represents the empty set of values, while `object` represents the set of all values, so | ||
| `~Never` is equivalent to `object`, and `~object` is equivalent to `Never`: |
There was a problem hiding this comment.
Just to make sure I understand properly: this follows from the intuition that the type ~int is really a shorthand way of saying object & ~int, and therefore ~Never is a shorthand for object & ~Never, which is the same as <the set of all possible objects> - <the empty set>, which is the same as <the set of all possible objects>, which is the object type. Right?
There was a problem hiding this comment.
Yes, exactly. In this document, I tried to move away a bit from how we represent these types internally. I think it's not important that we represent ~T as an intersection with a single negative contribution (where the empty "positive side" represents object). What's more important is that the negation-operation represents the set-theoretic complement w.r.t. the set of all possible values (object).
Set theory calls this set of all possible elements the "universe". In our case, object is the universe. And Never is the empty set ∅. The tests here are a manifestation of the universal complement laws
U∁ = ∅
∅∁ = U
I wonder if it makes sense to refer to these more set-theoretic terms in the document. And if it makes sense to test a few more of the laws in a systematic way (I think we probably test most of them already, but it's distributed across the whole document).
There was a problem hiding this comment.
That actually revealed one more thing that we could simplify. I chose not to implement this right now, as it seems rather costly: if we see T | ~T, we could simplify that to object. I added a test that describes that we don't perform this optimization at the moment.
There was a problem hiding this comment.
Let me know if you think that we should add this. I think it would be straightforward to add a (simple) version of this.
There was a problem hiding this comment.
Let me know if you think that we should add this.
The simplification of T | ~T to object? Yes, I think we probably should simplify that. But it can probably be done as a followup, right? This PR looks mergeable right now to me
crates/red_knot_python_semantic/resources/mdtest/intersection_types.md
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
Nice. The code changes feel like they're kinda papering over the underlying issue a little bit (we really should recognise int & Any as being assignable to int & Any!!), but I think skipping the assignability check for function-parameter definitions is probably a worthwhile optimisation anyway. So this LGTM
|
|
||
| ### Single-element unions | ||
|
|
||
| If we have a union of a single element, we can simplify to that element. Similarly, we show an |
There was a problem hiding this comment.
This should say "intersection of a single element"?
|
|
||
| #### Negative type and negative subtype | ||
|
|
||
| For negative contributions, this property is reversed. Here we can get remove superfluous |
There was a problem hiding this comment.
"Here we can get remove" -> "Here we can remove"
| #### Positive and negative contributions | ||
|
|
||
| If we intersect a type `X` with the negation of a disjoint type `Y`, we can remove the negative | ||
| contribution `~Y`, as it necessarily overlaps with the positive contribution `X`: |
There was a problem hiding this comment.
"overlaps" seems not strong enough here, since it only means "not disjoint from" -- what is needed for this simplification to be valid is recognizing that ~Y is necessarily a super-set of X, if X and Y are disjoint.
Summary
Rendered version of the new test suite
Moves most of our existing intersection-types tests to a dedicated Markdown test suite, extends the test coverage, unifies the notation for these tests, groups tests into a proper structure, and adds some explanations for various simplification strategies.
This changeset also:
~Neveris removed from intersections.~objectsimplifies the whole intersection toNeverResolves the task described in this old comment here.
Test Plan
Running the new Markdown tests