[joshuamorton]

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

[higherkinded]

>Much like java and javac are different tools, python and pytype/mypy are different tools

I get where you're heading. The `java` one is for JVM bytecode interpretation and the `javac` is for actual Java. Ok. Cool. I suppose that you do understand it well that leaving the choice on typechecking to external tools is something rather atrocious, do you?

>All of the python _I write_

The factory that produces the hammers for us carpenters provides just hammerheads alone and leaves us to choose and get the grips, so oftentimes fellow woodworkers use them without any grip whatsoever, some make flails and flail the nails, and I just go buy the soft grip from a third-party vendor. What's the problem here?

>[throws a Wikipedia link with the term definition at me, goes on showing me what must be done by a sum type]

You sure do consider me stupid, right? Anyway, what dependent types _usually_ do is they limit a category (think set) to some sub-category. Your example indeed describes dependent types but the problem with it is that it isn't a good place for dependent types. 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?

>has generic types, not dependent types

(1) Look. 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? Consider this: Java can express Peano numbers at the type level, along with Rust, C# and whatever there is with even remotely working generics. Do you know what that means to us here? Yes. We can express anything number-related at the type level, thus getting one little step closer to dependent typing. The most modest example of what you can do with that is a list with length limited on a type level, which qualifies pretty ok for dependent typing.

>not the _type_

Dependent typing is still about types, and if you work with these on a type level, you will deal with types. The type isn't inferred here but the value is limited by the type in question, so please don't say this, otherwise it will not constitute a sane type system. Imagine the types that just constatate the fact once it happened instead of setting an invariant (ah yes).

>with some massaging

Zero massaging[0] but ok. I hope that, knowing about [0], you've already guessed that there's an implementation of matrix multiplication with actual dependent types[1].

Actually, if you want, I could implement type-level floats for you but I'm not sure if they have any good use case and I'm pretty sure that some operations will compile for a little while: type families operating on numbers are usually defined in terms of recursion. Not sure if we're going to flex type systems at each other at this point, there's a clear winner even if we're not bringing the said to the table: static typing in Python isn't provided out of the box, and while your little example makes me check it out and appeals to me, it's still a third-party tool and that's not how it must be. I will not mention anything about types describing here. If that's not enforced by type system, it's pretty bad but there's no point in discussing that already, enough's been said.

>plainly cannot

Refer to (1).

[0]: http://hackage.haskell.org/package/base-4.12.0.0/docs/GHC-Ty...

[1]: https://hackage.haskell.org/package/linear-code-0.1.0/docs/M...

Edit 1: one more link.

Edit 2: a suggestion and some out-of-place conclusion.

[joshuamorton]

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

[higherkinded]

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

[joshuamorton]

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.