This is already defined on page 144 of the latest spec at spec.dart.dev, consider just referencing that rather than duplicating?

As I see it, there’s an important difference. The spec notion of “T is T₀ bounded” is a relation between types but not a function. For example, if A and B are type variables, the bound of A is B, and the bound of B is C, then A is considered to simultaneously be A bounded, B bounded, and C bounded.

The notion I’m defining here is a total function: considering the same example, the “bound resolution” of A is uniquely C. The way I use this notion later in the PR relies on it being a total function (a step in the “Method invocation inference” procedure is "Let U_0 be the bound resolution of T_0").

The two notions are definitely related, and I guess we could define bound resolution in terms of "T₀ bounded" as follows:

The bound resolution of T is the unique type T₀ such that T₀ is neither a type variable nor a union of the form X&B.

But then we would need to justify why such a type is known to exist and be unique for all T, and at that point it seems to me like defining it procedurally is both clearer and easier to reconcile with what the implementations do.

I really don't like having this duplicated here, and I still think it is duplicated for all practical purposes. I think what you are getting at is that the spec chooses to say that T0 is T0 bounded without the qualification that T0 is neither a type variable nor an intersection. I think all we need to do to make these definitions coincide is add that qualification - I see no reason that we want to say that a type variable X is X bounded. I'd suggest fixing the spec on this rather than duplicating this here. cc @eernstg what do you think?

I've created a sketch of what this might look like here: #4013

I couldn't parse out of here which forms are intended to cover which subsets of the semantic space. I think it would be helpful to be clear about that, even if it's not essential to your point. For example, does dynamic e; e.foo() correspond to a DYNAMIC_INVOKE of the call method? Or a FUNCTION_INVOKE?

Added some informative text to clarify. Let me know if this section makes more sense now.

What is the syntactic category of f? Is it only an identifier? Or prefixed identifier perhaps? Probably not an expression?

Hmm, this is a situation where my choice of notation really fails to capture what’s in my head.

