diff --git a/docs/language/informal/subtyping.md b/docs/language/informal/subtyping.md deleted file mode 100644 index 65df0ea9996..00000000000 --- a/docs/language/informal/subtyping.md +++ /dev/null @@ -1,474 +0,0 @@ -# Dart 2.0 Static and Runtime Subtyping - -leafp@google.com - -**Status**: This document is now background material. -For normative text, please consult the language specification. - -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` -- `FutureOr` -- Interface types `C`, `C` -- Function types - - `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])` - - `U Function(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` - - and `Future <: 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**: Promoted`T0` 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` and - - either `T0 <: Future` - - 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` - and `T1` is `C0` - - 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(V0 x0, ..., Vn xn, [Vn+1 xn+1, ..., Vm xm])` - - and `T1` is - `U1 Function(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(V0 x0, ..., Vn xn, {Vn+1 xn+1, ..., Vm xm})` - - and `T1` is - `U1 Function(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 <: T` if `Future <: T` and `S <: T` - -Right union introduction: - - `S <: FutureOr` if `S <: Future` 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 <: T`, then there is a -derivation ending in a use of left union introduction. - -Proof. By induction on derivations. Consider a derivation of `FutureOr <: -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`, and either - - we have a sub-derivation of `FutureOr <: Future` - - by induction we therefore have a derivation ending in left union - introduction, so by inversion we have: - - a derivation of `Future <: Future `, and so by right union - introduction we have `Future <: FutureOr` - - a derivation of `S <: Future `, and so by right union - introduction we have `S <: FutureOr` - - by left union introduction, we have `FutureOr <: FutureOr` - - QED - - we have a sub-derivation of `FutureOr <: T0` - - by induction we therefore have a derivation ending in left union - introduction, so by inversion we have: - - a derivation of `Future <: T0 `, and so by right union - introduction we have `Future <: FutureOr` - - a derivation of `S <: T0 `, and so by right union - introduction we have `S <: FutureOr` - - by left union introduction, we have `FutureOr <: FutureOr` - - QED - - - Right intersection introduction. Then `T` is of the form `X & T0`, and - - we have sub-derivations `FutureOr <: X` and `FutureOr <: T0` - - By induction, we can get derivations of the above ending in left union - introduction, so by inversion we have derivations of: - - `Future <: X`, `S <: X`, `Future <: 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 <: X`, `Future <: T0`, so by right - intersection introduction we have - - `Future <: X & T0` - - so by left union introduction, we have a derivation of `FutureOr <: X & T0` - - QED - -Note: The reverse is not true. Counter-example: - -Given arbitrary `B <: A`, suppose we wish to show that `(X extends FutureOr) -<: FutureOr`. If we apply right union introduction first, we must show -either: - - `X <: Future` - - only variable bounds rule applies, so we must show - - `FutureOr <: Future` - - Only left union introduction applies, so we must show both of: - - `Future <: Future` (yes) - - `B <: Future` (no) - - `X <: A` - - only variable bounds rule applies, so we must show that - - `FutureOr <: A` - - Only left union introduction applies, so we must show both of: - - `Future <: Future` (no) - - `B <: Future` (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` 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`, and - - we have sub-derivations `Future <: 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 <: X`, `S0 <: X`, `Future <: T`, `S0 <: T` - - so we have derivations of `S0 <: X`, `Future <: X`, so by left - union introduction we have - - `FutureOr <: X` - - so we have derivations of `S0 <: T`, `Future <: T`, so by left - union introduction we have - - `FutureOr <: T` - - so by right intersection introduction, we have a derivation of `FutureOr <: X & T` - - QED - -**Conjecture 1**: `FutureOr <: FutureOr` is derivable iff `A <: B` is -derivable. - -Showing that `A <: B => FutureOr <: FutureOr` 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` 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` - - and `Future <: 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`. The rules above have eliminated the possibility -that `T0` is of the form `FutureOr` and - - either `T0 <: Future` - - 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` 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` is redundant with `T0 <: Future`, 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` and - - either `T0 <: Future` - - 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`, 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`, 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.