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.
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.
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.
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.