dart-lang / language

Design of the Dart language
Other
2.65k stars 202 forks source link

Proposal: context-gated field promotion with runtime checking #1188

Open stereotype441 opened 4 years ago

stereotype441 commented 4 years ago

This is an attempt to flesh out @mraleph's proposal from https://github.com/dart-lang/language/issues/1187#issuecomment-682352586 into something a little more concrete that we can use as the starting point for discussion. Note that I'm calling it "field promotion" because this is the terminology we've been using to discuss it, but I think that for consistency it should apply to instance getters as well.

Motivation

For some time users have been asking for type promotion to apply to fields, e.g. users want to be able to say:

class C {
  Object o;
  f() {
    if (o is int) {
      print(o + 1); // I know `o` is an int; I just checked it.
    }
  }
}

With null safety, the desire for this feature is even stronger, because it would permit patterns like if (x != null) x.doSomething(); where x is a field.

The reason we haven't allowed this is because it has soundness loopholes:

However, many users don't find this reasoning very compelling because in practice the loopholes don't tend to arise for one reason or another. For the case of writes:

And for the case of overrides:

So we want to explore the possibility of allowing fields to promote, and see what consequences this has on other aspects of the language.

Proposal

Extend the existing flow analysis algorithm so that in addition to tracking promoted types of local variables, it tracks the promoted types of getters defined on this, where the "declared type" of a getter is considered to be its return type.

Within a method declaration inside a class, mixin, or extension declaration, if there is an expression E of the form this.g (or g, where scoping rules cause g to be equivalent to this.g), then its static type is computed as follows:

If the rules above assign E a static type of T0, then execution of E happens in the usual way. Otherwise, let T1 be the static type of E. Then, execution of E proceeds as follows:

This ensures that the runtime semantics will respect the static type assigned to E, preserving soundness.

Examples

class C {
  Object? o;
  int? i
  test() {
    if (o is int) {
      print(o + 1); // Ok; throws if `o` is not an int
      print(o.isEven); // Ok; throws if `o` is not an int
      print(o.hashCode); // Ok; does not throw 
      print(o.foo()); // Compile-time error: no method `foo` on Object
    }
    if (o is int?) {
      print(o!.isEven); // Ok; throws if `o` is not an int
      print(o?.isEven); // Ok; throws if `o` is neither `null` or an int
    }
    if (o is num) {
      if (o is int) {
        print(o.isEven); // Ok; throws if `o` is not an int
        var y = o + 1; // Ok; throws if `o` is not a num
        y = 1.0; // Ok; `y` has static type `num`
      }
    }
    if (i != null) {
      print(i + 1); // Ok, throws if `i` is null
      print(i?.isEven); // Ok; does not throw
    }
  }
}

Consequences

This feature introduces some runtime overhead, since it modifies the execution semantics of some field references to include a type check. Partial mitigating factors:

This feature introduces implicit runtime checks, which means it can cause exceptions to be produced by code that otherwise appears exception-proof. The historical evolution of the Dart language (including, particularly, the null safety feature) has been to try to reduce the amount of implicit type checking so that users have an easier time identifying possible exceptions by code inspection (and thus hopefully reducing the number of exceptions that happen in production). This feature seems to work against that trend. Counterpoints:

This feature introduces the potential for user confusion, since it means that the type of an expression is now more context dependent than it used to be. Counterpoint: we already have several instances where the type of an expression is context dependent (inference of generic function calls, type inference of collection literals, and inference of numbers as int or double), and these context dependencies seem on the whole to be useful more often than they are confusing.

stereotype441 commented 4 years ago

Hmm, on further reflection, there should also be cases for E being the target of a setter dispatch (e.g. E.setter = ..., E?.setter = ..., E!.setter = ...). These will probably be a little delicate to specify due to compound assignments and increment/decrement operators (e.g. if T0 specifies a setter called x but no getter, then maybe E.x += ... promotes but E.x = ... does not).

lrhn commented 4 years ago

Is using the most general type (first match in p) the right choice?

Example:

class A {}
class B extends A { B get foo => this; }
class C extends B { C get foo => this; C get bar => this;}

class Z {
  A x = C();
  void func() {  
    if (x is B) {
      if (x is C) {
        x.foo.bar;
      }
    }
  }
}

If I read the algorithm correctly, the p of x is [B, C]. When we do x.foo, we pick B as the type we read foo at, because it's the first one which has a foo. That makes x.foo a B which does not have a bar. If we had used C, the code would compile.

