4 ms·
TypeScript's type foundations are not sound, and I would argue that this is a major factor why it is so good. I have yet to see a sound type system that is as p
by auggierose 2y ago
TypeScript's type foundations are not sound, and I would argue that this is a major factor why it is so good. I have yet to see a sound type system that is as pleasant to use as TypeScript's—certainly not Idris.
I am not a fan of encoding all sorts of correctness statements into a static type system. I'd much rather use a theorem proving environment for correctness, but one that is not based on type theory.
- agentultra 2y agoWhat 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 agoThe 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 agoI 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 agoHow are you sure you haven’t introduced bugs if the specification/type has an error it doesn’t tell you about?
- auggierose 2y agoI 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 agoBecause 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 agoYes, 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.
- valenterry 2y agoYes, I think that's what I said. The pragmatic approach makes to very ergonomic to use in most use cases. That it breaks on for edge-cases is not very relevant in practice usually. > I'd much rather use a theorem proving environment for correctness, but one that is not based on type theory. Based on what then?
- auggierose 2y agoI like Abstraction Logic: http://abstractionlogic.com http://abstractionlogic.com