Infer generic from callbacks

[terryl1900]

Hello! I noticed that this works fine:

class Emitter<T> {
  Emitter(this.create);
  final void Function(void Function(T) emit) create;
}

void main() {
  Emitter<int>((emit) => emit(1));
}

While this throws The argument type 'int' can't be assigned to the parameter type 'Never'.

void main() {
  Emitter((emit) => emit(1));  // Omit type int
}

I'm curious what stops Dart infer the type here? I couldn't find an existing issue about this.

[Levi-Lesches]

Perhaps this is related to #731, because it can't infer T even though it is in the given argument.

[leafpetersen]

This is just the way the style of inference that Dart uses (so called "local type inference", which is also used by C#, Scala, and other similar languages) works. Basically information flows down from the enclosing context, and then back up, but there is no iterative process. Here, we must choose a type for the parameter emit in order to do inference on the body. If there were more information from the enclosing context, we would use that, but there isn't - all we know is that the parameter must be a void Function(?) for some value of ?. So here, we choose Never for ? and continue. Once we've made that choice, we can't revisit it (without having to do some kind of fixed point iteration, which we don't do). So we're stuck with it, and the result is what you see above.

#731 does not solve this, since there are no additional parameters to flow information from.

[Levi-Lesches]

all we know is that the parameter must be a void Function(?) for some value of ?. So here, we choose Never for ? and continue.

How does Dart determine that ? is a Never? Never would mean it can be statically shown that no argument would be valid, but it sees emit being called with 1 right there. That means that at least 1 works, maybe even 1.0 or null as well. Shouldn't it then choose Object? or at least dynamic instead? That way this error wouldn't be there in the first place.

[terryl1900]

Thanks for the explanation.

[munificent]

How does Dart determine that ? is a Never?

I believe it's because T appears in a contravariant position (as a function parameter).

Never would mean it can be statically shown that no argument would be valid, but it sees emit being called with 1 right there.

Using Never for the function's parameter type means that any function type accepting any parameter type is a valid callback to be passed to Emitter().

[leafpetersen]

How does Dart determine that ? is a Never?

https://github.com/dart-lang/language/blob/master/resources/type-system/inference.md#type-variable-elimination-least-and-greatest-closure-of-a-type

Never would mean it can be statically shown that no argument would be valid, but it sees emit being called with 1 right there. That means that at least 1 works, maybe even 1.0 or null as well. Shouldn't it then choose Object? or at least dynamic instead? That way this error wouldn't be there in the first place.

The reason for the use of the greatest closure is as follows:

• Inference is attempting to find a solution for T which makes the program well typed
• At the point that it attempts to infer the closure, it must choose a type for the parameter, with no constraints on T
• The parameter must take the form void Function(?) for some choice of replacement for ?
• The algorithm we use chooses to take the greatest closure of void Function(?) as the type, which results in void Function(Never)

It is true that in this case there is a different choice which make the code work, but in general that is not true: choosing to use (e.g.) the least closure will cause other examples to fail to infer. In general, the principle that we are using is to make a choice for the type of emit which maximizes the chances that the argument (here (emit) => emit(1)) is assignable to it's parameter type. By choosing void Function(Never) as the type for emit, we make (emit) => (emit(1) maximally assignable, and hence most likely to be an acceptable choice.

Again, this is a heuristic choice, and in this case it results in a failed inference where a different choice would have worked. But any other heuristic choice has the same property.

There are other approaches one can try to take (e.g. unification based approaches), but in a type system like Dart's, they are almost guaranteed to be undecidable (look for results around the undecidability of type inference for system F for relevant background), and if a decidable fragment is found, likely to be much more expensive to compute which is an issue for a language which is still intended to be runnable from source.

I've always been somewhat interested in exploring the ideas from this paper, but realistically, I don't think it's likely to be feasible for us to do anything along these lines given the various constraints we're working under.