[flow analysis] Clean up documentation of promotion chains, add Lean model. by stereotype441 · Pull Request #4754 · dart-lang/language

stereotype441 · 2026-08-27T00:31:52Z

This PR adds a top level directory lean, containing the beginnings of a Lean model of the behavior of flow analysis. Currently the model includes:

An abstraction of the Dart type system, defining some of the operations needed by flow analysis (I will expand on this abstaction as needed).
A concrete simplified model of the Dart type system, omitting complications that are irrelevant to flow analysis (such as support for f-bounded types). This model is defined as an instantiation of the above abstraction.
A model of promotion chains and their properties.

I intend to build out this model as part of documenting (and improving) the flow analysis specification.

The Lean code builds locally without errors (which validates all the theorems contained in it). In a follow-up PR I intend to add a github check that will verify that the code continues to build without errors.

The PR also makes the following improvements to flow-analysis.md:

The notation for lists has been changed to use ++ for list concatenation. This is easier to precisely explain than the old notation using ..., and is more consistent with the Lean model.
The notion of a subsequence is defined, using the symbol <+ (which Lean also uses, though it uses the terminology "sublist"). This is used to prove that the join of two promotion chains is a promotion chain (see below).
The notion of strict subtyping is defined, using the symbol <<:. Note that the Lean model uses ≤ for subtyping and < for strict subtyping, since this allows a number of convenient theorems to come into play.
The definition of promotion chains has been moved to its own section.
The notion of a promotion chain being "valid for declared type T" has been renamed to "strictly bounded by T". This lays the groundwork for future PRs that will specify the behavior of private field promotion. (I will want to avoid talking about the "declared type" of a field, because of ambiguities that arise when a field is declared with one type in one class and then overridden with another type in a subclass.)
The join algorithm for promotion chains is now fully specified. A sketch is given of the proof that this algorithm is idempotent and commutative, and a counterexample illustrates that it is not associative. I will file an issue to discuss whether to change to an algorithm that is associative.

…model. This PR adds a top level directory `lean`, containing the beginnings of a Lean model of the behavior of flow analysis. Currently the model includes: - An abstraction of the Dart type system, defining some of the operations needed by flow analysis (I will expand on this abstaction as needed). - A concrete simplified model of the Dart type system, omitting complications that are irrelevant to flow analysis (such as support for f-bounded types). This model is defined as an instantiation of the above abstraction. - A model of promotion chains and their properties. I intend to build out this model as part of documenting (and improving) the flow analysis specification. The Lean code builds locally without errors (which validates all the theorems contained in it). In a follow-up PR I intend to add a github check that will verify that the code continues to build without errors. The PR also makes the following improvements to `flow-analysis.md`: - The notation for lists has been changed to use `++` for list concatenation. This is easier to precisely explain than the old notation using `...`, and is more consistent with the Lean model. - The notion of a subsequence is defined, using the symbol `<+` (which Lean also uses, though it uses the terminology "sublist"). This is used to prove that the join of two promotion chains is a promotion chain (see below). - The notion of strict subtyping is defined, using the symbol `<<:`. Note that the Lean model uses `≤` for subtyping and `<` for strict subtyping, since this allows a number of convenient theorems to come into play. - The definition of promotion chains has been moved to its own section. - The notion of a promotion chain being "valid for declared type `T`" has been renamed to "strictly bounded by `T`". This lays the groundwork for future PRs that will specify the behavior of private field promotion. (I will want to avoid talking about the "declared type" of a field, because of ambiguities that arise when a field is declared with one type in one class and then overridden with another type in a subclass.) - The join algorithm for promotion chains is now fully specified. A sketch is given of the proof that this algorithm is idempotent and commutative, and a counterexample illustrates that it is not associative. I will file an issue to discuss whether to change to an algorithm that _is_ associative.

lrhn · 2026-08-27T13:50:45Z

-    type in `p` is a subtype of `T`. _Note that since the subtyping relation is
-    transitive, in order to establish that `p` is valid for declared type `T`,
-    it is sufficient to check that the first type in `p` is a subtype of `T`._
+  - We use the notation `l₁ ++ l₂` to denote the concatenation of lists.


