Friday, January 6, 2012

Why I find Dart's production mode evil

Why Dart Types Are Optional and Unsound contains the following example:
class Mammal {}
class Cow extends Mammal { String moo() => 'moo!'; }
class Pig extends Mammal { String oink() => 'oink!'; }

Mammal mammal = new Mammal();
Cow cow = new Cow();
Pig pig = new Pig();

mammal = cow; // [1]
pig = mammal; // [2] Checks OK statically, but now pig holds a Cow.
print(pig.oink()); // [3] NoSuchMethodException if we get this far.
In production mode, the type declaration that pig holds instances of Pig is simply ignored at [2]! IMO, this should never happen. The Dart team's reasoning is that this is still "safe", because you'll get a NoSuchMethodException at [3].

But think about it: you might get the NoSuchMethodException at a completely different place in the program! What good are type declarations/assertions when you never know whether they are true? It actually feels worse than having no type declarations at all!

Thankfully, in Dart's checked mode, you will get the error at [2], making this behavior less troubling. But given that the page says that "type checks are not a major drain on performance", why have production mode at all?

Update: Relief! Bob Nystrom writes on HN:
My understanding was that the prime original motivation for unchecked mode was indeed performance. As our Dart implementations are getting more mature, we're starting to get a better picture of how it does actually impact performance.

I think what we're starting to see is that the performance implications aren't that bad. Given that, I think we're focusing less and less on production mode. It's still a valid option and it may make sense for some users but it may not be commonly used, sort of like -Ofast in gcc.

4 comments:

John Shutt said...

If there's no apparent type infrastructure, and type enforcement is lazy, that's dynamic typing. If there's an apparent infrastructure enforced eagerly, that's static typing. If there's no apparent infrastructure but eager enforcement, I suppose that's type inference (more or less). But if there's an apparent type infrastructure yet lazy enforcement, that's a pig.

dmbarbour said...

It can be useful to have type infrastructure without static enforcement. Pluggable type systems are similar to use of Lint, and use type annotations to support static analysis but still require a robust runtime behavior in case of type errors. The cost is that runtime behavior cannot depend on types, either - e.g. no type-based multimethod dispatch.

I currently favor pluggable type systems because of the limits inherent to analyzing open distributed programs - i.e. some subprograms (foreign services and the like) aren't subject to analysis and might be malicious or buggy, so I need that robust behavior anyway.

But I'd prefer not to have software that depends on runtime-observable type errors - i.e. no dynamic typing. So, rather than

I grant, Dart is not providing pluggable typing. Just saying the basic approach isn't all bad, and can be done well.

Eli Brandt said...

Hi, Manuel. I also would prefer never to run in unchecked mode if I don't have to, so I'm sympathetic to your question. On the other hand, I think there are reasons why what Dart's doing here is not crazy.

One way to look at this is to think about these as type assertions. It's common for assertions to be stripped out of a production build, with C's assert() for example. The hope is that by the time you're running in production mode, your tests exercise all of your assertions, and that they're still true facts even now that you stop testing them. Granted, a counterargument can be made that production is the place you *most* need correctness checks. But this practice seems to work reasonably well.

Another reason for unchecked mode is more philosophical, that it's nice to be able to say that Dart type annotations can be complete no-ops at runtime. If they always unavoidably insert a type assertion, that property is no longer as simple.

Aaron said...

> What good are type declarations/assertions when you never know whether they are true?

Well, Gilad Bracha answered in this talk [1] that Dart tries to make sense to "the guy on the street". Its generics are _always_ covariant, sound or not, because the "guy on the street" expects it to be that way, right or wrong.

Others [2] have already chimed in on why this might be a bad idea.


[1] http://blog.sethladd.com/2011/11/transcription-of-quick-tour-of-dart-by.html

[2] http://conway.rutgers.edu/~ccshan/wiki/blog/posts/Unsoundness/