Well... how much of actual software is written using those type systems? Less than 1%? So such type systems might be able to prevent bugs, but in practice, they don't.
Why aren't they used? Probably existing code bases, inertia, and ignorance play a role. I suspect, though, that at least part of the problem is that most programmers find those type systems too hard to use. In that sense, the type systems aren't practical.
And if you're going to blame the programmers for that, well, if your plan for making programming better requires different programmers than the ones we have, your plan isn't very practical, either.
Today less than 1% of all software is written in null safe languages. But I believe Swift has non-nullable types, and it's the promoted language for a really big ecosystem. There's also Rust and Scala, but those have less of a captive audience. I do have high hopes for Rust, which also is data-race safe.
I think Java 8 and optionals show it doesn't have to be that hard, it's just that there's too much old code that relies on nulls for the Java ecosystem to ever be fully null safe.
Use-after-free is solved in a language without manual memory management, so that's actually quite common.
Programmers get comfortable with new ideas over time. Higher order functions and type inference used to be obscure concepts. Today they're par for the course. I don't know if we'll all use dependent types some day, but I think we'll keep getting more powerful types in mainstream languages for a while.
Kotlin is plenty practical. It was born out of a desire for a safer yet practical language on the JVM (provides null safety at the type level). It is at least practical for it be getting gaining lots of traction.
Rust is another good example. It's not very ergonomic, but it is getting better every release.
I think how those two languages do will show whether type systems can me made practical for reducing wider classes of bugs. They seem practical and have the backing to help drive adoption.
> So such type systems might be able to prevent bugs, but in practice, they don't.
Rockets might be able to carry humans up to space, but in practice they don't because only a small set of humans actually get to go.
Isn't that a slightly absurd interpretation of "in practice"?
Why these languages aren't used may have absolutely nothing to do with their technical merits. It's a myth that technical merits is the only consideration for language popularity.
To protect against NPEs you need to make nullable and non-nullable types different and forbid the programming from trying to use a nullable value without doing a null check first (doing a null check returns a non-nullable reference in case of success). One example of this is any of the languages with Albegraic Data Types, where it is super easy to create an Option type that encapsulates this concept.
For an example of preventing use-after-free there is the typesystem used in Rust. It is based on the theory of linear types, which lets you have operations that mark a value as "used" and forbid you from using it again after that point. The same system is used to protect against data races because you can guarantee that a value is only accessible from one thread at a time.
Rust's borrow checker isn't a type system, is it? Sure, its benefits are similar to a linear type system, but actually it's a separate compiler pass whose internals are described imperatively and don't look type-based to me: https://github.com/rust-lang/rust/blob/master/src/librustc_b...
If anything, I agree with zzzcpan and disagree with swsieber. Types are nice but people oversell them. OO languages appeared at the same time as ML family languages, but one got successful and the other got stuck in the realm of "new ideas".
It wouldn't be possible without an affine (at least) type system such as Rust's.
Affine logic rejects contraction, i.e.
Γ, A, A ⊢ B
-------------
Γ, A ⊢ B
My intuition (so take a liberal dose of salt) is that this pretty directly translates to disallowing reuse: we can't see a type twice and continue (inference) as if we saw it once.
Of course, that's very hand-wavy, and doesn't say (as I believe is the case) that there wouldn't be some other way to proceed through a combination of other rules.
Why aren't they used? Probably existing code bases, inertia, and ignorance play a role. I suspect, though, that at least part of the problem is that most programmers find those type systems too hard to use. In that sense, the type systems aren't practical.
And if you're going to blame the programmers for that, well, if your plan for making programming better requires different programmers than the ones we have, your plan isn't very practical, either.