sdk/docs/language/informal/subtyping.md

Dart 2.0 Static and Runtime Subtyping

leafp@google.com

Status: Implemented.

This is intended to define the core of the Dart 2.0 static and runtime subtyping relation.

Types

The syntactic set of types used in this draft are a slight simplification of full Dart types.

The meta-variables X, Y, and Z range over type variables.

The meta-variables T, S, U, and V range over types.

The meta-variable C ranges over classes.

The meta-variable B ranges over types used as bounds for type variables.

As a general rule, indices up to k are used for type parameters and type arguments, n for required value parameters, and m for all value parameters.

The set of types under consideration are as follows:

• Type variables X
• Promoted type variables X & T Note: static only
• Object
• dynamic
• void
• Null
• Function
• Future<T>
• FutureOr<T>
• Interface types C, C<T0, ..., Tk>
• Function types
  • U Function<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])
  • U Function<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})

We leave the set of interface types unspecified, but assume a class hierarchy which provides a mapping from interfaces types T to the set of direct super-interfaces of T induced by the superclass declaration, implemented interfaces, and mixins of the class of T. Among other well-formedness constraints, the edges induced by this mapping must form a directed acyclic graph rooted at Object.

The types Object, dynamic and void are all 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).

The type X & T represents the result of a type promotion operation on a variable. In certain circumstances (defined elsewhere) a variable x of type X that is tested against the type T (e.g. x is T) will have its type replaced with the more specific type X & T, indicating that while it is known to have type X, it is also known to have the more specific type T. Promoted type variables only occur statically (never at runtime).

Given the current promotion semantics the following properties are also true:

• If X has bound B then for any type X & T, T <: B will be true.
• Promoted type variable types will only appear as top level types: that is, they can never appear as sub-components of other types, in bounds, or as part of other promoted type variables.

Notation

We use S[T0/Y0, ..., Tk/Yk] for the result of performing a simultaneous capture-avoiding substitution of types T0, ..., Tk for the type variables Y0, ..., Yk in the type S.

Type equality

We say that a type T0 is equal to another type T1 (written T0 === T1) if the two types are structurally equal up to renaming of bound type variables, and equating all top types.

TODO: make these rules explicit.

Algorithmic subtyping

By convention the following rules are intended to be applied in top down order, with exactly one rule syntactically applying. That is, rules are written in the form:

Syntactic criteria.
  - Additional condition 1
  - Additional or alternative condition 2

and it is the case that if a subtyping query matches the syntactic criteria for a rule (but not the syntactic criteria for any rule preceeding it), then the subtyping query holds iff the listed additional conditions hold.

This makes the rules algorithmic, because they correspond in an obvious manner to an algorithm with an acceptable time complexity, and it makes them syntax directed because the overall structure of the algorithm corresponds to specific syntactic shapes. We will use the word algorithmic to refer to this property.

The runtime subtyping rules can be derived by eliminating all clauses dealing with promoted type variables.

Rules

We say that a type T0 is a subtype of a type T1 (written T0 <: T1) when:

• Reflexivity: T0 and T1 are the same type.

  • Note that this check is necessary as the base case for primitive types, and type variables but not for composite types. In particular, algorithmically a structural equality check is admissible, but not required here. Pragmatically, non-constant time identity checks here are counter-productive

• Right Top: T1 is a top type (i.e. Object, dynamic, or void).

• Left Bottom: T0 is Null

• Left FutureOr: T0 is FutureOr<S0>

  • and Future<S0> <: T1
  • and S0 <: T1

• Type Variable Reflexivity 1: T0 is a type variable X0 or a promoted type variables X0 & S0 and T1 is X0.

  • Note that this rule is admissible, and can be safely elided if desired

• Type Variable Reflexivity 2: PromotedT0 is a type variable X0 or a promoted type variables X0 & S0 and T1 is X0 & S1

  • and T0 <: S1.
  • Note that this rule is admissible, and can be safely elided if desired

• Right Promoted Variable: T1 is a promoted type variable X1 & S1

  • and T0 <: X1
  • and T0 <: S1

