diff --git a/accepted/future-releases/records/records-feature-specification.md b/accepted/future-releases/records/records-feature-specification.md index 189258ba40..d7df684cb0 100644 --- a/accepted/future-releases/records/records-feature-specification.md +++ b/accepted/future-releases/records/records-feature-specification.md @@ -297,6 +297,11 @@ class extends Record { ### Subtyping +Subtyping for record types has been incorporated into the main subtyping +specification +[here](https://github.com/dart-lang/language/blob/master/resources/type-system/subtyping.md). +Briefly: + The class `Record` is a subtype of `Object` and `dynamic` and a supertype of `Never`. All record types are subtypes of `Record`, and supertypes of `Never`. @@ -308,6 +313,11 @@ no "row polymorphism" or "width subtyping".* ### Upper and lower bounds +Bounds computations for record types have been incorporated into the main +specification +[here](https://github.com/dart-lang/language/blob/master/resources/type-system/upper-lower-bounds.md). +Briefly: + If two record types have the same shape, their least upper bound is a new record type of the same shape where each field's type is the least upper bound of the corresponding field in the original types. @@ -337,13 +347,86 @@ var c = cond ? a : b; // c has type `Record`. The greatest lower bound of records with different shapes is `Never`. -### Type inference and promotion +### Type inference + +Every record literal has a static type, which is associated with it via +inference (there is no syntax for explicitly associating a specific static type +with a record literal). As with other constructs, we define type inference for +record expressions with respect to a context type schema which is determined by +the surrounding context of the inferred expression. Unlike nominal classes (but +like function literals) we choose to infer the most specific possible type for +record literals, even if that type is more precise than the type specified by +the context type schema. This choice (as with function literals) reflects the +fact that record types (like function types in Dart) are soundly variant: that +is, the subtyping is properly covariant and requires no runtime checking. + +For convenience, we generally write function types with all named parameters in +an unspecified canonical order, and similarly for the named fields of record +types. In all cases unless otherwise specifically called out, order of named +parameters and fields is semantically irrelevant: any two types with the same +named parameters (named fields, respectively) are considered the same type. + +Similarly, function and method invocations with named arguments and records with +named field entries are written with their named entries in an unspecified +canonical order and position. Unless otherwise called out, position of named +entries is semantically irrelevant, and all invocations and record literals with +the same named entries (possibly in different orders or locations) and the same +positional entries are considered equivalent. + +Given a type schema `K` and a record expression `E` of the general form `(e1, +..., en, d1 : e{n+1}, ..., dm : e{n+m})` inference proceeds as follows. + +If `K` is a record type schema of the form `(K1, ..., Kn, {d1 : K{n+1}, ...., +dm : K{n+m}})` then: + - Each `ei` is inferred with context type schema `Ki` to have type `Si` + - Let `Ri` be the greatest closure of `Ki` + - If `Si` is a subtype of `Ri` then let `Ti` be `Si` + - Otherwise, if `Si` is `dynamic`, then we insert an implicit cast on `ei` + to `Ri`, and let `Ti` be `Ri` + - Otherwise, if `Si` is coercible to `Ri` (via some sequence of call method + tearoff or implicit generic instantiation coercions), then we insert the + appropriate implicit coercion(s) on `ei`. Let `Ti` be the type of the + resulting coerced value (which must be a subtype of `Ri`, possibly + proper). + - Otherwise, it is a static error. + - The type of `E` is `(T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})` + +If `K` is any other type schema: + - Each `ei` is inferred with context type schema `_` to have type `Ti` + - The type of `E` is `(T1, ..., Tn, {d1 : T{n+1}, ...., dm : T{n+m}})` + +As noted above, contrary to the practice for runtime checked covariant nominal +types, we do not prefer the context type over the more precise upwards type. +The following example illustrates this: +```dart + // No static error. + // Inferred type of the record is (int, double) + (num, num) r = (3, 3.5)..$0.isEven; +``` -Type inference and promotion flows through records in much the same way it does -for instances of generic classes (which are covariant in Dart just like record -fields are) and collection literals. +Also note that implicit casts and other coercions are considered to be applied +as part of inference, hence: +```dart + class Callable { + void call(num x) {} + } + T id(T x) => x; + // No static error. + // Inferred type of the record is: + // (int, double, int Function(int), void Function(num)) + var c = Callable(); + dynamic d = 3; + (num, double, int Function(int), void Function(int)) r = (d, 3, id, c); +``` +and the record initialization in the last line above is implicitly coerced to be +the equivalent of: +```dart + (num, double, int Function(int), void Function()) r = + (d as num, 3.0, id, c.call); +``` -**TODO: Specify this more precisely.** +See issue [2488](https://github.com/dart-lang/language/issues/2488) for some of +the background discussion on the choices specified in this section. ### Constants @@ -588,6 +671,10 @@ covariant in their field types. ## CHANGELOG +### 1.14 + +- Specify type inference, add static semantics to resources/type-system + ### 1.13 - Introduce `()` syntax for empty record expressions and remove `Record.empty`. diff --git a/resources/type-system/inference.md b/resources/type-system/inference.md index 2d735569bc..f33b439e78 100644 --- a/resources/type-system/inference.md +++ b/resources/type-system/inference.md @@ -407,6 +407,18 @@ The meta-variable `C` ranges over classes. The meta-variable `B` ranges over types used as bounds for type variables. +For convenience, we generally write function types with all named parameters in +an unspecified canonical order, and similarly for the named fields of record +types. In all cases unless otherwise specifically called out, order of named +parameters and fields is semantically irrelevant: any two types with the same +named parameters (named fields, respectively) are considered the same type. + +Similarly, function and method invocations with named arguments and records with +named field entries are written with their named entries in an unspecified +canonical order and position. Unless otherwise called out, position of named +entries is semantically irrelevant, and all invocations and record literals with +the same named entries (possibly in different orders or locations) and the same +positional entries are considered equivalent. ### Type schemas @@ -444,14 +456,16 @@ The covariant occurrences of a type (schema) `T` in another type (schema) `S` ar - the covariant occurrencs of `T` in `U` - if `S` is an interface type `C` - the union of the covariant occurrences of `T` in `Ti` for `i` in `0, ..., k` - - if `S` is `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, + - if `S` is `U Function(T0 x0, ..., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, the union of: - the covariant occurrences of `T` in `U` - the contravariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - - if `S` is `U Function(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` + - if `S` is `U Function(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})` the union of: - the covariant occurrences of `T` in `U` - the contravariant occurrences of `T` in `Ti` for `i` in `0, ..., m` + - if `S` is `(T0, ..., Tn, {Tn+1 xn+1, ..., Tm xm})`, + - the covariant occurrences of `T` in `Ti` for `i` in `0, ..., m` The contravariant occurrences of a type `T` in another type `S` are: - if `S` is `Future` @@ -460,14 +474,16 @@ The contravariant occurrences of a type `T` in another type `S` are: - the contravariant occurrencs of `T` in `U` - if `S` is an interface type `C` - the union of the contravariant occurrences of `T` in `Ti` for `i` in `0, ..., k` - - if `S` is `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, + - if `S` is `U Function(T0 x0, ..., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, the union of: - the contravariant occurrences of `T` in `U` - the covariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - - if `S` is `U Function(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` + - if `S` is `U Function(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})` the union of: - the contravariant occurrences of `T` in `U` - the covariant occurrences of `T` in `Ti` for `i` in `0, ..., m` + - if `S` is `(T0, ..., Tn, {Tn+1 xn+1, ..., Tm xm})`, + - the contravariant occurrences of `T` in `Ti` for `i` in `0, ..., m` The invariant occurrences of a type `T` in another type `S` are: - if `S` is `Future` @@ -476,16 +492,18 @@ The invariant occurrences of a type `T` in another type `S` are: - the invariant occurrencs of `T` in `U` - if `S` is an interface type `C` - the union of the invariant occurrences of `T` in `Ti` for `i` in `0, ..., k` - - if `S` is `U Function(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, + - if `S` is `U Function(T0 x0, ..., Tn xn, [Tn+1 xn+1, ..., Tm xm])`, the union of: - the invariant occurrences of `T` in `U` - the invariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - all occurrences of `T` in `Bi` for `i` in `0, ..., k` - - if `S` is `U Function(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})` + - if `S` is `U Function(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})` the union of: - the invariant occurrences of `T` in `U` - the invariant occurrences of `T` in `Ti` for `i` in `0, ..., m` - all occurrences of `T` in `Bi` for `i` in `0, ..., k` + - if `S` is `(T0, ..., Tn, {Tn+1 xn+1, ..., Tm xm})`, + - the invariant occurrences of `T` in `Ti` for `i` in `0, ..., m` ### Type variable elimination (least and greatest closure of a type) @@ -530,40 +548,47 @@ replaced with `Never`, and every covariant occurrence of `Xi` replaced with is the least closure of `Ti` with respect to `L` - The greatest closure of `S` with respect to `L` is `C` where `Ui` is the greatest closure of `Ti` with respect to `L` -- if `S` is `T Function(T0 x0, ...., Tn xn, +- if `S` is `T Function(T0 x0, ..., Tn xn, [Tn+1 xn+1, ..., Tm xm])` and no type variable in `L` occurs in any of the `Bi`: - The least closure of `S` with respect to `L` is `U Function(U0 x0, ...., Un1 xn, [Un+1 xn+1, ..., Um xm])` where: + ..., Xk extends Bk>(U0 x0, ..., Un1 xn, [Un+1 xn+1, ..., Um xm])` where: - `U` is the least closure of `T` with respect to `L` - `Ui` is the greatest closure of `Ti` with respect to `L` - with the usual capture avoiding requirement that the `Xi` do not appear in `L`. - The greatest closure of `S` with respect to `L` is `U Function(U0 x0, ...., Un1 xn, [Un+1 xn+1, ..., Um xm])` where: + ..., Xk extends Bk>(U0 x0, ..., Un1 xn, [Un+1 xn+1, ..., Um xm])` where: - `U` is the greatest closure of `T` with respect to `L` - `Ui` is the least closure of `Ti` with respect to `L` - with the usual capture avoiding requirement that the `Xi` do not appear in `L`. -- if `S` is `T Function(T0 x0, ...., Tn xn, +- if `S` is `T Function(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})` and no type variable in `L` occurs in any of the `Bi`: - The least closure of `S` with respect to `L` is `U Function(U0 x0, ...., Un1 xn, {Un+1 xn+1, ..., Um xm})` where: + ..., Xk extends Bk>(U0 x0, ..., Un1 xn, {Un+1 xn+1, ..., Um xm})` where: - `U` is the least closure of `T` with respect to `L` - `Ui` is the greatest closure of `Ti` with respect to `L` - with the usual capture avoiding requirement that the `Xi` do not appear in `L`. - The greatest closure of `S` with respect to `L` is `U Function(U0 x0, ...., Un1 xn, {Un+1 xn+1, ..., Um xm})` where: + ..., Xk extends Bk>(U0 x0, ..., Un1 xn, {Un+1 xn+1, ..., Um xm})` where: - `U` is the greatest closure of `T` with respect to `L` - `Ui` is the least closure of `Ti` with respect to `L` - with the usual capture avoiding requirement that the `Xi` do not appear in `L`. -- if `S` is `T Function(T0 x0, ...., Tn xn, - [Tn+1 xn+1, ..., Tm xm])` or `T Function(T0 x0, ...., Tn xn, +- if `S` is `T Function(T0 x0, ..., Tn xn, + [Tn+1 xn+1, ..., Tm xm])` or `T Function(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})`and `L` contains any free type variables from any of the `Bi`: - The least closure of `S` with respect to `L` is `Never` - The greatest closure of `S` with respect to `L` is `Function` +- if `S` is `(T0 x0, ..., Tn xn, {Tn+1 xn+1, ..., Tm xm})`: + - The least closure of `S` with respect to `L` is `(U0 x0, ..., Un1 xn, {Un+1 + xn+1, ..., Um xm})` where: + - `Ui` is the least closure of `Ti` with respect to `L` + - The greatest closure of `S` with respect to `L` is `(U0 x0, ..., Un1 xn, + {Un+1 xn+1, ..., Um xm})` where: + - `Ui` is the greatest closure of `Ti` with respect to `L` ### Type schema elimination (least and greatest closure of a type schema) @@ -935,6 +960,15 @@ with respect to `L` under constraints `C0` - And `C2` is `C1` with each constraint replaced with its closure with respect to `[Z0, ..., Zn]`. +- A type `P` is a subtype match for `Record` with respect to `L` under no constraints: + - If `P` is a record type or `Record`. + +- A record type `(M0,..., Mk, {M{k+1} d{k+1}, ..., Mm dm])` is a subtype match + for a record type `(N0,..., Nk, {N{k+1} d{k+1}, ..., Nm dm])` with respect + to `L` under constraints `C0 + ... + Cm` + - If for `i` in `0...m`, `Mi` is a subtype match for `Ni` with respect to `L` + under constraints `Ci`. +