4 ms·

What do you gain from an unsound type system? Implicit casts still exist and one dependency returning Any means that your specification is meaningless (you can

What do you gain from an unsound type system? Implicit casts still exist and one dependency returning Any means that your specification is meaningless (you can prove anything, including false).

valenterry 2y ago
The point is that making a typesystem sound is really hard and requires trade-offs. I think Scala is a wonderful example. Check: https://www.baeldung.com/scala/dotty-scala-3 https://www.baeldung.com/scala/dotty-scala-3 To quote from there: > Scala 3 has dropped some unsound and useless features to make the language smaller and more regular. It has added some new constructs to increase its expressiveness. Also, it has changed some constructs to remove warts and increase simplicity, consistency, and usability. Some of the features they dropped because they were unsound were still useful (to me). Typescript tries neither to make their typesystem (perfectly) sound, nor to make it as elegant as possible. That results in it to be very useful/pragmatic for everyday-programming tasks.
nyssos 2y ago
> What do you gain from an unsound type system? The ability to type most idiomatic javascript circa 2014. It's definitely a Faustian bargain.
auggierose 2y ago
I don't rely on the type system for my specification. I just rely on it to significantly reduce the number of bugs I inadvertently introduce into the implementation of my specification.
- agentultra 2y ago
  How are you sure you haven’t introduced bugs if the specification/type has an error it doesn’t tell you about?
  - auggierose 2y ago
    I have trouble parsing your sentence, to be honest. What are you asking? Are you asking how am I sure that/if my specification is correct? Are you asking how do I make sure I have no bugs without a proof? Maybe you are asking something else entirely?
    - agentultra 2y ago
      Because the type system is unsound, you could add an error to your implementation and the type system will not catch it. It will happily tell you that everything type checks. How do you use that to prevent errors?
      - auggierose 2y ago
        Yes, that can happen. Just as a sound type system will also not prevent all possible bugs. So what? TypeScript's type system helps me to prevent many bugs by performing standard sanity checks, and is a very practical tool. Just rephrase your question as "How will a pervasive system of sanity checks help me prevent errors?", and I hope you agree that it kind of answers itself.

What do you gain from an unsound type system? Implicit casts still exist and one dependency returning Any means that your specification is meaningless (you can prove anything, including false).

valenterry 2y ago

The point is that making a typesystem sound is really hard and requires trade-offs. I think Scala is a wonderful example. Check: https://www.baeldung.com/scala/dotty-scala-3 https://www.baeldung.com/scala/dotty-scala-3 To quote from there: > Scala 3 has dropped some unsound and useless features to make the language smaller and more regular. It has added some new constructs to increase its expressiveness. Also, it has changed some constructs to remove warts and increase simplicity, consistency, and usability. Some of the features they dropped because they were unsound were still useful (to me). Typescript tries neither to make their typesystem (perfectly) sound, nor to make it as elegant as possible. That results in it to be very useful/pragmatic for everyday-programming tasks.

nyssos 2y ago

> What do you gain from an unsound type system? The ability to type most idiomatic javascript circa 2014. It's definitely a Faustian bargain.

auggierose 2y ago

I don't rely on the type system for my specification. I just rely on it to significantly reduce the number of bugs I inadvertently introduce into the implementation of my specification.

agentultra 2y ago
How are you sure you haven’t introduced bugs if the specification/type has an error it doesn’t tell you about?
- auggierose 2y ago
  I have trouble parsing your sentence, to be honest. What are you asking? Are you asking how am I sure that/if my specification is correct? Are you asking how do I make sure I have no bugs without a proof? Maybe you are asking something else entirely?
  - agentultra 2y ago
    Because the type system is unsound, you could add an error to your implementation and the type system will not catch it. It will happily tell you that everything type checks. How do you use that to prevent errors?
    - auggierose 2y ago
      Yes, that can happen. Just as a sound type system will also not prevent all possible bugs. So what? TypeScript's type system helps me to prevent many bugs by performing standard sanity checks, and is a very practical tool. Just rephrase your question as "How will a pervasive system of sanity checks help me prevent errors?", and I hope you agree that it kind of answers itself.