Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add a strict type checking mode #20443

Closed
bwilkerson opened this issue Aug 9, 2014 · 15 comments
Closed

Add a strict type checking mode #20443

bwilkerson opened this issue Aug 9, 2014 · 15 comments
Labels
area-analyzer P2 A bug or feature request we're likely to work on type-enhancement A request for a change that isn't a bug

Comments

@bwilkerson
Copy link
Member

There have been a number of requests recently (many on the mailing lists) to have a strict type checking mode that acts as if Dart had a sound type system. I'm creating this issue to give people a single place to record their interest, and as a blocking issue for more specific requests related to how such a mode should operate.

@bwilkerson
Copy link
Member Author

Marked this as blocking #20441.

@DartBot
Copy link

DartBot commented Aug 9, 2014

This comment was originally written by @zoechi


This would be incredible!

@bwilkerson
Copy link
Member Author

Where I can read in the specification about that the "'superclass' is assignable to 'subclass'"?

Please see my response in issue #20441.

Q: If both of them has the same behavior in "checked" and "production" modes than what
difference between them?
A: No diffrenece.

But you just said that they both failed in checked mode and succeeded in production mode, so there is a difference. In checked mode, the runtime types of the actual values are compared against the declared (static) types. In production mode they are not.

Q: Is 'String' assignable to 'int'?
A: No (fails in "checked" mode and success in "production" modes).

Correct.

Q: Is 'Object' assignable to 'int'?
A: No (fails in "checked" mode and success in "production" modes).

Actually, the answer to your question is "yes": 'Object is assignable to 'int'. But according to section 15.19:

    In checked mode, it is a dynamic type error if o is not null and the interface of the class of o
    is not a subtype of the actual type of v.

I think you're assuming that the static type checks are defined to be the same as the dynamic type checks, but they are not.

Q: Is 'superclass' assignable to 'subclass'?
A: No (see question and behavior above).

Again, the real answer is "yes": a superclass is assignable to a subclass. But it will produce a runtime error in checked mode.

Q: Is 'Base' assignable to 'Child'?
A: No (see questions and behaviors above).

Again, the answer is "yes".

Q: Have we warning for "test1" method?
A: Yes.

Which is the correct behavior according to the specification.

Q: Have we warning for "test2" method?
A: No.

Which is also the correct behavior.

Q: If we do not see difference in behavior then why we should think that it exists?

There is a difference in behavior.

Q: Why do you think the same behavior should imply some invisible differences?

I don't. But you reported that there is a difference in behavior.

Q: What makes you think that the "'superclass' is assignable to 'subclass'"?

Please see my response in issue #20441 for references to the specification sections that lead to this conclusion.

@DartBot
Copy link

DartBot commented Aug 9, 2014

This comment was originally written by @Emasoft


Thank you, this is a long awaited feature. I know so many developers that would consider adopting Dart if this happens.

@DartBot
Copy link

DartBot commented Aug 9, 2014

This comment was originally written by @Emasoft


The only reason to keep a non strict type checked is to allow code like this:

Object lookup(String key) { /* ... */ } // a lookup method in a heterogenous table or list
String s = lookup('Frankenstein');

Unlike a classic mandatory type system, in Dart code like this will not cause any complaints from the checker.
We don't need to specify type informations for the table or the list entries. You can store anything there, and because you have semantic knowledge that a typechecker does not, you know that the value stored in the table under ‘Frankenstein’ will be probably a string, even though the lookup method is declared to return Object. So you will take a small risk, but you will gain a flexible table or list method that can return objects of any class. No need to write additional methods for them. This is why this is so loved by javascript programmers: because it's faster.

But there are ways to solve this without loosing strict type checking.

You should consider for example a simple solution like pattern matching.
Here’s Haskell:

doSomething (DivNode n) = does something with a div node
doSomething (TableNode n) = does something with a table node
doSomething _ = do nothing

or a visitor pattern in C++:

struct visit_node : static_visitor<void> {
    void operator ()(DivNode const& n) {
        // Do something with a div node.
    }

    void operator ()(TableNode const& n) {
        // Do something with a table node.
    }

    template <typename T>
    void operator ()(T const& n) {
        // Do nothing.
    }
}

or the use of reflection or a dynamic typeOf method like C# for checking the type:

Object s = lookup('Frankenstein');
switch(typeOf(s)) {
case String:
 String my_txt = s;
 break;
case Int:
 Int my_num = s;
 break;
case SomeClass:
 SomeClass my_class = s;
 break;
default:
 doNothing()
 break;
}

In more general terms, the answer to the problem:
"How to get elements from a mixed or untyped set and do something with then?"
is always solved with (in pseudocode):

foreach (element T of mixed_or_untyped_set A)
 {
  recognize the type of T
  do something different with T according to its type or its interface
}

This is why I don't see any reasons to renounce type checking. All we need is to add a way to inject objects with informations about their original types. Then with a method like "typeOf" and a type comparer operator we can be as flexible in a strict type checked language as in any dynamically or optionally typed script language.

@bwilkerson
Copy link
Member Author

In reply to comment 7.

Analyzer report error for "production" mode or for "checked" mode?

Neither.

In Dart there is a distinction between the static type checking performed by the analyzer and the dynamic type checking that is performed by the runtime (Dart VM or dart2js) when running in checked mode. Production mode disables the dynamic type checking. Think of it this way: in production mode all type annotations are erased, as if everything had been defined as 'dynamic'.

Static type checking does not attempt to report all errors that might occur at runtime. In fact, it was explicitly and intentionally designed to not report some things that are usually errors but which might in some rare cases not be errors.

Whether or not you agree with the philosophy followed by the language designers, the fact is that you won't understand the language unless you first understand that the rules used for static checking and the behavior at runtime (under either mode) are intentionally not the same.

