Static semantics for records

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>(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<int>, 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`.

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<T0, ..., Tk>`
     - the union of the covariant occurrences of `T` in `Ti` for `i` in `0, ..., k`
-  - if `S` is `U Function<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`,
+  - if `S` is `U Function<X0 extends B0, ..., Xk extends Bk>(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<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})`
+  - if `S` is `U Function<X0 extends B0, ..., Xk extends Bk>(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<U>`
@@ -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<T0, ..., Tk>`
     - the union of the contravariant occurrences of `T` in `Ti` for `i` in `0, ..., k`
-  - if `S` is `U Function<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`,
+  - if `S` is `U Function<X0 extends B0, ..., Xk extends Bk>(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<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})`
+  - if `S` is `U Function<X0 extends B0, ..., Xk extends Bk>(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<U>`
@@ -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<T0, ..., Tk>`
     - the union of the invariant occurrences of `T` in `Ti` for `i` in `0, ..., k`
-  - if `S` is `U Function<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, [Tn+1 xn+1, ..., Tm xm])`,
+  - if `S` is `U Function<X0 extends B0, ..., Xk extends Bk>(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<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn, {Tn+1 xn+1, ..., Tm xm})`
+  - if `S` is `U Function<X0 extends B0, ..., Xk extends Bk>(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<U0, ..., Uk>` where
     `Ui` is the greatest closure of `Ti` with respect to `L`
-- if `S` is `T Function<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn,
+- if `S` is `T Function<X0 extends B0, ..., Xk extends Bk>(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<X0 extends B0,
-  ...., Xk extends Bk>(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<X0 extends B0,
-  ...., Xk extends Bk>(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<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn,
+- if `S` is `T Function<X0 extends B0, ..., Xk extends Bk>(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<X0 extends B0,
-  ...., Xk extends Bk>(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<X0 extends B0,
-  ...., Xk extends Bk>(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<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn,
-    [Tn+1 xn+1, ..., Tm xm])` or `T Function<X0 extends B0, ...., Xk extends Bk>(T0 x0, ...., Tn xn,
+- if `S` is `T Function<X0 extends B0, ..., Xk extends Bk>(T0 x0, ..., Tn xn,
+    [Tn+1 xn+1, ..., Tm xm])` or `T Function<X0 extends B0, ..., Xk extends Bk>(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`.
+
 
 <!--
 

resources/type-system/normalization.md

@@ -21,6 +21,13 @@ document
 We assume that type aliases are fully expanded, and that prefixed types are
 resolved to a canonical name.
 
+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.
+
+
 ## Normalization
 
 The **NORM** relation defines the canonical representative of classes of
@@ -93,6 +100,9 @@ equations apply gives us something like the following:
   - where `R1` = **NORM**(`R`)
   - and `B1` = **NORM**(`B`)
   - and `S1` = **NORM**(`S`)
+- **NORM**(`(S0, ..., Sn, {T0 d0, ..., Tm dm})`) = `(S0', ..., Sn', {T0' d0, ..., Tm' dm})`
+  - where `Si'` = **NORM**(`Si`)
+  - and `Ti'` = **NORM**(`Ti`)
 
 Note that there is currently no place in the type system where normalization can
 apply to intersection types (promoted types). The rule is included here for

resources/type-system/subtyping.md

@@ -35,6 +35,7 @@ The set of types under consideration are as follows:
 - `Null`
 - `Never`
 - `Function`
+- `Record`
 - `Future<T>`
 - `FutureOr<T>`
 - `T?`
@@ -43,6 +44,8 @@ The set of types under consideration are as follows:
 - 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})`
+- Record types
+  - `(T0, ...., Tn, {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
@@ -81,6 +84,11 @@ Given the current promotion semantics the following properties are also true:
      they can never appear as sub-components of other types, in bounds, or as
      part of other promoted 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.
 
 ## Notation
 
@@ -208,6 +216,8 @@ promoted type variables `X0 & S0` and `T1` is `X0 & S1` then:
 
 - **Function Type/Function**: `T0` is a function type and `T1` is `Function`
 
+- **Record Type/Record**: `T0` is a record type and `T1` is `Record`
+
 - **Interface Compositionality**: `T0` is an interface type `C0<S0, ..., Sk>`
   and `T1` is `C0<U0, ..., Uk>`
   - and each `Si <: Ui`
@@ -241,6 +251,10 @@ promoted type variables `X0 & S0` and `T1` is `X0 & S1` then:
   - 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]`
 
+- **Record Types**: `T0` is `(V0, ..., Vn, {Vn+1 dn+1, ..., Vm dm})`
+  - and `T1` is `(S0, ..., Sn, {Sn+1 dn+1, ..., Sm dm})`
+  - and `Vi <: Si` for `i` in `0...m`
+
 *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*

resources/type-system/upper-lower-bounds.md

@@ -30,6 +30,12 @@ full Dart types, as described in the subtyping
 document
 [here](https://github.com/dart-lang/language/blob/master/resources/type-system/subtyping.md)
 
+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.
+
 ## Syntactic conventions
 
 The predicates here are defined as algorithms and should be read from top to
@@ -173,6 +179,20 @@ We define the upper bound of two types T1 and T2 to be **UP**(`T1`,`T2`) as foll
 - **UP**(`T Function<...>(...)`, `S Function<...>(...)`) = `Function` otherwise
 - **UP**(`T Function<...>(...)`, `T2`) = **UP**(`Object`, `T2`)
 - **UP**(`T1`, `T Function<...>(...)`) = **UP**(`T1`, `Object`)
+
+- **UP**(`(...)`, `Record`) = `Record`
+- **UP**(`Record`, `(...)`) = `Record`
+
+- **UP**(`(S0, ... Sk, {T0 d0, ..., Tn dn})`,
+         `(S0', ... Sk', {T0' d0, ..., Tn' dn})`) =
+   `(Q0, ...,Qk, {R0, ..., Rn})` if:
+     - `Qi` is **UP**(`Si`, `Si'`)
+     - `Ri` is **UP**(`Ti`, `Ti'`)
+
+- **UP**(`(...)`, `(...)`) = `Record` otherwise
+- **UP**(`(...)`, `T2`) = **UP**(`Object`, `T2`)
+- **UP**(`T1`, `(...)`) = **UP**(`T1`, `Object`)
+
 - **UP**(`FutureOr<T1>`, `FutureOr<T2>`) = `FutureOr<T3>` where `T3` = **UP**(`T1`, `T2`)
 - **UP**(`Future<T1>`, `FutureOr<T2>`) = `FutureOr<T3>` where `T3` = **UP**(`T1`, `T2`)
 - **UP**(`FutureOr<T1>`, `Future<T2>`) = `FutureOr<T3>` where `T3` = **UP**(`T1`, `T2`)
@@ -280,6 +300,13 @@ follows.
 
 - **DOWN**(`T Function<...>(...)`, `S Function<...>(...)`) = `Never` otherwise
 
+- **DOWN**(`(S0, ... Sk, {T0 d0, ..., Tn dn})`,
+         `(S0', ... Sk', {T0' d0, ..., Tn' dn})`) =
+   `(Q0, ...,Qk, {R0, ..., Rn})` if:
+     - `Qi` is **DOWN**(`Si`, `Si'`)
+     - `Ri` is **DOWN**(`Ti`, `Ti'`)
+
+- **DOWN**(`(...)`, `(...)`) = `Never` otherwise
 
 - **DOWN**(`T1`, `T2`) = `T1` if `T1` <: `T2`
 - **DOWN**(`T1`, `T2`) = `T2` if `T2` <: `T1`