Add --no-implicit-dynamic flag to analyzer

[floitschG]

It would be nice to have a --no-implicit-dynamic flag on the analyzer. It should give a warning when the analyzer can't statically infer the type of a "var" (or missing type). This would be equivalent to C#'s --no-implicit-any [0].
The most important property of this flag should be that refactorings are guaranteed to find all uses of a class or a function. Furthermore, there should be no NSM errors (except for null-pointer exceptions).

Examples:

foo() => 499;  // OK: inferred int.
var x = foo();  // OK: inferred int.
bar(x) { return x < 0 ? "str" : false; }  // warning: can't infer type.
// Open questions:
var x = ["str", 499];   // maybe ok depending on use?
x.length;  // OK: supported by List.
var element = x[0];  // should probably be a warning.
x[0].substring(1);   // should probably be a warning.

[0] http://blogs.msdn.com/b/typescript/archive/2013/08/06/announcing-0-9-1.aspx

[eernstg]

Yes, please!

However, it would be easier to maintain the specified language semantics if
we require annotations (as they do for TypeScript in the blog entry you
mentioned) than it is if we infer any missing type annotations. In
particular, if it is inferred that [3.14, 499] means <num>[3.14, 499]
then x.add("str") will fail in checked mode and if it means
<Object>[3.14, 499] then List<num> myNumbers = x; will fail (contrary
to the spec in both cases). Why not let the IDEs offer quickfixes such that
missing type annotations can easily be added by programmers? They would
then get the chance to decide whether they intend one or the other. The
IDEs could even use folding to make the resulting code look nice! ;-)

On Wed, Sep 2, 2015 at 10:26 AM, Florian Loitsch notifications@github.com
wrote:

It would be nice to have a --no-implicit-dynamic flag on the analyzer. It
should give a warning when the analyzer can't statically infer the type of
a "var" (or missing type). This would be equivalent to C#'s
--no-implicit-any [0].
The most important property of this flag should be that refactorings are
guaranteed to find all uses of a class or a function. Furthermore, there
should be no NSM errors (except for null-pointer exceptions).

Examples:

foo() => 499; // OK: inferred int.
var x = foo(); // OK: inferred int.
bar(x) { return x < 0 ? "str" : false; } // warning: can't infer type.
// Open questions:
var x = ["str", 499]; // maybe ok depending on use?
x.length; // OK: supported by List.
var element = x[0]; // should probably be a warning.
x[0].substring(1); // should probably be a warning.

[0]
http://blogs.msdn.com/b/typescript/archive/2013/08/06/announcing-0-9-1.aspx

—
Reply to this email directly or view it on GitHub
#24267.

Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 København K, Denmark
CVR no. 28866984

[floitschG]

How can the analyzer affect the specified language semantics? --no-implicit-dynamic should only exist in the analyzer. Neither dart2js nor the VM need to know about it (although dart2js could also potentially implement it, since they already cover a lot of what the analyzer does).

I don't see the annotation in the blog entry.

The analyzer/IDE should tell the user when it cannot infer a specific type (at least when it could lead to a NSM) and require the least amount of code to get to a clean state. This is different from strong mode which follows strict rules. The analyzer can be much more sophisticated (in the same way that dart2js' type inference propagates types much further than the strong-mode rules could ever specify).

[eernstg]

On Wed, Sep 2, 2015 at 1:26 PM, Florian Loitsch notifications@github.com
wrote:

How can the analyzer affect the specified language semantics?
--no-implicit-dynamic should only exist in the analyzer. Neither
dart2js nor the VM need to know about it (although dart2js could also
potentially implement it, since they already cover a lot of what the
analyzer does).

I don't see the annotation in the blog entry.

Oops, I misread: For TypeScript with --noImplicitAny they only complain if
the type any is inferred, inferring other types is OK.

But I think that inferring types for Dart that do not correspond to the
language semantics is dangerous, it would be much better to aim for an
adjusted language semantics such that those inferred types would be aligned
with the semantics. For instance, with

var x = foo(); // OK: inferred int.

we should either infer dynamic or make it a runtime error in checked mode
to do x = "Hello"; in the next line.

The analyzer/IDE should tell the user when it cannot infer a specific type
(at least when it could lead to a NSM) and require the least amount of code
to get to a clean state. This is different from strong mode which follows
strict rules.

Interesting! ;)

