Feature specification of class interfaces in Dart

class-interfaces.md

Flattened Interfaces

Author: eernst@.

Version: 0.1 (2018-01-10)

Status: Under discussion.

This document is a feature specification of the notion of a flattened interface in Dart that generalizes the concept of an interface in Dart such that it handles covariant parameters more precisely, and such that it threads the distinctions between Object, dynamic, and void appropriately through the interface computation.

PS: This is still a rough draft; in particular it's surely necessary to check and possibly revise the notion of a 'correct override', where we currently rely on the negation of statements of the form it is a static warning if .. overrides .. in dartLangSpec.tex.

Motivation

The current Dart language specification introduces the notion of interfaces, but they do not take covariant parameters into account, and we need to clarify how to handle the distinctions between Object, dynamic, and void properly. This feature specification specifies how to enhance this notion with a richer notion of method signatures, such that covariant parameters are handled more precisely, and it specifies an erasure technique that is used to handle the distinctions among the top types.

In the section 'Interfaces' in the existing Dart language specification, interfaces are introduced as follows:

An {\em interface} defines how one may interact with an object.
An interface has methods, getters and setters and a set of
superinterfaces.

An implicit interface is ascribed to each class as follows:

The {\em interface of class $C$} is an implicit interface that declares
instance members that correspond to the instance members declared by
$C$, and whose direct superinterfaces are the direct superinterfaces
of $C$ (\ref{superinterfaces}).

Using a separate set of rules for inheritance among interfaces, the implicit interface of a class is populated with the methods declared in the class itself, as well as the ones inherited from all the superinterfaces. The distinction between members that an interface declares and members that an interface has correspond precisely to the same concepts for classes: It declares the ones that are present syntactically, and it has those ones as well as the ones which are inherited.

This document introduces the notion of a flattened interface which is an entity that involves only method signatures (as opposed to 'methods, getters and setters'), and no superinterfaces.

A method signature is a generalization of the notion of a 'method, getter or setter' which is used for interfaces. It is the signature of a method (which is taken, here, to include setters, getters, and named methods as well as operators), and it includes a return type, a name (which can be an operator), and a parameter signature type list.

A parameter signature type list is a list of parameter signature types, and it allows for the specification of the signature types of a number of required positional parameters as well as, optionally, either some optional positional parameters, or some optional named parameters.

A signature type is either a Dart type, or it is the special construct covariant {...}, where the braces contain a set of Dart types. In other words, a signature type is just a regular Dart type, or it is a set of Dart types, marked as "covariant".

Compared to the notion of an implicit class interface that we have currently, the purpose of having the notion of a flattened interface is that (1) it allows us to explicitly state the rules for conflict resolution in the case where the interface of a given class inherits multiple conflicting method declarations from its superinterfaces; (2) it allows us to collect the relevant information about the types involved in the static checks pertaining to covariant formal parameters; (3) we use it as a framework for specifying how to thread the choice of top type through the computation, and (4) it allows the type system to provide better type analysis, such that programs which have actual problems will be detected in some cases where they are currently accepted without any diagnostic feedback.

Syntax

This specification does not include grammar changes.

It does, however, use grammar rules to define certain data structures which are used in order to specify flattened interfaces. It is not intended that these grammar rules will ever be part of the Dart grammar.

Language Concepts

A top type is one of Object, dynamic, or void, or one of the equivalent types expressible using FutureOr.

For instance, FutureOr<Object> is just a different notation for the type Object. In this document we assume that such types have been normalized to their most concise form, e.g., we have List<dynamic> rather than List<FutureOr<dynamic>>.

Top type erasure is an inductive transformation (that is, a transformation which is applied recursively on subterms) that maps every type to itself, except that in covariant positions dynamic and void are mapped to Object. Top type erasure can be applied to the header of a method declaration, which means that it is applied to the type annotations of its formal parameters.

