Skip to content

[flow analysis] Rework demotion and type of interest promotion. #4370

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 3 commits into
base: main
Choose a base branch
from

Conversation

stereotype441
Copy link
Member

@stereotype441 stereotype441 commented May 9, 2025

This formulation will be consisent with the behavior of the implementation once https://dart-review.googlesource.com/c/sdk/+/427920 lands.

Fixes dart-lang/sdk#60646.

This formulation is consisent with the behavior of the implementation.

Fixes dart-lang/sdk#60646.
Copy link
Member

@eernstg eernstg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM, with a bunch of comments.

- If `promoted` is `[]`, `T` is `declared`.
- Otherwise, `T` is the last type in the `promoted` list.

- `demote(promoted, written)`, where `promoted` is a list of types and `written`
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would expect this function to return the declared type if nothing else works, in which case we'd expect it to be invoked like demote([declared]+promoted, written). Is this true? In that case it would probably be easier to read the spec as a whole if declared is always included as part of promoted (and in that case it's guaranteed to be non-empty), or it is never included as part of promoted (in which case we might want to make it demote(declared, promoted, written)).

Another thing that came to mind: Perhaps the name could be something like demotionTypeCandidates rather than demote (or something which is shorter than demotionTypeCandidates, but still informative), because the operation isn't actually "promoting" anything, it is finding a set of candidates.

