I still don’t understand how a single language can have multiple (what is it now, half a dozen?) different type checkers, all with different behaviour.

Do library authors have to test against every type checker to ensure maximum compatibility? Do application developers need to limit their use of libraries to ones that support their particular choice of type checker?

▲ WD-42 6 days ago | parent | next [-]

You’re talking about a duck typed language with optional type annotations. I love python but that’s a combination that should explain a bit why there are so many different implementations.

▲ MangoToupe 5 days ago | parent [-]

It doesn't. Either the optional type annotations have precise semantics or they don't.

▲ dragonwriter 5 days ago | parent | next [-]

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.

▲ dwattttt 5 days ago | parent | prev | next [-]

What should a type checker say about this code?

  x = []
  x.append(1)
  x[0] = "new"
  x[0] + "oops"

It's optionally typed, but I would credit both "type checks correctly" and "can't assign 'new' over a number" as valid type checker results.

▲ jitl 5 days ago | parent | next [-]

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

https://www.typescriptlang.org/play/?#code/GYVwdgxgLglg9mABA...

▲ kurtis_reed 5 days ago | parent | prev | next [-]

https://github.com/microsoft/pyright/blob/main/docs/type-inf...

▲ MangoToupe 5 days ago | parent | prev [-]

It depends on the semantics the language specifies. Whether or not the annotations are optional is irrelevant.

Either way, you didn't annotate the code so it's kind of pointless to discuss.

Also fwiw python is typed regardless of the annotations; types are not optional in any sense. Unless you're using BCPL or forth or something like that

▲

dwattttt 5 days ago | parent [-]

> 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.

▲

dragonwriter 5 days ago | parent | next [-]

> 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.

▲

dwattttt 5 days ago | parent [-]

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].

▲

MangoToupe 5 days ago | parent [-]

Right. And the fact that python doesn't specify the semantics of its type annotations is a super interesting experiment.

Optimally, this will result in a democratic consensus of semantics.

Pessimistically, this will result in dialects of semantics that result in dialects of runtime languages as folks adopt type checkers.

▲

dragonwriter 5 days ago | parent [-]

> 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).

▲

MangoToupe 5 days ago | parent [-]

So why do the type checkers differ in behavior?

	▲	dragonwriter 4 days ago \| parent [-]
		The existence of a specification does not make all things striving to implement it compliant with the spec. As the history of web standards (especially back when there were more browsers and the specs weren't entirely controlled by the people making them) illustrates.

▲

MangoToupe 5 days ago | parent | prev [-]

> 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.

▲ sagarm 5 days ago | parent | prev [-]

They don't. They're just documentation.

▲ carderne 5 days ago | parent | prev | next [-]

Users of a library will generally instruct their type-checker not to check the library.

So only the outer API surface of the library matters. That’s mostly explicitly typed functions and classes so the room for different interpretations is lower (but not gone).

This is obviously out the window for libraries like Pydantic, Django etc with type semantics that aren’t really covered by the spec.

▲ mikepurvis 6 days ago | parent | prev | next [-]

At least some of it is differing policies on what types can be inferred/traced through the callers vs what has to be given explicitly.

I think everyone basically agrees that at the package boundary, you want explicit types, but inside application code things are much more murky.

(plus of course, performance, particularly around incremental processing, which Astral is specifically calling out as a design goal here)

▲ lou1306 5 days ago | parent | prev | next [-]

I am not that surprised, to be honest. Basically every C/C++ static analyzer out there does (among other things) some amount of additional "custom" type checking to catch operations that are legal up to the standard, but may cause issues at runtime. Of course in Python you have gradual typing which adds to the complexity, but truly well-formalised type systems are not that common in the industry.

▲ mirashii 6 days ago | parent | prev [-]

> Do library authors have to test against every type checker to ensure maximum compatibility?

Yes, but in practice, the ecosystem mostly tests against mypy. pyright has been making some inroads, mostly because it backs the diagnostics of the default VS Code Python extension.

> Do application developers need to limit their use of libraries to ones that support their particular choice of type checker?

You can provide your own type stubs instead of using the library's built-in types or existing stubs.