• Right FutureOr: T1 is FutureOr<S1> and

  • either T0 <: Future<S1>
  • or T0 <: S1
  • or T0 is X0 and X0 has bound S0 and S0 <: T1
  • or T0 is X0 & S0 and S0 <: T1

• Left Promoted Variable: T0 is a promoted type variable X0 & S0

  • and S0 <: T1

• Left Type Variable Bound: T0 is a type variable X0 with bound B0

  • and B0 <: T1

• Function Type/Function: T0 is a function type and T1 is Function

• Interface Compositionality: T0 is an interface type C0<S0, ..., Sk> and T1 is C0<U0, ..., Uk>

  • and each Si <: Ui

• Super-Interface: T0 is an interface type with super-interfaces S0,...Sn

  • and Si <: T1 for some i

• Positional Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn, [Vn+1 xn+1, ..., Vm xm])

  • and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sp yp, [Sp+1 yp+1, ..., Sq yq])
  • and p >= n
  • and m >= q
  • and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...q
  • and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
  • and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
  • where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]

• Named Function Types: T0 is U0 Function<X0 extends B00, ..., Xk extends B0k>(V0 x0, ..., Vn xn, {Vn+1 xn+1, ..., Vm xm})

  • and T1 is U1 Function<Y0 extends B10, ..., Yk extends B1k>(S0 y0, ..., Sn yn, {Sn+1 yn+1, ..., Sq yq})
  • and {yn+1, ... , yq} subsetof {xn+1, ... , xm}
  • and Si[Z0/Y0, ..., Zk/Yk] <: Vi[Z0/X0, ..., Zk/Xk] for i in 0...n
  • and Si[Z0/Y0, ..., Zk/Yk] <: Tj[Z0/X0, ..., Zk/Xk] for i in n+1...q, yj = xi
  • and U0[Z0/X0, ..., Zk/Xk] <: U1[Z0/Y0, ..., Zk/Yk]
  • and B0i[Z0/X0, ..., Zk/Xk] === B1i[Z0/Y0, ..., Zk/Yk] for i in 0...k
  • where the Zi are fresh type variables with bounds B0i[Z0/X0, ..., Zk/Xk]

Note: the requirement that Zi are fresh is as usual strictly a requirement that the choice of common variable names avoid capture. It is valid to choose the Xi or the Yi for Zi so long as capture is avoided

Derivation of algorithmic rules

This section sketches out the derivation of the algorithmic rules from the interpretation of FutureOr as a union type, and promoted type bounds as intersection types, based on standard rules for such types that do not satisfy the requirements for being algorithmic.

Non-algorithmic rules

The non-algorithmic rules that we derive from first principles of union and intersection types are as follows:

Left union introduction:

• FutureOr<S> <: T if Future<S> <: T and S <: T

Right union introduction:

• S <: FutureOr<T> if S <: Future<T> or S <: T

Left intersection introduction:

• X & S <: T if X <: T or S <: T

Right intersection introduction:

• S <: X & T if S <: X and S <: T

The only remaining non-algorithmic rule is the variable bounds rule:

Variable bounds:

• X <: T if X extends B and B <: T

All other rules are algorithmic.

Note: We believe that bounds can be treated simply as uses of intersections, which could simplify this presentation.

Preliminaries

Lemma 1: If there is any derivation of FutureOr<S> <: T, then there is a derivation ending in a use of left union introduction.

Proof. By induction on derivations. Consider a derivation of FutureOr<S> <: T.

If the last rule applied is:

• Top type rules are trivial.

• Null, Function and interface rules can't apply.

• Left union introduction rule is immediate.

• Right union introduction. Then T is of the form FutureOr<T0>, and either

  • we have a sub-derivation of FutureOr<S> <: Future<T0>
    • by induction we therefore have a derivation ending in left union introduction, so by inversion we have:
      • a derivation of Future<S> <: Future<T0> , and so by right union introduction we have Future<S> <: FutureOr<T0>
      • a derivation of S <: Future<T0> , and so by right union introduction we have S <: FutureOr<T0>
    • by left union introduction, we have FutureOr<S> <: FutureOr<T0>
    • QED
  • we have a sub-derivation of FutureOr<S> <: T0
    • by induction we therefore have a derivation ending in left union introduction, so by inversion we have:
      • a derivation of Future<S> <: T0 , and so by right union introduction we have Future<S> <: FutureOr<T0>
      • a derivation of S <: T0 , and so by right union introduction we have S <: FutureOr<T0>
    • by left union introduction, we have FutureOr<S> <: FutureOr<T0>
    • QED