The set of candidates can be empty if written is unrelated to the declared type, so I wouldn't assume that we can use the empty result to encode anything like "just the declared type". Alternatively, it could give rise to a compile-time error if written is unrelated to the declared type, and then we could assign some other meaning to the empty result. (But this is probably not the abstraction level where compile-time errors should be mentioned).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would expect this function to return the declared type if nothing else works, in which case we'd expect it to be invoked like demote([declared]+promoted, written). Is this true? In that case it would probably be easier to read the spec as a whole if declared is always included as part of promoted (and in that case it's guaranteed to be non-empty), or it is never included as part of promoted (in which case we might want to make it demote(declared, promoted, written)).

Another thing that came to mind: Perhaps the name could be something like demotionTypeCandidates rather than demote (or something which is shorter than demotionTypeCandidates, but still informative), because the operation isn't actually "promoting" anything, it is finding a set of candidates.

If you're thinking of this operation as returning a set of candidates, then I think that's a sign that I've done a poor job of communicating my intent. My intent that at any given point in program execution, each variable is associated with a list of types called its "promotion chain". Informally, I imagine these promotion chains as dynamic entities that get updated in place by operations in the user's program. But since it's necessary for flow analysis to be able to refer back to previous states of the program (e.g., when handling control flow joins), the promotion chains are actually implemented (and specified) as immutable data structures, and with the operations that manipulate them returning updated promotion chains rather than modifying the existing promotion chains in place.

So, informally, the assign operation consists of two steps:

  • Demotion: Types are removed from the end of the promotion chain that are not supertypes of the written type.
  • Type of interest promotion: If there is a single "best" type of interest available to promote to, it is appended to the end of the promotion chain.

And then that gets converted to a purely functional form that looks more like:

  • Demotion: Given the promotion chain before the assignment, and the written type, a new promotion chain is formed. The new promotion chain is the same as the one before the assignment, but with zero or more types removed from the end.
  • Type of interest promotion: If there is a single "best" type of interest available to promote to, then a new promotion chain is formed by concatenating that type onto the end of the promotion chain that resulted from demotion. Otherwise, the promotion chain that resulted from demotion is kept without further modification.

This demote function is intended to implement the "demotion" step, which is why the thing it returns is a promotion chain rather than a set of candidates.

The set of candidates can be empty if written is unrelated to the declared type, so I wouldn't assume that we can use the empty result to encode anything like "just the declared type". Alternatively, it could give rise to a compile-time error if written is unrelated to the declared type, and then we could assign some other meaning to the empty result. (But this is probably not the abstraction level where compile-time errors should be mentioned).

It's true that if written is not a subtype of the declared type, the list returned by demote will be empty. But the converse isn't true: if the list returned by demote is empty, that doesn't mean that the assignment was erroneous. It could simply be that the assignment was fully demoting, and so the promotion chain is now empty. For example:

f(Object x) { // Declared type of `x` is `Object`, and promotion chain is `[]`.
  x as num; // Promotion chain is now `[num]`.
  x as int; // Promotion chain is now `[num, int]`.
  x = ''; // Promotion chain is now `[]` again.
}

Side note: my original informal description of flow analysis used the terminology "promotion chain"; that terminology got dropped when Leaf wrote the first draft of this spec. But I've noticed that others (Lasse in partuclar) still use that terminology. I wonder if it would be helpful to re-introduce it to this spec.

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

.. done a poor job of communicating my intent ..

Oh, that would be my bad, I don't think there is anything about the 'promotion chain' (immutable or mutable) or the following explanation which is surprising. I think I was incorrectly combining the roles played by the promotion chain and the types of interest.

However, I still don't think it's obvious why this function should have the name demote (it doesn't demote anything, as far as I can see). I think it's reducing the promotion chain by removing the types that are incompatible with written (such that we can maintain the invariant that the promotion chain is strictly decreasing). Perhaps the name could be reducePromotionChain? .. or something shorter and more elegant with a similar meaning, if anything comes to mind (reducePromoted?). filter is probably not a good word to use here because it sounds like it could remove elements from anywhere in promoted, not just a prefix.

(The phrase "promotion chain" makes a lot of sense to me, so let's just use that if it works well).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

.. done a poor job of communicating my intent ..

Oh, that would be my bad, I don't think there is anything about the 'promotion chain' (immutable or mutable) or the following explanation which is surprising. I think I was incorrectly combining the roles played by the promotion chain and the types of interest.

Ok, glad to hear it!

However, I still don't think it's obvious why this function should have the name demote (it doesn't demote anything, as far as I can see). I think it's reducing the promotion chain by removing the types that are incompatible with written (such that we can maintain the invariant that the promotion chain is strictly decreasing). Perhaps the name could be reducePromotionChain? .. or something shorter and more elegant with a similar meaning, if anything comes to mind (reducePromoted?). filter is probably not a good word to use here because it sounds like it could remove elements from anywhere in promoted, not just a prefix.

The reason demote makes sense to me (and the reason I think that it does, in fact, demote something), is because it's doing precisely the opposite job of promotion: promotion adds an entry to the end of the promotion chain; this function removes one or more entries from the end of the promotion chain. When we informally say something like "x used to be promoted to int, but then I assigned a double to it, so it's been demoted back to num", what's happening under the hood is that the type int is being removed from the promotion chain, and this is the function that's doing so.

(The phrase "promotion chain" makes a lot of sense to me, so let's just use that if it works well).

Cool. I'll add in that terminology in a separate PR.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(The phrase "promotion chain" makes a lot of sense to me, so let's just use that if it works well).

Cool. I'll add in that terminology in a separate PR.

Upon further reflection, the other changes I want to make to this PR will only make sense if I add the terminology now. So I will do so.

- If the `written` type is in `p2`, then `promoted` is `[demoted,
written]`. _Writing a value whose static type is a type of interest promotes
to that type._
- Otherwise:
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would be the location where written is not in p2, so this might be helpful:

Suggested change
- Otherwise:
- Otherwise _(when `written` is not in `p2`)_:

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done, although I'm not as certain that this is an improvement now that I've accepted your suggestion from line 441 that we require written to be a subtype of the current type. Let me know what you think.

denotes set subtraction)_.
- If the `written` type is in `p2`, then `promoted` is `[demoted,
written]`. _Writing a value whose static type is a type of interest promotes
to that type._
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would then be the location where written is a type in p2, and it is not a subtype of theCurrentType. So this is about demotion to a type of interest.

I think we'd use demote([declared, ...demoted], written) (possibly renamed as demotionTypeCandidates([declared, ...demoted], written)) to find the list of types that are of interest and supertypes of T, which would then be the value of promoted.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would then be the location where written is a type in p2, and it is not a subtype of theCurrentType. So this is about demotion to a type of interest.

I don't have a notion of "demotion to a type of interest" in my head when I think of flow analysis. As I mentioned above, I think of assignment as a two-step process: demotion, followed by promotion to a type of interest. In some cases a user might think that what's happening is demotion to a type of interest, e.g.:

f(Object x) {
  if (x is num) {} // `num` is now a type of interest
  x as int; // `x` is promoted to `int`
  x = 1.5; // `x` looks like it got "demoted" to `num`
}

But what really happened was that x got demoted from int to Object and then promoted to type of interest num.

Note that there are plenty of cases where type of interest promotion happens without any demotion, e.g.:

f(int? x) { // `int` is a type of interest
  if (x == null) {
    x = 0; // `x` is promoted to `int`
  }
}

In this case, demote returns an empty promotion chain (since there was no promotion prior to the assignment), and then toi_promote forms a new promotion chain by appending int onto it.

I think we'd use demote([declared, ...demoted], written) (possibly renamed as demotionTypeCandidates([declared, ...demoted], written)) to find the list of types that are of interest and supertypes of T, which would then be the value of promoted.

See my previous comment about why demote returns a promotion chain, not a set of type candidates.


- `demote(promoted, written)`, where `promoted` is a list of types and `written`
is a type, is a list containing all types `T` from `promoted` such that
`written <: T`. _In effect, this removes any type promotions that are not
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

And said list is ordered in the same way as promoted (that is, the list can be obtained by deleting some elements from promoted).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like this way of phrasing it, thanks! I've updated the text accordingly.

- Let `p3` be the set of all types `T` in `p2` such that `written <: T <:
currentType(declared, demoted)`.
- If `p3` contains exactly one type `T` that is a subtype of all the others,
then `promoted` is `[demoted, T]`. _Writing a value whose static type is
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Probably:

Suggested change
then `promoted` is `[demoted, T]`. _Writing a value whose static type is
then `promoted` is `[...demoted, T]`. _Writing a value whose static type is

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed, thanks!

Copy link
Member Author

@stereotype441 stereotype441 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks, Erik! I've made updates based on your comments. I saw that you gave me an LGTM, but since there's no rush here, I'll wait another day before landing the change in case you want to comment further.

- If `promoted` is `[]`, `T` is `declared`.
- Otherwise, `T` is the last type in the `promoted` list.

- `demote(promoted, written)`, where `promoted` is a list of types and `written`
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would expect this function to return the declared type if nothing else works, in which case we'd expect it to be invoked like demote([declared]+promoted, written). Is this true? In that case it would probably be easier to read the spec as a whole if declared is always included as part of promoted (and in that case it's guaranteed to be non-empty), or it is never included as part of promoted (in which case we might want to make it demote(declared, promoted, written)).

Another thing that came to mind: Perhaps the name could be something like demotionTypeCandidates rather than demote (or something which is shorter than demotionTypeCandidates, but still informative), because the operation isn't actually "promoting" anything, it is finding a set of candidates.

If you're thinking of this operation as returning a set of candidates, then I think that's a sign that I've done a poor job of communicating my intent. My intent that at any given point in program execution, each variable is associated with a list of types called its "promotion chain". Informally, I imagine these promotion chains as dynamic entities that get updated in place by operations in the user's program. But since it's necessary for flow analysis to be able to refer back to previous states of the program (e.g., when handling control flow joins), the promotion chains are actually implemented (and specified) as immutable data structures, and with the operations that manipulate them returning updated promotion chains rather than modifying the existing promotion chains in place.

So, informally, the assign operation consists of two steps:

  • Demotion: Types are removed from the end of the promotion chain that are not supertypes of the written type.
  • Type of interest promotion: If there is a single "best" type of interest available to promote to, it is appended to the end of the promotion chain.

And then that gets converted to a purely functional form that looks more like:

  • Demotion: Given the promotion chain before the assignment, and the written type, a new promotion chain is formed. The new promotion chain is the same as the one before the assignment, but with zero or more types removed from the end.
  • Type of interest promotion: If there is a single "best" type of interest available to promote to, then a new promotion chain is formed by concatenating that type onto the end of the promotion chain that resulted from demotion. Otherwise, the promotion chain that resulted from demotion is kept without further modification.

This demote function is intended to implement the "demotion" step, which is why the thing it returns is a promotion chain rather than a set of candidates.

The set of candidates can be empty if written is unrelated to the declared type, so I wouldn't assume that we can use the empty result to encode anything like "just the declared type". Alternatively, it could give rise to a compile-time error if written is unrelated to the declared type, and then we could assign some other meaning to the empty result. (But this is probably not the abstraction level where compile-time errors should be mentioned).

It's true that if written is not a subtype of the declared type, the list returned by demote will be empty. But the converse isn't true: if the list returned by demote is empty, that doesn't mean that the assignment was erroneous. It could simply be that the assignment was fully demoting, and so the promotion chain is now empty. For example:

f(Object x) { // Declared type of `x` is `Object`, and promotion chain is `[]`.
  x as num; // Promotion chain is now `[num]`.
  x as int; // Promotion chain is now `[num, int]`.
  x = ''; // Promotion chain is now `[]` again.
}

Side note: my original informal description of flow analysis used the terminology "promotion chain"; that terminology got dropped when Leaf wrote the first draft of this spec. But I've noticed that others (Lasse in partuclar) still use that terminology. I wonder if it would be helpful to re-introduce it to this spec.


- `demote(promoted, written)`, where `promoted` is a list of types and `written`
is a type, is a list containing all types `T` from `promoted` such that
`written <: T`. _In effect, this removes any type promotions that are not
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like this way of phrasing it, thanks! I've updated the text accordingly.

- Let `p2` be the set `p1 \ { currentType(declared, demoted) }` _(where `\`
denotes set subtraction)_.
- If the `written` type is in `p2`, then `promoted` is `[demoted,
written]`. _Writing a value whose static type is a type of interest promotes
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I feel like this is equivalent to what I've said, except that my way of saying it (promoted is [...demoted, written]) is consistent with the fact that promotion chains are considered to be immutable.

denotes set subtraction)_.
- If the `written` type is in `p2`, then `promoted` is `[demoted,
written]`. _Writing a value whose static type is a type of interest promotes
to that type._
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This would then be the location where written is a type in p2, and it is not a subtype of theCurrentType. So this is about demotion to a type of interest.

I don't have a notion of "demotion to a type of interest" in my head when I think of flow analysis. As I mentioned above, I think of assignment as a two-step process: demotion, followed by promotion to a type of interest. In some cases a user might think that what's happening is demotion to a type of interest, e.g.:

f(Object x) {
  if (x is num) {} // `num` is now a type of interest
  x as int; // `x` is promoted to `int`
  x = 1.5; // `x` looks like it got "demoted" to `num`
}

But what really happened was that x got demoted from int to Object and then promoted to type of interest num.

Note that there are plenty of cases where type of interest promotion happens without any demotion, e.g.:

f(int? x) { // `int` is a type of interest
  if (x == null) {
    x = 0; // `x` is promoted to `int`
  }
}

In this case, demote returns an empty promotion chain (since there was no promotion prior to the assignment), and then toi_promote forms a new promotion chain by appending int onto it.

I think we'd use demote([declared, ...demoted], written) (possibly renamed as demotionTypeCandidates([declared, ...demoted], written)) to find the list of types that are of interest and supertypes of T, which would then be the value of promoted.

See my previous comment about why demote returns a promotion chain, not a set of type candidates.

- If the `written` type is in `p2`, then `promoted` is `[demoted,
written]`. _Writing a value whose static type is a type of interest promotes
to that type._
- Otherwise:
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Done, although I'm not as certain that this is an improvement now that I've accepted your suggestion from line 441 that we require written to be a subtype of the current type. Let me know what you think.

- Let `p3` be the set of all types `T` in `p2` such that `written <: T <:
currentType(declared, demoted)`.
- If `p3` contains exactly one type `T` that is a subtype of all the others,
then `promoted` is `[demoted, T]`. _Writing a value whose static type is
Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fixed, thanks!

Copy link
Member

@eernstg eernstg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The assign operation will reduce the promotion chain by removing non-supertypes of written. Then it will add the best type of interest, iff there is a unique best one which is a supertype of written and a proper subtype of the last element in the reduced promotion chain. In any case, the new current type of the variable is the last element in [declared, promotionChain].

I think your informal description along these lines is very helpful.

However, I think the naming of various elements is confusing. I suggested a couple of changes (in particular demoted and current is confusing), but I think there may be a need to adjust even more names.

It is very much about local reasoning. If the requirements on each argument of the semantic functions are stated concisely and up front then those requirements can be relied upon when reading the rest of that definition (e.g., the definition of toi_promote). With the current style there is some post-hoc reasoning about why certain properties are guaranteed to hold, but that's too late because the reader needs to know these things already when reading from the beginning of the definition of each semantic function.

- If `promoted` is `[]`, `T` is `declared`.
- Otherwise, `T` is the last type in the `promoted` list.

- `demote(promoted, written)`, where `promoted` is a list of types and `written`
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

.. done a poor job of communicating my intent ..

Oh, that would be my bad, I don't think there is anything about the 'promotion chain' (immutable or mutable) or the following explanation which is surprising. I think I was incorrectly combining the roles played by the promotion chain and the types of interest.

However, I still don't think it's obvious why this function should have the name demote (it doesn't demote anything, as far as I can see). I think it's reducing the promotion chain by removing the types that are incompatible with written (such that we can maintain the invariant that the promotion chain is strictly decreasing). Perhaps the name could be reducePromotionChain? .. or something shorter and more elegant with a similar meaning, if anything comes to mind (reducePromoted?). filter is probably not a good word to use here because it sounds like it could remove elements from anywhere in promoted, not just a prefix.

(The phrase "promotion chain" makes a lot of sense to me, so let's just use that if it works well).

`tested` are lists of types, and `declared` and `written` are types, is the
list `promoted`, defined as follows. _("toi" stands for "type of interest".)_
- Let `current = currentType(declared, demoted)`. _(This is the type of the
variable after demotions, but before type of interest promotion.)_
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking at the invocation of toi_promote, I can see that the argument passed to demoted is the reduced promotion chain (that is, only the supertypes of written). However, it would surely be better to avoid the non-local reasoning and directly state that this is a requirement for every invocation of toi_promote: demoted contains only supertypes of written. This would be specified at the point where demoted is introduced in line 429-430.

This means that toi_promote is known to be a "pure" promotion operation: written is a subtype of the entire promotion chain already, so we'll leave it unchanged or add a single element (which is a subtype of the last element of [declared, ...demoted]).

But in that case I think it would be nice to use the name promotionChain for the second argument, because that's the role it is playing. We may or may not have reduced the previous promotion chain in order to get the one which is valid for an assignment of the type written, but that doesn't matter here, we just need to know that demoted/promotionChain is the current promotion chain.

Next, I think it's really confusing to use the word current and the function currentType to describe the last element in [declared, ...demoted], because there may not be any location in code where this type is the current type of that variable, it only occurs in the middle of the assign process.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking at the invocation of toi_promote, I can see that the argument passed to demoted is the reduced promotion chain (that is, only the supertypes of written). However, it would surely be better to avoid the non-local reasoning and directly state that this is a requirement for every invocation of toi_promote: demoted contains only supertypes of written. This would be specified at the point where demoted is introduced in line 429-430.

Done.

This means that toi_promote is known to be a "pure" promotion operation: written is a subtype of the entire promotion chain already, so we'll leave it unchanged or add a single element (which is a subtype of the last element of [declared, ...demoted]).

But in that case I think it would be nice to use the name promotionChain for the second argument, because that's the role it is playing. We may or may not have reduced the previous promotion chain in order to get the one which is valid for an assignment of the type written, but that doesn't matter here, we just need to know that demoted/promotionChain is the current promotion chain.

Done.

Next, I think it's really confusing to use the word current and the function currentType to describe the last element in [declared, ...demoted], because there may not be any location in code where this type is the current type of that variable, it only occurs in the middle of the assign process.

That's a fair point. I've removed the currentType function entirely (I just inlined it at the one place it was used), and I renamed current to provisionalType.

- Let `current = currentType(declared, demoted)`. _(This is the type of the
variable after demotions, but before type of interest promotion.)_
- If `written` and `current` are the same type, then `promoted` is
`demoted`. _(No type of interest promotion is necessary in this case.)_
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If demoted is renamed as promotionChain then promoted could be renamed as newPromotionChain.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

If demoted is renamed as promotionChain then promoted could be renamed as newPromotionChain.

Done.

interest promotes to that type._
- _Since `written` is the type assigned to the variable (after type
coercion), in non-erroneous code it is guaranteed to be a subtype of
`declared`. And `toi_promote` is always applied to the result of `demote`,
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should require at the beginning of the specification of toi_promote that [declared, ...demoted] is strictly decreasing, and written is a subtype of the last element in that list (not necessarily a proper subtype). We would then have that property here, and it could be checked for all invocations of toi_promote (of which we may have exactly one, but it generalizes easily if needed).

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think we should require at the beginning of the specification of toi_promote that [declared, ...demoted] is strictly decreasing, and written is a subtype of the last element in that list (not necessarily a proper subtype). We would then have that property here, and it could be checked for all invocations of toi_promote (of which we may have exactly one, but it generalizes easily if needed).

Done.

`declared`. And `toi_promote` is always applied to the result of `demote`,
so all types in `demoted` are guaranteed to be supertypes of
`written`. Therefore, the requirement that `written <: current` is
automatically satisfied for non-erroneous code._
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Again, stating the requirements up front and then checking them on invocations would eliminate the need for non-local reasoning.

I'm not quite sure about where to mention the compile-time errors that are raised when these constraints are violated, but it might be possible to say that the promotion operation can succeed or fail, and it is a compile-time error when it fails.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Again, stating the requirements up front and then checking them on invocations would eliminate the need for non-local reasoning.

Done.

I'm not quite sure about where to mention the compile-time errors that are raised when these constraints are violated, but it might be possible to say that the promotion operation can succeed or fail, and it is a compile-time error when it fails.

Ok, I think my latest rewrite addresses this. Rather than making wishy-washy statements about non-erroneous code, what I'm doing now is:

  • I've explicitly stated that a precondition of assign(x, E, M) is that the inferred type of E must be a subtype of x's declared type.
  • At each use of asign(x, E, M), I've clarified that E is the result of performing type coercion to the declared type of x, and therefore the precondition is satisfied.

@stereotype441
Copy link
Member Author

The assign operation will reduce the promotion chain by removing non-supertypes of written. Then it will add the best type of interest, iff there is a unique best one which is a supertype of written and a proper subtype of the last element in the reduced promotion chain. In any case, the new current type of the variable is the last element in [declared, promotionChain].

I think your informal description along these lines is very helpful.

However, I think the naming of various elements is confusing. I suggested a couple of changes (in particular demoted and current is confusing), but I think there may be a need to adjust even more names.

It is very much about local reasoning. If the requirements on each argument of the semantic functions are stated concisely and up front then those requirements can be relied upon when reading the rest of that definition (e.g., the definition of toi_promote). With the current style there is some post-hoc reasoning about why certain properties are guaranteed to hold, but that's too late because the reader needs to know these things already when reading from the beginning of the definition of each semantic function.

This is a really good point, thank you. I think my latest revisions should address most of these issues. (I'm still using the name demote, though; see #4370 (comment) for why I still think it's a good name).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Flow analysis. Variable can be promoted to the type which is not subtype of its current type.
2 participants