Why Dart Types Are Optional and Unsound

http://www.dartlang.org/articles/why-dart-types/

by fogus • 15 years ago

25 26 15 years ago

ot• 15 years ago

  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.

As far as I understand this means that no precondition can be encoded in the variable type. A function with a Pig argument can still cause a NoSuchMethodException exception because the argument can actually hold a Cow instance.

jbri• 15 years ago

You still have a precondition encoded in the parameter type. It's just a precondition for the programmer to see and understand, rather than one for the machine to rigorously enforce.

jashkenas3• 15 years ago

    > Correctness is easier to achieve for a VM that doesn't
    > rely on static soundness guarantees, because you don't
    > need the complexity of bytecode verification.

I don't follow. You only need to verify bytecode if a), you have bytecode in the first place, and b), you assume the existence of a hostile compiler or other external bytecode source. Neither of these apply to Dart.

roestava4• 15 years ago

Maybe with static typing and bytecodes the author was meaning lower level and hence riskier stuff. Not that Dart was lower level.

By being higher level Dart can work from a subset, keeping the surface area smaller as a result.

jashkenas3• 15 years ago

Also, writing this:

    > We don't want Dart to be a testbed for active programming
    > languages research, but I think we're open to taking up
    > ideas after they become well understood and unsurprising,
    > a.k.a. a little bit boring.

... after saying this in the first paragraph:

    > Dart uses types in a way that might seem strange. Most
    > popular languages that offer a type system use it very 
    > differently. If you're familiar with types in Java, Haskell, 
    > Scala, or any statically typed language, you may wonder 
    > why on earth Dart makes the choices that it does.

... makes me wonder why on earth Dart makes the type system choices that it does ;)

roestava4• 15 years ago

That's a good point to make. Miguel de Icaza has said that after taking a brief look at Dart he thought it was pretty academic. Maybe he was refering to more than the optional typing that Dart makes use of. The truth though is that Dart is in some ways experimental while folks such as Miguel are sitting on already established tech in c#. They aren't going to welcome potential competitors.

azakai3• 15 years ago

>> Don't you want strong typing for better performance?

> That's what I thought, too. The VM designers say that in practice, type guarantees really don't help them nearly as much as you might think, because type checks are not a major drain on performance.

If this is the case, what is supposed to make Dart faster than JavaScript? It sounds like they will end up around the same speed.

roestava4• 15 years ago

Dart is built with c++ and the algorithms won't always be super-optimized. I'm a little skeptical regarding performance as well, but the idea is that Dart makes code a little more static than JavaScript and that can help with calling methods in tight loops for example. If anything, it will allow Dart to close the gap to more static languages in that regard. More optimizations will only be possible with the longterm success of the platform. And for that will have both JavaScript and Dart.

jashkenas3• 15 years ago

The main difference that may allow Dart to run faster than JavaScript isn't type checks, but objects having static shape at runtime.

In JavaScript, I can write this:

    var dog = new Animal();
    dog.name = "Fido";

... adding a new field to the "dog" object, even though other objects of the same class may have no such field. Objects that share common sets of fields are the famous "hidden classes" that V8 is able to optimize.

You can't write the above example in Dart. Dart doesn't have to work as hard as V8 to discover and cache hidden classes, because the shape of an object is statically fixed to be the same as its class.

azakai3• 15 years ago

Yes, but how much of a slowdown is it to manage hidden classes? Furthermore, in the most performance sensitive code, you might not even have classes at all, just raw calculations (for example on typed arrays), which Dart will be no faster than JS at.

lmkg• 15 years ago

So what do types and type annotations actually do in Dart? I may have missed something obvious, but it looks like all the code samples given in the article will all pass static verification. Can someone give me an example of a code error that Dart will catch statically at compile time? My biggest confusion about Dart's type system (or at least its static one) is that it simply doesn't seem to do very much, so I wonder why it exists at all.

roestava4• 15 years ago

Hehe. I guess Dart users are troubled by it as well because the way it works is surprising based on our previous experiences. Basically you can run the program in checked mode so you do get more feedback from the usage of the types. But checked mode is meant for development as it isn't as optimized as in other languages. We need to recall that Dart gets translated into JavaScript and adding type checks and stuff to all the code required puts an extra burden on it that can be hard to justify.

All in all, you should run in checked mode for more feedback. The idea is that you get warnings when stuff is bad. When stuff is super bad you get runtime exception.

Dart is optimist and will give you warnings and let your code run until it cannot.

JoshTriplett• 15 years ago

I certainly agree that the translated JavaScript shouldn't need to enforce types in any way, unless Dart provides some kind of "downcasting" mechanism to give something a type it doesn't already have. However, that only applies if the Dart compiler doesn't statically enforce the types when compiling the code to JavaScript.

For one example: Haskell's strong static types all go away when you compile; the generated code does not do any type enforcement or verification.

The biggest thing I hoped the article would talk about got shot down in the very first section, which just said "Dart is dynamically typed" and explicitly dismissed any need to justify that, other than by saying "Users of dynamically typed languages ... will understand why we chose this".

I honestly can't even begin to understand why people consider dynamic typing a feature; when I saw the headline I hoped to see an interesting justification, but instead I saw it taken as a given and then used to justify many other things. I agree that almost all of those things do follow naturally from the assumption of dynamic typing, but I'd still like to know the rationale for that assumption.

The only justification I've ever seen for dynamic typing amounted to "because I like duck typing". However, a static type system can trivially enforce duck typing.

kkowalczyk• 15 years ago

Type annotations are optional and for people who do use them, they provide at least 2 substantial benefits:

