`@pragma` for dart analyzer to hint null type promotion.

[ManuelRauber]

Hi,

the following code will work perfectly fine with current Dart 3.1.3:

String? foo = null; 

if (foo != null) {
  String x = foo; // works, no ! needed
}

Now, I often want to check if the String has content, which leads to:

String? foo = null; 

if (foo != null && foo.isNotEmpty) {
  String x = foo; // works, no ! needed
}

Since I use that quite often in my app, I thought it might be nice to have an extension method for that:

extension NullableStringExtension on String? {
  bool get hasContent => this != null && this!.isNotEmpty;
}

The usage should be:

String? foo = null;

if (foo.hasContent) {
  String x = foo; // Urgh, does not work, because Dart thinks, that foo could be null.
}

However, this does not work, because the analyzer still thinks, that the foo could be null. Since hasContent already checks for that and only returns true, when foo is not null, it would be nice, if either the analyzer can actually analyze it, or it would be nice, if there was some pragma, like:

extension NullableStringExtension on String? {
  @pragma('not-null-when-true')
  bool get hasContent => this != null && this!.isNotEmpty;
}

This is similar to a C# feature: NotNullWhen.

It would be great so have something similar in Dart as well.

[eernstg]

Interesting! That kind of feature would surely be useful.

However, Dart null safety is strict and sound, so we couldn't introduce support for declaring that a given invocation has any particular implications like "the receiver is non-null", and then allowing the compiler to rely on the veracity of that assumption "just because a human being claims that it is true".

So if we were to introduce a mechanism like @pragma('not-null-when-true') then it would presumably have to be a request for performing an analysis which is already possible, but it just doesn't occur here because it involves an interprocedural element (that is, during the analysis of one function body we need to look at the body of some other function in order to obtain the desired result; currently, Dart flow analysis stops at function boundaries).

An easy way to get there, apparently, would be to inline the "other" function and then perform the flow analysis based on the inlined version of hasContents.

This won't help us in the case where the "other" function is too complex to inline, or too complex to analyze, but it could be helpful in some cases where we just want a concise and consistent way to write a specific expression.

It could entail a lot of work, and/or it might break some important invariants in the implementation of the static analysis, so we shouldn't assume that it is (realistically) possible, or that it will happen anytime soon.

However, @stereotype441 and @johnniwinther, WDYT? Would it be doable to perform inlining early and unconditionally for functions marked with some metadata (say @pragma('not-null-when-true')), and then proceed to perform flow analysis on the result? It could be a compile-time error to have that metadata on a function that can't be inlined into every call site. Or it could be a compile-time error to have that metadata on a function that can't be inlined into any call sites, and the inlined flow analysis could then be available only at call sites where the inlining is possible. Crazy or possible? ;-)

[lrhn]

Since this is immutable (right? RIGHT?!), any check that this is not null can be taken as evidence for promotion.

However, I don't expect us to do that at the member level, because then the behavior of code using hasContent depends on the implementation of hasContent. Implementation which could change tomorrow, possibly to something that the type inference cannot recognize as guaranteeing that this is not null. And then the client code breaks, because it depended on internal implementation details.

So, a getter which should be usable for promotion would need to be declared as such, which is not a feature we have. (And an annotation won't do, we won't be defining language semantics in terms of annotations.)

So this needs a bigger language change to be viable and sound.

[eernstg]

So, a getter which should be usable for promotion would need to be declared as such,

Of course.

.. which is not a feature we have.

This is a discussion about possibly adding a feature, so that wouldn't be particularly surprising. ;-)

I think it could make sense to say that the feature is "this function is guaranteed to be inlined, and flow analysis will take place based on the inlined code". Promotion would be affected by this behavior, and other things might as well.

Obviously, this can only be used with functions which are resolved statically (such as extension members, extension type members, top-level functions, static methods, local functions), and the fact that the declaration explicitly marks the given function as always-inlined ensures that it is possible for developers to know that they are committing to a very detailed dependency: It's basically a breaking change to change this kind of function declaration in any way whatsoever. But that's part of the contract, if you don't like that kind of constraints then don't write that kind of function.

Thinking about it a bit more, it looks very much like this kind of function would be a better match for a macro mechanism. So we'd need to mark some statically resolved functions as "expression macros", and it would then be a very natural property of those functions that they are inlined at compile time, rather than being called an run time.

(And an annotation won't do, we won't be defining language semantics in terms of annotations.)

We can of course use any syntax we want, as long as it's well defined.

[eernstg]

I moved this issue to the language repository because it's a proposal for a semantics that isn't expressible in current Dart.

[mateusfccp]

Isn't it similar to #2253? But #2253 seems to be more general.

[eernstg]

@mateusfccp, thanks for the link, I hadn't thought about #2253!

I think it's difficult to say which proposal is more general. #2253 is definitely rather broad in the claimed scope, but it will only be able to do a lot of general things if we invent a new mini-language for specifying the contributions to the local flow analysis which will be provided by an invocation of one of those promotion abstractions, and I'd think that's a rather tall order. As @lrhn wrote:

But then, we'd have introduced an awful lot of complication into the type system, basically a generalized contract format, which the compiler would have to be able to understand and propagate correctly.

The idea that a boolean type would be associated with evidence is obviously powerful, but it seems to be approximately the same thing as embedding Coq into Dart. So maybe we won't do that. ;-)

On the other hand, an expression macro would be quite straightforward, we just need to think about the inlined code and follow normal rules for promotion:

// --- Library.

extension<X1> on X1 {
  macro bool are<Y1 extends X1>() => this is Y1;
}

extension<X1, X2> on (X1, X2) {
  macro bool are<Y1 extends X1, Y2 extends X2>() => $1 is Y1 && $2 is Y2;
}

extension<X1, X2, X3> on (X1, X2, X3) {
  macro bool are<Y1 extends X1, Y2 extends X2, Y3 extends X3>() => $1 is Y1 && $2 is Y2 && $3 is Y3;
}

// ... and so on as needed.

// --- Example usage.
import 'are.dart';

void main() {
  num x = 1;
  Object y = 'Hello!';

  // Example use case:
  if ((x, y).are<int, String>()) print('${x.isEven}, ${y.substring(1)}');

  // .. which is compiled into the following:
  // if (x is int && y is String) print('${x.isEven}, ${y.substring(1)}');
}

So are can be used to perform a type test (guaranteed to be a type test for a subtype of the statically known type) on a group of expressions, and the ones that are promotable variables will be promoted. If some of them aren't promotable we just get the type test, and it's not a problem (this could be because they are non-local variables or in some other way not promotable, or they could just be expressions that aren't variables at all).

Just that tiny little fact that we're restricting the type test to be for a subtype of the statically known type can be beneficial, even if we're just testing a single variable: Otherwise we might do if (x is Set<num>) in a situation where x has static type Iterable<int>, and then be puzzled that there was no promotion (because we aren't testing for a subtype).

In other words, this kind of abstraction could be useful, in spite of the fact that this abstraction will always be unfolded completely at the "call site".