mirror of
https://github.com/dart-lang/sdk
synced 2024-09-16 02:57:35 +00:00
Refactored this and uploaded here:
https://github.com/dart-lang/dev_compiler/blob/strong/STRONG_MODE.md PTAL R=jmesserly@google.com, rnystrom@google.com Review URL: https://codereview.chromium.org/1541833002 .
This commit is contained in:
Vijay Menon
parent
dee054e23b
commit
a763c43486
|
|
@ -1,88 +1,39 @@
|
|||
# Strong Mode
|
||||
|
||||
## Overview
|
||||
Strong mode applies a more restrictive type system to Dart to address its unsound, surprising behavior in certain cases.
|
||||
|
||||
The Dart Development Compiler (DDC) is a new Dart-to-JavaScript compiler that supports a large subset of the Dart programming language. DDC is motivated by the following goals:
|
||||
Strong mode helps with:
|
||||
|
||||
First, we aim to generate clean, readable, consumable JavaScript output. This simplifies debugging Dart applications across multiple web platforms. It also enables better, seamless interoperability between Dart and JavaScript components.
|
||||
|
||||
Second, we aim to compile in a fast, modular fashion. This enables a faster, better development cycle across a number of platforms and devices that lack native Dart support. It also allows Dart libraries to be packaged and distributed separately for use in other Dart or JavaScript applications.
|
||||
|
||||
To accomplish these goals, we focus on a subset of Dart applications we can statically type check. This subset can be viewed as a **strong mode** analogous to Dart’s checked mode and production mode. A program that runs correctly in strong mode will run the same in checked mode and, thus, in production mode. The subset we support entails:
|
||||
|
||||
- A stricter, sounder, type system
|
||||
- Type inference
|
||||
- Restrictions on certain language constructs
|
||||
|
||||
DDC is intended to complement our existing Dart2JS compiler. Unlike DDC, Dart2JS is focused on raw performance and support for the entire Dart language rather than readability, JavaScript interoperability, or modular compilation.
|
||||
|
||||
This document provides a high-level overview of strong mode. A corresponding formalism of strong mode can also be found [here](https://dart-lang.github.io/dev_compiler/strong-dart.pdf).
|
||||
- [Stronger static checking](doc/STATIC_SAFETY.md) to find more errors during static analysis or compilation.
|
||||
- [Stronger runtime checking](doc/RUNTIME_SAFETY.md) in the Dart Dev Compiler (DDC) to find errors at runtime.
|
||||
- [Idiomatic JavaScript code generation](doc/JS_CODEGEN.md) via DDC for more readable output and better interoperability.
|
||||
|
||||
## Motivation
|
||||
|
||||
The standard Dart type system is unsound by design. This means that static type annotations may not match the actual runtime values even when a program is running in checked mode. This allows considerable flexibility, but it also means that Dart implementations cannot easily use these annotations for optimization or code generation.
|
||||
|
||||
Because of this, existing Dart implementations require dynamic dispatch. Furthermore, because Dart’s dispatch semantics are different from JavaScript’s, it effectively precludes mapping Dart calls to idiomatic JavaScript. For example, the following Dart code:
|
||||
Strong mode aims to ensure that static type annotations are actually correct at runtime. For this to work, strong mode provides a stricter type system than standard Dart. Consider the following example:
|
||||
|
||||
```dart
|
||||
var x = a.bar;
|
||||
b.foo("hello", x);
|
||||
```
|
||||
|
||||
cannot easily be mapped to the identical JavaScript code. If `a` does not contain a `bar` field, Dart requires a `NoSuchMethodError` while JavaScript simply returns undefined. If `b` contains a `foo` method, but with the wrong number of arguments, Dart again requires a `NoSuchMethodError` while JavaScript either ignores extra arguments or fills in omitted ones with undefined.
|
||||
|
||||
To capture these differences, the Dart2JS compiler instead generates code that approximately looks like:
|
||||
|
||||
```dart
|
||||
var x = getInterceptor(a).get$bar(a);
|
||||
getInterceptor(b).foo$2(b, "hello", x);
|
||||
```
|
||||
The “interceptor” is Dart’s dispatch table for the objects `a` and `b`, and the mangled names (`get$bar` and `foo$2`) account for Dart’s different dispatch semantics.
|
||||
|
||||
The above highlights why Dart-JavaScript interoperability hasn’t been seamless: Dart objects and methods do not look like normal JavaScript ones.
|
||||
|
||||
DDC relies on strong mode to map Dart calling conventions to normal JavaScript ones. If `a` and `b` have static type annotations (with a type other than `dynamic`), strong mode statically verifies that they have a field `bar` and a 2-argument method `foo` respectively. In this case, DDC safely generates the identical JavaScript:
|
||||
|
||||
```javascript
|
||||
var x = a.bar;
|
||||
b.foo("hello", x);
|
||||
```
|
||||
|
||||
Note that DDC still supports the `dynamic` type, but relies on runtime helper functions in this case. E.g., if `a` and `b` are type `dynamic`, DDC instead generates:
|
||||
|
||||
```javascript
|
||||
var x = dload(a, "bar");
|
||||
dsend(b, "foo", "hello", x);
|
||||
```
|
||||
|
||||
where `dload` and `dsend` are runtime helpers that implement Dart dispatch semantics. Programmers are encouraged to use static annotations to avoid this. Strong mode is able to use static checking to enforce much of what checked mode does at runtime. In the code above, strong mode statically verifies that `b`’s type (if not `dynamic`) has a `foo` method that accepts a `String` as its first argument and `a.bar`’s type as its second. If the code is sufficiently typed, runtime checks are unnecessary.
|
||||
|
||||
## Strong Mode Type System
|
||||
|
||||
DDC uses strong mode to ensure that static type annotations are actually correct at runtime. For this to work, strong mode requires a stricter type system than standard Dart. To understand this, consider the following, which we will use as our running example:
|
||||
|
||||
```dart
|
||||
library util;
|
||||
// util.dart
|
||||
|
||||
void info(List<int> list) {
|
||||
var length = list.length;
|
||||
if (length != 0) print("$length ${list[0]}");
|
||||
if (length != 0) print(length + list[0]);
|
||||
}
|
||||
```
|
||||
|
||||
A developer might reasonably expect the `info` function to print either nothing (empty list) or two integers (non-empty list), and that Dart’s static tooling and checked mode would enforce this.
|
||||
A developer might reasonably expect the `info` function to print either nothing (empty list) or a single integer (non-empty list), and that Dart’s static tooling and checked mode would enforce this.
|
||||
|
||||
However, in the following context, the info method prints “hello world” in checked mode, without any static errors or warnings:
|
||||
However, in the following context, the info method prints “helloworld” in checked mode, without any static errors or warnings:
|
||||
|
||||
```dart
|
||||
import ‘dart:collection’;
|
||||
import ‘utils.dart’;
|
||||
import ‘util.dart’;
|
||||
|
||||
class MyList extends ListBase<int> implements List {
|
||||
Object length;
|
||||
|
||||
|
||||
MyList(this.length);
|
||||
|
||||
|
||||
operator[](index) => "world";
|
||||
operator[]=(index, value) {}
|
||||
}
|
||||
|
|
@ -90,388 +41,17 @@ class MyList extends ListBase<int> implements List {
|
|||
void main() {
|
||||
List<int> list = new MyList("hello");
|
||||
info(list);
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
The lack of static or runtime errors is not an oversight; it is by design. It provides developers a mechanism to circumvent or ignore types when convenient, but it comes at cost. While the above example is contrived, it demonstrates that developers cannot easily reason about a program modularly: the static type annotations in the `utils` library are of limited use, even in checked mode.
|
||||
The lack of static or runtime errors in the Dart specification's type rules is not an oversight; it is by design. It provides developers a mechanism to circumvent or ignore types when convenient, but it comes at cost. While the above example is contrived, it demonstrates that developers cannot easily reason about a program modularly: the static type annotations in the `util` library are of limited use, even in checked mode.
|
||||
|
||||
For the same reason, a compiler cannot easily exploit type annotations if they are unsound. A Dart compiler cannot simply assume that a `List<int>` contains `int` values or even that its `length` is an integer. Instead, it must either rely on expensive (and often brittle) whole program analysis or on additional runtime checking.
|
||||
For the same reason, a compiler cannot easily exploit type annotations if they are unsound. A Dart compiler cannot simply assume that a `List<int>` contains `int` values or even that its `length` is an integer. Instead, it must either rely on expensive (and often brittle) whole program analysis or on additional runtime checking. That [additional checking](doc/JS_CODEGEN.md) may lead to larger, slower code and harder-to-read output when Dart is transpiled to a high level language like JavaScript.
|
||||
|
||||
The fundamental issue above is that static annotations may not match runtime types, even in checked mode: this is a direct consequence of the unsoundness of the Dart type system. This can make it difficult for both programmers and compilers to rely on static types to reason about programs.
|
||||
|
||||
Strong mode enforces the correctness of static type annotations. It simply disallows examples such as the above. It relies on a combination of static checking and runtime assertions. In our running example, standard Dart rules (checked or otherwise) allow `MyList` to masquerade as a `List<int>`. DDC disallows this by statically rejecting the declaration of `MyList`. This allows both the developer and the compiler to better reason about the info method. For statically checked code, both may assume that the argument is a proper `List<int>`, with integer-valued length and elements.
|
||||
|
||||
DDC’s strong mode is strictly stronger than checked mode. A Dart program execution where (a) the program passes DDC’s static checking and (b) the execution does not trigger DDC’s runtime assertions, will also run in checked mode on any Dart platform.
|
||||
Strong mode solves that by enforcing the correctness of static type annotations. It disallows examples such as the above. In this example, standard Dart rules (checked or otherwise) allow `MyList` to masquerade as a `List<int>`. Strong mode statically rejects the declaration of `MyList`.
|
||||
|
||||
DDC augments strong mode static checking with a minimal set of runtime checks required to enforce soundness, similar to how Java and C# handle potentially unsafe casts. This allows both the developer and the compiler to better reason about the info method. For statically checked code, both may assume that the argument is a proper `List<int>`, with integer-valued length and elements.
|
||||
|
||||
### Static typing
|
||||
|
||||
The primary sources of unsoundness in Dart are generics and functions. Both introduce circularity in the Dart subtyping relationship.
|
||||
|
||||
#### Generics
|
||||
|
||||
Generics in Dart are co-variant, with the added rule that the `dynamic` type may serve as both ⊤ (top) and ⊥ (bottom) of the type hierarchy in certain situations. For example, let *<:<sub>D</sub>* represent the standard Dart subtyping rule. Then, for all types `S` and `T`:
|
||||
|
||||
`List<S>` <:<sub>D</sub> `List<dynamic>` <:<sub>D</sub> `List<T>`
|
||||
|
||||
where `List` is equivalent to `List<dynamic>`. This introduces circularity - e.g.,:
|
||||
|
||||
`List<int>` <:<sub>D</sub> `List` <:<sub>D</sub> `List<String>`<:<sub>D</sub> `List` <:<sub>D</sub> `List<int>`
|
||||
|
||||
|
||||
From a programmer’s perspective, this means that, at compile-time, values that are statically typed `List<int>` may later be typed `List<String>` and vice versa. At runtime, a plain `List` can interchangeably act as a `List<int>` or a `List<String>` regardless of its actual values.
|
||||
|
||||
Our running example exploits this. A `MyList` may be passed to the `info` function as it’s a subtype of the expected type:
|
||||
|
||||
`MyList` <:<sub>D</sub> `List` <:<sub>D</sub>`List<int>`
|
||||
|
||||
In strong mode, we introduce a stricter subtyping rule <:<sub>S</sub> to disallow this. In this case, in the context of a generic type parameter, dynamic may only serve as ⊤. This means that this is still true:
|
||||
|
||||
`List<int>` <:<sub>S</sub> `List`
|
||||
|
||||
but that this is not:
|
||||
|
||||
`List<int>` ~~<:<sub>S</sub> `List`~~
|
||||
|
||||
|
||||
Our running example fails in strong mode:
|
||||
|
||||
`MyList` <:<sub>S</sub> `List` ~~<:<sub>S</sub> `List<int>`~~
|
||||
|
||||
|
||||
#### Functions
|
||||
|
||||
The other primary source of unsoundness in Dart is function subtyping. An unusual feature of the Dart type system is that function types are bivariant in both the parameter types and the return type (see Section 19.5 of the [Dart specification](http://www.google.com/url?q=http%3A%2F%2Fwww.ecma-international.org%2Fpublications%2Ffiles%2FECMA-ST%2FECMA-408.pdf&sa=D&sntz=1&usg=AFQjCNGoFPzBNx2fgejKQgSgiS2dUBstBw)). As with generics, this leads to circularity:
|
||||
|
||||
`(int) -> int` <:<sub>D</sub> `(Object) -> Object` <:<sub>D</sub> `(int) -> int`
|
||||
|
||||
And, as before, this can lead to surprising behavior. In Dart, an overridden method’s type should be a subtype of the base class method’s type (otherwise, a static warning is given). In our running example, the (implicit) `MyList.length` getter has type:
|
||||
|
||||
`() -> Object`
|
||||
|
||||
while the `List.length` getter it overrides has type:
|
||||
|
||||
`() -> int`
|
||||
|
||||
This is valid in standard Dart as:
|
||||
|
||||
`() -> Object` <:<sub>D</sub> `() -> int`
|
||||
|
||||
Because of this, a `length` that returns "hello" (a valid `Object`) triggers no static or runtime warnings or errors.
|
||||
|
||||
Strong mode enforces the stricter, [traditional function subtyping](https://en.wikipedia.org/wiki/Subtyping#Function_types) rule: subtyping is contravariant in parameter types and covariant in return types. This permits:
|
||||
|
||||
`() -> int` <:<sub>S</sub> `() -> Object`
|
||||
|
||||
but disallows:
|
||||
|
||||
`() -> Object` <:<sub>S</sub> `() -> int`
|
||||
|
||||
With respect to our example, strong mode requires that any subtype of a List have an int-typed length. It statically rejects the length declaration in MyList.
|
||||
|
||||
Formal details of the strong mode type system may be found [here](https://dart-lang.github.io/dev_compiler/strong-dart.pdf).
|
||||
|
||||
### Implicit runtime assertions
|
||||
|
||||
Although strong mode relies heavily on static checking, it also requires some runtime checking for soundness. For example, the following code is allowed:
|
||||
|
||||
```dart
|
||||
dynamic x = …;
|
||||
List y = x;
|
||||
int z = y.length;
|
||||
```
|
||||
|
||||
but a runtime check is required (and inserted by DDC) to ensure that `y` is assigned a `List`. This is similar to checked mode, but much less pervasive. Checked mode would also require a runtime check on the assignment of `z`. Strong mode would not as this is enforced statically instead.
|
||||
|
||||
## Type Inference
|
||||
|
||||
A secondary goal of DDC is to preserve the terseness of Dart. While strong mode requires and/or encourages more static type annotations, our aim is make this as lightweight as possible.
|
||||
|
||||
In Dart, per the specification, the static type of a variable `x` declared as:
|
||||
|
||||
```dart
|
||||
var x = <String, String>{ "hello": "world"};
|
||||
```
|
||||
|
||||
is `dynamic` as there is no explicit type annotation on the left-hand side. To discourage code bloat, the Dart style guide generally recommends omitting these type annotations in many situations. In these cases, the benefits of strong mode would be lost.
|
||||
|
||||
To avoid this, strong mode uses limited inference. In the case above, the strong mode infers and enforces the type of `x` as `Map<String, String>`. An important aspect to inference is ordering: when an inferred type may be used to infer other type. To maximize the impact, we perform the following inference in the following order:
|
||||
|
||||
- Top-level and static fields
|
||||
- Instance fields and methods
|
||||
- Local variables
|
||||
- Allocation expressions
|
||||
|
||||
In all cases, inference tightens the static type or runtime type as compared to the Dart specification. The `dynamic` type, either alone or in the context of a function or generic parameter type, is inferred to a more specific type. The effect of this inference (other than stricter type errors) should not be observable at runtime outside the use of the mirrors API or by explicitly examining Object.runtimeType. (Note, in the next section, we discuss corresponding restrictions on `is` and `as` type checks.)
|
||||
|
||||
### Top-level and Static Fields
|
||||
|
||||
Strong mode will infer the static type of any top-level or static field with:
|
||||
|
||||
- No static type annotation
|
||||
- An initializer expression
|
||||
|
||||
The static type of the declared variable is inferred as the static type of the initializer. For example, consider:
|
||||
|
||||
```dart
|
||||
var PI = 3.14159;
|
||||
var TAU = PI * 2;
|
||||
```
|
||||
|
||||
Strong mode would infer the static type of `PI` as `double` directly from its initializer. It would infer the static type of `TAU` as `double`, transitively using `PI`’s inferred type. Standard Dart rules would treat the static type of both `PI` and `TAU` as `dynamic`. Note that the following later assignment would be allowed in standard Dart, but disallowed (as a static type error) in strong mode:
|
||||
```dart
|
||||
PI = "\u{03C0}"; // Unicode string for PI symbol
|
||||
```
|
||||
Strong mode inference avoids circular dependences. If a variable’s initializer expression refers to another variable whose type would be dependent (directly or transitively) on the first, the static type of that other variable is treated as `dynamic` for the purpose of inference. In this modified example,
|
||||
|
||||
```dart
|
||||
var _PI_FIRST = true;
|
||||
var PI = _PI_FIRST ? 3.14159 : TAU / 2;
|
||||
var TAU = _PI_FIRST ? PI * 2 : 6.28318;
|
||||
```
|
||||
|
||||
the variables `PI` and `TAU` are circularly dependent on each other. Strong mode would leave the static type of both as `dynamic`.
|
||||
|
||||
<em>
|
||||
Note - we’re experimenting with a few arguably simpler variants here:
|
||||
- Limiting inference to final or const fields (i.e., not var).
|
||||
- Limiting transitive inference to explicit program order.
|
||||
</em>
|
||||
|
||||
### Instance Fields and Methods
|
||||
|
||||
Strong mode performs two types of inference on instances fields and methods.
|
||||
|
||||
The first uses base types to constrain overrides in subtypes. Consider the following example:
|
||||
|
||||
```dart
|
||||
abstract class A {
|
||||
Map get m;
|
||||
int value(int i);
|
||||
}
|
||||
|
||||
class B extends A {
|
||||
var m;
|
||||
value(i) => m[i];
|
||||
…
|
||||
}
|
||||
```
|
||||
|
||||
In Dart, overridden method, getter, or setter types should be subtypes of the corresponding base class ones (otherwise, static warnings are given). In standard Dart, the above declaration of `B` is not an error: both `m`’s getter type and `value`’s return type are `dynamic`.
|
||||
|
||||
Strong mode - without inference - would disallow this: if `m` in `B` could be assigned an arbitrarily typed value, it would violate the type contract in the declaration of `A`.
|
||||
|
||||
However, rather than rejecting the above code, strong mode employs inference to tighten the static types to obtain a valid override. The corresponding types in B are inferred as if it was:
|
||||
|
||||
```dart
|
||||
class B extends A {
|
||||
Map m;
|
||||
int value(i) => m[i];
|
||||
…
|
||||
}
|
||||
```
|
||||
|
||||
Note that the argument type of `value` is left as `dynamic`. Tightening this type is not required for soundness.
|
||||
|
||||
The second form inference is limited to instance fields (not methods) and is similar to that on static fields. For instance fields where the static type is omitted and an initializer is present, the field’s type is inferred as the initializer’s type. In this continuation of our example:
|
||||
|
||||
```dart
|
||||
class C extends A {
|
||||
var y = 42;
|
||||
var m = <int, int>{ 0: 38};
|
||||
...
|
||||
}
|
||||
```
|
||||
the instance field `y` has inferred type `int` based upon its initializer. Note that override-based inference takes precedence over initializer-based inference. The instance field `m` has inferred type `Map`, not `Map<int, int>` due to the corresponding declaration in `A`.
|
||||
|
||||
<em>
|
||||
Note - we’re considering with a few variants here as well:
|
||||
- Limiting inference to final or const fields (i.e., not var).
|
||||
- Inference on parameter types when omitted (e.g., the argument to `B.value` above).
|
||||
- When to allow or prefer override-based inference.
|
||||
</em>
|
||||
|
||||
### Local Variables
|
||||
|
||||
As with fields, local variable types are inferred if the static type is omitted and an initializer expression is present. In the following example:
|
||||
|
||||
```dart
|
||||
Object foo(int x) {
|
||||
final y = x + 1;
|
||||
var z = y * 2;
|
||||
return z;
|
||||
}
|
||||
```
|
||||
|
||||
the static types of `y` and `z` are both inferred as `int` in strong mode. Note that local inference is done in program order: the inferred type of `z` is computed using the inferred type of `y`. Local inference may result in strong mode type errors in otherwise legal Dart code. In the above, a second assignment to `z` with a string value:
|
||||
```dart
|
||||
z = “$z”;
|
||||
```
|
||||
would trigger a static error in strong mode, but is allowed in standard Dart. In strong mode, the programmer must use an explicit type annotation to avoid inference. Explicitly declaring `z` with the type `Object` or `dynamic` would suffice in this case.
|
||||
|
||||
### Allocation Expressions
|
||||
|
||||
The final form of strong mode inference is on allocation expressions. This inference is rather different from the above: it tightens the runtime type of the corresponding expression using the static type of its context. Contextual inference is used on expressions that allocated a new object: closure literals, map and list literals, and explicit constructor invocations (i.e., via `new` or `const`).
|
||||
|
||||
#### Closure literals
|
||||
|
||||
Consider the following example:
|
||||
|
||||
```dart
|
||||
int apply(int f(int arg), int value) {
|
||||
return f(value);
|
||||
}
|
||||
|
||||
void main() {
|
||||
int result =
|
||||
apply((x) { x = x * 9 ~/ 5; return x + 32; }, 41);
|
||||
print(result);
|
||||
}
|
||||
```
|
||||
|
||||
The function `apply` takes another function `f`, typed `(int) -> int`, as its first argument. It is invoked in `main` with a closure literal. In standard Dart, the static type of this closure literal would be `(dynamic) -> dynamic`. In strong mode, this type cannot be safely converted to `(int) -> int` : it may return a `String` for example.
|
||||
|
||||
Dart has a syntactic limitation in this case: it is not possible to statically annotate the return type of a closure literal.
|
||||
|
||||
Strong mode sidesteps this difficulty via contextual inference. It infers the closure type as `(dynamic) -> int`. This is the most general type allowed by the context: the parameter type of apply.
|
||||
|
||||
#### List and map literals
|
||||
|
||||
Similarly, strong mode infers tighter runtime types for list and map literals. E.g., in
|
||||
|
||||
```dart
|
||||
List<String> l = [ "hello", "world" ];
|
||||
```
|
||||
|
||||
the runtime type is inferred as `List<String>` in order to match the context of the left hand side. In other words, the code above executes as if it was:
|
||||
|
||||
```dart
|
||||
List<String> l = <String>[ "hello", "world" ];
|
||||
```
|
||||
|
||||
Contextual inference may be recursive:
|
||||
|
||||
```dart
|
||||
Map<List<String>, Map<int, int>> map =
|
||||
{ ["hello"]: { 0: 42 }};
|
||||
```
|
||||
|
||||
In this case, the inner map literal is inferred and allocated as a `Map<int, int>`. Note, strong mode will statically reject code where the contextually required type is not compatible. This will trigger a static error:
|
||||
|
||||
```dart
|
||||
Map<List<String>, Map<int, int>> map =
|
||||
{ ["hello"]: { 0: "world" }}; // STATIC ERROR
|
||||
```
|
||||
|
||||
as "world" is not of type `int`.
|
||||
|
||||
#### Constructor invocations
|
||||
|
||||
Finally, strong mode performs similar contextual inference on explicit constructor invocations via new or const. For example:
|
||||
|
||||
```dart
|
||||
Set<String> string = new Set.from(["hello", "world"]);
|
||||
```
|
||||
|
||||
is treated as if it was written as:
|
||||
|
||||
```dart
|
||||
Set<String> string =
|
||||
new Set<String>.from(<String>["hello", "world"]);
|
||||
```
|
||||
|
||||
Note, as above, context is propagated downward into the expression.
|
||||
|
||||
## General Language Restrictions
|
||||
|
||||
In addition to stricter typing rules, DDC enforces other restrictions on Dart programs.
|
||||
|
||||
### Warnings are Errors
|
||||
|
||||
DDC effectively treats all standard Dart static warnings as static errors. Most of these warnings are required for soundness (e.g., if a concrete class is missing methods required by a declared interface). A full list of Dart static warnings may found in the [Dart specification](http://www.google.com/url?q=http%3A%2F%2Fwww.ecma-international.org%2Fpublications%2Ffiles%2FECMA-ST%2FECMA-408.pdf&sa=D&sntz=1&usg=AFQjCNGoFPzBNx2fgejKQgSgiS2dUBstBw), or enumerated here:
|
||||
|
||||
[https://github.com/dart-lang/sdk/blob/master/pkg/analyzer/lib/src/generated/error.dart#L3772](https://www.google.com/url?q=https%3A%2F%2Fgithub.com%2Fdart-lang%2Fsdk%2Fblob%2Fmaster%2Fpkg%2Fanalyzer%2Flib%2Fsrc%2Fgenerated%2Ferror.dart%23L3772&sa=D&sntz=1&usg=AFQjCNFc4E37M1PshVcw4zk7C9jXgqfGbw)
|
||||
|
||||
### Is / As Restrictions
|
||||
|
||||
Dart is and as runtime checks expose the unsoundness of the type system in certain cases. For example, consider:
|
||||
|
||||
```dart
|
||||
var list = ["hello", "world"];
|
||||
if (list is List<int>) {
|
||||
...
|
||||
} else if (list is List<String>) {
|
||||
...
|
||||
}
|
||||
```
|
||||
|
||||
Perhaps surprisingly, the first test - `list is List<int>` - evaluates to true here. Such code is highly likely to be erroneous.
|
||||
|
||||
DDC strong mode statically disallows problematic `is` or `as` checks.. In general, an expression:
|
||||
|
||||
```dart
|
||||
x is T
|
||||
```
|
||||
|
||||
or
|
||||
|
||||
```dart
|
||||
x as T
|
||||
```
|
||||
|
||||
is only allowed where `T` is a *ground type*:
|
||||
|
||||
- A non-generic class type (e.g., `Object`, `String`, `int`, ...).
|
||||
- A generic class type where all type parameters are implicitly or explicitly `dynamic` (e.g., `List<dynamic>`, `Map`, …).
|
||||
- A function type where the return type and all parameter types are `dynamic` (e.g., (`dynamic`, `dynamic`) -> `dynamic`, ([`dynamic`]) -> `dynamic`).
|
||||
|
||||
In all other cases, strong mode reports a static error.
|
||||
|
||||
### Super Invocations
|
||||
|
||||
In the context of constructor initializer lists, DDC restricts `super` invocations to the end. This restriction simplifies generated code with minimal effect on the program.
|
||||
|
||||
*Note: Both the VM and Dart2JS ignore the Dart specification on ordering: i.e., they appear to invoke the super constructor after other items on the initializer list regardless of where it appears.*
|
||||
|
||||
### For-in Loops
|
||||
|
||||
In for-in statements of the form:
|
||||
|
||||
```dart
|
||||
for (var i in e) { … }
|
||||
```
|
||||
|
||||
Strong mode requires the expression `e` to be an `Iterable`. When the loop variable `i` is also statically typed:
|
||||
|
||||
```dart
|
||||
for (T i in e) { … }
|
||||
```
|
||||
|
||||
the expression `e` is required to be an `Iterable<T>`.
|
||||
|
||||
*Note: we may weaken these.*
|
||||
|
||||
### Await Expressions
|
||||
|
||||
In an await expression of the form:
|
||||
```dart
|
||||
await expr
|
||||
```
|
||||
strong mode requires `expr` to be a subtype of `Future`. In standard Dart, this is not required although tools may provide a hint.
|
||||
|
||||
### Open Items
|
||||
|
||||
We do not yet implement but are considering the following restrictions as well.
|
||||
|
||||
- Disallow overriding fields: this results in complicated generated
|
||||
code where a field definition in a subclass shadows the field
|
||||
definition in a base class but both are generally required to be
|
||||
allocated. Users should prefer explicit getters and setters in such
|
||||
cases. See [issue 52](https://github.com/dart-lang/dev_compiler/issues/52).
|
||||
|
||||
- `Future<Future<T>>`: the Dart specification automatically flattens
|
||||
this type to `Future<T>` (where `T` is not a `Future`). This can be
|
||||
issue as far as soundness. We are considering forbidding this type
|
||||
altogether (with a combination of static and runtime checks). See
|
||||
[issue 228](https://github.com/dart-lang/dev_compiler/issues/228).
|
||||
|
||||
DDC execution is stricter than checked mode. A Dart program execution where (a) the program passes DDC’s static checking and (b) the execution does not trigger DDC’s runtime assertions, will also run in checked mode on any Dart platform.
|
||||
|
|
|
|||
|
|
@ -73,7 +73,7 @@ mode tools, but will be interpreted as `T` by strong mode. For example:
|
|||
// foo is a generic method which takes a single generic method parameter S.
|
||||
// In strong mode, the parameter x will have type S, and the return type will
|
||||
// be S
|
||||
// In normal mode, the parameter x will have type dynamic, and the return
|
||||
// In normal mode, the parameter x will have type dynamic, and the return
|
||||
// type will be dynamic.
|
||||
dynamic/*=S*/ foo/*<S>*/(dynamic/*=S*/ x) { return x; }
|
||||
```
|
||||
|
|
@ -102,7 +102,7 @@ declaring local variables and parameters, you can also use the `/*=T*/` syntax w
|
|||
// foo is a generic method that takes a single generic parameter S, and a value
|
||||
// x of type S
|
||||
void foo/*<S>*/(var /*=S*/ x) {
|
||||
// In strong mode, y will also have type S
|
||||
// In strong mode, y will also have type S
|
||||
var /*=S*/ y = x;
|
||||
|
||||
// In strong mode, z will also have type S
|
||||
|
|
@ -135,7 +135,7 @@ List<dynamic /*=S*/> foo/*<S>*/(/*=S*/ x) {
|
|||
// l0 is a list literal whose reified type will be List<S> in strong mode,
|
||||
// and List<dynamic> in normal mode.
|
||||
var l0 = <dynamic /*=S*/>[x];
|
||||
|
||||
|
||||
// as above, but with a regular constructor.
|
||||
var l1 = new List<dynamic /*=S*/>();
|
||||
return l1;
|
||||
|
|
@ -150,7 +150,7 @@ enclosed in parentheses, eliminating the need for explicitly writing `dynamic`.
|
|||
List/*<S>*/ foo/*<S>*/(/*=S*/ x) {
|
||||
// The shorthand syntax is not yet supported for list and map literals
|
||||
var l0 = <dynamic /*=S*/>[x];
|
||||
|
||||
|
||||
// but with regular constructors you can use it
|
||||
var l1 = new List/*<S>*/();
|
||||
return l1;
|
||||
41
pkg/dev_compiler/doc/JS_CODEGEN.md
Normal file
41
pkg/dev_compiler/doc/JS_CODEGEN.md
Normal file
|
|
@ -0,0 +1,41 @@
|
|||
# Strong Mode and Idiomatic JavaScript
|
||||
|
||||
The Dart Dev Compiler (DDC) uses [Strong Mode](STRONG_MODE.md) to safely generate
|
||||
idiomatic JavaScript. This enables better interoperability between Dart and JavaScript code.
|
||||
|
||||
The standard Dart type system is unsound by design. This means that static type annotations may not match the actual runtime values even when a program is running in checked mode. This allows considerable flexibility, but it also means that Dart implementations cannot easily use these annotations for optimization or code generation.
|
||||
|
||||
Because of this, existing Dart implementations require dynamic dispatch. Furthermore, because Dart’s dispatch semantics are different from JavaScript’s, it effectively precludes mapping Dart calls to idiomatic JavaScript. For example, the following Dart code:
|
||||
|
||||
```dart
|
||||
var x = a.bar;
|
||||
b.foo("hello", x);
|
||||
```
|
||||
|
||||
cannot easily be mapped to the identical JavaScript code. If `a` does not contain a `bar` field, Dart requires a `NoSuchMethodError` while JavaScript simply returns undefined. If `b` contains a `foo` method, but with the wrong number of arguments, Dart again requires a `NoSuchMethodError` while JavaScript either ignores extra arguments or fills in omitted ones with undefined.
|
||||
|
||||
To capture these differences, the Dart2JS compiler instead generates code that approximately looks like:
|
||||
|
||||
```dart
|
||||
var x = getInterceptor(a).get$bar(a);
|
||||
getInterceptor(b).foo$2(b, "hello", x);
|
||||
```
|
||||
The “interceptor” is Dart’s dispatch table for the objects `a` and `b`, and the mangled names (`get$bar` and `foo$2`) account for Dart’s different dispatch semantics.
|
||||
|
||||
The above highlights why Dart-JavaScript interoperability hasn’t been seamless: Dart objects and methods do not look like normal JavaScript ones.
|
||||
|
||||
DDC relies on strong mode to map Dart calling conventions to normal JavaScript ones. If `a` and `b` have static type annotations (with a type other than `dynamic`), strong mode statically verifies that they have a field `bar` and a 2-argument method `foo` respectively. In this case, DDC safely generates the identical JavaScript:
|
||||
|
||||
```javascript
|
||||
var x = a.bar;
|
||||
b.foo("hello", x);
|
||||
```
|
||||
|
||||
Note that DDC still supports the `dynamic` type, but relies on runtime helper functions in this case. E.g., if `a` and `b` are type `dynamic`, DDC instead generates:
|
||||
|
||||
```javascript
|
||||
var x = dload(a, "bar");
|
||||
dsend(b, "foo", "hello", x);
|
||||
```
|
||||
|
||||
where `dload` and `dsend` are runtime helpers that implement Dart dispatch semantics. Programmers are encouraged to use static annotations to avoid this. Strong mode is able to use static checking to enforce much of what checked mode does at runtime. In the code above, strong mode statically verifies that `b`’s type (if not `dynamic`) has a `foo` method that accepts a `String` as its first argument and `a.bar`’s type as its second. If the code is sufficiently typed, runtime checks are unnecessary.
|
||||
198
pkg/dev_compiler/doc/RUNTIME_SAFETY.md
Normal file
198
pkg/dev_compiler/doc/RUNTIME_SAFETY.md
Normal file
|
|
@ -0,0 +1,198 @@
|
|||
# Strong Mode in the Dart Dev Compiler
|
||||
|
||||
## Overview
|
||||
|
||||
In the Dart Dev Compiler (DDC), [static strong mode](STATIC_SAFETY.md) checks are augmented with stricter runtime behavior. Together, they enforce the soundness of Dart type annotations.
|
||||
|
||||
In general, and in contrast to Dart's checked mode, most safety is enforced statically, at analysis time. DDC exploits this to generate relatively few runtime checks while still providing stronger guarantees than checked mode.
|
||||
|
||||
In particular, DDC adds the following:
|
||||
|
||||
- Stricter (but fewer) runtime type checks
|
||||
- Reified type narrowing
|
||||
- Restricted `is`/`as` checks
|
||||
|
||||
In all these cases, DDC (with static checks) is stricter than standard checked mode (or production mode). It may reject (either statically or at runtime) programs that run correctly in checked mode (similar to how checked mode may reject programs that run in production mode).
|
||||
|
||||
On the other hand, programs that statically check and run correctly in DDC should also run the same in checked mode. A caveat to note is that mirrors (or `runtimeType`) may show a more narrow type in DDC (though, in practice, programmers are discouraged from using these features for performance / code size reasons).
|
||||
|
||||
## Runtime checks
|
||||
|
||||
In practice, strong mode enforces most type annotations at compile time, and, thus, requires less work at runtime to enforce safety. Consider the following Dart code:
|
||||
|
||||
```dart
|
||||
String foo(Map<int, String> map, int x) {
|
||||
return map[x.abs()];
|
||||
}
|
||||
```
|
||||
|
||||
Strong mode enforces that the function `foo` is only invoked in a manner consistent with its signature. DDC - which assumes strong mode static checking - inserts no further runtime checks. In contrast, standard Dart checked mode would check the type of the parameters -- `map` and `x` -- along with the type of the return value at runtime on every invocation of `foo`. Even Dart production mode, depending on the implementation and its ability to optimize, may require similar checking to dynamically dispatch the map lookup and the method call in the body of `foo`.
|
||||
|
||||
Nevertheless, there are cases where DDC still requires runtime checks. (Note: DDC may eventually provide a mode to elide these checks, but this would violate soundness and is beyond the scope of this document.)
|
||||
|
||||
### Implicit casts
|
||||
|
||||
Dart has flexible assignability rules. Programmers are not required to explicitly cast from supertypes to subtypes. For example, the following is valid Dart:
|
||||
|
||||
```dart
|
||||
Object o = ...;
|
||||
String s = o; // Implicit downcast
|
||||
String s2 = s.substring(1);
|
||||
```
|
||||
|
||||
The assignment to `s` is an implicit downcast from `Object` to `String` and triggers a runtime check in DDC to ensure it is correct.
|
||||
|
||||
Note that checked mode would also perform this runtime test. Unlike checked mode, DDC would not require a check on the assignment to `s2` - this type is established statically.
|
||||
|
||||
### Inferred variables
|
||||
|
||||
Dart's inference may narrow the static type of certain variables. If the variable is mutable, DDC enforces the narrower type at runtime when necessary.
|
||||
|
||||
In the following example, strong mode will infer of the type of the local variable `y` as an `int`:
|
||||
|
||||
```dart
|
||||
int bar(Object x) {
|
||||
var y = 0;
|
||||
if (x != null) {
|
||||
y = x;
|
||||
}
|
||||
return y.abs();
|
||||
}
|
||||
```
|
||||
|
||||
This allows it to, for example, static verify the call to `y.abs()` and determine that it returns an `int`. However, the parameter `x` is typed as `Object` and the assignment from `x` to `y` now requires a type check to ensure that `y` is only assigned an `int`.
|
||||
|
||||
Note, strong mode and DDC are conservative by enforcing a tighter type than required by standard Dart checked mode. For example, checked mode would accept a non-`int` `x` with an `abs` method that happened to return an `int`. In strong mode, a programmer would have to explicitly opt into this behavior by annotating `y` as an `Object` or `dynamic`.
|
||||
|
||||
### Covariant generics
|
||||
|
||||
Strong mode preserves the covariance of Dart's generic classes. To support this soundly, DDC injects runtime checks on parameters in method invocations whose type is a class type parameter. Consider the call to `baz` in the parameterized class `A`:
|
||||
|
||||
```dart
|
||||
class A<T> {
|
||||
T baz(T x, int y) => x;
|
||||
}
|
||||
|
||||
void foo(A<Object> a) {
|
||||
a.baz(42, 38);
|
||||
}
|
||||
|
||||
void main() {
|
||||
var aString = new A<String>();
|
||||
foo(aString);
|
||||
}
|
||||
```
|
||||
|
||||
Statically, sound mode will not generate an error or warning on this code. The call to `baz` in `foo` is statically valid as `42` is an `Object` (as required by the static type of `a`). However, the runtime type of `a` in this example is the narrower `A<String>`. At runtime, when baz is executed, DDC will check that the type of `x` matches the reified type parameter and, in this example, fail.
|
||||
|
||||
Note, only `x` requires a runtime check. Unlike checked mode, no runtime check is required for `y` or the return value. Both are statically verified.
|
||||
|
||||
### Dynamic operations
|
||||
|
||||
Strong mode allows programmers to explicitly use `dynamic` as a type. It also allows programmers to omit types, and in some of these cases inference may fall back on `dynamic` if it cannot determine a static type. In these cases, DDC inserts runtime checks (typically in the form of runtime helper calls).
|
||||
|
||||
For example, in the following:
|
||||
|
||||
```dart
|
||||
int foo(int x) => x + 1;
|
||||
|
||||
void main() {
|
||||
dynamic bar = foo;
|
||||
bar("hello"); // DDC runtime error
|
||||
}
|
||||
```
|
||||
|
||||
`foo` (via `bar`) is incorrectly invoked on a `String`. There is no static error as `bar` is typed `dynamic`. Instead DDC, performs extra runtime checking on the invocation of `bar`. In this case, it would generate a runtime type error. Note, if the type of `bar` had been omitted, it would have been inferred, and the error would have been reported statically.
|
||||
|
||||
Nevertheless, there are situations where programmers may prefer a dynamic type for flexibility.
|
||||
|
||||
## Runtime type Narrowing
|
||||
|
||||
Strong mode statically infers tighter types for functions and generics. In DDC, this is reflected in the reified type at runtime. This allows DDC to enforce the stricter type soundly at runtime when necessary.
|
||||
|
||||
In particular, this means that DDC may have a stricter concrete runtime type than other Dart implementations for generic classes and functions. The DDC type will always be a subtype.
|
||||
|
||||
This will impact execution in the following ways:
|
||||
- DDC may trigger runtime errors where checked mode is forgiving.
|
||||
- Code that uses reflection may observe a narrower type in DDC.
|
||||
|
||||
### Allocation inference
|
||||
|
||||
When strong infers a narrower type for a closure literal or other allocation expression, DDC reifies this narrower type at runtime. As a result, it can soundly enforce typing errors at runtime.
|
||||
|
||||
The following is an example of where static checking fails to catch a typing error:
|
||||
|
||||
```dart
|
||||
apply(int g(x), y) {
|
||||
print(g(y));
|
||||
}
|
||||
|
||||
typedef int Int2Int(int x);
|
||||
|
||||
void main() {
|
||||
Int2Int f = (x) => x + x;
|
||||
apply(f, "hello");
|
||||
}
|
||||
```
|
||||
|
||||
A programmer examining `apply` would reasonably expect it to print an `int` value. The analyzer (with or without strong mode) fails to report a problem. Standard Dart checked simply prints `"hellohello"`. In DDC, however, a runtime error is thrown on the application of `g` in `apply`. The closure literal assigned to `f` in `main` is reified as an `int -> int`, and DDC enforces this at runtime.
|
||||
|
||||
In this example, if `apply` and its parameters were fully typed, strong mode would report a static error, and DDC would impose no runtime check.
|
||||
|
||||
### Generic methods
|
||||
|
||||
[Note: This is not yet implemented correctly.](https://github.com/dart-lang/dev_compiler/issues/301)
|
||||
|
||||
Similarly, DDC requires that [generic methods](GENERIC_METHODS.md) return the correct reified type. In strong mode, `Iterable.map` is a generic method. In DDC, `lengths` in `main` will have a reified type of `List<int>`. In `foo`, this will trigger a runtime error when a string is added to the list.
|
||||
|
||||
```dart
|
||||
void foo(List l) {
|
||||
l.add("a string");
|
||||
}
|
||||
|
||||
void main() {
|
||||
Iterable<String> list = <String>["hello", "world"];
|
||||
List<int> lengths = list.map((x) => x.length).toList();
|
||||
foo(lengths);
|
||||
print(lengths[2]);
|
||||
}
|
||||
```
|
||||
|
||||
Standard checked mode would print `"a string"` without error.
|
||||
|
||||
## Is / As restrictions
|
||||
|
||||
In standard Dart, `is` and `as` runtime checks expose the unsoundness of the type system in certain cases. For example, consider:
|
||||
|
||||
```dart
|
||||
var list = ["hello", "world"];
|
||||
if (list is List<int>) {
|
||||
...
|
||||
} else if (list is List<String>) {
|
||||
...
|
||||
}
|
||||
```
|
||||
|
||||
Perhaps surprisingly, the first test - `list is List<int>` - evaluates to true here. Such code is highly likely to be erroneous.
|
||||
|
||||
Strong mode provides a stricter subtyping check and DDC enforces this at runtime. For compatibility with standard Dart semantics, however, DDC throws a runtime error when an `is` or `as` check would return a different answer with strong mode typing semantics.
|
||||
|
||||
In the example above, the first `is` check would generate a runtime error.
|
||||
|
||||
Note, we are exploring making this a static error or warning in strong mode. In general, an expression:
|
||||
|
||||
```dart
|
||||
x is T
|
||||
```
|
||||
|
||||
or
|
||||
|
||||
```dart
|
||||
x as T
|
||||
```
|
||||
|
||||
is only guaranteed safe when `T` is a *ground type*:
|
||||
|
||||
- A non-generic class type (e.g., `Object`, `String`, `int`, ...).
|
||||
- A generic class type where all type parameters are implicitly or explicitly `dynamic` (e.g., `List<dynamic>`, `Map`, …).
|
||||
- A function type where the return type and all parameter types are `dynamic` (e.g., (`dynamic`, `dynamic`) -> `dynamic`, ([`dynamic`]) -> `dynamic`).
|
||||
413
pkg/dev_compiler/doc/STATIC_SAFETY.md
Normal file
413
pkg/dev_compiler/doc/STATIC_SAFETY.md
Normal file
|
|
@ -0,0 +1,413 @@
|
|||
# Strong Mode Static Checking
|
||||
|
||||
## Overview
|
||||
|
||||
The Dart programming language has an optional, unsound type system. Although it is similar in appearance to languages such as Java, C#, or C++, its type system and static checking are fundamentally different. It permits erroneous behavior in ways that may be surprising to programmers coming from those and other conventional typed languages.
|
||||
|
||||
In Dart, static type annotations can be often misleading. Dart code such as:
|
||||
|
||||
```dart
|
||||
var list = ["hello", "world"];
|
||||
List<int> listOfInts = list;
|
||||
```
|
||||
|
||||
produces neither static nor runtime errors. Actual errors may show up much later on, e.g., with the following code, only at runtime on the invocation of `abs`:
|
||||
|
||||
```dart
|
||||
Iterable<int> iterableOfInts = listOfInts.map((i) => i.abs());
|
||||
```
|
||||
|
||||
Strong mode aims to catch such errors early by validating that variables - e.g., `listOfInts` - actually match their corresponding static type annotations - e.g., `List<int>`. It constrains the Dart programming language to a subset of programs that type check under a restricted set of rules. It statically rejects examples such as the above.
|
||||
|
||||
To accomplish this, strong mode involves the following:
|
||||
|
||||
- **Type inference**. Dart’s standard type rules treats untyped variables as `dynamic`, which
|
||||
suppresses any static warnings on them. Strong mode infers static types based upon context. In the example above, strong mode infers that `list` has type `List`. Note, in strong mode, programmers may still explicitly use the `dynamic` type.
|
||||
|
||||
- **Strict subtyping**. Dart’s primary sources of unsoundness are due to its subtyping rules on function types and generic classes. Strong mode restricts these: e.g., `List` may not used as `List<int>` in the example above.
|
||||
|
||||
- **Generic methods**. Standard Dart does not yet provide generic methods. This makes certain polymorphic methods difficult to use soundly. For example, the `List.map` invocation above is statically typed to return an `Iterable<dynamic>` in standard Dart. Strong mode allows methods to be annotated as generic. `List.map` is statically typed to return an `Iterable<T>` where `T` is bound to `int` in the previous example. A number of common higher-order methods are annotated and checked as generic in strong mode, and programmers may annotate their own methods as well.
|
||||
|
||||
Strong mode is designed to work in conjunction with the Dart Dev Compiler (DDC), which uses static type verification to generate better code. DDC augments strong mode static checking with a minimal set of [runtime checks](RUNTIME_SAFETY.md) that aim to provide full soundness of types.
|
||||
|
||||
Strong mode static analysis may also be used alone for stricter error checking.
|
||||
|
||||
Formal details of the strong mode type system may be found [here](https://dart-lang.github.io/dev_compiler/strong-dart.pdf).
|
||||
|
||||
## Usage
|
||||
|
||||
Strong mode is now integrated into the Dart Analyzer. The analyzer may be invoked in strong mode as follows:
|
||||
|
||||
$ dartanalyzer --strong myapp.dart
|
||||
|
||||
Strong mode may also be enabled in IDEs by creating (if necessary) an `.analysis_options` file in your project and appending the following entry to it:
|
||||
|
||||
```
|
||||
analyzer:
|
||||
strong-mode: true
|
||||
```
|
||||
|
||||
## Type Inference
|
||||
|
||||
With strong mode, we want to provide stronger typing while preserving the
|
||||
terseness of Dart. [Idiomatic Dart
|
||||
code](https://www.dartlang.org/effective-dart/) discourages type annotations
|
||||
outside of API boundaries, and user shouldn't have to add more types to get
|
||||
better checking. Instead, strong mode uses type inference.
|
||||
|
||||
In Dart, per the specification, the static type of a variable `x` declared as:
|
||||
|
||||
```dart
|
||||
var x = <String, String>{ "hello": "world"};
|
||||
```
|
||||
|
||||
is `dynamic` as there is no explicit type annotation on the left-hand side. To discourage code bloat, the Dart style guide generally recommends omitting these type annotations in many situations. In these cases, the benefits of strong mode would be lost.
|
||||
|
||||
To avoid this, strong mode uses type inference. In the case above, strong mode infers and enforces the type of `x` as `Map<String, String>`. An important aspect to inference is ordering: when an inferred type may be used to infer another type. To maximize the impact, we perform the following inference:
|
||||
|
||||
- Top-level and static fields
|
||||
- Instance fields and methods
|
||||
- Local variables
|
||||
- Constructor calls and literals
|
||||
- Generic method invocations
|
||||
|
||||
Inference may tighten the static type as compared to the Dart specification. An implicitly dynamic type, either alone or in the context of a function or generic parameter type, is inferred to a more specific type. This inference may result in stricter type errors than standard Dart.
|
||||
|
||||
In [DDC](RUNTIME_SAFETY.md), inference may also affect the reified runtime type.
|
||||
|
||||
### Top-level and Static Fields
|
||||
|
||||
Strong mode infers any untyped top-level field or static field from the type of
|
||||
its initializer. The static type of the declared variable is inferred as the static type of the initializer. For example, consider:
|
||||
|
||||
```dart
|
||||
var PI = 3.14159;
|
||||
var radius = 2;
|
||||
var circumference = 2 * PI * radius;
|
||||
```
|
||||
|
||||
Strong mode infers the static type of `PI` as `double` and `radius` as `int` directly from their initializers. It infers the static type of `circumference` as `double`, transitively using the other inferred types. Standard Dart rules would treat all of these static types as `dynamic`. Note that the following later assignment would be allowed in standard Dart, but disallowed (as a static type error) in strong mode:
|
||||
```dart
|
||||
radius = "five inches";
|
||||
```
|
||||
Strong mode inference avoids circular dependences. If a variable’s initializer expression refers to another variable whose type would be dependent (directly or indirectly) on the first, the static type of that other variable is treated as `dynamic` for the purpose of inference.
|
||||
|
||||
### Instance Fields and Methods
|
||||
|
||||
Strong mode performs two types of inference on instance fields and methods.
|
||||
|
||||
The first uses base types to constrain overrides in subtypes. Consider the following example:
|
||||
|
||||
```dart
|
||||
abstract class A {
|
||||
Map get m;
|
||||
int value(int i);
|
||||
}
|
||||
|
||||
class B extends A {
|
||||
var m;
|
||||
value(i) => m[i];
|
||||
…
|
||||
}
|
||||
```
|
||||
|
||||
In Dart, overridden method, getter, or setter types should be subtypes of the corresponding base class ones (otherwise, static warnings are given). In standard Dart, the above declaration of `B` is not an error: both `m`’s getter type and `value`’s return type are `dynamic`.
|
||||
|
||||
Strong mode -- without inference -- would disallow this: if `m` in `B` could be assigned any kind of object, including one that isn't a Map, it would violate the type contract in the declaration of `A`.
|
||||
|
||||
However, rather than rejecting the above code, strong mode employs inference to tighten the static types to obtain a valid override. The corresponding types in B are inferred as if it was:
|
||||
|
||||
```dart
|
||||
class B extends A {
|
||||
Map m;
|
||||
int value(int i) => m[i];
|
||||
…
|
||||
}
|
||||
```
|
||||
|
||||
Note that tightening the argument type for `i` to `int` is not required for soundness; it is done for convenience as it is the typical intent. The programmer may explicitly type this as `dynamic` or `Object` to avoid inferring the narrower type.
|
||||
|
||||
The second form inference is limited to instance fields (not methods) and is similar to that on static fields. For instance fields where the static type is omitted and an initializer is present, the field’s type is inferred as the initializer’s type. In this continuation of our example:
|
||||
|
||||
```dart
|
||||
class C extends A {
|
||||
var y = 42;
|
||||
var m = <int, int>{ 0: 38};
|
||||
...
|
||||
}
|
||||
```
|
||||
|
||||
the instance field `y` has inferred type `int` based upon its initializer. Note that override-based inference takes precedence over initializer-based inference. The instance field `m` has inferred type `Map`, not `Map<int, int>` due to the corresponding declaration in `A`.
|
||||
|
||||
### Local Variables
|
||||
|
||||
As with fields, local variable types are inferred if the static type is omitted and an initializer expression is present. In the following example:
|
||||
|
||||
```dart
|
||||
Object foo(int x) {
|
||||
final y = x + 1;
|
||||
var z = y * 2;
|
||||
return z;
|
||||
}
|
||||
```
|
||||
|
||||
the static types of `y` and `z` are both inferred as `int` in strong mode. Note that local inference is done in program order: the inferred type of `z` is computed using the inferred type of `y`. Local inference may result in strong mode type errors in otherwise legal Dart code. In the above, a second assignment to `z` with a string value:
|
||||
```dart
|
||||
z = "$z";
|
||||
```
|
||||
would trigger a static error in strong mode, but is allowed in standard Dart. In strong mode, the programmer must use an explicit type annotation to suppress inference. Explicitly declaring `z` with the type `Object` or `dynamic` would suffice in this case.
|
||||
|
||||
### Constructor Calls and Literals
|
||||
|
||||
Strong mode also performs contextual inference on allocation expressions. This inference is rather different from the above: it tightens the runtime type of the corresponding expression using the static type of its context. Contextual inference is used on expressions that allocate a new object: closure literals, map and list literals, and explicit constructor invocations (i.e., via `new` or `const`).
|
||||
|
||||
In DDC, these inferred types are also [reified at runtime](RUNTIME_SAFETY.md) on the newly allocated objects to provide a stronger soundness guarantee.
|
||||
|
||||
#### Closure literals
|
||||
|
||||
Consider the following example:
|
||||
|
||||
```dart
|
||||
int apply(int f(int arg), int value) {
|
||||
return f(value);
|
||||
}
|
||||
|
||||
void main() {
|
||||
int result =
|
||||
apply((x) { x = x * 9 ~/ 5; return x + 32; }, 41);
|
||||
print(result);
|
||||
}
|
||||
```
|
||||
|
||||
The function `apply` takes another function `f`, typed `(int) -> int`, as its first argument. It is invoked in `main` with a closure literal. In standard Dart, the static type of this closure literal would be `(dynamic) -> dynamic`. In strong mode, this type cannot be safely converted to `(int) -> int` : it may return a `String` for example.
|
||||
|
||||
Dart has a syntactic limitation in this case: it is not possible to statically annotate the return type of a closure literal.
|
||||
|
||||
Strong mode sidesteps this difficulty via contextual inference. It infers the closure type as `(int) -> int`. Note, this may trigger further inference and type checks in the body of the closure.
|
||||
|
||||
#### List and map literals
|
||||
|
||||
Similarly, strong mode infers tighter runtime types for list and map literals. E.g., in
|
||||
|
||||
```dart
|
||||
List<String> words = [ "hello", "world" ];
|
||||
```
|
||||
|
||||
the runtime type is inferred as `List<String>` in order to match the context of the left hand side. In other words, the code above type checks and executes as if it was:
|
||||
|
||||
```dart
|
||||
List<String> words = <String>[ "hello", "world" ];
|
||||
```
|
||||
|
||||
Similarly, the following will now trigger a static error in strong mode:
|
||||
|
||||
```dart
|
||||
List<String> words = [ "hello", 42 ]; // Strong Mode Error: 42 is not a String
|
||||
```
|
||||
|
||||
Contextual inference may be recursive:
|
||||
|
||||
```dart
|
||||
Map<List<String>, Map<int, int>> map =
|
||||
{ ["hello"]: { 0: 42 }};
|
||||
```
|
||||
|
||||
In this case, the inner map literal is inferred as a `Map<int, int>`. Note, strong mode will statically reject code where the contextually required type is not compatible. This will trigger a static error:
|
||||
|
||||
```dart
|
||||
Map<List<String>, Map<int, int>> map =
|
||||
{ ["hello"]: { 0: "world" }}; // STATIC ERROR
|
||||
```
|
||||
|
||||
as "world" is not of type `int`.
|
||||
|
||||
#### Constructor invocations
|
||||
|
||||
Finally, strong mode performs similar contextual inference on explicit constructor invocations via `new` or `const`. For example:
|
||||
|
||||
```dart
|
||||
Set<String> string = new Set.from(["hello", "world"]);
|
||||
```
|
||||
|
||||
is treated as if it was written as:
|
||||
|
||||
```dart
|
||||
Set<String> string =
|
||||
new Set<String>.from(<String>["hello", "world"]);
|
||||
```
|
||||
|
||||
Note, as above, context is propagated downward into the expression.
|
||||
|
||||
## Strict subtyping
|
||||
|
||||
The primary sources of unsoundness in Dart are generics and functions. Both introduce circularity in the Dart subtyping relationship.
|
||||
|
||||
### Generics
|
||||
|
||||
Generics in Dart are covariant, with the added rule that the `dynamic` type may serve as both ⊤ (top) and ⊥ (bottom) of the type hierarchy in certain situations. For example, let *<:<sub>D</sub>* represent the standard Dart subtyping rule. Then, for all types `S` and `T`:
|
||||
|
||||
`List<S>` <:<sub>D</sub> `List<dynamic>` <:<sub>D</sub> `List<T>`
|
||||
|
||||
where `List` is equivalent to `List<dynamic>`. This introduces circularity - e.g.:
|
||||
|
||||
`List<int>` <:<sub>D</sub> `List` <:<sub>D</sub> `List<String>`<:<sub>D</sub> `List` <:<sub>D</sub> `List<int>`
|
||||
|
||||
From a programmer’s perspective, this means that, at compile-time, values that are statically typed `List<int>` may later be typed `List<String>` and vice versa. At runtime, a plain `List` can interchangeably act as a `List<int>` or a `List<String>` regardless of its actual values.
|
||||
|
||||
Our running example exploits this. A `MyList` may be passed to the `info` function as it’s a subtype of the expected type:
|
||||
|
||||
`MyList` <:<sub>D</sub> `List` <:<sub>D</sub>`List<int>`
|
||||
|
||||
In strong mode, we introduce a stricter subtyping rule <:<sub>S</sub> to disallow this. In this case, in the context of a generic type parameter, dynamic may only serve as ⊤. This means that this is still true:
|
||||
|
||||
`List<int>` <:<sub>S</sub> `List`
|
||||
|
||||
but that this is not:
|
||||
|
||||
`List<int>` ~~<:<sub>S</sub> `List`~~
|
||||
|
||||
Our running example fails in strong mode:
|
||||
|
||||
`MyList` <:<sub>S</sub> `List` ~~<:<sub>S</sub> `List<int>`~~
|
||||
|
||||
|
||||
### Functions
|
||||
|
||||
The other primary source of unsoundness in Dart is function subtyping. An unusual feature of the Dart type system is that function types are bivariant in both the parameter types and the return type (see Section 19.5 of the [Dart specification][dartspec]). As with generics, this leads to circularity:
|
||||
|
||||
`(int) -> int` <:<sub>D</sub> `(Object) -> Object` <:<sub>D</sub> `(int) -> int`
|
||||
|
||||
And, as before, this can lead to surprising behavior. In Dart, an overridden method’s type should be a subtype of the base class method’s type (otherwise, a static warning is given). In our running example, the (implicit) `MyList.length` getter has type:
|
||||
|
||||
`() -> Object`
|
||||
|
||||
while the `List.length` getter it overrides has type:
|
||||
|
||||
`() -> int`
|
||||
|
||||
This is valid in standard Dart as:
|
||||
|
||||
`() -> Object` <:<sub>D</sub> `() -> int`
|
||||
|
||||
Because of this, a `length` that returns "hello" (a valid `Object`) triggers no static or runtime warnings or errors.
|
||||
|
||||
Strong mode enforces the stricter, [traditional function subtyping](https://en.wikipedia.org/wiki/Subtyping#Function_types) rule: subtyping is contravariant in parameter types and covariant in return types. This permits:
|
||||
|
||||
`() -> int` <:<sub>S</sub> `() -> Object`
|
||||
|
||||
but disallows:
|
||||
|
||||
`() -> Object` <:<sub>S</sub> `() -> int`
|
||||
|
||||
With respect to our example, strong mode requires that any subtype of a List have an int-typed length. It statically rejects the length declaration in MyList.
|
||||
|
||||
## Generic Methods
|
||||
|
||||
Strong mode introduces generic methods to allow more expressive typing on polymorphic methods. Such code in standard Dart today often loses static type information. For example, the `Iterable.map` method is declared as below:
|
||||
|
||||
```dart
|
||||
abstract class Iterable<E> {
|
||||
...
|
||||
Iterable map(f(E e));
|
||||
}
|
||||
```
|
||||
|
||||
Regardless of the static type of the function `f`, the `map` always returns an `Iterable<dynamic>` in standard Dart. As result, standard Dart tools miss the obvious error on the following code:
|
||||
|
||||
```dart
|
||||
Iterable<int> results = <int>[1, 2, 3].map((x) => x.toString()); // Static error only in strong mode
|
||||
```
|
||||
|
||||
The variable `results` is statically typed as if it contains `int` values, although it clearly contains `String` values at runtime.
|
||||
|
||||
The [generic methods proposal](https://github.com/leafpetersen/dep-generic-methods/blob/master/proposal.md) adds proper generic methods to the Dart language as a first class language construct and to make methods such as the `Iterable.map` generic.
|
||||
|
||||
To enable experimentation, strong mode provides a [generic methods prototype](GENERIC_METHODS.md) based on the existing proposal, but usable on all existing Dart implementations today. Strong mode relies on this to report the error on the example above.
|
||||
|
||||
The `Iterable.map` method is now declared as follows:
|
||||
|
||||
```dart
|
||||
abstract class Iterable<E> {
|
||||
...
|
||||
Iterable/*<T>*/ map/*<T>*/(/*=T*/ f(E e));
|
||||
}
|
||||
```
|
||||
|
||||
At a use site, the generic type may be explicitly provided or inferred from context:
|
||||
|
||||
```
|
||||
var l = <int>[1, 2, 3];
|
||||
var i1 = l.map((i) => i + 1);
|
||||
var l2 = l.map/*<String>*/((i) { ... });
|
||||
```
|
||||
|
||||
In the first invocation of `map`, the closure is inferred (from context) as `int -> int`, and the generic type of map is inferred as `int` accordingly. As a result, `i1` is inferred as `Iterable<int>`. In the second, the type parameter is explicitly bound to `String`, and the closure is checked against this type. `i2` is typed as `Iterable<String>`.
|
||||
|
||||
Further details on generic methods in strong mode and in DDC may be found [here](GENERIC_METHODS.md).
|
||||
|
||||
## Additional Restrictions
|
||||
|
||||
In addition to stricter typing rules, strong mode enforces other
|
||||
restrictions on Dart programs.
|
||||
|
||||
### Warnings as Errors
|
||||
|
||||
Strong mode effectively treats all standard Dart static warnings as static errors. Most of these warnings are required for soundness (e.g., if a concrete class is missing methods required by a declared interface). A full list of Dart static warnings may found in the [Dart specification][dartspec], or enumerated here:
|
||||
|
||||
[https://github.com/dart-lang/sdk/blob/master/pkg/analyzer/lib/src/generated/error.dart#L3772](https://www.google.com/url?q=https%3A%2F%2Fgithub.com%2Fdart-lang%2Fsdk%2Fblob%2Fmaster%2Fpkg%2Fanalyzer%2Flib%2Fsrc%2Fgenerated%2Ferror.dart%23L3772&sa=D&sntz=1&usg=AFQjCNFc4E37M1PshVcw4zk7C9jXgqfGbw)
|
||||
|
||||
### Super Invocations
|
||||
|
||||
In the context of constructor initializer lists, strong mode restricts `super` invocations to the end. This restriction simplifies generated code with minimal effect on the program.
|
||||
|
||||
### For-in loops
|
||||
|
||||
In for-in statements of the form:
|
||||
|
||||
```dart
|
||||
for (var i in e) { … }
|
||||
```
|
||||
|
||||
Strong mode requires the expression `e` to be an `Iterable`. When the loop variable `i` is also statically typed:
|
||||
|
||||
```dart
|
||||
for (T i in e) { … }
|
||||
```
|
||||
|
||||
the expression `e` is required to be an `Iterable<T>`.
|
||||
|
||||
*Note: we may weaken these.*
|
||||
|
||||
### Field overrides
|
||||
|
||||
By default, fields are overridable in Dart.
|
||||
|
||||
```dart
|
||||
int init(int n) {
|
||||
print('Initializing with $n');
|
||||
return n;
|
||||
}
|
||||
|
||||
class A {
|
||||
int x = init(42);
|
||||
}
|
||||
|
||||
class B extends A {
|
||||
int x;
|
||||
}
|
||||
```
|
||||
|
||||
Disallow overriding fields: this results in complicated generated
|
||||
code where a field definition in a subclass shadows the field
|
||||
definition in a base class but both are generally required to be
|
||||
allocated. Users should prefer explicit getters and setters in such
|
||||
cases. See [issue 52](https://github.com/dart-lang/dev_compiler/issues/52).
|
||||
|
||||
### Open Items
|
||||
|
||||
- Is / As restrictions: Dart's `is` and `as` checks are unsound for certain types
|
||||
(generic classes, certain function types). In [DDC](RUNTIME_SAFETY.md), problematic
|
||||
`is` and `as` checks trigger runtime errors. We are considering introducing static
|
||||
errors for these cases.
|
||||
|
||||
[dartspec]: https://www.dartlang.org/docs/spec/ "Dart Language Spec"
|
||||
Loading…
Reference in a new issue