Comment by valenterry
5 years ago
Great list!
It shows that is important to take soundness of type-systems serious. I like what they did with Scala: they boiled down the language into the fundamental parts and built a language from it that has a sound type-system (machine-checked). This has now finally become Scala 3.
Here are some more details: https://www.scala-lang.org/blog/2016/02/03/essence-of-scala....
Cries in removal of abstract types (e.g. `val x: A#T = ...`).
While Scala 3 filled a soundness hole, it opened a practical crater (and no, path dependent types are not a viable substitute).
Too bad, many nice improvements overall.
Existential type syntax ("forSome") also got removed for the same reason. I still think it's better to build a sound typesystem than having a bad foundation with some extra features.
> It shows that is important to take soundness of type-systems serious.
Does it show that? I see it more like a set of examples demonstrating there's no such thing as "a sound type system".
There is difference between bugs that make a type-system unsound and the actual fundamental design / specification that makes it unsound. The former is easily possible but also easy to fix. The latter is sometimes impossible to fix without breaking compatibility to a degree that makes it impossible to do so.