[ty] Some more simplifications when rendering constraint sets

[dcreager]

This PR adds another useful simplification when rendering constraint sets: T = int instead of T = int ∧ T ≠ str. (The "smaller" constraint T = int implies the "larger" constraint T ≠ str. Constraint set clauses are intersections, and if one constraint in a clause implies another, we can throw away the "larger" constraint.)

While we're here, we also normalize the bounds of a constraint, so that we equate e.g. T ≤ int | str with T ≤ str | int, and change the ordering of BDD variables so that all constraints with the same typevar are ordered adjacent to each other.

Lastly, we also add a new display_graph helper method that prints out the full graph structure of a BDD.

[dcreager]

Pushing this up for initial CI checks and to checkpoint my work. Will add some mdtests highlighting the rendering change tomorrow

[github-actions]

Diagnostic diff on typing conformance tests

No changes detected when running ty on typing conformance tests ✅

[github-actions]

mypy_primer results

No ecosystem changes detected ✅
No memory usage changes detected ✅

[dcreager]

Before this PR, this rendered as

((T@_ = bool) ∧ (U@_ = bool) ∧ (U@_ ≠ str)) ∨ ((T@_ = bool) ∧ (U@_ = str)) ∨ ((T@_ = str) ∧ (T@_ ≠ bool) ∧ (U@_ = bool) ∧ (U@_ ≠ str)) ∨ (T@_ = str)

and the display_graph rendering for this BDD is

  (T@_ = str)
  ┡━₁ (U@_ = str)
  │   ┡━₁ always
  │   └─₀ (U@_ = bool)
  │       ┡━₁ always
  │       └─₀ never
  └─₀ (T@_ = bool)
      ┡━₁ (U@_ = str)
      │   ┡━₁ always
      │   └─₀ (U@_ = bool)
      │       ┡━₁ always
      │       └─₀ never
      └─₀ never

[dcreager]

This is the big one that lets us simplify T = int ∧ T ≠ str to T = int when displaying.

[AlexWaygood]

thank you!

[AlexWaygood]

I think I might have stumbled across this terminology in one of your PRs before 😅

When you say "render" here, are you just talking about "display rendering"? I.e., this "rendering" should have no impact on semantics?

[dcreager]

Yeah, I mean "render" in the sense of "create a visual representation of", like you'd render an image. It doesn't change the semantics at all, just how the constraint sets are displayed. I can change this to "display"

[AlexWaygood]

I sort of have the same question as Micha in #21009 (review) in that case. If we do this simplification only when displaying these constraints, isn't there a risk that we'll be seeing something different to what is "actually happening behind the scenes" when we try to debug these constraints? The simplification logic isn't trivial! It feels like it would be safer to always apply these simplifications, so that we can be sure that what we see when we debug these constraints is actually what's being used in our subtyping/assignability logic by ty in production

[dcreager]

The issue is that we're talking about two completely different representations, that are used for different purposes.

As an example, one of the display simplifications that this PR adds would simplify T = int ∧ T ≠ str into T = int. If you know that T is an int, it doesn't add any information to say that it is also not a str.

We could create a BDD for T = int ∧ T ≠ str. Depending on what ordering Salsa assigns IDs, the BDD structure you get is either

(T = int)
  ┡━₁ (T = str)
  │   ┡━₁ never
  │   └─₀ always
  └─₀ never

or

(T = str)
  ┡━₁ never
  └─₀ (T = int)
      ┡━₁ always
      └─₀ never

The equivalent transformation that you'd perform on the BDD would be something like "for any path through the BDD where T = int is true, you don't need to check T = str, because it must always be false".

We actually do already perform that transformation! But it's not necessarily going to simplify the BDD. It might actually make it more complex! For instance, if the BDD is checking other stuff as well, there might be other reasons we need a node that checks T = str. Since every node must have two outgoing edges, it might not be possible to remove it even if we wanted to.

(And going further into the weeds as an aside, in the BDD structure, we actually don't really ever want to throw information away, since it makes it easier to compare two BDDs without having to know in advance which particular constraints they check. The better analogue of the transformation we perform is "it's impossible for T = int to be true and T = str to be false, so when comparing two BDDs ignore any path with those assignments".)

So even though we have performed these transformations on the BDD already, we might still end up with constraints in the rendered formula that are redundant. And so I wanted to be able to print out the simplest formula that faithfully captures the BDD.

that we can be sure that what we see when we debug these constraints is actually what's being used in our subtyping/assignability logic by ty in production

The other possibility here is that we would avoid performing any display substitutions at all. Then the formula that we print out would be a more direct representation of the BDD structure. But I was finding that very confusing, because even simple cases end up looking more complex than they need to. (A prime example is that half of the time x ∨ y will display as x ∨ y, and half the time as (x ∧ ¬y) ∨ y.)

[AlexWaygood]

Thanks for the explanation. That makes sense to me :-)

[MichaReiser]

I'm a bit out of my comfort zone here, so please forgive any dumb questions 😅

This PR adds another useful simplification when rendering constraint sets: T = int instead of T = int ∧ T ≠ str. (The "smaller" constraint T = int implies the "larger" constraint T ≠ str. Constraint set clauses are intersections, and if one constraint in a clause implies another, we can throw away the "larger" constraint.)

What's the reason why we only do this during rendering and don't apply this as a general simplification?

[MichaReiser]

Clever :)

[github-actions]

ruff-ecosystem results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

Formatter (stable)

✅ ecosystem check detected no format changes.

Formatter (preview)

✅ ecosystem check detected no format changes.