In order to be able to promise "no NSM" we need a suitable invariant on the
heap (e.g., checking values on the way into all variables, as checked mode
mostly does). But even that would be difficult to strengthen sufficiently
in the case where we have some explicit occurrences of dynamic:

List<String> myStrings = <dynamic>[];
myStrings.add(2);
myStrings[0].toUpperCase();  // "NSM"

The instance of List<dynamic> may of course have been transferred from
anywhere in the program to myStrings, so we'd need global analysis of the
data flow in order to try to keep track of objects like that --- which is
not typically considered to be a nice task for a type checker ..

The analyzer can be much more sophisticated (in the same way that dart2js'
type inference propagates types much further than the strong-mode rules
could ever specify).

.. and even though dart2js does in fact perform exactly such an analysis,
it will have to be a conservative approximation, and it won't produce
results that are valid for your next program where any given piece of code
is used in the context of a different set of libraries.

best regards,

Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 København K, Denmark
CVR no. 28866984

[floitschG]

There is already too much noise, but to clarify my request:
for every 'var' (or missing type) the analyzer should find a type (potentially even union type) that makes the variable's uses warning free. If it can't find such a type it should warn the user that it needs to work with the variable as if it was 'dynamic' (and therefore won't be able to warn for any of its uses, and won't be able to do proper refactorings).
The analyzer should not need to follow hard-coded rules (Dart typing-rules, or strong mode) as these generally limit what the analyzer can do.

I would be happy if the analyzer furthermore inferred a new type for every assignment (but that's not a requirement and probably makes the reporting harder).

var x = 499;
print(x * 32);
if (...) {
  x = "str";  // Find new type for x.
  print(x.substring(2));
}  // Merge the two paths -> 'int|String'.
print(x);  // OK: since the union-type int|String supports 'toString'.

[leafpetersen]

This seems like a worthwhile idea, but I don't think either of these claims are true, unless you propose to change the type system:

The most important property of this flag should be that refactorings are guaranteed to find all uses of a
class or a function. Furthermore, there should be no NSM errors (except for null-pointer exceptions).

The program attached below illustrates this. It is fully annotated - there are no variables or expressions of type dynamic anywhere in the program, it passes the analyzer with no warnings, and yet refactoring based on the types will change the production mode semantics. Changing the name of the A.foo method will introduce a NSM error (while preserving the "no-dynamic" property). Changing the name of the B.foo method will also introduce a NSM error. Changing the name of one of these methods to something that is already implemented by the other class could introduce other arbitrary changes in behavior.

This program does throw in checked mode, but if these types were the result of inference (rather than being fully annotated), then the code would run fine in checked mode as well, but again, refactoring would change the semantics.

// This program has no expressions or variables of type dynamic.
class A {
  void foo() => print("A's foo");
}

class B {
  void foo() => print("B's foo");
}

typedef A V2A();

typedef B V2B();

typedef Object V2O();

// The static type of f() is A, but B.foo can reach this call site.
void callsAFoo(V2A f) => f().foo();

void mixesThingsUp(V2O f) => callsAFoo(f);

void losesACallToBFoo(V2B f) => mixesThingsUp(f);

B mkB() => new B();

void main() {
  losesACallToBFoo(mkB);
}

[eernstg]

Sorry about the additional noise, but it's just too tempting to add a
comment here:

Using the very flexible notion of function type subtyping it is even OK to
skip a couple of steps in this example:

// This program has no expressions or variables of type dynamic.
class A {
void foo() => print("A's foo");
}

class B {
void foo() => print("B's foo");
}

typedef A V2A();
typedef B V2B();
typedef Object V2O();

// The static type of f() is A, but B.foo can reach this call site.
void callsAFoo(V2A f) => f().foo();

Object mkB() => new B();

void main() {
callsAFoo(mkB);
}

The dartanalyzer is happy, checked mode execution is happy, and we still
get "B's foo". (Yes, we need to strengthen function subtyping to require
covariant return types). The "refactoring correctness" property actually
seems to be very nearly identical to message-safety (DLS-15), so the
connection is not surprising.

On Wed, Sep 2, 2015 at 6:38 PM, Leaf Petersen notifications@github.com
wrote:

This seems like a worthwhile idea, but I don't think either of these
claims are true, unless you propose to change the type system:

The most important property of this flag should be that refactorings are
guaranteed to find all uses of a
class or a function. Furthermore, there should be no NSM errors (except
for null-pointer exceptions).

The program attached below illustrates this. It is fully annotated - there
are no variables or expressions of type dynamic anywhere in the program, it
passes the analyzer with no warnings, and yet refactoring based on the
types will change the production mode semantics. Changing the name of the
A.foo method will introduce a NSM error (while preserving the "no-dynamic"
property). Changing the name of the B.foo method will also introduce a NSM
error. Changing the name of one of these methods to something that is
already implemented by the other class could introduce other arbitrary
changes in behavior.

This program does throw in checked mode, but if these types were the
result of inference (rather than being fully annotated), then the code
would run fine in checked mode as well, but again, refactoring would change
the semantics.

// This program has no expressions or variables of type dynamic.class A {
void foo() => print("A's foo");
}
class B {
void foo() => print("B's foo");
}
typedef A V2A();
typedef B V2B();
typedef Object V2O();
// The static type of f() is A, but B.foo can reach this call site.void callsAFoo(V2A f) => f().foo();
void mixesThingsUp(V2O f) => callsAFoo(f);
void losesACallToBFoo(V2B f) => mixesThingsUp(f);

