Hacker News Reader

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

View on HN

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.

Reply on news.ycombinator.com