1. Better code documentation. Based on my experience with Python, reading someone else's code (or even my own code after a while) is harder than e.g. C or Java code because types do provide useful information. When reading Python function in isolation I often wander: is the argument to a function a list? a dictionary? a string? Knowing that makes a big difference when reading a code and when I don't know that it's hard to figure that out because you have to trace the whole control flow to that function. This is especially important in large projects where you can't keep all the code in your head and how to read small parts of it.

2. Tools can tell you about errors. Part of the Dart project are lint-like tools that check annotations and notify you about mistakes. If you e.g. annotate a function as taking integer but you pass string to it, a tool can tell you about such mistake. This is what statically typed compilers always do and, again, it's especially important on large projects where you're only responsible for part of the code. Dart doesn't force you to use type annotations but you can choose to use it in your project and get less bugs by using Dart code lint tool.

dextorious2• 15 years ago

One thing I don't get (not knowing much about type theory, and only having implemented a toy C++ subset compiler in a university class once):

Take a dynamically typed language, say, Python:

a = 1

a = "foo"

What disadvantage would you have if the language used type inference to set a to a static type of int when it encountered it?

a = 1

a = "foo" # compile/interpretation time error, "a is an int"

1) You get the speed/optimizations + tooling of static typing. 2) You get the dynamic typing benefit of not messing with type definitions etc.

Do people really do stuff like changing the type of a variable in normal Python use, anyway? Usually when I set something to something, I keep it in the same type.

Is there a disadvantage, besides having to initialize every variable upfront? Polymorphism/Generics are orthogonal to this, no?

Are there any languages that do it this way?

Groxx• 15 years ago

One problem I can see is that you lose the ability to define and use interfaces, unless you declare them explicitly every time you wish to make a variable which holds that type.

There's nothing wrong with that, but what it does mean is that people are much more likely to simply use classes and inheritance trees for everything, to simplify the syntax. Laziness will win out often enough to make writing / finding good code a nightmare.

edit: also, if you try to infer polymorphic changes / interface changes, then it gets harder and harder to figure out what's correct and what's not. Was the change earlier dropping your collection to an enumerable correct, or was it the hash you just tried to save? And what if you are interface or inheritance-happy, and have hundreds of possible options? It can probably be solved reasonably quickly, but not for free.

rst• 15 years ago

There are several languages with type inference, although most can't infer types in all cases: Haskell, ML variants (SML, CaML, etc.), and Scala are the most thorough.

There are some common language features that make type inference tough, most notably mutable data. It's difficult to infer the element type of an array unless you know where it's been, which can be difficult or impossible to know in situations involving separate compilation. Some ML variants can infer all types for programs that avoid using mutable data.

DasIch2• 15 years ago

Type Inference only works nicely if your have static and strong types. Heterogenous data structures are non-trivial in such a language, duck typing doesn't work anymore etc.

In other words people do use these features, they use these features a lot and that is not a problem. You are just using an overly trivial example in which you make assumptions without considering all the consequences.

dextorious2• 15 years ago

"""Heterogenous data structures are non-trivial in such a language"""

Why would they be? You just need a common parent type, like object, or something like Objective-C's "id" type, to indicate that a structure/method can accept any type.

So:

a = 1 # int

b = "foo" # string

c = Cat() # cat object

d = Singer() #singer object

you could have a built-in, say list, structure:

mylist = [a, b, c]; mylist.append(d)

myadt = CustomDataType()

myadt.add(c); myadt.add(d);

"""duck typing doesn't work anymore etc."""

Wikipedia: "duck typing is a style of dynamic typing in which an object's current set of methods and properties determines the valid semantics, rather than its inheritance from a particular class or implementation of a specific interface".

So, why would duck typing not work? Duck typing is about the ability to call methods on any type that implements them. It's irrelevant if the type is static, not? Say:

foreach item in myadt: item.sound()

Cat and Singer could be from totally different objects hierarchies, and the compiler/language would know that both implement "sound()" and let you call it.

If an object on myadt doesn't implement sound() you get a runtime error.

"""You are just using an overly trivial example in which you make assumptions without considering all the consequences."""

Emm, the whole point of my comment was in me EXPLICITLY ASKING for possible consequences. Which you kinda missed, judging by this statement.

charliesome• 15 years ago

Don't you want strong typing for better performance? That's what I thought, too. The VM designers say that in practice, type guarantees really don't help them nearly as much as you might think, because type checks are not a major drain on performance.

No, but you can generate better code if you know exactly what types you're playing with ahead of time.

Say you have a function like this:

    void foo(SomeClass obj) {
        obj.bar();
    }

That could be compiled to just a straight 'jmp SomeClass::bar', whether you're compiling natively or to a VM.

If you don't have static types, the best code you can output is something along the lines of this:

    fn = lookup(obj, "bar")
    jmp fn

Of course there are tricks that you can use to optimize this second case a bit that involve fancy static analysis, fancy JIT business, etc. but the point is that you will never generate better code than just a single jump to the right code, based on the types you know at compile time in a static language.

extension• 15 years ago

In any sensible OO language (i.e. not C++) all method calls will be virtual, so there is always some sort of dynamic lookup involved.

AndrewDucker• 15 years ago

In C# you have to specify that a method is virtual if you want people to be able to override it. This makes it clear where you expect people to insert their changes, allows you to design extra safety into those points, and makes the code faster.

carsongross• 15 years ago

Pragmatically, typing is for tooling first, catching errors second, soundness a distant third.

My tastes run towards a C#-like language (cough Gosu): statically typed with inference, simple generics (covariance), proper function types to fill in most of the covariant holes, and a dynamic type escape hatch, just in case.

But of course they would.

soc88• 15 years ago

Yet another Dart post making no sense at all.

Why Dart Types Are Optional and Unsound

Related Stories