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.
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.
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.
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 D1..Dk 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 D1..Dk 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},Objectis chosen. - If Q is
{T, void}whereTisObjectordynamic,Tis chosen. - If Q is
{dynamic, Object, void},Objectis 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 D1..Dk are all getters, and none of the return types is most specific) a compile-time error occurs.
Otherwise (when D1..Dk are all non-getter
methods) if no formal parameter in D1..Dk is
covariant: If, for some j in 1..k, Dj is a correct
override of each of D1..Dk, then the method
signature in F named m is Dj. If Dj
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 D1..Dk are all non-getter
methods, and at least one formal parameter is covariant): If, for
some j in 1..k, Dj is a correct override for each
of D1..Dk, then the method signature in F
named m is Dj, except that the signature type of each
formal parameter f is replaced by
covariant { T1, ..., Tn }, where
T1, ..., Tn is the set of all type annotations
of that parameter in all superinterfaces of I, direct as well as
indirect. If Dj 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 D1..Dk 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.
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 Smin 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 Smin.
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.