Preferences

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

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

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.

> What do you gain from an unsound type system?

The ability to type most idiomatic javascript circa 2014. It's definitely a Faustian bargain.

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.
How are you sure you haven’t introduced bugs if the specification/type has an error it doesn’t tell you about?
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?

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?

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.

This item has no comments currently.

Keyboard Shortcuts

Story Lists

j
Next story
k
Previous story
Shift+j
Last story
Shift+k
First story
o Enter
Go to story URL
c
Go to comments
u
Go to author

Navigation

Shift+t
Go to top stories
Shift+n
Go to new stories
Shift+b
Go to best stories
Shift+a
Go to Ask HN
Shift+s
Go to Show HN

Miscellaneous

?
Show this modal