• Right intersection introduction. Then T is of the form X & T0, and

  • we have sub-derivations FutureOr<S> <: X and FutureOr<S> <: T0
  • By induction, we can get derivations of the above ending in left union introduction, so by inversion we have derivations of:
    • Future<S> <: X, S <: X, Future<S> <: T0, S <: T0
      • so we have derivations of S <: X, S <: T0, so by right intersection introduction we have
        • S <: X & T0
      • so we have derivations of Future<S> <: X, Future<S> <: T0, so by right intersection introduction we have
        • Future<S> <: X & T0
  • so by left union introduction, we have a derivation of FutureOr<S> <: X & T0
  • QED

Note: The reverse is not true. Counter-example:

Given arbitrary B <: A, suppose we wish to show that (X extends FutureOr<B>) <: FutureOr<A>. If we apply right union introduction first, we must show either:

• X <: Future<A>
• only variable bounds rule applies, so we must show
  • FutureOr<B> <: Future<A>
  • Only left union introduction applies, so we must show both of:
    • Future<B> <: Future<A> (yes)
    • B <: Future<A> (no)
• X <: A
• only variable bounds rule applies, so we must show that
  • FutureOr<B> <: A
  • Only left union introduction applies, so we must show both of:
    • Future<B> <: Future<A> (no)
    • B <: Future<A> (yes)

On the other hand, the derivation via first applying the variable bounds rule is trivial.

Note though that we can also not simply always apply the variable bounds rule first. Counter-example:

Given X extends Object, it is trivial to derive X <: FutureOr<X> via the right union introduction rule. But applying the variable bounds rule doesn't work.

Lemma 2: If there is any derivation of S <: X & T, then there is derivation ending in a use of right intersection introduction.

Proof. By induction on derivations. Consider a derivation D of S <: X & T.

If last rule applied in D is:

• Bottom types are trivial.

• Function and interface type rules can't apply.

• Right intersection introduction then we're done.

• Left intersection introduction. Then S is of the form Y & S0, and either

  • we have a sub-derivation of Y <: X & T
    • by induction we therefore have a derivation ending in right intersection introduction, so by inversion we have:
      • a derivation of Y <: X , and so by left intersection introduction we have Y & S0 <: X
      • a derivation of Y <: T , and so by left intersection introduction we have Y & S0 <: T
    • by right intersection introduction, we have Y & S0 <: X & T
    • QED
  • we have a sub-derivation of S0 <: X & T
    • by induction we therefore have a derivation ending in right intersection introduction, so by inversion we have:
      • a derivation of S0 <: X , and so by left intersection introduction we have Y & S0 <: X
      • a derivation of S0 <: T , and so by left intersection introduction we have Y & S0 <: T
  • by right intersection introduction, we have Y & S0 <: X & T
  • QED

• Left union introduction. Then S is of the form FutureOr<S0>, and

  • we have sub-derivations Future<S0> <: X & T and S0 <: X & T
  • By induction, we can get derivations of the above ending in right intersection introduction, so by inversion we have derivations of:
    • Future<S0> <: X, S0 <: X, Future<S0> <: T, S0 <: T
      • so we have derivations of S0 <: X, Future<S0> <: X, so by left union introduction we have
        • FutureOr<S0> <: X
      • so we have derivations of S0 <: T, Future<S0> <: T, so by left union introduction we have
        • FutureOr<S0> <: T
  • so by right intersection introduction, we have a derivation of FutureOr<S0> <: X & T
  • QED

Conjecture 1: FutureOr<A> <: FutureOr<B> is derivable iff A <: B is derivable.

Showing that A <: B => FutureOr<A> <: FutureOr<B> is easy, but it is not immediately clear how to tackle the opposite direction.

Lemma 3: Transitivity of subtyping is admissible. Given derivations of A <: B and B <: C, there is a derivation of A <: C.

