Clarify the notion of 'same type' used with augmenting declarations

[eernstg]

The augmentation feature specification relies on the notion of two types being the same type in a couple of locations. For example, it is an error if an introductory declaration specifies a type T1 as the return type of a method m, and an augmenting declaration of the same method has a return type T2, and T1 is not the same type as T2. A similar error occurs for corresponding parameter types that are not the same type, and similarly for any other type in the signature. For example:

void foo({required int i});
augment foo({required String i}) {} // Error.

It is not a problem that the return type is omitted from the augmenting declaration (it is then "inherited" from the introductory declaration), but it does give rise to a compile-time error that the parameter type is specified as two different types.

It is not specified which notion of 'same type' we must use in order to determine whether or not there is an error. Hence this issue, which is intended to select a specific, useful notion of 'same type' for this purpose.

It would not be appropriate to use mutual subtyping. In particular, if we were to do that then we could declare the return type of a method to be dynamic and then augment it as returning Object? (because they are "the same type" with respect to this criterion). The difference between those two types is highly significant to callers of this method, so we must avoid the ambiguity that appears to exist if we allow this (it won't suffice to specify unambiguously who wins, we just don't want programs to look ambiguous in this way).

We have another notion of 'same type' in the language already: Type literals are canonicalized according to the notion of 'same type' which is specified here. I'd recommend that we keep things simple and consistent, and reuse this notion of 'same type' also for the situations where types are required to be the same in an augmentation related construct.

I should mention one property which may give rise to some debate: This notion of 'same type' applies type normalization to the operands before they are compared structurally. In particular, this means that the following would not be an error:

void foo();
augment FutureOr<void> foo() {} // OK.

This is OK (according to this criterion) because normalization of FutureOr<T> where T is a top type (which includes void, but also dynamic and Object? and many others) reduces FutureOr<T> to T. So we're testing void against void, which succeeds.

Another possible choice would be to use a variant of this criterion which leaves out the normalization and otherwise works the same.

@dart-lang/language-team, WDYT?

[lrhn]

Agree. "NORM-alpha-equivalence" seems like the right choice for repeated types due to "writing the same declaration in multiple places".
There is only one declaration, it has only one type. If you write the same time more than once, you should write the same thing.

The FutureOr removal is annoying, but then don't do that.
The type will still be the type declared in the introductory declaration, not its normalization.

There is another option, though: structural alpha equivalence without NORM. It's what we do after NORM in the linked example.
We are not working with types created by arbitrary substitutions, only with types directly written in the code.
We can't end up with int?? and needing to determine that it's the same as int?.
We don't need to care if X extends Never and Never are both bottom types, just write the same thing everywhere.
And we won't lose FutureOr of a top type.

It's a stricter requirement than doing NORM first, but it's also very, very easy to just write the same type clause every time. You won't ever need to write something else.

---

If we do go with NORM, then a thing that worries me is that we otherwise never use NORM in the static type system.
The link is for canonicalization of constant-evaluation Type objects, which is still evaluation and works on (going-to-be-)runtime objects.