In local variable promotion, we use the most promoted/least general type for the variable when doing member lookups.

I assume that choosing the most general type is intended to cause fewer, or less strict, type checks at run-time, but I'm not sure it's worth it. Could we pick the most specific type, and then let it be a compiler optimization to figure out whether type checks are really needed? That is, if the code can run, even if we only check for B, not C, then the compiler is allowed to only check the value for being B.

lrhn commented 4 years ago

I've suggested something like this before. There are basically two ways to approach it:

The latter means that promotion is only considered sound when the value doesn't change, which will very likely account for the vast majority of cases where users test the type of something, and then want to use the same getter later at the same type. It's probably fairly efficiently implementable: Any promotion stores the current value that was checked as a sentinel, and any promoted use starts by doing an identity check against the stored sentinel value.

This removes the reason to use a more general type than the best known one. If promotion is allowed at all, we can use the best known type. We can still demote/promote on visible assignments, just keep the stored value as the new sentinel. We already have a ConcurrentModificationError that we can throw if the value changes unexpectedly between check and use.

I think users would be able to grok the rule: Instance getter promotion only works when the value doesn't change. The value you check is the value you use, or else!

It will probably cause a few errors where a getter synthesizes similar value on each access, but not the same one (I believe StreamController.stream does that, so a class with a Stream? get stream => _controller?.stream which checks if (stream != null) stream.forEach(...) would throw).

lrhn commented 4 years ago