Proof sketch: The proof should go through by induction on sizes of derivations, cases on pairs of rules used. For any pair of rules used, we can construct a new derivation of the desired result using only smaller derivations.

Observation 1: Given X with bound S, we have the property that for all instances of X & T, T <: S will be true, and hence S <: M => T <: M.

Algorithmic rules

Consider T0 <: T1.

Union on the left

By lemma 1, if T0 is of the form FutureOr<S0> and there is any derivation of T0 <: T1, then there is a derivation ending with a use of left union introduction so we have the rule:

• T0 is FutureOr<S0>
  • and Future<S0> <: T1
  • and S0 <: T1

Identical type variables

If T0 and T1 are both the same unpromoted type variable, then subtyping holds by reflexivity. If T0 is a promoted type variable X0 & S0, and T0 is X0 then it suffices to show that X0 <: X0 or S0 <: X0, and the former holds immediately. This justifies the rule:

• T0 is a type variable X0 or a promoted type variables X0 & S0 and T1 is X0.

If T0 is X0 or X0 & S0 and T1 is X0 & S1, then by lemma 1 it suffices to show that X0 & S0 <: X0 and X0 & S0 <: S1. The first holds immediately by reflexivity on the type variable, so it is sufficient to check T0 <: S1.

• T0 is a type variable X0 or a promoted type variables X0 & S0 and T1 is X0 & S1
  • and T0 <: S1.

Note that neither of the previous rules are required to make the rules algorithmic: they are merely useful special cases of the next rule.

Intersection on the right

By lemma 2, if T1 is of the X1 & S1 and there is any derivation of T0 <: T1, then there is a derivation ending with a use of right intersection introduction, hence the rule:

• T1 is a promoted type variable X1 & S1
  • and T0 <: X1
  • and T0 <: S1

Union on the right

Suppose T1 is FutureOr<S1>. The rules above have eliminated the possibility that T0 is of the form FutureOr<S0. The only rules that could possibly apply then are right union introduction, left intersection introduction, or the variable bounds rules. Combining these yields the following preliminary disjunctive rule:

• T1 is FutureOr<S1> and
  • either T0 <: Future<S1>
  • or T0 <: S1
  • or T0 is X0 and X0 has bound S0 and S0 <: T1
  • or T0 is X0 & S0 and X0 <: T1 and S0 <: T1

The last disjunctive clause can be further simplified to

• or T0 is X0 & S0 and S0 <: T1

since the premise X0 <: FutureOr<S1> can only derived either using the variable bounds rule or right union introduction. For the variable bounds rule, the premise B0 <: T1 is redundant with S0 <: T1 by observation 1. For right union introduction, X0 <: S1 is redundant with T0 <: S1, since if X0 <: S1 is derivable, then T0 <: S1 is derivable by left union introduction; and X0 <: Future<S1> is redundant with T0 <: Future<S1>, since if the former is derivable, then the latter is also derivable by left intersection introduction. So we have the final rule:

• T1 is FutureOr<S1> and
  • either T0 <: Future<S1>
  • or T0 <: S1
  • or T0 is X0 and X0 has bound S0 and S0 <: T1
  • or T0 is X0 & S0 and S0 <: T1

Intersection on the left

Suppose T0 is X0 & S0. We've eliminated the possibility that T1 is FutureOr<S1>, the possibility that T1 is X1 & S1, and the possibility that T1 is any variant of X0. The only remaining rule that applies is left intersection introduction, and so it suffices to check that X0 <: T1 and S0 <: T1. But given the remaining possible forms for T1, the only rule that can apply to X0 <: T1 is the variable bounds rule, which by observation 1 is redundant with the second premise, and so we have the rule:

T0 is a promoted type variable X0 & S0

• and S0 <: T1

Type variable on the left

Suppose T0 is X0. We've eliminated the possibility that T1 is FutureOr<S1>, the possibility that T1 is X1 & S1, and the possibility that T1 is any variant of X0. The only rule that applies is the variable bounds rule:

T0 is a type variable X0 with bound B0

• and B0 <: T1

This eliminates all of the non-algorithmic rules: the remainder are strictly algorithmic.