sdk/docs/language/informal/instantiate-to-bound.md

Feature: Instantiate to Bound

Author: eernst@

Version: 0.8 (2018-09-26)

Status: Implemented.

Based on this description by leafp@.

This document is an informal specification of the the instantiate to bound mechanism in Dart 2. The feature described here, instantiate to bound, makes it possible to omit some or all actual type arguments in some types using generic classes. The missing type arguments will be added implicitly, and the chosen value for a given type argument will be the bound on the corresponding formal type parameter. In some situations no such bound can be expressed, in which case a compile-time error occurs. To resolve that, the type arguments can be given explicitly.

Background

In Dart 1.x, missing actual type arguments were filled in with the value dynamic, which was always a useful choice because that would yield types which were at the bottom of the set of similar types, as well as at the top.

List xs = <int>[]; // OK, also dynamically: List<int> <: List<dynamic>.
List<int> y = new List(); // OK, also dynamically: List<dynamic> <: List<int>.

In Dart 2, type inference is used in many situations to infer missing type arguments, hence selecting values that will work in the given context. However, when the context does not provide any information to this inference process, some default choice must be made.

In Dart 2, dynamic is no longer a super- and subtype of all other types, and hence using dynamic as the default value for a missing actual type argument will create many malformed types:

class A<X extends num> {}
A a = null; // A is malformed if interpreted as A<dynamic>.

Hence, a new rule for finding default actual type arguments must be specified.

Motivation

It is convenient for developers to be able to use a more concise notation for some types, and instantiate to bound will enable this.

We will use a relatively simple mechanism which is allowed to fail. This means that developers will have to write actual type arguments explicitly in some ambiguous situations, thus adding visual complexity to the source code and requiring extra time and effort to choose and write those arguments. However, we consider the ability to reason straightforwardly about generic types in general more important than (possibly misleading) conciseness.

The performance characteristics of the chosen algorithm plays a role as well, because it is important to be able to find default type arguments in a short amount of time. Because of that, we have chosen to require explicit type arguments on bounds except for some "simple" cases. Again, this means that the source code will be somewhat more verbose, in return for overall simplicity.

Here are some examples:

class A<T extends int> {}

// The raw type A is completed to A<int>.
A x;

// T of A has a simple bound, so A can be a bound and is completed to A<int>.
class B<T extends A> {}

class C<T extends int, S extends A<T>> {}

// The raw type C is completed to C<int, A<int>>.
C x;

class D<T extends Comparable<T>> {}

// The raw type D is completed to D<Comparable<dynamic>>.
D x;

// Error: T of D does not have a simple bound, so raw D cannot be a bound.
class E<T extends D> {}

Syntax

This mechanism does not require any grammar modifications.

Static analysis

We will define simple bounds, but at first we need an auxiliary concept. Let T be a type of the form typeName. A type S then contains T if one of the following conditions hold:

• S is of the form typeName, and S is T.
• S is of the form typeName typeArguments, and one of the type arguments contains T.
• S is of the form typeName typeArguments? where typeName denotes a type alias F, and the body of F contains T.
• S is of the form returnType? 'Function' typeParameters? parameterTypeList and returnType? contains T, or a bound in typeParameters? contains T, or the type of a parameter in parameterTypeList contains T.

Multiple cases may be applicable, e.g., when a type alias is applied to a list of actual type arguments, and the type alias body as well as some type arguments may contain T.

In the rule about type aliases, F may or may not be parameterized, and it may or may not receive type arguments. However, there is no need to consider the result of substituting actual type arguments for formal type parameters in the body of the type alias, because we only need to inspect all types of the form typeName contained in its body, and they are not affected by such a substitution.

It is understood that name capture is avoided, that is, a type S does not contain p.C even if S contains F which denotes a type alias whose body contains the syntax p.C, say, as a return type, if p has different meanings in S and in the body of F. This could occur because S and F are declared in different libraries. Similarly, when a type parameter bound B contains a type variable X from the enclosing class, it is never because X is contained in the body of a type alias, it will always be as a syntactic subterm of B.

Let G be a generic class or parameterized type alias with k formal type parameter declarations containing formal type parameters X₁ .. X_k and bounds B₁ .. B_k. We say that the formal type parameter X_j has a simple bound when one of the following requirements is satisfied:

1. B_j is omitted.

2. B_j is included, but does not contain any of X₁ .. X_k. If B_j contains a type T of the form typeName (for instance, C or p.D) which denotes a generic class or parameterized type alias G₁ (that is, T is a raw type), every type argument of G₁ has a simple bound.

The notion of a simple bound must be interpreted inductively rather than coinductively, i.e., if a bound B_j of a generic class or parameterized type alias G is reached during an investigation of whether B_j is a simple bound, the answer is no.

For example, with class C<X extends C> {} the type parameter X does not have a simple bound: A raw C is used as a bound for X, so C must have simple bounds, but one of the bounds of C is the bound of X, and that bound is C, so C must have simple bounds: Cycle, hence error!

We can now specify in which sense instantiate to bound requires the involved types to be "simple enough". We impose the following constraint on all bounds because any generic type may be used as a raw type.

It is a compile-time error if a formal parameter bound B contains a type T on the form typeName and T denotes a generic class or parameterized type alias G (that is, T is a raw type), unless every formal type parameter of G has a simple bound.

In short, type arguments on bounds can only be omitted if they themselves have simple bounds. In particular, class C<X extends C> {} is a compile-time error because the bound C is raw, and the formal type parameter X that corresponds to the omitted type argument does not have a simple bound.

When a type annotation T on the form typeName denotes a generic class or parameterized type alias (so T is raw), instantiate to bound is used to provide the missing type argument list. It is a compile-time error if the instantiate to bound process fails.