Static types are more complex than runtime types. The static type system contains extension types, intersection types, unbound type variables and type schemas, which are all absent in the runtime system.
We need to ensure that NORM works with at least the parts that apply to member declaration signatures.
That rules out intesection types, which cannot be reified, and probably type schemas, but not extension types, and maybe not unbound type variables.
(Anything else I've forgotten?)

So, to be able to apply NORM to (some) static types ...

Well-defined types

NORM applies to types, not syntactic type clauses. We cannot check this equivalence before we're past the point in the static semantics where types are well-defined, and we have the ability to find the type that a type clause denotes. That means identifier resolution, knowing which type-introducing declarations exist, and how many type parameters they take (and the ability to expand type aliases).

Since augmentations include class declarations, which define types, we should make sure that we can define types from them before needing to check for type consistency.

Luckily we only need to know how many type arguments a declaration has. We don't care (yet) what the bounds are, or super-relatioons. For a generic type introducing declaration C with n type parameters, every instantiation of C<T1,...,Tn> is a type. Some of them may be mal-bounded types, but they are mal-bounded types.

It's a compile-time error if there are multiple declarations of a class/mixin/enum/extension type which have type parameters, and they don't agree on the number of type parameters. That's an easy syntactic check, which we can do without knowing anything other than name resolution (and having checked that all the declarations have the same kind to begin with.) Some augmenting declarations may omit type parameters entirely, but if any has type parameters, they must have the same number.

With that in place, we can start talking about the types of the program. The class hierarchy may still be bad, we don't have subtyping yet, but we have types themselves, which means we can defined NORM on them.

Extending NORM for extension types

The extension type spec doesn't mention NORM, so we need to extend NORM to extension types.

Should be as easy as saying: **NORM**(E<T1,...,Tn>) where E denotes an extension type is E<NORM(T1), ..., NORM(Tn)> (where n can be zero for a non-generic type).

Just like any other nominative type, like the ones introduced by a class declaration, the type is identified by the class definition introducing it and a vector of type arguments of the correct length, and normalizing it just means normalizing the type parameters.

Extending NORM for unbound type variables

I thought we may have needed to extend NORM to unbound type variables, but it seems it already handles that,
probably for recursing inside a generic function type.

The NORM rule for type variables is:

NORM(X extends T) =

• if T is Never then Never
• if T is a type variable Y and NORM(Y) is Never then Never
• else X extends T

That worries me a little, because it requires the bound of a type variable to be known
before being able to use NORM on it.

Take:

abstract class C<V extends T1<V>> {
   void foo(V v);
}
augment abstract class C<V extends T2<V>> {
   augment void foo(V v);
}

where T1<V> and T2<V> are some type clauses that contain V.

There is only one semantic V type variable, and types are semantic.
If we have both <V extends T1<V>> and <V extends T2<V>>, at most one of T1<V> and T2<V> can be the bound of V.
(Then the other one has to be NORM-equivalent for that V.)

It's probably all solved by one restriction on augmentations:
The introductory declaration cannot omit type parameters or their bounds. (I think this is true, correct me if I'm wrong! Or make it so!)

That means we have a canonical declararation of the bound of the type variable, and we just need to check that other bounds of that type variable are the same type.

So the bound of V is T1<V>. Then we check if NORM(T1<V extends T1<V>>) is alpha-equivalent to NORM(T2<V extends T1<V>>). If not, it's an error, otherwise the actual type probably never matter.

(Even if we don't require the introductory declaration to have all bounds and types, we can just use the bound of the first augmentation which has one as authoritative, and check that the others agree. That still avoids not knowing the bound until we have determined if the bounds are the same type.)

Other worries ...

We can't assume type inference is possible yet at the point where we check augmentation declaration validity.
That's probably why raw types are not inferred, they're instantiated to bounds which is a syntactic operation.

So:

class C<T extends List> {}
augment class C<T extends List<dynamic>> {}

This is valid because the type denoted by List is the same as the type denoted by List<dynamic>, because that's what instantiate-to-bounds makes it into.

Are there any cases where we do more than just instantiate to bounds, which may get confuses by augmentations that aren't complete or aren't consistent.
(Mixin inference is one place where we do something, but I don't think it has any relevance here.)

I only worry about the type-declarations here. When they're in place, we can define subtyping, and then we can start doing other type-related things like looking at member signatures.

(Yes, I wrote all that before realizing that just not NORM-alizing would be a better option. So it's here as argument for why it's a better option.)

[eernstg]

;-D

I'd prefer the non-normalizing approach as well, at this time. The situations where normalization actually does something noticeable, it's most likely going to cause confusion rather than helping anybody.

[lrhn]

One problem with pure "structural alpha-equivalent" is that it doesn't normalize at all, so something like:

typedef N<T> = T?;

int? foo();
augment N<int> foo();
augment N<N<int>> foo();

would report int? and N<int> to be the same type (int?), but not N<N<int>>, which is int??.

At least as specified. Implementations cannot represent ?? at all, so we couldnt' implement that specification.
So we probably do need at least specify ??->? normalization somewhere.
(And as discussed, maybe we should just build it into our type parameter substitution definition. Maybe we should formalize the shapes of our types so that you can't nest ?s.)

[leafpetersen]

As @lrhn mentions, we have a piece of tech debt in our specification in that we originally formulated the language with nullability being a constructor in the type system, so that e.g. int?, and int?? and int??? are all things that exist and have (the same) meaning. This was to make the underlying model of nullability as a union type line up closely with the primitive nullability we were building in. In practice, the implementations simply made nullability a property of types, essentially maintaining a normal form as an invariant. I don't think there is any deep issue here, but it does make specifying things in a way that communicates intent accurately to the implementations somewhat more challenging, and probably at some point we should just change our specification language to use the same approach as that used in the implementations.

In the meantime, I think it is reasonable here to simply be pragmatic in the same way that we are pragmatic about type aliases: that is, say something to the effect that the equality we want here is structural alpha-equality on types with all type aliases expanded to their definitions, and all nested nullability markers (?) coalesced. WDYT?

[lrhn]

structural alpha-equality on types with all type aliases expanded to their definitions, and all nested nullability markers (?) coalesced. WDYT?

Do we want to remove unnecessary ?s too?
Things like dynamic?, Null?, and probably even FutureOr<void>?.

Maybe. I don't know if the implementations can represent dynamic? or void? at all.

So not "nested nullability coalesced", but more like "unnecessary ? removed", if the type is already nullable, a following ? is ignored/removed.

The second ? of int?? is unnecessary to do it includes that.

Still leaves Null ≠ Never?.
(And X-with-bound-Never ≠ Never.)

Or we can just tell people to not write that. An augmentations should be able to write the same type, and if it omits a type, it won't be inferred to something new. It's just copied from the augmented declaration. Weird types won't be introduced indirectly.

Just on general principle, I tried specifying the "type entities" of our type system, and a consistent and capture-avoiding substitution in a way that doesn't allow redundant ?s, just to make sure it's possible. (It is, I think.)