Empty Top Types.

[modulovalue]

Consider the following:

void foo<T>(T a) {
  // ...
}

This code contains a top level function foo with a single type parameter T. It might look like T doesn't have any behavior at all, but T is implicitly declared to extend Object?. Any value of type T comes with everything that comes with Object e.g. equality, hashCode, an identity, runtimeType and much much more.

It could be argued that this is bad, but for purposes of practicality this seems to be a very good trade-off and I'm not arguing against that. However, I'd like to be able to specify and have the type checker statically prove that T does not need to be anything as capable as Object is.

This idea of a type not being an Object could seem to make no sense because everything in Dart is an Object. However, if we think of foo as a specification and not as a program, T is simply overspecified. None of its Object capabilities are being used in foo. They are redundant and not necessary.

Also, any reader of foo must for themselves first prove that e.g. the equality/hashCode/runtimeType/toString/... of a is used/unused before he can assume that to be a fact when reasoning about foo. An empty top type would make cases where that is needed much less painful.

What I'd like to be able to do is something like the following:

void foo<T extends Top>(T a) {
  // ...
}

where Top is e.g.

// dart:core

// Top is not an Object.
abstract class Top {}

class Object implements Top {
  /// ...
  external bool operator ==(Object other);
/// ...

i.e. bound T to a Type that has no methods or other properties and is not an Object.

---

One interesting consequence of that is that it would mean that T could not be used as a key in Maps and could not be the value of Sets. Unfortunately, I think that Lists could also not contain values of type Top because they need equality for e.g. Iterable.contains. But I claim that that is not a bad thing, but a useful feature. We would just need to be explicit about using Lists or Maps with T by e.g. injecting the construction of a List with T and using that instead.

void foo<T extends Top>(
  T a,
  List<T> Function() list,
) {
  final newList = list();
  newList.add(a);
  // ...
}

[eernstg]

equality, hashCode, an identity, runtimeType and much much more.

It's actually equality (operator == and hashCode), runtimeType, noSuchMethod, and toString.

It's true that some of these members are somewhat misplaced in some situations: toString can be used during debugging, but it doesn't take much of a business context before there is a need for a much more flexible kind of support for obtaining a textual representation of a given object (and it's probably going to be different APIs for different types of objects); noSuchMethod is needed in order to support a very basic kind of reflective coding, but many applications don't do that at all; runtimeType should basically have been a top-level function (it's really, really hard to come up with a good reason for overriding it); so we're left with the two equality related operations that make it possible for every Dart object to be a member of a set, or a key in a map.

If we say that it is pragmatically useful to have at least some members on Object, even if it's only == and hashCode, then I'd tend to think that it isn't much of a problem that those members are known to exist for instances of any type, including a type variable with no declared bound.

Which problems does it create that there is no compile-time error for void foo<T>(T a) { print(a.hashCode); }?

[modulovalue]

Which problems does it create that there is no compile-time error for void foo(T a) { print(a.hashCode); }?

One instance where this comes up a lot is when I try to generalize some piece of code.

E.g. consider a foo that takes a String and consider a situation where we'd like to generalize and take a sequence-of-something instead.

i.e. we'd like to go from:

void foo(String a) {
  // ...
  print(a.hashCode);
  // ...
}

to

void foo<E>(List<E> a) {
  // ...
  print(a.hashCode);
  // ...
}

String has an equality that doesn't at all behave like the List equality. It would make little sense to use the equality that comes with the new type here. I'd like to be able to use the static type system to prove that I'm not using the default equality of the type that I'm migrating to.

For small examples this is trivial to verify manually, but it is hard to do that with bigger examples because the equality may leak in various places such as when the previous type has been used in e.g. a Set.

void foo<E>(List<E> a) {
  final b = a;
  final c = b;
  // ...
  print(a.hashCode);
  // ...
  final d = {c};
  // ...
}

The type that we are migrating to might not even have a sensible equality. Unfortunately, today I can't communicate that to the type system so I've been using the following mixin instead:

mixin ForbidEqHash {
  @override
  bool operator ==(
    final Object other,
  ) {
    throw Exception(
      "Cannot use .== on " +
          runtimeType.toString(),
    );
  }

  @override
  int get hashCode {
    throw Exception(
      "Cannot use .hashCode on " +
          runtimeType.toString(),
    );
  }
}

Edit: In the example above, I'd swap String with the hypothetical "Top" type first to let the analyzer tell me whether any of its Object members are being used (or I'd use a custom interface implementing Top instead of using List.)

---

It's true that some of these members are somewhat misplaced in some situations:

Did it come across like I was implying that? I actually have no issues with Object containing any of the methods that it does. Being general comes with a lot of overhead that is not worth it in many cases and I think Dart balances that very well.

[lrhn]

Too bad using void as a type bound doesn't work for that - it allows you to do anything to the value, because the code preventing you from using void values only apply to the actual void type, not T extends /*alias for*/ void.

But in seriousness, I don't see much value in being able to pretend that a type doesn't have members that all objects do have.
If you don't want to call those members, directly or indirectly, it's going to be very hard to enforce, so it will at most be skin-deep. For example, it's not clear whether you can can use them in string interpolations (Top x = ...; print("$x");?).

It might be occasionally useful, but unlikely to be worth the implementation effort, maybe not even in the absolute, but definitely not in opportunity cost.

[modulovalue]

Too bad using void as a type bound doesn't work for that - it allows you to do anything to the value, because the code preventing you from using void values only apply to the actual void type, not T extends /alias for/ void.

I see, you are referring to the following;

void main() {
  bar(0);
}

void bar<T extends foo>(T a) {
  print(a == a); // true
}

typedef foo = void;

Repurposing void for this would be wonderful.

---

[...] to pretend that a type doesn't have members that all objects do have [...]

Perhaps I am misunderstanding what you are saying, or I wasn't clear enough, but another way how the Top type could be used is as an alternative to the default Object superclass.

Consider the following:

class Bar implements Top {
  final int i;
  const Bar(this.i);
}

We wouldn't be pretending that Bar doesn't have those members, it actually wouldn't have those members because it wouldn't be of type Object and i would be its only member.
Even without that, as this would probably involve big changes, the implementation of Bar could always be hidden and only its interface exposed.

For example, it's not clear whether you can can use them in string interpolations (Top x = ...; print("$x");

The answer to this question would be no if String interpolations are syntax sugar over calling the toString() of a value of type Object, using x in an interpolation would not be possible because the type of x has no supertype of type Object.

It might be occasionally useful, but unlikely to be worth the implementation effort [...]

Thank you, I appreciate the honesty.

[eernstg]

@modulovalue wrote:

One instance where this comes up a lot is when I try to generalize some piece of code.

OK, thanks for the careful response!

i.e. we'd like to go from:

void foo(String a) {
  // ...
  print(a.hashCode);
  // ...
}

to

void foo<E>(List<E> a) {
  // ...
  print(a.hashCode);
  // ...
}

---

I get the impression that we're talking about concepts like parametricity (a la Theorems for free), where the core point is that a generic entity (say, a generic function) treats entities whose type is a type parameter X in exactly the same way, no matter which value X has at any given time during execution. With pervasive parametricity, it's obviously sound to erase type parameters, and we even get the properties that Wadler describes as free theorems.

However, Dart does not support parametricity. One counterexample is that it is possible to evaluate e is X, which could yield true for some values of X and false for other values of X, even in the case where e evaluates to exactly the same object in both cases.

Next, not even parametricity would suffice to make a transformation like the parameter type change from String to List<E> safe (in the sense that the body of the function will "continue to do the same thing" in some sense, and hence it isn't broken, in some other sense ;-).

So I don't think it's a goal for Dart to be able to provide any particular guarantees about the before-and-after properties of code where this kind of change is performed. You'd simply have to check manually that the change yields code which is still plausibly error-free, based on whatever constraints you have on the expected behavior of foo.

---

Drilling down, we have the issue about using hashCode or operator == by accident, and worrying about those methods having a different (and incompatible) semantics before-and-after a given change.

This issue would come up for any member access x.m (or x.m(...), x.m<...>(...), etc.) during a change of a declaration from T1 x to T2 x where T1 and T2 are sufficiently different. E.g., they may be different subtypes of a type T0 that declares a member named m (that's like the Object.hashCode example), or, worse, they may both have a member named m, but they don't have a common supertype that declares m, etc.

With unrelated declarations there's basically no hope that the before-and-after situation would be related, and we would definitely just have to study (and possibly debug) the code from scratch.

With the related declarations we ought to have a safe situation, because both the declaration of T1.m and the declaration of T2.m were written by a developer who knew about the declaration T0.m, and hence T1.m and T2.m should satisfy all the constraints on T0.m (which is just the Liskov substitution principle). Of course, we cannot prove (or hope to get a type checker to prove) that this is so, but we're certainly allowed to frown on the developer who wrote an implementation of one of those m members such that it isn't true. To some extent. Hopefully. ;-)

@lrhn mentioned void, and that would indeed be a useful type here: It allows us to make every use of an expression other than data transfer into a target with type void a compile-time error.

In particular, print(x) and x.toString() are compile-time errors when the type of x is void.

void foo<T>(T a) {
  void safeA = a;
  ... // Same body as before, but using `safeA` rather than `a` when possible.
}

The exception (where we cannot use safeA) is the case where the required type is T:

T foo<T>(T a) {
  void safeA = a;
  ... // Same body as before, using `safeA`. Except things like:
  return a; // Can't use `return safeA;`, and `return safeA as T;` is silly.
}

I have proposed introducing the notion of a void type (with the "don't use this object" constraint) associated with an arbitrary different type:

T foo<T>(void<T> a) {
  // Same body as before.
  ...
  print('$a, ${a.hashCode}, ${a.toString()}'); // Compile-time errors now.
  Object? o = a; // Compile-time error.
  Object? o2 = a as Object?; // We have always allowed for `as` as an escape.
  ...
  return a; // OK: Type `void<T>` is assignable to type `T`.
}

The point is the same as with the current void type: "If you want to use this object then you're mistaken!", and we're just slightly generalizing the ability to perform data flow (void x = 1; and than void y = x; is OK, with the generalization void<int> z = 1; and void<num> w = z; and y = z; are ok, too).

However, that proposal didn't generate much enthusiasm. Also, it hasn't been fleshed out, (e.g, how do we treat void<void<int>>? ;-).

[lrhn]

If Top was a type, and implementable, without any methods, it would have serious consequences in all the little corners of the language that assumes everything is an Object?.

Would Top be a proper supetype of dynamic, so Bar implements Top cannot be assigned to dynamic?
Or would dynamic be able to hold Top objects, in which cast dynamicExpression.toString() would no longer have type String. (And if the call failed, it would not be able to call noSuchMethod either, so what should it then do? Probably just throw directly.)

Is void a proper subtype of Top? If so, you can no longer return everything from a void returning function.
If not, well, nothing big happens then, but void is not a valid type argument to class List<T extends Object?>.
And if we change the default bound of a type parameter to be Top instead of Object?, you can no longer use .toString and == on the values, which, as you mention, is a problem for List.contains.

An object which is not an Object? is severely hampered in how it can interact with other Dart types, because everything is built assuming that everything is an Object?.

[modulovalue]

This issue would come up for any member access [...]

Thank you, this captures a much broader idea that also includes the one that I am referring to and I agree with your conclusions. But it looks at it from a different angle and I don't think that what I'm referring to applies to this more general idea because of the following:

[...] Of course, we cannot prove (or hope to get a type checker to prove) that this is so [...]

I agree with you. I meant to say that I'd like to have the type checker be able to prove the absence of the members that come with Object, and not to directly prove a new property e.g. that two declarations are safe in some way.

Consider the following:

abstract class Cat {}

abstract class Dog implements Cat {}

Assume that we have inherited this code. Obviously a Dog is not a Cat, but the previous developer didn't know that. We can 'tell' the type system that a Dog is not a cat by removing the constraint that the Dog is a Cat. i.e.

abstract class Cat {}

abstract class Dog {}

If we assume that our program doesn't use any unsafe features (is, as, covariant & dynamic) and If we assume that the Dart type system is sound, then the type checker will prove that Dog is not a Cat by not allowing code that assumes that to be the case to compile. (Or rather, we have to provide a proof and the type checker will prove that our proof is correct)

A more realistic example:

abstract class BinaryTree<T> {
  T get value;
  
  BinaryTree<T> get left;

  BinaryTree<T> get right;
}

Conceptually, a BinaryTree is not an Object. It does not have a single sensible equality (we could compare the shape of two binary trees, we could compare the value, we could compare both, we could look at whether they are identical). It also does not have a single sensible toString() method.

Today, we can tell the type system that a Dog is not a Cat and use the analyzer to help us fix our wrong assumptions, but we can't tell the type system that a BinaryTree is not an Object to let the analyzer help us fix our wrong assumptions. A hypothetical Top type would allow us to do that i.e. to (soundly, (that's the most important part to me here)) prove the absence of the members that Object comes with.

---

I have proposed introducing the notion of a void type (with the "don't use this object" constraint)

This could be helpful in solving the issue that I have raised, but I see a usability related issue with this idea (as a solution to the problem discussed here). Adding such a constraint would result in a plethora of unrelated errors. (i.e. 'don't use x... here, don't use x.hashCode here, don't use x... here, ...'). The errors that a Top type would produce would only be about the use of members that exist on Object.

---

Would Top be a proper supetype of dynamic, so Bar implements Top cannot be assigned to dynamic?
Or would dynamic be able to hold Top objects, in which cast dynamicExpression.toString() would no longer have type String. (And if the call failed, it would not be able to call noSuchMethod either, so what should it then do? Probably just throw directly.)

Making 'Top' a supertype of dynamic would be in my opinion too invasive. Developers that don't want to use a type system can ignore the type system and use dynamic. I wouldn't want to remove this feature. I agree with dynamic being able to hold values of type Top and throwing directly as a solution to that problem.

it would have serious consequences in all the little corners of the language that assumes everything is an Object?.

Wouldn't these places already have to consider dynamic and be covered by that if Top is a subtype of dynamic?

And if we change the default bound of a type parameter to be Top instead of Object?

I should have mentioned that I do not want this to be the case. This would break a lot of code and I think the default behavior of Object? being the default bound of a type parameter is a good compromise.

Is void a proper subtype of Top?

I'll have to think more about the potential consequences of this decision.

---

'Top' is probably a misnomer. If dynamic would be a supertype of 'Top' then Top is obviously not the Top Type. Calling it Top would be confusing. I'd like to propose Always as an alternative name to Top.

[eernstg]

[as opposed to errors produced for expressions of type void<T> ..]
The errors that a Top type would produce would only be about the use of members that exist on Object.

Right, (except for the fact that we never got around to spell out the details): if T is any given type then an expression e of type void<T> could only be used in a context where it is assigned to a variable/parameter of type void<S> for some S where T <: S (where void means void<Object?>), and no member accesses (at all) would be allowed.

As usual ;-), we drilled some holes in this armor, so there's a whitelist of things you can do, and the most significant one is e as U for any type U. So if you wish to extract the T as such then you do e as T, and it is then usable in all the T ways (which would be determined by the interface of the bound B if T is a type variable with bound B).

The typical use case is actually the following:

class A {
  bool foo() { /* do the foo thing and then return 'true' if successful, otherwise return 'false' */ }
}

class B implements A {
  void<bool> foo() { /* do the foo thing, which in this case is guaranteed to succeed*/ return true; }
}

The point is that it is unnecessary to check the returned value in the case where the receiver has type B, and we can express this property if we can mark a non-top type as "voidy".

The ability to complain about member accesses is just accidentally relevant here.

[modulovalue]

Quote from Dart 2.0 Static and Runtime Subtyping

The types dynamic and void are both referred to as top types, and are considered equivalent as types (including when they appear as sub-components of other types). They exist as distinct names only to support distinct errors and warnings (or absence thereof).

Lasse wrote:

Is void a proper subtype of Top? If so, you can no longer return everything from a void returning function.
If not, well, nothing big happens then [...]

Given that dynamic and void are both considered to be equivalent types, I'd say the answer should be no. I described in my previous response why I think Top i.e. Always should not become the Top type. My intention would be for it to only lie just above Object and not contain any of Objects members.

[eernstg]

Given that dynamic and void are both considered to be equivalent types

Well, they are subtypes of each other, which means that they occupy the same equivalence class according to the subtype relationship. In particular, exactly the same objects will yield true when evaluating is void and is dynamic (except that we need to use a type alias typedef Void = void; and then do is Void because is void is a syntax error). This equivalence class is the set of top types (containing all objects), and Object? is yet another member of this club.

However, the static analysis of an expression of type void and an expression of type dynamic and an expression of type Object? is very different.

You may have various philosophical takes on what it means to be a type, but we can at least say that the static analysis of Dart doesn't ignore these distinctions. So from that perspective all those top types can be considered to be the same type or not, depending on the purpose of the discussion.

But if we add a new Top type then we don't (currently) have any objects that belong to Top and not to Object. In other words, they are also extensionally the same type (and they might as well be mutual subtypes). This is again a hint in the direction of considering Top as just another top type which has the special property that there are no members.

[modulovalue]

If you are saying that my use of the idea of the top type was not entirely correct here, then I agree. I did not mean to treat Object? as something different from what it is. This was a mistake on my part and I'd like to apologize.

My proposal to call this new type Top might have caused some confusion. As I pointed out earlier, I hope that by referring to it as Always, my intent becomes more clear.

---

I hope that the following diagrams are a more accurate representation of my intent:

i.e. this is an incomplete model of the current type system.

i'd like to propose the following:

Where Always is a Dart Type that comes with no members, and Always? acts like Object? where any access to members that Always doesn't have (in e.g. a dynamic setting) would throw.

---

But if we add a new Top type then we don't (currently) have any objects that belong to Top and not to Object.

Could Null 'belong' to Top (i.e. Always) and not to Object as a fix for #2759?

[eernstg]

.. this is an incomplete model of the current type system.

Yes, and I'd prefer that we had a name for the top element, say Any.

dynamic and void and all the other top types would then just be different ways to denote the top type (same type extensionally) in ways that have various implications during static analysis (like "member invocations on a receiver of type dynamic are checked dynamically, not statically").

With a regular name for a regular class, Any, we could simply say that its interface contains those 5 members that both Object and Null are known to have, and then there's no anomaly to explain when we type check x.toString() in a situation where the static type of x includes null.

(With the current approach it is a pure but convenient accident that Null and Object have exactly the same member signatures. We would never allow for an invocation of foo() on a receiver of type either-A-or-B in a situation where A and B both have a member foo that admits such invocations—we don't otherwise abstract over several independently declared members that happen to have the same name and signature, they are just considered unrelated. Hence, it's an anomaly that we type check and allow x.toString() when x has type int? or Object?).

The second subtype graph doesn't eliminate that anomaly, assuming that Always doesn't have any members.

I still think your scenario would be served just fine by being able to specify that any given members of a given type cannot be invoked, and void<T> would be a wholesale version of this (with void<T> x, any member access x.m/x.m()/etc. would be a compile-time error). It may or may not be useful to allow for assignments from void<T> to T, but that's just one of many details that would need to be settled before we'd have a real language feature.

[modulovalue]

would then just be different ways to denote the top type [...] in ways that have various implications during static analysis

This sounds awesome because being able to think of those types in that way would make Dart much easier to teach and learn i.e. make Dart even better at what it already is very good at.

---

I still think your scenario would be served just fine by being able to specify that any given members of a given type cannot be invoked, and void would be a wholesale version of this

That may be the case, but what worries me about a solution like that is that it seems like this would be a new idea that new and existing users would have little intuition for.

By having a type/interface that a user can assume not to carry ==, hashCode, and .toString(), a user can use pre-existing knowledge to reason about his code. If he wanted them, he could add them, like with other interfaces. If he didn't want them, he could not depend on Object, like with other interfaces.

Other languages like e.g. Swift have special interfaces for these behaviors e.g. Equatable, Hashable, CustomStringConvertible (It's more complicated because there's also e.g. AnyHashable.)
Also, there's an Equality interface in the collection package which indicates that a need for more explicitness here exists. Having E in that interface be bound to a type that has == and hashCode doesn't seem to make much sense to me, would you agree?

I'm not suggesting that Dart should adopt Swifts approach and be as granular as Swift is, but I do oftentimes miss that.

The second subtype graph doesn't eliminate that anomaly, assuming that Always doesn't have any members.

I will have to think more about that. (Yes, I intended for Always to have no other members except for perhaps runtimeType and noSuchMethod, but I wasn't completely clear about that.)

[modulovalue]

@eernstg I had some time to think more about your void<T> idea from a more general point of view and I think that it is fascinating and could lead to a more general framework for solving issues of this kind without 'polluting' the type hierarchy. I am aware of some of the concepts that it depends on, but my understanding of them isn't deep enough yet for me to feel confident enough to discuss them further at this time.

Your approach seems to be much more expressive and could be made to 'feel' like my proposal without some of its downsides. I think that solving this particular issue with the solution that I proposed is not necessarily the best approach.

Thank you Erik and @lrhn for your feedback and valuable input. I think I will come back to this in the future.