> And how's it helping you verify the correctness of your codebase at compile time (it still compiles the source to byte-code before evaluation)? Last time I checked, it didn't care too much about type annotations, and it didn't type-check anything before execution without additional shoehorning.

All of the python I write is checked at compile time. Much like java and javac are different tools, python and pytype/mypy are different tools. This is nothing new.

>C#, Rust. Notice that I don't even mention my man Haskell or Scala while the latter one is really big.

Neither supports dependent types.

> Uh, even Java has dependent types, anyway. Read the docs.

No, Java has generic types, not dependent types[0]. Dependent types are types that depend on the value, not the type of an argument. As a concrete example:

    @overload
    def open(
        path: _PathType, 
        mode: Literal["r", "w", "a", "x", "r+", "w+", "a+", "x+"],
    ) -> IO[Text]: ...
    @overload
    def open(
        path: _PathType,
        mode: Literal["rb", "wb", "ab", "xb", "r+b", "w+b", "a+b", "x+b"],
    ) -> IO[bytes]: ...

Java, rust, and C# don't support this. C++ does for certain types (integers). Python and typescript support this for certain types (integers, strings, enum values).

Other common examples are type-safe matrix multiplication that at compile time can ensure that the matrix sizes all match correctly. Eigen in C++ does this. Haskell and Scala can do this with some massaging, although its not natural. Java, Rust, C# just plainly cannot.

[0]: https://en.wikipedia.org/wiki/Dependent_type

[1]: https://www.python.org/dev/peps/pep-0586/

> It can be expressed by sum types and I don't see any reason not to do so. By the way, do you have the sum types in Python nowadays?

I'd suggest you attempt to do so. If you mean that, with the benefit of hindsight, you could go back and replace the string with an enum or set of flags, sure, but no, the signature of the function in question is, and due to historical baggage, must stay

    def open(path: _PathType, mode: str) -> Union[IO[Text], IO[bytes]]: ...    

It's just that the set of values `mode` can take on is restricted to a list of ~30 valid strings, which importantly can affect the output type and swap it from Text to bytes. Python already has sum types, and they, uhh, can't solve this problem, as you should know.

> Dependent typing is still about types

Well kind of, in the sense that Literal[4] or Nat::2 is a type, yes. In the sense that Literal[4] is a subclass of int, yes. But it's very different, and much more powerful, because most type systems force you to deal with types as sets of values, and you can't introspect into the sets at all. Dependent types let you introspect and care about particular values, and so you don't have to deal with the types as opaque things. You can care about values, and you aren't restricted to working with only types. But yes the values are still types.

> Have you heard it anywhere that once you get powerful-enough generics, you can at least emulate dependent typing to some extent if not outright get it?

Yes, but implementing peano numerals in java or rust's type system isn't the same as having literal-dependent types, in which you can dispatch based on the actual values present in the language. PEANO_FOUR isn't the same as `4`, and short of a massive amount of codegeneration, you're not gonna have PEANO_FIFTEEN in java generics. Or I mean, if you want to do that, be my guest, but I'll just use `4`.

Or to put it another way: yes, Java's type system is technically turing complete. That doesn't mean that it is pleasant to write programs that execute only during java compilation. Support for literal dependent types makes that more pleasant (and in some cases possible, I'm not actually clear on how you'd write a java function that compiles if passed `4`, and fails to compile otherwise, bridging the gap between PEANO_FOUR and `4` isn't, I don't believe, possible in java. You can no longer use java's own integer class in your code, you have to use your new peano integer class). Native support for dependent types inverts that.

> I suppose that you do understand it well that leaving the choice on typechecking to external tools is something rather atrocious, do you?

This depends. There's a gradient: I run probably 20-30 static analysis tools on my code, from linters to typecheckers to autoformatters. Things that check for malformed TODO comments and all kinds of other fun things. They all prevent various classes of errors. I think not investing in typechecking for large programs is bad, but I also think there's a huge value in gradual typing. Being able to explore interactively in a repl is something that would be painful in java or C++, but is quite pleasant in python. Being able to then convert that code to be production ready by adding types and type-checking, without rewriting in a totally new language, is also quite pleasant. Leaving a user without the choice is also atrocious for many styles of development. That python is able to work for more than one is imo, a feature more than a bug.

>cross the bridge

No one really wants that in any use cases of type-level numbers. Type-level numbers are generally used to do just opposite: silently (well, loudly, if you ask the compiler to check it) govern the structure in question, limiting, say, its arity or whatever. But if you want to "cross the bridge", I think it's still possible but tricky in case of Java. Don't get me wrong, I don't advocate for Java nor intend to write it, I just use it as a dummy trashcan language to illustrate concepts and their latency in a sense that you don't really need to use fancy X in order to do Y or express Z.

>20-30 static analysis tools

Too bad. I'm usually pretty happy with just plain compiler and a 80-char bar.

>huge value in gradual typing

Doubt that. It's actually a good safety net to stop a project from turning into a big ball of mud but it won't help unless used correctly and with the right intent.

>being able to explore interactively

Hindley-Milner type systems can infer your stuff so well that you usually don't have to worry about supplying type signatures at all. For instance, in Haskell you don't have to "add types" compared to what you do in REPL, you have them all the time and oftentimes you don't have to annotate anything, it's still static and usually done just to give an idea to other people what's doing what.

Oh, not about our little conflict but about Python: does it have some form of traits/typeclasses/whatever? I mean, yes, it has them in form of mixins but can it, in modern days, put a constraint on some type variable, saying that it must have some properties that are described in different traits?

Protocols, which are essentially traits are a WIP. I think there's an experimental impl supported by mypy, but it's not in common use just yet.