3 ms·
The distinction isn't too hard to make: a type system's "goodness" is: * proportional to the number of constraints you can express with it (that you're inter
by spion 11y ago
The distinction isn't too hard to make: a type system's "goodness" is:
* proportional to the number of constraints you can express with it (that you're interested in)
* inversely proportional the effort necessary to express those constraints
* inversely proportional to the number of lies it tells (times probability to encounter a lie)
I'd like to expand on #3 via examples:
Assignable nulls is an example of a type system lying. It lowers the guarantees without reducing the burden. The more you rely on that lie being the truth in your code, the less useful the type system is in preventing bugs in your code.
`null` is a pervasive hole as every time you invoke a method on any object, you may actually be throwing a null pointer exception
Checking for null every time will help - now we have the guarantee back. However then we get to another hole which is caused by shared mutable state: if you check for nulls by the time you get to executing the method inside the block the reference may become null.
Luckily, this doesn't pertain to code that doesn't deal with shared mutable state, so this "unsoundness" is less "bad" i.e. more avoidable than the previous one. However in the presence of concurrency, immutability or the inability to share mutable state become another useful constraint.
So its simply a question of how much potential certain lie has to cause problems in your particular code or domain. For example, the answer for `null` is pretty much "most code". The answer for "bivariant function types in TypeScript" is "a lot less, but here are cases X Y and Z and they are common in our code, and here is how to avoid it.."
But yes, I agree that its not a binary unsound vs sound. And I do prefer type systems where I can say "trust me, this results with the type I say it will" when its not possible to express it otherwise. I'm okay with lying to the type system: just not okay with it lying to me.