In this document we often refer to this transformation simply as 'erasure'. For example, dynamic erases to Object, and so does void, and List<dynamic> erases to List<Object>; but void Function(dynamic, void) erases to Object Function(dynamic, void), and Function(Function(void)) erases to Object Function(Function(Object)). A method header like void foo(dynamic, void) erases to void foo(Object, Object).

A signature type is a term on one of the following syntactic forms (non-terminals with no definition in this document are taken from the specification grammar Dart.g):

signatureType ::=
    type |
    'covariant' '{' typeList '}'

The former is just a regular Dart type, and the latter is a collection of Dart types marked as "covariant".

A parameter signature type list is a construct of the following form:

parameterSignatureTypeList ::=
    '(' requiredParameterSignatureTypeList?
        optionalPositionalSignatureTypeList? ')' |
    '(' requiredParameterSignatureTypeList?
        namedSignatureTypeList ')' |
requiredParameterSignatureTypeList ::=
    signatureType (',' signatureType)*
optionalPositionalSignatureTypeList ::=
    '[' requiredParameterSignatureTypeList ']'
namedSignatureTypeList ::=
    '{' namedSignatureTypes '}'
namedSignatureTypes ::=
    namedSignatureType (',' namedSignatureType)*
namedSignatureType ::=
    signatureType identifier

The intention is that a parameter signature type list specifies a particular argument list shape, just like the non-terminal formalParameterList, but it associates a set of types rather than a single type with each covariant parameter. Moreover, convenience features like trailing commas are omitted.

A flattened method signature is a construct of the following form:

flattenedMethodSignature ::=
    type 'get' identifier |
    type 'set' '(' signatureType ')' |
    type (identifier | operator) parameterSignatureTypeList

Finally, a flattened interface is a set of flattened method signatures.

An interface has a method name m if the interface has a method (including getters, setters, and operators) named m.

The flattened interface F of an interface I consists of the method signatures for the instance methods (including getters, setters, and operators, as always) declared by I, as well as one method signature for each method name m which at least one of the direct superinterfaces of C has, unless a method named m is also declared by C. The details of this method signature are specified in the following; at this point we have just chosen the name: m.

It is a compile-time error if multiple direct superinterfaces of I have a method named m and at least one of them is a getter and at least one of them is a non-getter method. It is a compile-time error if a direct superinterface of I has a method declaration D named m, and I declares a method named m, and the latter is not a correct override of D (TODO: specify 'correct override' relation, or check that the given one in the spec is OK.).

Otherwise (when there are none of these errors), let D₁..D_k be the top type erasure of the declarations of m that the direct superinterfaces of I have.

The erasure ensures that the class interface ignores the distinction between Object, dynamic, and void when specified as type annotations in contravariant positions, which primarily means the types of formal parameters. For such parameters, it is only relevant to the body of a method implementation whether a given formal parameter has type dynamic, void, or Object, it makes no difference for a caller. That information is eliminated when we compute a class interface, which reduces the need for developers to resolve ambiguities (by means of an explicit declaration which makes the choice).

If D₁..D_k are all getters and their return types are such that T is one of them and it is a subtype of them all, the method signature in F named m is T get m.

In the case where this set Q of return types contains only top types (which are all subtypes of each other) we disambiguate as follows:

• If Q is a singleton set, the sole element of Q is chosen.
• If Q is {dynamic, Object}, Object is chosen.
• If Q is {T, void} where T is Object or dynamic, T is chosen.
• If Q is {dynamic, Object, void}, Object is chosen.

The rationale is that we choose void only when no other top type is present, which matches the intuition about being more specific because a method with a void return type can be overridden by a method with some other return type, including other top types, but not vice versa. We choose dynamic only when all available method signatures agree on dynamic (possibly ignoring some having void, because they are less specific), such that the lack of type checking is never implicitly imposed on an "unsuspecting" supertype. Otherwise, Object is chosen.

