Skip to content

[extension-types] Cyclic dependencies in bounds should imply potentially nullable #3263

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
eernstg opened this issue Aug 11, 2023 · 6 comments
Labels
extension-types question Further information is requested

Comments

@eernstg
Copy link
Member

eernstg commented Aug 11, 2023

[Update: At this point I'd actually recommend that we do allow an extension type with cyclic dependencies via type parameter bounds, but make it potentially nullable. This allows us to express extension type families safely.]

Thanks to @scheglov for spotting this issue! Consider the following program:

extension type V<X extends V<X>>(X it) {
  void foo() {
    Object o = this; // OK?
  }
}

In order to determine whether or not V<X> is a subtype of Object we need to check whether X is non-nullable. For that (applying the existing rules about non-nullable types) we need to check whether the bound of X is non-nullable, that is, whether V<X> is non-nullable, that is, whether V<X> is a subtype of Object. Etc.

So we have a termination problem with the nullability check.

Possible Specification Change

We could make it a compile-time error for an extension type to have a dependency on itself in its type parameter bounds.

We already have this kind of cyclic dependency check on the representation type, so we just need to extend that rule to include type parameter bounds in the set of dependencies that are traversed.

As a consequence, the above declaration of V would be a compile-time error because V depends on V in a type parameter bound, which is already a cycle. Of course, cycles with more than one node are errors as well:

extension type V1<X extends V1<X, Y>, Y extends V2<X, Y>>(int it) {}
extension type V2<X extends V1<X, Y>, Y extends V2<X, Y>>(String it) {}

var v1 = V1<Never, Never>(42);
var v2 = V2<Never, Never>("Hello!");

void main() {
  print(v1.it + v2.it.length);
}

This example compiles and runs with no issues today, but we make no attempt to find particular cases where this kind of cycle may be benign. In this proposal we just make all dependency cycles an error, to be safe.

Alternative specification change

An extension type with cyclic dependencies via type parameter bounds is allowed, and is potentially nullable.

In this proposal we allow the cycles, but assume that a value which is typed by this extension type could be null, which is always safe.

I'd recommend this option, because it allows us to express extension type families using F-bounded type parameters, which is a useful technique (cf. this comment).

Discussion

Note that essentially the same proposal came up in #3109, though for a different reason. You could say that the nullability check is an example of a case where the cyclic dependency does actually create the termination failure which was the motivation behind #3109 in the first place.

Anyway, now take one step back and consider the issue semantically. We might wonder whether it would actually be sound to allow declarations like V above, given that the example with the declarations of V1 and V2 is running just fine today.

Here is an example showing that it is not sound, currently, to assume that V<X> is non-nullable:

extension type V<X extends V<X>>(X it) {
  Object foo() => this; // Unsound.
}

extension type U(Null n) implements V<U> {}

void main() {
  var u = U(null);
  Object o = u.foo();
  print(o); // 'null'.
}

This is currently running code, and it shows a soundness violation.

The program does have a compile-time error with the current specification (and this would of course still be true with the additional error that this issue proposes): It is required that the representation type of U (which is Null) is a subtype of the representation type of V<U>, which is U, but we can't actually prove that Null <: U. So there may or may not be an example which shows that it is plainly unsound to keep the current ruleset, but it doesn't look like a safe bet that it is sound. ;-)

@dart-lang/language-team, WDYT?

@eernstg eernstg added question Further information is requested extension-types labels Aug 11, 2023
@lrhn
Copy link
Member

lrhn commented Aug 11, 2023

Do we have a problem without self-refernces too?

class C<X extends E<X>> {}
extension type E<X>(X _) {}

We don't allow class C<X extends X>, because X cannot be a supertype of itself.
But E<X> is the same as X at runtime, so by allowing the above, we effectively allow X bounded by itself.

void main() {
  C<X> Function<X extends E<X>>() f = C.new;
  print(f.runtimeType);  // C<T1> Function<T1 extends T1>(); 
}

(Tested using inline class in dartpad.dev.)

