> Is the Python type system improving or is it the type annotation system that's improving?
Both. (The type annotation system is deeply tied to the type system, since the latter is what is statically verified, but there are improvements both in what can be checked—the type system—and how that is expressed/annotated.)
It's important to understand that the type systems for Python are not really an inherent feature of Python, but the systems enforced by each of the static checkers (which tend to adopt each other's advancements and drive syntactic support into the core system of annotations, so there's a common baseline advancing with the individual systems). A recent advancement in one of those type systems would be pylance (actually pyright, since that's the typechecker for the pylance language server) support for higher-kinded type variables [0]. Mypy, I believe, has identified this as a thing to support, too.
An example of an improvement in annotations specifically to enable type system improvements that require supporting syntax improvement is PEP 646 support for Variadic Generics. [1] Even though it is in draft, pyright has already landed support for it for the type system improvements motivating it. [2]
Oh, okay, the problem here is that we have different understanding of the relevant meanings of “type” and therefore “type system”, which is unsurprising because the term has many different uses in programming.
I am using “type” in the standard computer science sense of statically enforced invariant and “type system” as the system of statically enforced invariants, distinct from annotations which are the syntax by which types are expressed.
You seem to be referring to “types” and “type system” to refer to something else, perhaps some aspect run-time behavior / “dynamic typing”. whatever it is, there's probably also some improvement in that, too, but given that the original concept of the uphtread comment about type system improvements was about type safety, which is what the system of types that are statically verified addresses, it's not really a germane issue.
There's multiple aspects to what a type system can entail.
There's dynamic/static typing which is what most of the thread is about. Python is dynamically typed , which makes it really easy to pickup and make stuff in, but you get issues like runtime errors/bugs since there's no inherent type checking other than attribute access failure, or explicit isinstance calls. To the best of my knowledge, there's no advancement here in Python since it's antithetical to the language design. It is strongly typed however which is great, but not really part of the discussion since it's being assessed in the thread on the virtues of static/dynamic typing and not weak/strong typing.
Type annotation helps partially here since you can statically check the types notated post facto but this is not the type system. The type system in a language is a contract by the compiler/interpreter to enforce type safety. Annotations have no contract for correctness of description or even guarantees of being checked.
This is why I'm trying to draw the distinction between the type system vs the type annotation system. The type system itself hasn't improved much/at all in years by design. The type annotation system has however improved significantly.
> Type annotation helps partially here since you can statically check the types notated post facto but this is not the type system.hatever a static type checker enforces is exactly a type system (and the only thing that is), in the standard CS sense.
The fact that the type checker isn't integrated with the compiler/interpreter is a different design choice from other systems, but it doesn't change what it is.
Effectively, mypy (and this was explictly what mypy was originally envisioned as, as is still reflected in its domain name) and other typecheckers for Python create separate statically typed languages with the same relation to Python as TypeScript has to JavaScript, except that source code in those languages is also valid Python source code with identical runtime behavior. That is, each typechecker creates a new language that is a statically typed strict subset of Python, with its own type system (most of which is common across the whole set of languages, but there are slight variations as each are ahead of the common baseline in different ways.)
> The type system in a language is a contract by the compiler/interpreter to enforce type safety
No, it's enforced by the typechecker. Now, in most languages implementations that have a type system, that's part of the compiler, or more rarely interpreter, but there is no inherent reason it needs to be.
> This is why I'm trying to draw the distinction between the type system vs the type annotation system.
Yes, you've invented artificial nonstandard terminology here that is clearly not the terminology that was being in the post you argued against, in order to make a really extended argument that vigorously exercises the fallacy of equivocation and badly misses the point of the post it sought to dispute.
To the extent there is a legitimate point here it boils down to “Strictly speaking, Python remains untyped, and what is advancing are the type systems of a family of statically typed languages built around Python, that are strict subsets of Python, that leverage feature built in to Python specifically to enable such languages, and which are developed in close collaboration with Python, in some cases sharing core team members.”
The lack of algebraic data types is what python gets criticisms about. That situation is improving, but I would have preferred match to be an expression rather than a statement.
I get that you're not particularly excited about gradual typing and the fact that type checkers are optional and live in a separate ecosystem from the interpreter/language runtime.
I actually like the fact that python code without type annotations continues to work as before and allows for easy transcription of ideas into testable code.
If a certain use case requires "forced" type checking, it shouldn't be hard to write a lint rule that disallows code from being committed if there are type checking errors, including missing type annotations.
The issue though is that Python's type annotation is not a substitute for type checking. Annotations are optional and can be inaccurate.
That's fine, this is part of the design of Python. However strict type systems are a benefit of other languages, that may not fit Python. Type annotation shouldn't be considered an alternative to a type system.