Otherwise (when D₁..D_k are all getters, and none of the return types is most specific) a compile-time error occurs.

Otherwise (when D₁..D_k are all non-getter methods) if no formal parameter in D₁..D_k is covariant: If, for some j in 1..k, D_j is a correct override of each of D₁..D_k, then the method signature in F named m is D_j. If D_j has any occurrences of Object in a covariant position, it is disambiguated using the same rules as for the return type of a getter.

Otherwise (when D₁..D_k are all non-getter methods, and at least one formal parameter is covariant): If, for some j in 1..k, D_j is a correct override for each of D₁..D_k, then the method signature in F named m is D_j, except that the signature type of each formal parameter f is replaced by covariant { T₁, ..., T_n }, where T₁, ..., T_n is the set of all type annotations of that parameter in all superinterfaces of I, direct as well as indirect. If D_j has any occurrences of Object in a covariant position, it is disambiguated using the same rules as for the return type of a getter.

Otherwise (when D₁..D_k are all non-getter methods, and none of the declarations is a correct override of them all) a compile-time error occurs.

Note that we may conveniently compute the flattened interface of the implicit interface of a class C based on the flattened interfaces of its direct superinterfaces.

Discussion

The disambiguation of top types does not match the treatment which would be implied by an enhancement of the subtyping structure with rules like dynamic < Object < void (no matter which order we choose). Assume that we would consider dynamic to be more specific than Object. We would then have the following situation:

abstract class A { Object foo(); }
abstract class B { foo(); }
abstract class C implements A, /* and, lots, of, others, */ B {}

main() {
  C c = ...;
  c.foo().bar(42); // OK!
}

The invocation of bar is OK because c.foo() has type dynamic, and this type was introduced by implementing B, which might not be noticed by developers who know about Object foo() in A.

When the flattened interface of an interface I has been computed, it directly indicates for each parameter of each method whether it is covariant. Assume that a method foo takes one parameter f, which is covariant. From its signature type, we can extend the notion of being assignable to a concept which is relevant for a covariant parameter. Here is a variant of an example that came up in issue #31596:

class A {}
class I0 {}
class B extends A implements I0 {}
class BB implements B {}
abstract class C {
  void f(B x, B y) {}
  // Or like this, which makes no difference
  // for the static checks:
  //   void f(B x, B y);
}
abstract class I {
  void f(covariant A x, B y);
}
class D extends C implements I {}

main() {
  C c = new D();
  c.f(new B(), new B()); // Lots of interesting variants here.
}

The flattened interface of C has void f(covariant {A, B}, B) for f, which reflects the fact that the dynamically invoked f must be declared in a subtype of C, which means that it must specify a type annotation for the first parameter which is a subtype or a supertype of A, and same for B (it's enough to be a supertype of A, including A itself, or a subtype of B, including B itself, but we will not be able to simplify all situations that much).

Now we simply use the existing assignability criterion on all the types in each covariant set. For example:

The first argument to c.f(_, _), being covariant { A, B }, is considered type correct (1) if it is a supertype or a subtype of each type in the covariant set. Or (2) let S be the covariant set of types (here: {A, B}), and let S_min be the subset of S where each member T is such that no other element in S is a proper subtype of T (that is, the minimal members of S), and then the argument is type correct if it is a subtype or a supertype of every element in S_min.

In particular, a String is rejected (it is unrelated to at least one of the types in the set, actually both); I0 is prohibited with approach (1) (it is unrelated to A) and allowed in approach (2) (which is more like the approach today: we just take the most specific type into account, which is usually the one we have in the class interface); but Object is OK (downcast), A is OK (match for A, downcast for B), B is OK (upcast for A, match for B), and BB is OK (upcast for both A and B).

In short, we will handle assignability for covariant parameters simply by taking all the "known types of the parameter" into account, and check each of them as we have always done it; and that will give us an analysis which is as tight as it can be, based on interfaces alone.