B mkB() => new B();
void main() {
losesACallToBFoo(mkB);
}

—
Reply to this email directly or view it on GitHub
#24267 (comment).

Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 København K, Denmark
CVR no. 28866984

[sethladd]

OMG YES. :)

[munificent]

See also: dart-archive/dev_compiler#363

[jmesserly]

(Labeled strong-mode as that's where we're likely to implement this first.)

[floitschG]

Please create a different issue for strong-mode.
This is a flag that should have no relationship to strong-mode.

[jmesserly]

I've opened #25573 for this feature in strong mode. It's been an oft-requested feature, so it's likely to happen there. :)

[bwilkerson]

It's fine to ensure that this works correctly with strong mode, but it should be possible to specify the option in the absence of strong mode.

[jmesserly]

I've removed the tag, sorry about causing confusion.

(I'd tagged it as analyzer-strong-mode so we could find it in our hotlist, as we're likely to implement it. For example, that's how we've been tracking the generic method prototype work. Definitely didn't mean to imply that it was a strong-mode exclusive feature. Anyway, sorry about that--I think everything's back how it was, hopefully no harm done :) )

[jmesserly]

If this was implemented for the Dart 1 type system, wouldn't it reject most programs? Dart 1 has no inference so even something like var x = 42 would be rejected (x has implicit type dynamic). Unless there is some type inference work that goes along with this task?

[jmesserly]

Ah I see inference is requested (#24267 (comment)) ... that makes sense, but it probably needs to be specified how the inference should work (e.g. here is where we describe inference for strong mode: https://github.com/dart-lang/dev_compiler/blob/master/doc/STATIC_SAFETY.md).

Anyway the reason I asked: in the process of addressing #25573, I can allow the flag to be specified regardless of strong mode, but I'm not sure it will be very useful without strong mode's type inference.

[munificent]

in the process of addressing #25573, I can allow the flag to be specified regardless of strong mode

I don't think there's any value in supporting it in non-strong mode. If it's more work to prevent using it in non-strong mode, then I wouldn't worry about allowing it. But I wouldn't suggest spending any extra effort to support no implicit dynamic outside of strong mode.

[chalin]

This can be closed, right? E.g., for Dart VM version: 2.0.0-dev.26.0:

> dartanalyzer -h
Usage: dartanalyzer [options...] <directory or list of files>
    ...
    --no-implicit-dynamic       Disable implicit dynamic (https://goo.gl/m0UgXD).

cc @kwalrath

[bwilkerson]

Yes, thanks for noticing and letting us know.