[hajile]

I think this is not a very good example. Not only does it also throw in TS, but it even throws in Haskell which is pretty much the poster boy for sound type systems.

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)

[recursive]

Yes it throws in typescript. Typescript isn't the the language chasing soundness at any cost. This just illustrates the futility of chasing soundness.

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.

[hajile]

My balance point is StandardML. SML and TS both have structural typing (I believe this is why people find TS to be more ergonomic). SML has an actually sound type system (I believe there is an unsoundness related to assigning a function to a ref, but I've never even seen someone attempt to do that), but allows mutation, isn't lazy, and allows side effects.

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.

[recursive]

Personally, I think javascript kind of sucks, but it's approximately* the only choice for targeting browsers. If it wasn't for this face, I probably never would have touched TS. SML sounds pretty good.