Very nice use of Unicode!
I don't think there is anything looking like <+, but how about ⪿? Or any of ⋲, ⋳ or just plain old ∊? (I'll stop now 😁 )

I could possibly get behind ⪿, though I worry a little that it people will interpret it as an exclusive subsequence (by analogy to ⊂). The relation I'm trying to define is inclusive.

⋲, ⋳, and ∊ worry me because of potential confusion with ∈, which I would like to reserve for denoting list membership (i.e. x ∈ l iff ∃k, l[k] = x).

<+ has the advantage of being consistent with the Lean code.

I asked Gemini for suggestions and it offered some more alternatives:

⊑ (apparently common in computer science papers, although some people use this to mean "contiguous prefix")

≼

⊆ₒ ("subset ordered")

🤷 I could probably be happy with any of these.

I like using operators for operations that are extremely common and have a well-known familiar operator already. For other operations, I would be inclined to use a readable name.

I think ++ for concatenation is familiar enough to work well (and I like that it disambiguates from addition).

I'm less enthused about using a Unicode operator for "subsequence" which is already a fairly unfamiliar operation. Maybe just subseq(l₁, l₂) or l₁ subseq l₂ if you think the latter helps clarify which argument is a subsequence of the other?

Ok, I'm convinced that using a custom operator for "subsequence" is more clever than necessary. I've changed to subseq(l₁, l₂).

lrhn · 2026-08-27T14:07:05Z

+### Promotion chains
+
+A list of types `c` is called a _promotion chain_ iff, for all `i < c.length -
+1`, `c[i + 1] <<: c[i]`.


(Complete side-track, because I was looking at it for another reason. If we have

void foo<X extends Never, Y extends X>(X value) { if (value is Y) { // Not promoting to X&Y because X and Y are mutual subtypes (both bottom). } }

Should we promote value to X&Y here? Or will flow analysis recognize that we never take the branch anyway, and not promote because of that. (Not that we can ever call the function.)

It probably doesn't matter in any way, because the result is assignable to Y whether we promote or not (it's a bottom type), and it has all members (it's a bottom type).
And because the code can't possibly be run either way.
That means we can't ever have an X&R where X is bottom-bounded, and UP of any two bottom types can just be Never, you can't tell the difference.)

Currently we don't promote to X&Y because, as you say, X and Y are mutual subtypes. Despite the messy state of the spec, I believe the implementation is solidly consistent in maintaining the invariants that

Every type in a promotion chain is a strict subtype of the previous.

The promotion chain for a local variable is always strictly bounded by the local variable's (declared or inferred) unpromoted type. (Private field promotion is a whole other story that I'll get to documenting in a later PR.)

I definitely want to keep the first invariant, because without it, join gets messy. I'd prefer to keep second invariant too, because it feels nicely consistent with the first. So my vote would be to keep the current behavior of not promoting to X&Y in this case.

lrhn · 2026-08-27T15:52:42Z

-  valid for declared type `declared`, and all types `T` in `promotionChain`
-  satisfy `written <: T`, is the promotion chain `newPromotionChain`, defined as
+  strictly bounded by `declared`, and all types `T` in `promotionChain` satisfy
+  `written <: T`, is the promotion chain `newPromotionChain`, defined as


<:, not <<: ....

Yeah, this section is a bit of a mess, and definitely doesn't line up with the current implementation behavior. I'd prefer to leave it as is for now, and come back to it in a later PR so I can think about it as a whole and get it right.

lrhn · 2026-08-27T15:55:48Z

    difference)_.
  - If the `written` type is in `p2` then `newPromotionChain` is
-    `[...promotionChain, written]`. _Writing a value whose static type is a
+    `promotionChain ++ [written]`. _Writing a value whose static type is a


.... and here we push written even though the last element of promotionChain could be a mutual subtype of it.
(We only check whether they're the same type in the case above, not whether it's a mutual subtype, and the constraints on promotionChain only requires written <: T, not <<:.)

Acknowledged. I will address this in a follow-up PR.