Other mechanisms may be considered for this situation, e.g., inference could be used to select a possible type annotation, and type arguments could then be transferred from the inferred type annotation to the given incomplete type annotation. For instance, Iterable could be specified explicitly for a variable, List<int> could be inferred from its initializing expression, and the partially inferred type annotation would then be Iterable<int>. However, even if such a mechanism is introduced, it will not make the instantiate to bound feature obsolete: instatiate to bound would still be used in cases where no information is available to infer the omitted type arguments, e.g., for List xs = [];.

When type inference is providing actual type arguments for a term G on the form typeName which denotes a generic class or a parameterized type alias, instantiate to bound may be used to provide the value for type arguments where no information is available for inferring such an actual type argument. This document does not specify how inference interacts with instantiate to bound, that will be specified as part of the specification of inference. We will hence proceed to specify instantiate to bound as it applies to a type argument list which is omitted, such that a value for all the actual type arguments must be computed.

Let T be a typeName term which denotes a generic class or parameterized type alias G (so T is a raw type), let F₁ .. F_k be the formal type parameter declarations in the declaration of G, with type parameters X₁ .. X_k and bounds B₁ .. B_k with types T₁ .. T_k. For i in 1 .. k, let S_i denote the result of performing instantiate to bound on the type in the bound, T_i; in the case where B_i is omitted, let S_i be dynamic.

Note that if T_i for some i is raw then we know that all its omitted type arguments have simple bounds, which limits the complexity of the instantiate to bound step for T_i.

Instantiate to bound then computes an actual type argument list for G as follows:

Let U_i,1 be S_i, for all i in 1 .. k. (This is the "current value" of the bound for type variable i, at step 1; in general we will consider the current step, m, and use data for that step, e.g., the bound U_i,m, to compute the data for step m + 1).

Let -->_m be a relation among the type variables X₁ .. X_k such that X_p -->_m X_q iff X_q occurs in U_p,m (so each type variable is related to, that is, depends on, every type variable in its bound, possibly including itself). Let ==>_m be the transitive closure of -->_m. For each m, let U_i,m+1, for i in 1 .. k, be determined by the following iterative process:

1. If there exists a j in 1 .. k such that X_j ==>_m X_j (that is, if the dependency graph has a cycle) let M₁ .. M_p be the strongly connected components (SCCs) with respect to -->_m (that is, the maximal subsets of X₁ .. X_k where every pair of variables in each subset are related in both directions by ==>_m; note that the SCCs are pairwise disjoint; also, they are uniquely defined up to reordering, and the order does not matter). Let M be the union of M₁ .. M_p (that is, all variables that participate in a dependency cycle). Let i be in 1 .. k. If X_i does not belong to M then U_i,m+1 = U_i,m. Otherwise there exists a q such that X_i belongs to M_q; U_i,m+1 is then obtained from U_i,m by replacing every covariant occurrence of a variable in M_q by dynamic, and replacing every contravariant occurence of a variable in M_q by Null.

2. Otherwise, (if no dependency cycle exists) let j be the lowest number such that X_j occurs in U_p,m for some p and X_j -/->_m X_q for all q in 1..k (that is, U_j,m is closed, that is, the current bound of X_j does not contain any type variables; but X_j is being depended on by the bound of some other type variable). Then, for all i in 1 .. k, U_i,m+1 is obtained from U_i,m by replacing every covariant occurrence of X_j by U_j,m, and replacing every contravariant occurrence of X_j by Null.

3. Otherwise, (when no dependencies exist) terminate with the result <U_1,m ..., U_k,m>.

This process will always terminate, because the total number of occurrences of type variables from {X₁ .. X_k} in the current bounds is strictly decreasing with each step, and we terminate when that number reaches zero.

Note that this process may produce a super-bounded type.

When instantiate to bound is applied to a type it proceeds recursively: For a generic instantiation G<T₁ .. T_k> it is applied to T₁ .. T_k; for a function type T₀ Function(T₁ .. T_j, {T_j+1 x₁ .. T_k x_j+k}) and a function type T₀ Function(T₁ .. T_j, [T_j+1 .. T_j+k]) it is applied to T₀ .. T_j+k.

This means that instantiate to bound has no effect on a type that does not contain any raw types; conversely, instantiate to bound will act on types which are syntactic subterms, no matter where they occur.

Dynamic semantics

The instantiate to bound transformation which is specified in the static analysis section is used to provide type arguments to dynamic invocations of generic functions, when no actual type arguments are passed. Otherwise, the semantics of a given program P is the semantics of the program P' which is created from P by applying instantiate to bound where applicable.

Updates

• Sep 26th 2018, version 0.8: Fixed unintended omission: the same rules that we specified for a generic class are now also specified to hold for parameterized type aliases.

• Feb 26th 2018, version 0.7: Revised cycle breaking algorithm for F-bounded type variables to avoid specifying orderings that do not matter.

• Feb 22nd 2018, version 0.6: Revised cycle breaking algorithm for F-bounded type variables to replace all members by an extreme type, not just one of them.

• Jan 11th 2018, version 0.5: Revised treatment of variance based on strongly connected components in the dependency graph.

• Dec 13th 2017: Revised to allow infinite substitution sequences when the value of a type argument is computed, specifying how to detect that the substitution sequence is infinite, and how to obtain a result from there.

• Sep 15th 2017: Transferred to the SDK repository as instantiate-to-bound.md.

• Sep 15th 2017: Adjusted to include the enhanced expressive power described in SDK issue #28580.

• Sep 14th 2017: Created this informal specification, based on this description by leafp@.