The annotations have fairly well defined semantics, the behavior of typecheckers in the absence of annotations, where types are ambiguous (a common case being when the type is a generic collection type but the defining position is assignment to an empty collection so that the correct specialization of the generic type is ambiguous) is less defined.
TypeScript widens the type of x to allow `number | string`, there are no type errors below:
const x = []
x.push(1)
type t = typeof x
// ^? type t = number[]
x[0] = "new"
type t2 = typeof x
// ^? type t2 = (number | string)[]
const y = x[0] + "oops"
// ^? const y: string
> Either way, you didn't annotate the code so it's kind of pointless to discuss.
There are several literals in that code snippet; I could annotate them with their types, and this code would still be exactly as it is. You asked why there are competing type checkers, and the fact that the language is only optionally typed means ambiguity like that example exists, and should be a warning/bug/allowed; choose the type checker that most closely matches the semantics you want to impose.
> There are several literals in that code snippet; I could annotate them with their types, and this code would still be exactly as it is.
Well, no, there is one literal that has an ambiguous type, and if you annotated its type, it would resolve entirely the question of what a typechecker should say; literally the entire reason it is an open question is because that one literal is not annotated.
True, you could annotate 3 of the 4 literals in this without annotating the List, which is ambiguous. In the absence of an explicit annotation (because those are optional), type checkers are left to guess intent to determine whether you wanted a List[Any] or List[number | string], or whether you wanted a List[number] or List[string].
> And the fact that python doesn't specify the semantics of its type annotations is a super interesting experiment.
That hasn't been a fact for quite a while. Npw, it does specify the semantics of its type annotations. It didn't when it first created annotations for Python 3.0 (PEP 3107), but it has progressively since, starting with Python 3.5 (PEP 484) through several subsequent PEPs including creation of the Python Typing Council (PEP 729).
> I could annotate them with their types, and this code would still be exactly as it is.
Well, no, you didn't. Because it's not clear whether the list is a list of value or a list of values of a distinct type. And there are many other ways you could quibble with this statement.