My intention is for @STATIC_INVOKE to be the spec counterpart of the kernel’s StaticInvocation class (https://github.com/dart-lang/sdk/blob/f1febd2cf3bf754ae641eb3fda8ee885b8bda5e5/pkg/kernel/lib/ast.dart#L6531), with f corresponding to StaticInvocation.targetReference, which has type Reference. A kernel Reference is an indirection mechanism allowing different parts of the kernel representation of a program to refer to one another unambiguously. In practice it’s serialized as a sequence of strings separated by ::, the first of which is a URI (e.g. dart:core::int::tryParse), but that’s an unimportant implementation detail. What’s important is that StaticInvocation.targetReference is some way of referring to unambiguously to a top level function or static method defined in a library somewhere in the user’s program.

Putting on my spec writer’s hat, I guess if we want to be really formal about it, we could say that f is either a pair (URI, name) referring to a top level function named name in the library located at URI, or a triple (URI, name1, name2), where name1 is the name of a class, mixin, enum, or extension, and name2 is the name of a static method inside the thing named by name1. But I don’t really want to be this formal because it will make my examples really unwieldy (e.g. I want to say @STATIC_INVOKE(print(s)) rather than @STATIC_INVOKE(('dart:core', 'print')(s))).

Also, even (URI, name1, name2) isn’t good enough to uniquely identify a static method inside an unnamed extension, since a single library could have multiple unnamed extensions containing static methods with the same name. The kernel representation deals with this by giving every unnamed extension a synthetic name, but that feels like an implementation detail of the kernel that doesn’t belong in the spec.

What I really want to say is: “gentle reader, please think of f using whatever representation suits you for unambiguously referring to a static method or top level function that exists somewhere in the program being type inferred. Maybe that’s a combination of a URI and some strings, with some synthetic naming magic to disambiguate methods in unnamed extensions. Maybe it’s a unique integer identifier you assign to each static method or top level function in the user’s program. For my purposes in this document, I’m going to try to stick to examples where it’s clear from context what I’m referring to, like @STATIC_INVOKE(print(s)) (which clearly refers to the top level function print in dart:core or @STATIC_INVOKE(int.tryParse(s)) (which clearly refers to the static method tryParse in the class int in dart:core).”

I’m not really sure how to express that idea in the sort of formal style that we typically use for specifications. Any suggestions?

Why do you want to move to the semantic layer here? In the examples above, you just use the elaborated expression as the target. Why not something similar here? That is, you are starting with an expression (or maybe prefixed identifier?) f, why not just continue to use that in the meta-syntax?

Technically I think "evaluating the lookup of id in m_i" is interposed in here. This is required for at least the DYNAMIC_INVOKE, since you don't know whether you are invoking a method or calling a function typed getter. Whether it is required for any of the others depends a bit on the answer to my previous question about what semantic forms are intended to be covered here. That is, do you intend

class A {
  int Function(int) f = throw "yeehaw"; 
  void test() {
      this.f(3);
  }
}

to be covered by one of the above, or do you intend to add something else to cover this later?

Ok, I’ve tried to clarify this as much as I can without formally specifying the exact semantics of each form.

As to your example with this.f(3), I intend to eventually represent this as something like @FUNCTION_INVOKE(@INSTANCE_GET(m_0.id).call(3)). In this section, I’ve tried to hint at this in the non-normative text I’ve added under @FUNCTION_INVOKE.

The full details are in the “Method invocation inference” section, under the bullet “Otherwise, if U_0 has an accessible instance getter named id, then:”, but that text is a little wishy washy because I haven’t introduced the notion of @INSTANCE_GET yet as of this PR.

"known as" reads oddly, maybe just say "result type R"?

Done.

From reading the below, I think (but am not positive) that it would be very easy to just split out the case where F is not present into a single section, instead of interspersing it throughout. If this is relatively easy to do (and I think it should be, because it basically boils down to "do inference on the arguments in the empty context") I think it will help a fair bit in making this more readable, because I'm getting lost in the nested series of "if we are in this case do X" below.

Yeah, I can definitely see the appeal of that. If you don’t mind, I’d like to try to do it in a follow-up PR after landing this one, because it might involve moving a lot of text around and duplicating some things, so I want to make sure I’ve fully addressed all your other code review comments before I do that.

ack.

The P_i must be type schemas, not types.

Done.

I wonder whether it would also be helpful to just split out the case where type arguments are explicitly passed into a separate section as well? There will be some redundancy, but I don't think a lot, and it would make all of this much more readable. Basically, instead of re-branching on which case you're in many times throughout the description (which is super hard to read), you'd end up with something that has the structure:

if we're in the dynamic case, do {
downwards inference on arguments using _
} else if we're in the explicit type argument case, do {
compute the contexts for downward inference K_i
downwards inference on arguments using K_i
} else if we're in the type inference case do {
stuff (with some overlap from the above)
}

Good point. I’ll attempt this in a follow-up PR as well.

constaint -> constraint

Fixed.

Nit: I would avoid saying "match R_f as a subtype of K because it risks confusing two separate relations: subtyping and subtype matching. I would prefer to either use the symbolic notation I introduced above, or say something like "check whether R_f is a subtype match for K with respect to ...". The point is, the relation is "subtype match" not "subtype" (which is not defined for schemas, and is a binary relation rather than a trinary relation).

Done (here and elsewhere in the PR).

Maybe say "Let the new values of {U_1, ...} be {V_1...}? Saying "replace" is a little confusing here.

Done (here and elsewhere in the PR).

I think this should be P_i right? K_i is has been closed WRT the X_i by substituting in the partial solutions U_i above?

Yes, thank you. I double checked the implementation and you are absolutely right. Fixed.

Also I noticed that the “For each e_i in stage k” bullet enclosing this bullet doesn’t specify the order in which the e_i are considered. I’ve clarified that the order is the same as the order in which expression inference was performed.

As above WRT terminology "subtype" vs "subtype match"

Fixed, thanks.

constaint -> constraint

Fixed.

constaint -> constraint

Fixed.

At some point up above (in the case that the function type was missing) you set P_i to _, in which case this is not true. It's not clear to me whether you ever end up at this particular point in the algorithm if you are in the "missing function type" case, but this is an example of why I think it might be much clearer to just split out the three cases (dynamic, explicit type arguments, inferred type arguments) into three sections instead of trying to interleave them.

Hmm, you are right; this doesn’t make sense. And I agree that this is a good argument for splitting the algorithm into three cases.

This example is very hard to parse as written. Consider formatting it with arguments on different lines parallel to the declaration below?

