const arr = ["abcd"];
const str = arr[1];
const num = str.length; // this throws
console.log(num);
This isn't a type error unless your type system is also encoding lengths, but most type systems aren't going to do that and leave it to the runtime (I suspect the halting problem makes a general solution impossible).
main = putStrLn (["a", "b", "c"]!!4)Soundness is good as long as the type-checking benefit is worth the cost of the constraints in the language. If the poster child for soundness isn't able to account for this very simple and common scenario, then nothing will actually be able to deliever full soundness.
It's just a question of how far down the spectrum you're willing to go. Pure js is too unsound for my taste. Haskell is too constrained for my taste. You might come to a different conclusion, but for me, typescript is a good balance.
Put another way, SML is all the best parts of TS, but with more soundness and none of the worst parts of TS and non of the many TS edge cases baked into the language because they keep squashing symptoms of unsoundness or adding weird JS edge cases that you shouldn't be doing anyway.
Compare these two programs.
const arr = ["abcd"];
const str = arr[1];
const num = str.length; // this throws at runtime
const arr = [new Date];
const dt = arr[1];
const num = dt.length; // fails to type check main = putStrLn (["a", "b", "c"]!!4)The result of the an OOB access of an array is specified to be `undefined`. The throw only happens later when the value is treated as the wrong type.
I don't consider a runtime error to be a failure of the type system for OOB array access. But in javascript, it's explicitly allowed by specification. It's a failure of any type system that fails to account for this specified behavior in the language.
This is like arguing that a null exception is fine because it's allowed by the language. If you get `undefined` when you expect another type, most future interaction are guaranteed to have JS throw because of the JS equivalent of a null pointer exception. They are technically different because a dynamic language runtime can prevent a total crash, but the effect on your web app is going to be essentially the same.
[1,2,3][4].toFixed(2)
Haskell has the ability to handle the error.
How do you recommend a compiler to detect out-of-bounds at compile time? It can certainly do this for our trivial example, but that example will also be immediately evident the first time you run the code too, so it's probably not worth the effort. What about the infinite number of more subtle variants?
I wouldn't make the recommendation that they do at all. Full soundness is not my thing. But... if Flow wanted to do it, it would have to change the type of indexing into `(Element[])[number]` with a read from `Element` to `Element | undefined`.
I went looking for where on their website they claim to be sound. There's definitely some misleading wording here: https://flow.org/en/docs/lang/types-and-expressions/#toc-sou... but if you read the whole section, it ends up also acknowledging that it's not entirely sound.