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 computatinos for record types has 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,42 @@ 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
+
+As usual, 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.  Given a type schema `K` and a record expression `E` of the
+general form `(e0, ..., en, d0 : t0, ..., dm : tm)`, then inference proceeds as
+follows.
+
+If `K` is a record type schema of the form `(K0, ..., Kn, {d0 : P0, ...., dm :
+Pm})`, then:
+  - Each `ei` is inferred with context type schema `Ki` to have type `Ti`
+  - Each `ti` is inferred with context type schema `Pi` to have type `Si`
+  - The type of `E` is `(T0, ..., Tn, {d0 : S0, ...., dm : Sm})`
+
+If `K` is any other type schema:
+  - Each `ei` is inferred with context type schema `_` to have type `Ti`
+  - Each `ti` is inferred with context type schema `_` to have type `Si`
+  - The type of `E` is `(T0, ..., Tn, {d0 : S0, ...., dm : Sm})`
+
+Note that 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 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.
+Note that implicit casts are not considered to be applied as part of inference,
+hence:
+
+```dart
+  // Static error, inferred type of the record is (dynamic, double)
+  (num, num) r = (3 as dynamic, 3.5);
+```
 
-**TODO: Specify this more precisely.**
 
 ### Constants
 
@@ -565,6 +604,10 @@ covariant in their field types.
 
 ## CHANGELOG
 
+### 1.9
+
+- Specify type inference, add static semantics to resources/type-system
+
 ### 1.8
 
 - Move to accepted

resources/type-system/inference.md

@@ -452,6 +452,8 @@ The covariant occurrences of a type (schema) `T` in another type (schema) `S` ar
       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>`
@@ -468,6 +470,8 @@ The contravariant occurrences of a type `T` in another type `S` are:
       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>`
@@ -486,6 +490,8 @@ The invariant occurrences of a type `T` in another type `S` are:
     - 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)
 
@@ -564,6 +570,13 @@ replaced with `Never`, and every covariant occurrence of `Xi` replaced with
   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 +948,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 (including `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

@@ -93,6 +93,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 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
@@ -208,6 +211,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 +246,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 x0, ..., Vn xn, {Vn+1 dn+1, ..., Vm xm})`
+  - and `T1` is `(S0 y0, ..., Sn yn, {Sn+1 yn+1, ..., Sm ym})`
+  - 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

@@ -173,6 +173,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 +294,16 @@ follows.
 
 - **DOWN**(`T Function<...>(...)`, `S Function<...>(...)`) = `Never` otherwise
 
+- **DOWN**(`(...)`, `Record`) = `(...)`
+- **DOWN**(`Record`, `(...)`) = `(...)`
+
+- **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`