Could we allow cascades if every cascade selector would be allowed individually? It would be at the most specific type needed for any cascade selector (if we don't always use the most specific type).

stereotype441 commented 4 years ago

Further notes based on a discussion with @leafpetersen:

  1. In this proposal, when deciding whether to insert an implicit check based on a call to a method that's defined in an extension, we don't pay any attention to the type of the extended method, only to whether it's present or not. So for example, in the following code, at (1), there are two promoted types for o in the flow model: List<num> and List<int>. Both of those types permit a method call of .foo(), so we promote to the more general type (List<num>) and consequently the type of o.foo() is num, so o.foo().isEven is a compile-time error.
    extension E1 on List<num> {
    num foo() => ...;
    }
    extension E2 on List<int> {
    int foo() => ...;
    }
    class C {
    Object o;
    f() {
    if (o is List<num>) {
      if (o is List<int>) {
        print(o.foo().isEven); // (1)
      }
    }
    }
    }
  2. Although this proposal is inspired by the notion of "promote when necessary to avoid errors", we are being really deliberate here to restrict the extent of the analysis to just the immediate context of the field access, to avoid "spooky action at a distance". So for example in the following code, there would be no promotion at (1), so there would be a compile-time error at (2):
    class C {
    Object o;
    f() {
    if (o is int) {
      var x = o; // (1)
      ...
      print(x + 1); // (2)
    }
    }
    }
  3. We expect that in practice, this feature would frequently create downcasts from a type to its non-nullable counterpart (e.g. casting int? to int). For good performance, back-ends should definitely optimize such a cast to a null check (rather than trying to implement it using more general case casting machinery). One possible way to achieve this would be to have the front end automatically convert such casts into null checks. (This optimization could be applied to explicit casts as well).
stereotype441 commented 4 years ago

Is using the most general type (first match in p) the right choice?

Example:

class A {}
class B extends A { B get foo => this; }
class C extends B { C get foo => this; C get bar => this;}

class Z {
  A x = C();
  void func() {  
    if (x is B) {
      if (x is C) {
        x.foo.bar;
      }
    }
  }
}

If I read the algorithm correctly, the p of x is [B, C]. When we do x.foo, we pick B as the type we read foo at, because it's the first one which has a foo. That makes x.foo a B which does not have a bar. If we had used C, the code would compile.

In local variable promotion, we use the most promoted/least general type for the variable when doing member lookups.

I assume that choosing the most general type is intended to cause fewer, or less strict, type checks at run-time, but I'm not sure it's worth it.

Yeah, it's not 100% clear to me what's going to be better from a user experience perspective. If we promote to the most general of the promotion candidates that works, there are going to be (admittedly rare) cases where that's not as much promotion as the user intended, and they're going to get a compile-time error. They'll have an easy workaround (use an explicit cast), but it'll be frustrating and confusing that it's necessary (similar to how it's frustrating and confusing today that fields don't promote at all). On the other hand, if we promote to the most specific of the promotion candidates, there are going to be (again rare) cases where that's more promotion than the user intended, and thye're going to get a runtime error. Again an explicit cast would work as a workaround.

I think I lean slightly toward promoting to the most general of the promotion candidates that works, on the theory that compile-time errors are better than runtime errors. But since the whole point of this feature is to change a compile-time error check into a runtime error check for the user's convenience, maybe that argument is invalid.

Could we pick the most specific type, and then let it be a compiler optimization to figure out whether type checks are really needed? That is, if the code can run, even if we only check for B, not C, then the compiler is allowed to only check the value for being B.

I'm all for back-ends doing optimizations, but I don't think that checking for B instead of C counts as an optimization because it changes semantics. Consider:

class C {
  Object o;
  void f(Object x) {
    o = x;
  }
  void g() {
    if (o is num) {
      if (o is int) {
        f(1.0);
        print(o + 1); // (1)
      }
    }
  }
}

If we say that this compiles (1) into print((o as int) + 1);, then this code will cause an exception to be thrown (because f(1.0); caused a double to be stored in o). Changing this to print((o as num) + 1); isn't an optimization, it's a change in the meaning of the program.

eernstg commented 4 years ago

@stereotype441 wrote:

it's frustrating and confusing today that fields don't promote at all

I think the proposal looks fine, and I'm sure the choice of which type to promote to can be resolved after the decision to do it at all.

But saying that developers find it confusing that fields don't promote at all probably skips over too much. I don't think such a developer will actually think "I want instance variable x to be promoted here, and I don't care that it is unsound. I also don't care that it could be expensive in terms of time spent on performing dynamic type checks in a tight loop." So I tend to think that we should make the unsafe nature of this mechanism explicit.

But (as I mentioned here) we already have a very similar mechanism in variables that are late. In this case it's just about the assumed type, rather than being about initialization.

We could leverage the knowledge about late variables and the correspondence between late initialization checks and late assumed-type checks by adding in the word late:

class C {
  Object? o;
  int? i
  test() {
    if (o is late int) { ... }
    if (o is late int?) { ... }
    ...
    if (i is! late Null) { ... }
  }
}

This is a reminder to any reader of the code that some implicit use-site checks on o may be needed, and that will probably help developers write code that has the amount of dynamic checking that they actually want.

rrousselGit commented 4 years ago

"I want instance variable x to be promoted here, and I don't care that it is unsound. I also don't care that it could be expensive in terms of time spent on performing dynamic type checks in a tight loop."

I would expect that most people would not care about soundness and performance here – partly because soundless is too abstract for many, and people tend to prefer syntax sugar over a few microseconds.

To begin with, a significant portion of the community is using Dart only because of Flutter, where they don't necessarily agree with the language but just use it because they have to. For example, a portion of the code found on StackOverflow doesn't even type variables and I've seen quite a few cases where people use Map<String, dynamic> instead of classes.

That's not my opinion and I do want a sound & fast language. But if this quote is what is used to make a decision, it may be important to double-check – maybe with the Flutter survey.

munificent commented 4 years ago

The historical evolution of the Dart language (including, particularly, the null safety feature) has been to try to reduce the amount of implicit type checking so that users have an easier time identifying possible exceptions by code inspection (and thus hopefully reducing the number of exceptions that happen in production). This feature seems to work against that trend. Counterpoints:

  • This trend has been largely driven by customer feedback, and customer feedback currently indicates that lack of promotion of fields is a problem.

In some ways, this parallels covariance. Users intuitively expect covariant generics (especially arrays) to "work" and are surprised if the language prohibits it. So Dart "makes it work", but that has quite long tail of negative consequences including that an intuitively correct program can throw an exception and crash at runtime.

My experience is that when once you explain to users why covariance is unsound and their intuition is wrong, they no longer want that behavior. Of course, we need to meet users where they are and there shouldn't be a mandatory education process to use the language well. But I do think it's reasonable for us to try to meet in the middle—give them a language that follows their intuition where reasonable but that also gives them the properties they explicitly request (no unexpected runtime failures) even if the latter can be unintuitive in some cases.

munificent commented 4 years ago

The latter means that promotion is only considered sound when the value doesn't change, which will very likely account for the vast majority of cases where users test the type of something, and then want to use the same getter later at the same type. It's probably fairly efficiently implementable: Any promotion stores the current value that was checked as a sentinel, and any promoted use starts by doing an identity check against the stored sentinel value.

The set of cases where this works (i.e. doesn't throw) is exactly the set of cases where a shadowing local variable would also work. You could imagine an "unchecked" form of your proposal that implicitly declares a local variable with the same name as the promoted getter, copies the getter's value to that, and then applies promotion as normal to the local.

This has the advantage of never throwing and requiring no checks. It has the disadvantage of potentially giving you a stale value in cases where your proposal would throw. Personally, I think either of those failure modes are too surprising to silently opt users into that behavior. That leads me to want some explicit opt in syntax, which is basically what pattern matching and declaring variables inside if would give you (at perhaps a little too much verbosity in common cases).

stereotype441 commented 4 years ago

A question about this came up in the language team meeting this morning: if we were to decide to do this, but didn't do it until after the null safety release, how breaking would it be?

I believe that it would be technically breaking, but low impact (and we have options to make it lower impact), because the vast majority of the cases in which this proposal changes the behavior of Dart are cases where we currently have a compile-time error. The exceptions I can think of are:

  1. If the field/getter has type dynamic, we may promote it, even though a dynamic usage would not have been an error. This could cause a change to a type inferred at runtime, e.g.:

    class C {
    method(void Function(int) callback) { ... }
    }
    class D {
    dynamic field;
    f() {
    if (field is C) {
      // Callback passed to `method` previously accepted any input, now only accepts ints.
      field.method((x) {});
    }
    }
    }

    Note: this is open to interpretation. In my proposal, I said that we decide whether to promote on method dispatch based on whether the given getter or method "exists" on the declared type. Do we say that all getters/methods "exist" on the dynamic type, or just those defined for Object? This is only a problem if our interpretation is the latter. And we could make the change less breaking by choosing the former interpretation.

  2. If the field/getter has type dynamic, we may promote it, even though a dynamic usage would not have been an error. This could cause a runtime cast failure when previously a dynamic dispatch would have succeeded, e.g.:

    class C {
    void method() { ... }
    }
    class D { // Unrelated class
    void method() { ... }
    }
    class E {
    dynamic field;
    f() {
    field = D();
    }
    g() {
    if (field is C) {
      f();
      // Previously, this call would succeed, since `D` also has a compatible method.  Now it fails at runtime.
      field.method();
    }
    }
    }

    Again, I'm having trouble imagining a non-contrived scenario where this would matter, but if one arises we could make the change less breaking via a similar remedy (in this case, by choosing not to promote fields/getters of type dynamic).

  3. If the field/getter is used in a scenario where the context type is narrower than the set of types that would be accepted at runtime, this could cause a change to type inference, leading to a static type error in a program that would have previously worked. E.g.:

    class C {
    method(void Function(int) callback) { ... }
    }
    class D {
    List<dynamic> field;
    f() {
    field = <dynamic>[];
    }
    g(bool b, dynamic d) {
    if (field is List<int>) {
      f();
      // Previously this would have worked; now it's a static error because a String can't be passed to List<int>.
      List<int> x = b ? d : field..add('foo');
    }
    }
    }

    Again, I'm having trouble imagining a non-contrived scenario for this. Unfortunately, I don't see an easy fix for this case.

Notably, this proposal is not breaking because of cascades. Assuming that we extend the rules above in the natural way for cascades (i.e. x..f()..g() is changed to (x as T)..f()..g() only if the declared type of x fails to support both f() and g()), then any cascade in which we promote the target is one that would have previously led to a static error.

eernstg commented 4 years ago

Of course, if the mechanism is marked syntactically then there is no breakage because no existing code gets a new meaning. Each developer can start using the mechanism one location at a time, and debugging it as needed.

If the late promotion is not marked, a snippet of code may now have a new meaning (even though nobody edited it, or even looked at it recently). We may then have a crash because the promotion was indeed not sound, but the pre-change code didn't rely on preserving the tested type anyway. Or we may have a crash half an hour later because the unedited code with a new meaning now creates an object with slightly different type arguments.

I like the mechanism, but I would like it to be marked explicitly. The fact that we don't need to worry about breakage is just an extra benefit.

esDotDev commented 3 years ago

Just a slow developer here, but it seems like the vast majority of real world use cases could be solved with simple base keyword, with the intent being that we want to hint to compiler that this field has not been overridden. 99.9% of the time we are in the base class, the other .1% we did not override the field anyways, let us just tell that to the compiler?

return (base widget.label != null) Text(label) : Container();

In the extremely rare use case that someone is using a sub-class, that has overridden a field with an accessor, then those tiny fraction of people can just make sure to do a local copy trick in their base class? Perhaps a linter warning would be nice here if using base on a field that has an accessor as an override down the chain, since this is conflicting intent. This would push those people towards using local copy instead (or a closure to do it for you, which is easy enough in one-off situations)

From an end user standpoint, I think this gets use where we need to be in an intuitive way for developers.

lrhn commented 3 years ago

If we are in the base class, the class where the variable was declared as a variable, then something like self.label would work. It won't be a hint, like super.label it statically determines which declaration to use instead of using virtual/late binding to find the most recent override. It's really like super. but just starting from the current class, not the superclass.

If the variable is final and declared in the same class (not a superclass), then we can probably allow inference to distinguish self.label from a getter and allow promotion (changing the variable to a getter will then only break code locally in the same class, which you will immediately discover).

That's still a very tiny corner, and won't work for a lot of other use-cases. I'd prefer to have at least one feature which you can always use to predictably promote a value from anywhere, without needing to know how it's declared. That probably means without needing to read the value twice.

esDotDev commented 3 years ago

It might be a tiny corner from a language perspective, but in Flutter world, this is more or less the issue. Everything except this is fitting nicely with nnbd as I go through my code, but this issue is quite ugly, and creates potential bugs if you're not well versed on the topic.

The self sounds nice but the issue I see would be with flutter, where we are forced into using a wrapper class, so our needs are more like:

class Foo extends StatefulWidget {
  const Foo({Key? key, this.label}) : super(key: key);
  final String? label;

  @override
  _FooState createState() => _FooState();
}

class _FooState extends State<Foo> {
  @override
  Widget build(BuildContext context) {
    return widget.label != null? Text(widget.label) : Container();
  }
}

Not sure how 'self' work there, since we're not actually inside the scope of the class we're calling (even though we just wrote it, and are calling it from a directly coupled 'state' class). base would be able to be used externally, or internally, so I can always just hint to the compiler it can safely promote this classes fields when analyzing.

esDotDev commented 3 years ago

I think if you go back to first principles, the fact we can not simply write this, is a fairly big flaw in the current language design:

class A {
  int? index;
  void increment() {
    if (index == null) index = 0;
    index++;
  }
}

The mental model that should be optimized for is 'a field is a field' imo. Even if dart doesn't work that way under the hood, thats a base construct developers rely on when scaffolding their own logic.

Almost any developer reading this code will be confused why the compiler is complaining, and need a multi-hour explanation of virtual fields and interceptor methods.

esDotDev commented 3 years ago

Another example showing how this forced usage of ! cuts right across a core goal of NNBD:

_client = Client();
_auth = FirebaseAuth(_client!, "KEY");

If nnbd is helping me, it's going to tell me to check client if I have not a) checked it myself, or b) provided a value myself.

Here I am providing a value, but the compiler appears clueless, and needs me to ! that it is not null. At this point I kill any advantage of nnbd with this variable.

Someone can remove the assignment, or a null check and compiler is useless. What's worse, is a developer might miss a tiny ! somewhere, and assume this is null safe since the compiler is not saying anything and we're running in 2.12, not looking as closely for manual null checks as they would've before.

The new "best practice" becomes this, any time you are working with anything that needs to be stored in the class.

final c= Client();
_auth = FirebaseAuth(c, "KEY");
this.client = c;

Which, while not horrible to use, is really unintuitive to scripters, if they have a class field they just want to store the thing there, not create a pointless 'holding var'. It's also less readable, if I'm skimming your code, and you're working on _client, I'd rather see that repeated over and over, not working on c and then sneakily in one line, assign that back to the class field. That's easy to miss, and harder to grok.

If you look at the full function, you can see these !'s hiding everywhere, and I should actually refactor this cause it's quite brittle right now, especially if your mental model is now relying on compiler to pick out missing null checks.

void signIn() async {
    setState(() => _errorMsg = "");
    _client = Client(); // If this is removed, null-pointer-error, no compiler warning
    _auth = FirebaseAuth(_client!, "KEY");
    try {
      FirebaseAccount account = await _auth!.signInWithPassword("email@test.com", "password");

      _db = FirebaseDatabase( // If this is removed, null-pointer-error, no compiler warning
        account: account,
        database: 'database-id',
        basePath: 'demo-app/',
      );
      _rootStore = _db!.createRootStore<AppUser>// If this is removed, null-pointer-error, no compiler warning
          onDataFromJson: (dynamic json) => AppUser.fromJson(json as Map<String, dynamic>),
          onDataToJson: (AppUser data) => data.toJson(),
          onPatchData: (AppUser data, updatedFields) {
            print(updatedFields);
            return data;
          });
      _acct = account;
      _rootStoreStream = (await _rootStore!.streamAll()).listen((e) => print('Stream update: $e')); 
      print('All data: ${await _rootStore!.all()}');
    } on Exception catch (e) {
      if (e is AuthException) {
        if (e.error.message == "EMAIL_NOT_FOUND") _errorMsg = "Email not found.";
        if (e.error.message == "INVALID_PASSWORD") _errorMsg = "Password is incorrect.";
        print(e.error.message);
      }
    }
    setState(() {});
  }

You can see I do use account temp var here, but really I need to create some for _db, _client, _rootStore. From a dev standpoint this feels really ackward, because from our perspective it's all right there, and this compiler appears quite dim-witted.

esDotDev commented 3 years ago

Seems like simply using the ! operator on the assignment/check side would work, it just has readability issues because of !=

 // For the duration of this method, "cast-away" the nullability
_client! = Client();
_auth = FirebaseAuth(_client, "");   // ! is not required, compiler is now treating this as non null

// Same idea, this isn't a great read for a developer, but semantically it makes sense
if(_client! == null){  return; }
_auth = FirebaseAuth(_client, "");

This would also serve as a marker to anyone subclassing this that they better be careful if they decide to override _client! with a method.

I guess the issue here is that we can not assign null back to _client if we want to, so it can't be as simple as just 'treat it as non-null` :(

eernstg commented 3 years ago

Nono, the pragma was added by one of the good people. :grin:

esDotDev commented 3 years ago

I do think that if this is not going to be addressed in a timely fashion, dart-lang team should be shouting from the rooftops: "Always make local copies of class fields, do your checks on those, and assign the results back to the class". This is the only safe way to work with this limitation.

?. does not serve all use cases, and ! is not really useable at scale if you actually intend to be "sound" in any true sense.

eernstg commented 3 years ago

! is not really useable at scale if you actually intend to be "sound" in any true sense.

The proposal in this issue will induce ! implicitly, so it's going to throw if the target getter actually returns null, e.g., because the associated field was modified, or because the getter has been overridden in the run-time type of this.

However, it's a very useful idiom to copy a field to a local variable and work on it, and (if needed) to copy it back. It is error prone because we may forget to write it back, but in addition to the support for promotion it may allow for the reference to be stored in a register, or to avoid re-loads if it's stored in an activation record on the stack and hasn't been updated since the previous load, etc.etc. So it may feel somewhat inconvenient and verbose and error prone, but there are many reasons why it's a rather useful habit. A compiler can't do it, because it can't (in general) know whether the field could be updated during the execution of a function body, or whether the associated getter is overridden.

One possible approach is this one: https://github.com/dart-lang/language/issues/1514.

esDotDev commented 3 years ago

I think when looking at small demo methods this is a reasonable thing, but as you can see from my example, when the rubber hits the road in production, this gets silly pretty fast. I would need to add a full 8 lines to a 28 line method, simply for house-keeping / variable shuffling.

Your typical flutter dev is not working on pure methods that do some calculation, they're strapped to state classes + widget configs, that have many fields that they may want to access at anytime. This just ends up feeling like busywork with no perceivable benefit.

eernstg commented 3 years ago

We have lots of trade-offs, as usual: The proposal in this issue is smooth in the sense that we get rid of the ! and we maintain dynamic soundness (so we won't dereference a null pointer, but we only discover that we're dealing with a null pointer at run time, and then we throw).

The proposal in #1514 allows us to maintain soundness statically (so we actually won't encounter an unexpected null pointer), and it improves performance (no need to invoke a getter several times); but it relies on caching being a non-bug, so I prefer to make it a visually explicit opt-in mechanism.

A third option which has been discussed many times is to break the abstraction: Allow the compiler to know for sure at the call site that the getter/setter hasn't been overridden and no other code has mutated the variable—which means that it's safe to assume that the instance variable is just a memory cell that we own, just like a local variable. We could use sealed classes, non-virtual instance member declarations, and a bunch of other devices to achieve this. That might very well be a useful direction to explore as well.