[lmm]

I'm not sure the evidence is any stronger. I mean, you can point to some bugs and say they were caused by a lack of memory safety, I can point to some bugs and say they were due to a poor type system.

Certainly there were problems I faced in day-to-day Java programming that were visibly due to a crude type system - NPEs, the awkwardness of working with checked exceptions (I do think Ceylon has missed a trick by not using union types to interoperate with Java checked exceptions), SQL injection vulnerabilities caused by not having a taint checker. Other problems I recognised as being due to crude typing in retrospect - the fact that missing transaction annotations could failed silently in confusing ways ( http://thecodelesscode.com/case/211 ), the ease of forgetting to close files, the way all the ways of doing async were either invisible or painfully verbose. Ultimately, everything that we resorted to (inherently non refactor-safe) annotations for. (For what it's worth, I originally picked up Scala based on my experience with the JSR308 checkers framework - the functionality was valuable but too many tools didn't interoperate with it properly, so I looked for a language that had the same thing built-in).

Any individual problem from that list you can solve at the language level - some of them have been solved in Java already, and more in the likes of Kotlin. But a powerful type system is a tool that, once it's built into the language, lets you solve them all even if you didn't think of them first. (Macros have the same kind of power, but maintainability of macros is a real problem). I don't think we'll find an example of a powerful type system being better at a specific feature any more than we'd find an example of a generic data structure being better than a specific one; the value comes in being able to do many things the same way.

Making a language that can be evolved effectively is certainly a real problem - again Perl is the clearest example, but I've also heard complaints about how long it's taken Java to implement features that have been agreed on for years (lambdas, modularization). I don't know whether it's the problem King was intending to solve with Ceylon (though I do think Rust represents a very deliberate effort at the same thing) and I don't think it's easy to prove that you have solved it short of waiting a few decades - I certainly don't have any hard evidence about what factors make a language able to evolve in the long run. Nor would it be a compelling marketing story even if you could prove it. But I think it's still worth working on.

[pron]

I really like your answer. I think it's very important to start with actual problems and then work your way towards a solution rather than vice-versa, because I've always been more troubled by all the bad things people do with rich types[1] rather than notice the importance of problems they do solve. On the other hand, any powerful general tool built into the language can be more trouble than it's worth. Macros are a good examples, but types can be worse. Macros are local to an expression, but types carry the magic with the variable. Sometimes types just carry restrictions, which is OK, but when traits/typeclasses/implicits are involved, they carry actual "bad" magic. So while other specific solutions may take time to implement, codebases live for a long time, so I'd rather wait and suffer some inconvenience, than have people turn a codebase into an unmaintainable, magical mess (which is what I've heard large companies using Scala say it's done to them). Linear types and intersection types are indeed less prone for abuse, and are mostly "restriction-only", so they seem safer, and are less likely to be abused for data types rather than cross-cutting concerns. Another approach -- my favorite -- is exactly Checker. I agree that at this point in time its UX is pretty bad, but it really doesn't have to be. It's mostly a result of the U-of-W putting more effort into the actual mechanics rather than the UX (which, IMO, is a mistake, but they're a university and naturally care more about research...). The Java annotation-processing mechanism generally works very well with IDEs.

Another question is, how bad those problems you mentioned really are. Concurrency bugs are terrible, and simple data typing bugs are usually a non-issue, but tainting/resource-use (i.e. solvable with intersection/linear types respectively) may be bad enough. I really wish someone would conduct an empirical research comprising a taxonomy of bugs, their frequency, and their cost. Such data would be infinitely more useful for language design in the industry than, say, all research going into session types (not trying to pick on session types research, but I hope you catch my meaning when I speak of actual applied utility).

BTW, I think any interesting idea is worth working on. The problem is that a language is a very expensive tool -- and a risky one -- so when it comes to industrial, rather than academic, use a lot of care should be taken when picking one, so it's better to err on the side of caution.

[1]: See Scala's collections as an extreme example. Is it really necessary to go through all that trouble of unreadable code just to save us a cast here and there that has never really bothered anyone?

[lmm]

Hmm, the reason I find types clearer than macros is that they do apply everywhere, so there's consistency across a codebase. <- will always mean a call to flatMap - which might do something different in one place or another, but only in the same way as a normal polymorphic method call - whereas different macros might use it to mean unrelated things. I think IDEs handle them better too - you can refactor in the normal way, you get types on mouseover. Last time I tried to use Checker it was similar - the IDE has good support for running the checkers, but it can't and won't apply the right annotations when extracting a method, or show you the checker-inferred types of local variables.

I do think implicit conversions allow too much; IMO we need typeclasses and extension methods. So my ideal design for a language would include implicit parameters but not implicit conversions, and instead have dedicated support for extension methods. That said we do need to be able to use typeclasses without disrupting method application syntax (i.e. support the use case that means Spray prefers the implicit-conversion-based "magnet pattern" rather than a typeclass).

More generally I think there will be languages that allow too much and languages that ban too much, and we need languages on both sides of the line to allow us to converge on something better. Most places I've worked have had a strong code review/pull request culture which may have coloured my experience - I just haven't seen the Scala maintainability problems you talk about.

(If I thought the complexity of collections was necessary to avoid casts then I would defend it - casts can fail and so it's very nice to have a codebase where they're banned entirely (enforced with wartremover). But I don't think it is - FWIW Odersky's asked for proposals for scala collections in version 3, and I think there's a substantial push towards at least some simplification - perhaps replacing CanBuildFrom with a 1-parameter typeclass that would retain most of the power and simplify the code. The showing-off cases like BitSet#map would require one more method call, but no casts)