4 ms·
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 funda
by valenterry 5y 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.html https://www.scala-lang.org/blog/2016/02/03/essence-of-scala....
- virtualwhys 5y agoCries 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.
- valenterry 5y agoExistential 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.
- slver 5y ago> 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".
- valenterry 5y agoThere 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.