It might not actually be a problem, but I can't completely convince myself it's not. We presumably have the restriction for a reason. (Maybe just because it's trivial, X extends X is unfalsifiable, so you never need to write it.)

About the restriction here, there are two causes of the cycle, and we can break it at either:

  • The type variable bound depends on itself
  • The representation type depends on the type variable

That, together, means that the representation type depends on the extension type itself at any point where the bound of the type variable is used.

We can disallow self-references generally in bounds (and it's probably the safest thing to do),
or we can disallow it only when that type variable occurs in the representation type, or any of the superinterfaces
... but if it doesn't, what use is that type variable?

So OK to disallowing self-reference through type parameter bounds (I honestly thought we did that already, we disallow it for type aliases, and extension types should have all the same problems as type aliases).

@eernstg
Copy link
Member Author

eernstg commented Aug 11, 2023

One alternative approach which is definitely sound is to perform the cyclicity check and report that the extension type is potentially nullable whenever it participates in a dependency cycle. This would allow us to use F-bounds with extension types, which can be useful.

For example, consider a family of mutually dependent classes of which we wish to create some variants. For example, we could have the pair of classes Vehicle and Operator that depend on each other, and then we could have a "subpair" Car and Driver, and another "subpair" Bicycle and Cyclist. The members of each pair depend on each other (so a Car works correctly with a Driver, but not with an Operator or a Cyclist).

Here is the straightforward design using current Dart classes. The mutual dependency is expressed by using covariant parameters:

// Superclass group.

class Vehicle {
  void move(covariant Operator operator) {
    print('${operator.name} is operating this vehicle!');
  }
}

class Operator {
  String name;
  Operator(this.name);
}

// Subclass group 1.

class Car extends Vehicle {
  void move(Driver driver) {
    print('${driver.name} is driving this car wearing a ${driver.hat}!');
  }
}

class Driver extends Operator {
  String hat;
  Driver(super.name, this.hat);
}

// Subclass group 2.

class Bicycle extends Vehicle {
  void move(Cyclist cyclist) {
    print('${cyclist.name} is riding '
        'this bike${cyclist.isVirtuoso ? ' backwards' : ''}!');
  }
}

class Cyclist extends Operator {
  bool isVirtuoso;
  Cyclist(this.isVirtuoso, super.name);
}

We can use this set of class families as follows:

void main() {
  Vehicle vehicle = Bicycle();
  Operator operator = Cyclist(true, 'Alice');
  vehicle.move(operator);
  operator = Driver('Bob', 'sombrero');
  vehicle.move(operator); // Run-time error.
}

As shown in the comment, it is a run time error if we try to combine a Bicycle and a Driver. Based on the common supertype Operator, there's no way we can obtain a compile-time error by combining members of different subfamilies if they are statically typed as the top famile (e.g., we are using a Driver but the static type is Operator, etc).

We can use type parameters to turn this into a compile-time error:

// Superclass group.

class Vehicle<V extends Vehicle<V, O>, O extends Operator<V, O>> {
  void move(Operator operator) {
    print('${operator.name} is operating this vehicle!');
  }
}

class Operator<V extends Vehicle<V, O>, O extends Operator<V, O>> {
  String name;
  Operator(this.name);
}

// Subclass group 1.

class Car extends Vehicle<Car, Driver> {
  void move(Driver driver) {
    print('${driver.name} is driving this car wearing a ${driver.hat}!');
  }
}

class Driver extends Operator<Car, Driver> {
  String hat;
  Driver(super.name, this.hat);
}

// Subclass group 2.

class Bicycle extends Vehicle<Bicycle, Cyclist> {
  void move(Cyclist cyclist) {
    print('${cyclist.name} is riding '
        'this bike${cyclist.isVirtuoso ? ' backwards' : ''}!');
  }
}

class Cyclist extends Operator<Bicycle, Cyclist> {
  bool isVirtuoso;
  Cyclist(this.isVirtuoso, super.name);
}

We can use these class families as follows:

// This function depends on `Vehicle` and `Operator`, not on their
// subtypes, and it is statically safe.
void callMove<V extends Vehicle<V, O>, O extends Operator<V, O>>(
  Vehicle<V, O> vehicle,
  Operator<V, O> operator,
) {
  vehicle.move(operator);
}

void main() {
  // We can use the types without subtyping.
  var vehicle = Bicycle();
  var operator = Cyclist(true, 'Alice');
  var operator2 = Driver('Bob', 'sombrero');
  vehicle.move(operator);
  // vehicle.move(operator2); // Compile-time error.

  // In order to allow subtyping we'd need to provide type arguments.
  callMove(vehicle, operator);
  // callMove(vehicle, operator2); // Compile-time error.
}

If we actually have the first (unsafe) hierarchy, and we want to adapt it post-hoc to use type parameters to turn run-time errors into compile-time errors, we can use extension types to wrap the unsafe hierarchy as follows:

import 'first_hierarchy.dart' as unsafe;

// Supertype group.

extension type Vehicle<V extends Vehicle<V, O>, O extends Operator<V, O>>(
  unsafe.Vehicle vehicle,
) {
  void move(Operator<V, O> operator) => vehicle.move(operator.operator);
}

extension type Operator<V extends Vehicle<V, O>, O extends Operator<V, O>>(
  unsafe.Operator operator,
) {
  String get name => operator.name;
}

// Subtype group 1.

extension type Car(unsafe.Car car) implements Vehicle<Car, Driver> {
  void move(Driver driver) => car.move(driver.driver);
}

extension type Driver(unsafe.Driver driver) implements Operator<Car, Driver> {
  String get hat => driver.hat;
}

// Subtype group 2.

extension type Bicycle(unsafe.Bicycle bicycle)
    implements Vehicle<Bicycle, Cyclist> {
  void move(Cyclist cyclist) => bicycle.move(cyclist.cyclist);
}

extension type Cyclist(unsafe.Cyclist cyclist)
    implements Operator<Bicycle, Cyclist> {
  bool get isVirtuoso => cyclist.isVirtuoso;
}

The code that uses this hierarchy is identical to the code that uses generic classes (and it causes compile-time errors in the same situations).

The ability to do use this kind of technique could be an argument in favor of saying that we accept the circularity, but we just mark the extension type as potentially nullable when a dependency cycle has been detected.

@eernstg
Copy link
Member Author

eernstg commented Aug 11, 2023

Do we have a problem without self-refernces too?

Cf. this rule.

@eernstg
Copy link
Member Author

eernstg commented Oct 10, 2023

I'd like to re-proposed that we allow cyclic dependencies in bounds, but consider an extension type to be potentially non-nullable (that is, subtype of Object?, not Object) when the bound is used during the nullability computation. In particular, we'd get the following error:

extension type V<X extends V<X>>(X it) {
  void foo() {
    Object o = this; // Compile-time error: `V<X>` is potentially nullable.
  }
}

The reason why we get this error is that this has the type V<X> which is potentially nullable if X is potentially nullable (because that's the representation type), which is potentially nullable if V<X> is potentially nullable (for a type variable we must consider the bound). However, we have now reached V, which makes this computation cyclic, so we bail out and declare that V<X> is potentially nullable.

@dart-lang/language-team, are you willing to adopt this rule?

@lrhn
Copy link
Member

lrhn commented Oct 10, 2023

SGTM.

@eernstg eernstg changed the title [extension-types] Make cyclic dependencies in bounds an error [extension-types] Cyclic dependencies in bounds should imply potentially nullable Oct 17, 2023
@eernstg
Copy link
Member Author

eernstg commented Oct 30, 2023

I'll close this issue: The language team has accepted #3415, which is a substantial simplification of the treatment of nullability of extension types. That decision makes this issue obsolete. (Woo-hoo!)

@eernstg eernstg closed this as completed Oct 30, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
extension-types question Further information is requested
Projects
None yet
Development

No branches or pull requests

2 participants