lrhn · 2026-08-27T15:57:30Z

      in `promotionChain`. Therefore, `newPromotionChain` satisfies the
-      definition of a promotion chain, and is valid for declared type
-      `declared`._
+      definition of a promotion chain, and is strictly bounded by `declared`._


Except it doesn't because written <: T is not sufficient, it needs written <<: T.
(Is this what's implemented, and can we make something break?)

Acknowledged. The current implementation doesn't have this mistake. I will address this in a follow-up PR.

lrhn · 2026-08-27T16:00:14Z

      to._
      - _Since `T <: provisionalType <: declared`, and all types `U` in
        `promotionChain` satisfy `provisionalType <: U`, it follows that all
        types `U` in `promotionChain` satisfy `T <: U`. Therefore


Probably can't break this. If the provisional type is a mutual subtype of written, then any type T in p2 where written <: T <: provisionalType is also a mutual subtype, and since provisionalType is probably also a type of interest, there won't be a least.

Acknowledged. I will clean this up in a follow-up PR.

lrhn · 2026-08-27T16:01:01Z

    - `VM = VariableModel(declared, promotionChain, tested, true, false, captured)`.
  - Otherwise:
    - Let `written = T`.
    - Let `promotionChain' = demote(promotionChain, written)`.


(Only place demote is used, right?)

lrhn · 2026-08-27T16:02:39Z

I think the promotion chain join can be improved.
(And there are some places where I don't think we're handling mutual subtypes correctly in assingment promotion, but not sure if it's something that's a real problem.)

munificent · 2026-08-28T19:50:35Z

-    type in `p` is a subtype of `T`. _Note that since the subtyping relation is
-    transitive, in order to establish that `p` is valid for declared type `T`,
-    it is sufficient to check that the first type in `p` is a subtype of `T`._
+  - We use the notation `l₁ ++ l₂` to denote the concatenation of lists.


I like using operators for operations that are extremely common and have a well-known familiar operator already. For other operations, I would be inclined to use a readable name.

I think ++ for concatenation is familiar enough to work well (and I like that it disambiguates from addition).

I'm less enthused about using a Unicode operator for "subsequence" which is already a fairly unfamiliar operation. Maybe just subseq(l₁, l₂) or l₁ subseq l₂ if you think the latter helps clarify which argument is a subsequence of the other?

munificent · 2026-08-28T19:52:31Z

+    l₂.length`._
+  - We use the notation `l₁ <+ l₂` to denote that `l₁` is a subsequence of
+    `l₂`. That is, `l₁ = [l₂[k₀], l₂[k₁], ... l₂[kₙ₋₁]]` for some `k₀ < k₁ <
+    ... < kₙ₋₁`. _Note that subsequences need not be contiguous._


The non-contiguous callout is helpful here. I definitely didn't assume that at first.

stereotype441 · 2026-08-28T22:55:11Z

I think the promotion chain join can be improved. (And there are some places where I don't think we're handling mutual subtypes correctly in assingment promotion, but not sure if it's something that's a real problem.)

To summarize my comments above (since Github makes it hard to thread conversations):

Regarding your proposed improvement to promotion chain join, I love it! I've filed Simplify promotion chain join #4757 to track it. I'll leave this PR as is since it correctly documents the current behavior (though I did add a link). Let me know if Simplify promotion chain join #4757 is missing any crucial information.
Regarding the mishandling of mutual subtypes correctly in assignment promotion, the text of the spec definitely doesn't match the implementation. Possibly in benign ways, possibly not. I'm not sure. I'd prefer to leave it as is and return to it in a later PR so I can think carefully about it and get it right.

stereotype441 requested a review from lrhn August 27, 2026 00:31

lrhn reviewed Aug 27, 2026

View reviewed changes

Address some code review comments

a260a26

munificent approved these changes Aug 28, 2026

View reviewed changes

stereotype441 mentioned this pull request Aug 28, 2026

Simplify promotion chain join #4757

Open

Address more code review comments

e64956c

Uh oh!

Conversation

stereotype441 commented Aug 27, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

lrhn commented Aug 27, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

stereotype441 commented Aug 28, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants