generics: Expand and revise demos of how to test generic types (per-account interlude, 3.2/n)

[gnprice]

This follows up on #5043 (comment) with a consolidated and reworked discussion of why (a) you need to make a value-level flow to or from a type in order to get any errors from the type itself being bogus, and (b) that flow doesn't help if it's from empty or to mixed.

[chrisbobbe]

Thanks, this is helpful! See a few comments below.

[chrisbobbe]

I think there's some room for confusion with names here.

In variance_again, we have S <: T. Here, and some more times below, S and T are part of what gets passed to IsSupertype.

IsSupertype's params are also named S and T. And in IsSupertype's happy case, its S and T have T <: S.

Does this make sense? I'm not sure if it needs to be fixed, or which side (or both) to change if so. But it stood out to me.

[gnprice]

Thanks, yeah. Probably clearest to give these different names (like A and B). In different test cases here, these two type variables we've gotten at variance_again end up getting fed into either side of IsSupertype; so if we give them the same names S and T, in either order, then if you're looking at the IsSupertype definition while reading these you'll find them confusingly cross-aligned some of the time.

[chrisbobbe]

nit: can remove declare var magic: empty; line above

[chrisbobbe]

nit: I think this blank line can be removed, so all of these three cases become one stanza. The bullet point above is, "If the flow is from a bogus type to mixed or to itself […]".

[gnprice]

Hmm, I think of these stanzas as corresponding to the three points above that 🙂, which describe the different logical rules Flow is using. That anything flows to mixed is one fact (symmetrical with the one that empty flows to anything); that anything flows to itself is another.

The two bullet points are about reasons why these rules don't lead to bogus types being actually realized at runtime without a type error somewhere. That reason happens to be the same for the T <: T rule as the T <: mixed rule, and different from the empty <: T rule.

I might try to make that clearer.

[chrisbobbe]

  //  * If the flow is from a bogus type to `mixed` or to itself, then that
  //    flow can only be realized at runtime if a value somehow got into the
  //    bogus type in the first place.

What if the flow is from a bogus type to something other than mixed or itself? Does that imply that the flow might be realizable at runtime even if a value didn't get into the bogus type in the first place? I think maybe it doesn't. Can this bullet point be made a bit clearer?

To check my understanding:

• When Flow checks a flow from F to T, it'll check as valid iff it thinks F <: T (where F and T aren't unclear types like any or Object, I guess).
• If T is mixed, the flow is always checked as valid. There, Flow reasonably thinks F <: T because mixed is a "top" type. And mixed is a "top" type whether or not F is bogus, so Flow doesn't bother checking if F is bogus.
• If T is F, the flow is always checked as valid. There, Flow reasonably thinks F <: T because the subtype relation is reflexive. And the subtype relation is reflexive whether or not F is bogus, so Flow doesn't bother checking if F is bogus.
• But since Flow can ignore F being bogus; and (a) F being bogus implies that no value can get into the F type in the first place, and (b) when you can't get a value into F in the first place, the flow from F to T can't be realized at runtime; then when Flow checks the flow from F to T, it sometimes doesn't catch that it can't be realized at runtime.

Is this right?

I do wonder if it's always a type error to try to get a value into a bogus type F (my "a" in the last bullet point). If so, then I wonder if the following two scenarios (higher up in this code comment) are redundant with each other and could be collapsed into one:

either there is a type error somewhere else, or it is impossible for an actual value at runtime to traverse that data flow.

(Looking at that, it seems like the first part was meant to refer to the flow-from-empty case, and the second was about this mixed and "the type itself" thing.)

[gnprice]

What if the flow is from a bogus type to something other than mixed or itself?

Then that's the normal case of using a bogus type. (Well, that together with a flow to a bogus type from something other than empty or itself.)

In that case (unless some other general rule of the type system applies, in the same spirit as the empty <: T, T <: mixed, and T <: T rules demo'd here), the flow should already cause Flow to look closer at the type and see it's bogus, and give an error.

Does that imply that the flow might be realizable at runtime even if a value didn't get into the bogus type in the first place?

Hmm. The background idea here is meant to be: if there's a flow from point A in the program (some expression, or variable, or object property, etc.) to point B, then for an actual value at runtime to go from point A to point B, the value must have gotten into point A in the first place.

So in particular if there's a flow from point A which has some bogus type, to point B which has whatever type, and that flow is realized at runtime, then the value must have gotten to point A, which has that bogus type. So if there isn't a type error somewhere, then whatever flow got it to point A must have somehow not caused a type error.

• When Flow checks a flow from F to T, it'll check as valid iff it thinks F <: T

Yeah. That's basically what the notation <: means when talking about Flow -- it means that Flow would accept a flow from something of type F to something of type T.

(where F and T aren't unclear types like any or Object, I guess).

(The way I'd describe this is actually that for all T, T <: any and any <: T. Similarly T <: Object and Object <: T for any T that's an object type.)

• If T is mixed, the flow is always checked as valid. There, Flow reasonably thinks F <: T because mixed is a "top" type. And mixed is a "top" type whether or not F is bogus, so Flow doesn't bother checking if F is bogus.
• If T is F, the flow is always checked as valid. There, Flow reasonably thinks F <: T because the subtype relation is reflexive. And the subtype relation is reflexive whether or not F is bogus, so Flow doesn't bother checking if F is bogus.

Yep!

• […] it sometimes doesn't catch that it can't be realized at runtime.

Hmm, perhaps this phrasing was confusing!

I mean "can't be realized at runtime" as a description of a good thing, a mitigating thing, when one of the ends of the flow is bogus.

That is: it seems bad that Flow cheerfully lets you write these bogus types. And it is somewhat bad and I think ideally Flow wouldn't do it. (One likely reason it doesn't is performance: it notices that some flow it's checking goes to mixed, and can immediately check it off as good and move on, without going and digging each time into the details of the source type.) But it's not too bad, because at least when that happens, it can't happen in a situation that's actually some part of the code that can actually operate at runtime (without a type error somewhere else.)

Does that help?

[chrisbobbe]

Does that help?

Yes, thanks very much!! 🙂

[gnprice]

And merged, with revisions. Thanks for the careful review!

Please take a look at the new version; if something's still unclear, we can always edit the comments further.

[chrisbobbe]

Please take a look at the new version; if something's still unclear, we can always edit the comments further.

Great, thanks! I've just looked at the range-diff and it LGTM. Thanks for adding all these comments and tests so attentively!