a superclass is assignable to a subclass. But it will produce a runtime error in checked mode.

But in "production" mode it can be assigned.

But in "production" mode also possible assign "String" to "int" but you answer that it is not
assignable and it also will produce a runtime error in checked mode.

The concept "is assignable to" is defined for the purposes of static type checking. It does not apply at runtime and it does not mean "an assignment can be performed without throwing an exception". Furthermore, it applies to static type information. That is, we say that one type T either is or is not assignable to another type S.

At runtime, under checked mode, a different rule is used: the rule that an exception will be thrown when an object is assigned to a variable if the class of the object being assigned is not a subtype of the static type of the variable. (Note the use of "subtype" rather than "assignable to"; this distinction is critical.)

So it is true that the static type 'String' is not assignable to the static type 'int'. It is also true that an exception will be thrown in checked mode if an instance of class String is assigned to a variable of type 'int'.

This should means that "String" also assignable to "int" because it has the same behavior as
for "superclass is assignable to a subclass".

Nope. The type 'String' is not a subclass of 'int', nor is 'int' a subclass of 'String', therefore 'String' is not assignable to 'int'.

My argument does not meet the specification, but the specification and, in turn, does not
much care about the correctness of the statements.

If you mean that the purpose of the static type checking defined by the specification is not to ensure that no exceptions will be thrown at runtime under checked mode as a result of a dynamic type checking rule, then you are absolutely correct.

How I can assume that something is always an assignable (no matter in which mode) to
something if in the some cases they can produce errors?

Under the static type checking rules defined by the specification, you can't.

I believe that a desire for this kind of validation is the primary reason for the request for a strict mode.

@DartBot
Copy link

DartBot commented Aug 10, 2014

This comment was originally written by @Emasoft


You can make the language as dynamic as you want at runtime. Ok. But at compile time, everything must be statically type checked. And the type checking must be done in a strict and sound way. No base classes must be assigned to derived classes without throwing errors. No List<T> would ever be allowed to accept types different from T. And so on.

@gbracha
Copy link
Contributor

gbracha commented Aug 14, 2014

I have long contended that people should be free to define different analyses with whatever rules they want. See, e.g.,

http://bracha.org/pluggable-types.pdf
http://bracha.org/pluggableTypesPosition.pdf

In particular, one can certainly choose to interpret Dart type annotations in a sound manner. I'm not sure it would make anyone more productive, or be more pleasant to work with, and I am quite skeptical about claims that it would improve software quality. However, I am pretty sympathetic to the idea in principle. Whatever rocks your boat.

Whether we should expend resources in putting this into the analysis engine is a separate debate. I think not. Instead, we should provide an extensible API which people could use to define their own analyses in general and plug them into the IDE.

@DartBot
Copy link

DartBot commented Aug 14, 2014

This comment was originally written by @Emasoft


Wow, the Bracha himself! :)
Well I don't want to be misanderstood here: All I ask is consistency. You can make a language dynamically typed or optionally typed, and you can make a compiler that can enable or disable static type checking at will. Great. But you cannot have inconsistencies.
If I can wrote:
List myList = new List()[1234,"Boat",0.144, myClass...]
its ok. But if can wrote:
List<String> = new List()new List()[1234,"Boat",0.144, myClass...]
then the language is inconsistent and misleading, because while at the left of the assignement operator I specify the types of the list as String, at the right I contraddict it. Why I'm allowed to specify the type of the List elements in the first place? You need to avoid specify things that are not real.
If I can write:
dynamic myVar = 12;
myVar = new String();
then it is ok, because I defined myVar as a dynamic type. I know it can contain any type.
But if you make me write:
int myVar = 12;
myVar = new String();
then there is something wrong, because you made me wrote a definition that is NOT TRUE and misleading.

@bwilkerson
Copy link
Member Author

Issue #20693 has been merged into this issue.

@kevmoo kevmoo added P2 A bug or feature request we're likely to work on type-enhancement A request for a change that isn't a bug and removed triaged labels Mar 1, 2016
@pankleks
Copy link

Well I'm new in Dart and I just discovered that - I agree with run-time approach, but IMO lack of such warnings at compilation time - well at least for me it's kind of show stopper.

I see it's P2 - medium - but it looks like 2 years after not much has moved. Any updates on that?

@a14n
Copy link
Contributor

a14n commented May 12, 2016

See https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md .

There are several ways to activate it :

  • with dartanalyzer --strong

  • with a .analysis_options file (at the root of your project) containing :

    analyzer:
      strong-mode: true
  • in DartPad with the checkbox in the right lower corner.

@bwilkerson
Copy link
Member Author

Yes, strong mode is the answer to these requests, so I'm closing this issue.

@pankleks
Copy link

Thanks - much much better!:)

Question - apart from all good hints I get one which I don't understand.

class A<T extends Node> {
  T element;
  A(this.element);
}

class B<T extends HtmlElement> extends A<T> {
  B(HtmlElement element) : super(element);
}

At B constructor I got warning:
WARNING: Unsound implicit cast from HtmlElement to T

IMO above construction is right.

Side question - I'm trying to learn Dart using material on the web - however more detailed knowledge I look for I'm finding more and more out of date articles (including official ones) - what is the most up to date reference?

@bwilkerson
Copy link
Member Author

At the point of B's constructor all we know is that element is some kind of HtmlElement. But the super constructor is expecting it to be a T (which could be any subclass of HtmlElement. There's no guarantee that the actual argument is of the right subclass. What you really want is

B(T element) : super(element);

@Sfshaza Can you address the question about documentation?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
area-analyzer P2 A bug or feature request we're likely to work on type-enhancement A request for a change that isn't a bug
Projects
None yet
Development

No branches or pull requests

6 participants