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