Types and the Dart Programming Language

Dart_logo_270x270

Yesterday at Lang.NEXT Gilad Bracha presented the Dart programming language. While there are some interesting things about Dart (like mirrors and isolates), a significant part of the talk was dedicated to Dart’s type system or the lack of one.

Dart aims to be a replacement for JavaScript; a cleaned up version of the same for web programming. In this sense, like Bracha says, it is easy to be better than the competition, because the competition has many well known design issues.

My interest is with the type-system. Due to its fuzzy nature Dart’s type-system is difficult to describe casually in a way that your words are not open to interpretation (and trolling). That said, in many ways Dart does not have a type-system, but it allows things that look like types to be written to serve as documentation for your program. By providing these types, the system can conservatively check that they hold. If I understand things correctly — if the system can show that the “type” does not hold then it will raise a warning (not a compile time error). The program will run anyway and if you execute the problematic part of code, you will get a run-time exception. If the system can’t tell if the type holds or not, I believe it will keep silent.

This implies that “types” can be specified or be entirely omitted. Bracha says that the language is designed this way not to address a technical issue, but to address a sociological issue — namely that thousands/millions of web programmers will have a negative reaction to being required to use any strong type system. Partly to justify the multitude’s point of view, rather that to genuinely criticize type systems (I think), Bracha spends some time “justifying” the fast-and-loose programming with respect to types.

This attitude is justified from a pragmatic point of view. After all, trying to replace something as pervasive as JavaScript with anything (no matter how good it is) is a nightmare. Too many companies — Mozilla, Microsoft, Apple and more — will have to be convinced to even allow this to happen, let alone help the effort. The politics of this issue is complex and a good recent example of this is the WEBM codec adoption effort. Hence having a technical barrier to adoption (like a strong type system) does not help your cause at all.

That said, I wonder how much of this same style of thinking was responsible for JavaScript being as bad as it is. Other than real design blunders, how many of JavaScript’s awkward features were intentionally put in for “mass appeal” or to write some “cool” hack or the other. Especially things like the terrible handling of equality and conditionals in JavaScript (for example). After some reflection about this however, I wonder if a different choice can be made.

If Dart gets adopted, I wonder if 10-15 years later we will look back and be apologetic about the design choices of the type system. After all in today’s world, languages like C# and C++ have higher order functions. Languages like Scala and F#, which have strong functional roots and rich type systems, are seeing adoption. It is becoming a well-known secret that there are companies making a killing by simply out-programming everyone else with small teams using languages like OCaml (and Haskell). The point is that in some years, type systems that seem radical to the masses today may not seem as radical.

However, if you do adopt a very weak notion of typing to start with, it is nearly impossible to remove it from the language — in much the same way that JavaScript cannot retract some of its design choices. What is a way out of this conundrum?

One way out of this, and I am only stating the obvious here, is something that significant research has already gone into: there are programming languages that allow both type-safe and untyped programming in the same system with “constraints” policing the boundary between the two. Keywords and people in this area are: Blame Calculus, Gradual Typing, multi-language semantics, constraints — Amal Ahmed, Phil Wadler, Jeremy Siek, Robby Findler and others. For a casual introduction click here.

The advantage of this approach is that Dart can have a type system of well-known expressive strength backing it. However people can choose to hack scripts in an untyped fashion and optionally choose to strengthen them as their programs get bigger and they need the guarantees of a type system. So the next time someone builds a system like Rhino-On-Rails it won’t have as many agonizing abstraction leaks. Dart’s current type-like documentation system can still be retained to aid the untyped fragment of the language.

If this cannot be built into the language right away, it may be worth designing the untyped fragment carefully enough such that there is room to add this seamlessly in the language. This means being careful about what sort of “reflection” is possible, for instance.

ps. I would also like to see algebraic datatypes and pattern matching, D-like “scope” based error handling, yield-based full delimited continuations (and its limited forms like async/await) and more. But those can wait.

Comments are closed.