Haha, this line was copied wholesale from https://github.com/dart-lang/language/blob/main/accepted/2.18/horizontal-inference/feature-specification.md, and no one complained about it there 🙂

But you have a good point. Reformatted.

Is there an implicit assumption here that all function calls e(...) have been rewritten to the form e.call(...)? If so maybe make that explicit?

Yes. It’s implicit in the text that follows (in the “Selector chain inference” section), but I’ve added a clarifying comment to this section to make it explicit.

Saying "a type schema K" is a little confusing because it has two natural interpretations: "some type schema K (I'm not saying what)" and "the type schema K that I mentioned above". I would either say "the type schema K" or "K as the type schema" to make it clear that K is not being bound here but rather is a reference to the K introduced above.

Same comment for each following bullet.

Good point. I went with “using ∅ as the target function type and K as the context”.

I believe argument part inference assumes as a pre-condition that the target function type will either be empty, or a function type. I don't think this step satisfies that precondition necessarily, since the return type of the getter could be dynamic, Never, Function and the code be well-typed, or it could be something else (like int) and the code is ill typed.

Good catch! Digging through the implementations, there’s definitely a problem here.

The core issue is that both the analyzer and CFE allow F to be any arbitrary type, provided that the interface of F contains a suitable member called call. The analyzer requires that this member be a function; the CFE allows it to be a getter (in which case the desugaring process happens recursively). The CFE can even be made to crash with a stack overflow if this recursive desugaring process doesn’t terminate (e.g. via class C { C get call => C(); }).

I need to spend some time reading and thinking about this issue in relation to #3482. That issue is mostly about how we handle this sort of thing in dynamic invocations, but the discussion touches on static analysis and desugaring as well.

I’ve added a note to myself to spend more time thinking about this. In the meantime, to avoid blocking this PR, I’ve added a TODO comment.

I may be missing something, but this seems wrong. If I follow the algorithm here, I think it implies that the following is an error:

int Function(int) f = (x) => x;
void test() {
 f(3);
}

because:

• Neither of the previous two cases apply to f(3)
• I think f(3) parses so as to match this case
• The selector chain here does not have access to this.

Am I missing something?

You’re right. As a band-aid, I’ve changed the text “cannot be resolved to the name of a local variable” to “cannot be resolved using local scope resolution rules” to resolve this problem, but this is not a good solution. In particular, it doesn’t handle the possibility that the identifier can be resolved using local scope resolution rules, and it resolves to an instance method or getter in the current class.

I’ve been working ahead a bit while this PR was under review, and I’ve got some ideas for how to address this, so I’m going to defer further work on this issue to a TODO comment.

String seems misleading here, maybe just say parameter name and leave it abstract?

Done.

I don't really understand the division between FUNCTION_INVOKE and STATIC_INVOKE. At a minimum, I think you need to say something here like "expressions which do not resolve to top level or static methods" because otherwise it is ambiguous what to do with f(3) where f is a top level method (because f is an expression whose type is a function type, and it is also a top level method). I'm also confused about something like x.call(). I guess maybe the screwy Dart grammar doesn't treat the x.call here as an expression and therefore we can say that it is unambiguously covered by INSTANCE_INVOKE instead of being ambiguous? Is that right? So (x.call)() is a FUNCTION_INVOKE, but x.call() is an INSTANCE_INVOKE?

Not just local variables though, right? Any expression, top level method etc could be in this form?

Yes, that's correct.

if -> is

Fixed, thanks!

(So the point of the bound resolution of T is to find a non-type-variable type which is a (minimal) supertype of T. If T is not a type variable, it's T.
If T is a type variable or a type variable intersection, then the least non-type-variable (upper) bound is the variables bound or the intersection type, respectively. Makes sense.)

I like this way of thinking about it, thanks! I’ve added some text to the PR to clarify this.

(Not sure using bold for types is a good idea, when we also use bold for semantic functions like UP. Consider "is dynamic bounded if and only if its bound resolution is the type dynamic" and similar for function.

Yeah, I see what you mean. I’m usually in the habit of using a monospaced font for type names, but in this case, since I’m referring directly to text in the spec, I figured I would imitate the style of the spec. If you look at page 144 of https://spec.dart.dev/DartLangSpecDraft.pdf, it uses boldface for dynamic and Function.