Add --no-implicit-dynamic flag to analyzer

floitschG commented 9 years ago

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 commented 9 years ago

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 https://github.com/dart-lang/sdk/issues/24267.

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

floitschG commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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 commented 9 years ago

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 https://github.com/dart-lang/sdk/issues/24267#issuecomment-137162724.

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

sethladd commented 9 years ago

OMG YES. :)